LeanPool.PointwiseComposition.FailureOfComposition.TheoryEnumerability

Supporting results for pointwise provable equality.

Enumerability of deductive closure from enumerability of the axioms. The general result uses pure-logic proofs of finite implications and does not assume a Delta-one presentation of the given theory.

source

def PointwiseComposition.FailureOfComposition.AxiomCodes (T : FFL.FirstOrder.ArithmeticTheory) (n : ℕ) :

Prop

Numerical codes of axioms, using the same sentence coding as TheoremCodes.

Equations

PointwiseComposition.FailureOfComposition.AxiomCodes T n = ∃ (σ : PointwiseComposition.FFL.FirstOrder.ArithmeticSentence), ⌜σ⌝ = n ∧ σ ∈ T

Instances For

source

theorem PointwiseComposition.FailureOfComposition.sentence_provability_re_of_delta1 (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] :

REPred fun (σ : FFL.FirstOrder.ArithmeticSentence) => T ⊢ σ

Provability in a Delta-one-presented theory is enumerable on sentences.

source

theorem PointwiseComposition.FailureOfComposition.theorem_codes_re_of_delta1 (T : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ T] :

REPred (TheoremCodes T)

Theorem codes are enumerable for every Foundation Delta-one presentation.

source

theorem PointwiseComposition.FailureOfComposition.theorem_codes_re_of_axiom_codes (T : FFL.FirstOrder.ArithmeticTheory) (hT : REPred (AxiomCodes T)) :

REPred (TheoremCodes T)

Recursively enumerable axiom codes yield recursively enumerable theorem codes. The theory need not have a Delta-one presentation.