Gödel's First and Second Incompleteness Theorems #
Source: doi:10.1007/BF01700692
Authors: Palalansoukî
Status: verified
Main declarations: LeanPool.Incompleteness.goedelFirst, LeanPool.Incompleteness.goedelSecond
Tags: incompleteness, provability, first-order-arithmetic, mathematical-logic
MSC: 03F40, 03F30
theorem
LeanPool.Incompleteness.goedelFirst
(T : LO.FirstOrder.Theory ℒₒᵣ)
[𝐑₀ wkn T]
[LO.FirstOrder.Arith.Sigma1Sound T]
[T.Delta1Definable]
:
Metadata alias for Gödel's first incompleteness theorem.
theorem
LeanPool.Incompleteness.goedelSecond
(T : LO.FirstOrder.Theory ℒₒᵣ)
[𝐈Sg1 wkn T]
[T.Delta1Definable]
[LO.Entailment.Consistent T]
:
Metadata alias for Gödel's second incompleteness theorem.