therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.32.1

True restricted Gƶdel

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...

formal logicmetatheoryproof theory

Source project: Foundation

Person-level attribution pending.

View proof record