Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ConcreteGodel

Supporting results for pointwise provable equality.

The complete arithmetization for the production history evaluator, and the independent second-incompleteness proof for theories with a Delta-one axiom presentation. The realization field is proved by the formula compiler; no arithmetization structure or realization premise is supplied by the caller.

source
noncomputable def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.arithmetization :
ProgramIndices.Arithmetization

The actual Mathlib numbering and production arithmetic graph satisfy all of the arithmetization properties used in the manuscript.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.index_noncongruence_via_godel (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] [𝐏𝐀 β‰Ό T] :
    βˆƒ (f : β„•) (i : β„•) (g : β„•), PointwiseIndex T f i ∧ Β¬PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex f g) (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex i g)

    The second-incompleteness witnesses are indices of the concrete evaluator. This proof uses the proof predicate of the chosen Delta-one presentation.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_via_godel (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] [FFL.Entailment.Consistent T] [𝐏𝐀 β‰Ό T] :
    NoIndexQuotientComposition T

    Concrete quotient composition fails by GΓΆdel II, independently of the productive-set proof. Only consistency and the displayed theory hypotheses are assumed; realization is supplied by the concrete formula compiler.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.pa_no_index_quotient_via_godel :
    NoIndexQuotientComposition 𝐏𝐀
    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.index_noncongruence_via_godel_of_equivalent_presentation (S T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ S] [FFL.Entailment.Consistent T] [𝐏𝐀 β‰Ό T] (hST : S β‰Ό T) (hTS : T β‰Ό S) :
    βˆƒ (f : β„•) (i : β„•) (g : β„•), PointwiseIndex T f i ∧ Β¬PointwiseIndex T (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex f g) (CategoricalRiceShapiro.PartialRecursive.canonicalPartrecCompIndex i g)

    Replacing a theory by a deductively equivalent Delta-one presentation preserves the external pointwise relation and its failure of congruence.

    source
    theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.no_index_quotient_via_godel_of_equivalent_presentation (S T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ S] [FFL.Entailment.Consistent T] [𝐏𝐀 β‰Ό T] (hST : S β‰Ό T) (hTS : T β‰Ό S) :
    NoIndexQuotientComposition T