Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,615 to 1,620 of 2,569 results.
LO.FirstOrder.Arithmetic.quote_ball
Mathematical statement
The code of the bounded universal ∀¹[#0 < bShift t] φ is qqBall (termBShift ⌜t⌝) ⌜φ⌝.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.true_restrictedGödel
Project documentation
Gödel sentence by restricted provability -/ noncomputable abbrev restrictedGödel (e : ℕ) (T : Theory L) [T.Δ₁] : ArithmeticSentence := fixedpoint (∼(T.restrictedProvable e)) private noncomputable abbrev restrictedGödel' (e : ℕ) (T : Theory L) [T.Δ₁] : ArithmeticSentence := ∼(T.restrictedProvable e)/[⌜restrictedGödel e T⌝] private lemma restrictedGödel'_si...
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Arithmetic.undecidability_first_order_logic
Project documentation
Church's theorem: the set of (purely logically, i.e. ∅-)provable sentences is not computable.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Language.ORing.of_mem_range_encode_rel
Mathematical statement
TODO: move to Basic/Syntax/Bootstrapping.Language.lean
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.ProvabilityAbstraction.unprovable_flon
Project documentation
Formalized law of noncontradiction cannot be proved. Alternative formulation of Gödel's second incompleteness theorem.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.Semiterm.step_table
Mathematical statement
On the table of all previously computed values, the step function returns the next one , the obligation Primrec.nat_strong_rec asks for. Four branches, matching ofNat's; the two atomic ones are arithmetic. In the func branch, natToVec succeeding is tested as natToList having the recorded length (natToVec_isSome_of_length/`natToVec_eq_none_of_l...
Source project: Foundation
Person-level attribution pending.