Documentation

Foundation.FirstOrder.Incompleteness.Examples

Examples of incompleteness theorems #

The definability infrastructure is provided by Foundation.FirstOrder.Incompleteness.Definability and is used by the examples below.

source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatUnionCon :
𝗜đšș₁ âȘ± 𝗜đšș₁ âˆȘ Theory.Con 𝗜đšș₁
source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionISigmaOfNatNatConFirstOrderTrueArith :
𝗜đšș₁ âˆȘ Theory.Con 𝗜đšș₁ âȘ± 𝗧𝗔
source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryISigmaOfNatNatUnionIncon :
𝗜đšș₁ âȘ± 𝗜đšș₁ âˆȘ Theory.Incon 𝗜đšș₁
source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryPeanoUnionCon :
𝗣𝗔 âȘ± 𝗣𝗔 âˆȘ Theory.Con 𝗣𝗔
source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionPeanoConFirstOrderTrueArith :
𝗣𝗔 âˆȘ Theory.Con 𝗣𝗔 âȘ± 𝗧𝗔
source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryPeanoUnionIncon :
𝗣𝗔 âȘ± 𝗣𝗔 âˆȘ Theory.Incon 𝗣𝗔
source
instance FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryUnionPeanoConIncon :
𝗣𝗔 âˆȘ Theory.Con 𝗣𝗔 âȘ± 𝗣𝗔 âˆȘ Theory.Con 𝗣𝗔 âˆȘ Theory.Incon (𝗣𝗔 âˆȘ Theory.Con 𝗣𝗔)