Supporting results for pointwise provable equality.

Sigma-one soundness is enough to make pointwise provability sound for the standard extensions of arbitrary Sigma-one graphs. This statement needs neither graph functionality nor an enumerability assumption on the theory.

def PointwiseComposition.FailureOfComposition.GeneratedCongruence.SigmaOneSound (T : FFL.FirstOrder.ArithmeticTheory) : Prop

Every Sigma-one sentence proved by the theory is true in the standard natural numbers.

Equations

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

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.not_sigmaOneSound_iff (T : FFL.FirstOrder.ArithmeticTheory) : ¬SigmaOneSound T ↔ ∃ (σ : FFL.FirstOrder.ArithmeticSentence), FFL.FirstOrder.Arithmetic.Hierarchy Σ 1 σ ∧ T ⊢ σ ∧ ¬ℕ↓[ℒₒᵣ] ⊧ σ

Failure of Sigma-one soundness supplies a single false proved Sigma-one sentence. No consistency hypothesis is required.

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.sigmaOneSound_iff_nonempty_soundOnHierarchy (T : FFL.FirstOrder.ArithmeticTheory) : SigmaOneSound T ↔ Nonempty (T.SoundOnHierarchy Σ 1)

The propositional formulation agrees with Foundation's soundness class.

theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.pointwise_implies_extensional_of_sigmaOneSound (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : SigmaOneSound T) (F G : ProofSearch.Graph) (hFG : ProofSearch.Pointwise T F G) : PiOneCharacterization.Extensional F G

Sigma-one soundness turns each pointwise proof into equality of standard graphs, without assuming that either graph is functional.