Supporting results for pointwise provable equality.

Common arithmetic proof-search obstruction. This module does not use Gödel II. U is the theory whose proofs are searched; T is the theory of pointwise equality.

@[reducible, inline]

abbrev PointwiseComposition.FailureOfComposition.ProofSearch.Graph : Type

The Graph construction in FailureOfComposition.ProofSearch.

Equations

• PointwiseComposition.FailureOfComposition.ProofSearch.Graph = Σ₁.Semisentence 2

noncomputable def PointwiseComposition.FailureOfComposition.ProofSearch.proofTarget (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : ∆₁.Semisentence 1

The proof Target construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FailureOfComposition.ProofSearch.notProofTarget (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : Σ₁.Semisentence 1

The not Proof Target construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FailureOfComposition.ProofSearch.guard (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : Graph

The guard construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PointwiseComposition.FailureOfComposition.ProofSearch.search (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : Graph

The search construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.identity : Graph

The identity construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.empty : Graph

The empty construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.comp (F G : Graph) : Graph

The comp construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.eqAt (F G : Graph) (n : ℕ) : FFL.FirstOrder.ArithmeticSentence

The eq At construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.Pointwise (T : FFL.FirstOrder.ArithmeticTheory) (F G : Graph) : Prop

The Pointwise construction in FailureOfComposition.ProofSearch.

Equations

• PointwiseComposition.FailureOfComposition.ProofSearch.Pointwise T F G = ∀ (n : ℕ), T ⊢ PointwiseComposition.FailureOfComposition.ProofSearch.eqAt F G n

def PointwiseComposition.FailureOfComposition.ProofSearch.uniformSentence (F G : Graph) : FFL.FirstOrder.ArithmeticSentence

The uniform Sentence construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.Uniform (T : FFL.FirstOrder.ArithmeticTheory) (F G : Graph) : Prop

The Uniform construction in FailureOfComposition.ProofSearch.

Equations

• PointwiseComposition.FailureOfComposition.ProofSearch.Uniform T F G = (T ⊢ PointwiseComposition.FailureOfComposition.ProofSearch.uniformSentence F G)

def PointwiseComposition.FailureOfComposition.ProofSearch.functionalSentence (F : Graph) : FFL.FirstOrder.ArithmeticSentence

The functional Sentence construction in FailureOfComposition.ProofSearch.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ProofSearch.Functional (F : Graph) : Prop

The Functional construction in FailureOfComposition.ProofSearch.

Equations

• PointwiseComposition.FailureOfComposition.ProofSearch.Functional F = (𝐏𝐀 ⊢ PointwiseComposition.FailureOfComposition.ProofSearch.functionalSentence F)

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.proofTarget_sigma_eval (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin 1 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma (proofTarget U σ)) ↔ FFL.FirstOrder.Arithmetic.Bootstrapping.Proof U (v 0) ⌜σ⌝

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.proofTarget_pi_eval (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin 1 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi (proofTarget U σ)) ↔ FFL.FirstOrder.Arithmetic.Bootstrapping.Proof U (v 0) ⌜σ⌝

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.notProofTarget_eval (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin 1 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(notProofTarget U σ) ↔ ¬FFL.FirstOrder.Arithmetic.Bootstrapping.Proof U (v 0) ⌜σ⌝

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.guard_eval (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin 2 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(guard U σ) ↔ ¬FFL.FirstOrder.Arithmetic.Bootstrapping.Proof U (v 0) ⌜σ⌝ ∧ v 1 = v 0

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.search_eval (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (v : Fin 2 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(search U σ) ↔ FFL.FirstOrder.Arithmetic.Bootstrapping.Proof U (v 1) ⌜σ⌝ ∧ ∀ r < v 1, ¬FFL.FirstOrder.Arithmetic.Bootstrapping.Proof U r ⌜σ⌝

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.identity_eval {V : Type u_1} [FFL.ORingStructure V] (v : Fin 2 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑identity ↔ v 1 = v 0

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.empty_eval {V : Type u_1} [FFL.ORingStructure V] (v : Fin 2 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑empty ↔ False

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.comp_eval {V : Type u_1} [FFL.ORingStructure V] (F G : Graph) (v : Fin 2 → V) : (FFL.FirstOrder.Semiformula.Evalb v) ↑(comp F G) ↔ ∃ (y : V), (FFL.FirstOrder.Semiformula.Evalb ![v 0, y]) ↑G ∧ (FFL.FirstOrder.Semiformula.Evalb ![y, v 1]) ↑F

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.eqAt_eval {V : Type u_1} [FFL.ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (F G : Graph) (n : ℕ) : (FFL.FirstOrder.Semiformula.Evalb ![]) (eqAt F G n) ↔ ∀ (y : V), (FFL.FirstOrder.Semiformula.Evalb ![↑n, y]) ↑F ↔ (FFL.FirstOrder.Semiformula.Evalb ![↑n, y]) ↑G

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.uniformSentence_eval {V : Type u_1} [FFL.ORingStructure V] (F G : Graph) : (FFL.FirstOrder.Semiformula.Evalb ![]) (uniformSentence F G) ↔ ∀ (x y : V), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑F ↔ (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑G

@[simp]

theorem PointwiseComposition.FailureOfComposition.ProofSearch.functionalSentence_eval {V : Type u_1} [FFL.ORingStructure V] (F : Graph) : (FFL.FirstOrder.Semiformula.Evalb ![]) (functionalSentence F) ↔ ∀ (x y z : V), (FFL.FirstOrder.Semiformula.Evalb ![x, y]) ↑F → (FFL.FirstOrder.Semiformula.Evalb ![x, z]) ↑F → y = z

theorem PointwiseComposition.FailureOfComposition.ProofSearch.numeral_negative (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) (hσ : U ⊬ σ) (n : ℕ) : 𝐏𝐀 ⊢ ↑(notProofTarget U σ)/[↑n]

U does not prove σ, so PA proves every fixed negative proof check.

theorem PointwiseComposition.FailureOfComposition.ProofSearch.universal_negative_bridge (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : 𝐏𝐀 ⊢ ∀¹ ∼↑(FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma (proofTarget U σ))/[FFL.FirstOrder.Semiterm.bvar 0] ⇔ₗ ∼(FFL.FirstOrder.Arithmetic.Bootstrapping.provabilityPred U σ)/[]

An internal bridge for this exact named proof predicate.

theorem PointwiseComposition.FailureOfComposition.ProofSearch.guard_functional (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : Functional (guard U σ)

theorem PointwiseComposition.FailureOfComposition.ProofSearch.identity_functional : Functional identity

theorem PointwiseComposition.FailureOfComposition.ProofSearch.search_functional (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : Functional (search U σ)

theorem PointwiseComposition.FailureOfComposition.ProofSearch.guard_pointwise_identity (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hσ : U ⊬ σ) : Pointwise T (guard U σ) identity

theorem PointwiseComposition.FailureOfComposition.ProofSearch.guard_search_empty (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : Uniform 𝐏𝐀 (comp (guard U σ) (search U σ)) empty

theorem PointwiseComposition.FailureOfComposition.ProofSearch.identity_comp (G : Graph) : Uniform 𝐏𝐀 (comp identity G) G

theorem PointwiseComposition.FailureOfComposition.ProofSearch.search_empty_implies_absence (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) : 𝐏𝐀 ⊢ eqAt (search U σ) empty 0 ⇒ₗ ∼FFL.FirstOrder.Arithmetic.Bootstrapping.provabilityPred U σ

theorem PointwiseComposition.FailureOfComposition.ProofSearch.composites_not_pointwise_equal (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hAbs : T ⊬ ∼FFL.FirstOrder.Arithmetic.Bootstrapping.provabilityPred U σ) : ¬Pointwise T (comp (guard U σ) (search U σ)) (comp identity (search U σ))

theorem PointwiseComposition.FailureOfComposition.ProofSearch.functional_graph_noncongruence (U : FFL.FirstOrder.ArithmeticTheory) [FFL.FirstOrder.Theory.Δ₁ U] (σ : FFL.FirstOrder.ArithmeticSentence) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hσ : U ⊬ σ) (hAbs : T ⊬ ∼FFL.FirstOrder.Arithmetic.Bootstrapping.provabilityPred U σ) : ∃ (F : Graph) (I : Graph) (G : Graph), Functional F ∧ Functional I ∧ Functional G ∧ Pointwise T F I ∧ ¬Pointwise T (comp F G) (comp I G)