Supporting results for pointwise provable equality.

Witness comparisons of provability

def PointwiseComposition.FFL.FirstOrder.Theory.ProvabilityComparisonLE {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ ψ : V) : Prop

The Provability Comparison LE construction in FFL.FirstOrder.Theory.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Theory.ProvabilityComparisonLT {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ ψ : V) : Prop

The Provability Comparison LT construction in FFL.FirstOrder.Theory.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.provabilityComparisonLE {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Σ₁.Semisentence 2

The provability Comparison LE construction in FFL.FirstOrder.Theory.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Theory.provability_comparison_le_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Σ₁-Relation T.ProvabilityComparisonLE via T.provabilityComparisonLE

instance PointwiseComposition.FFL.FirstOrder.Theory.provability_comparison_le_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Σ₁-Relation T.ProvabilityComparisonLE

instance PointwiseComposition.FFL.FirstOrder.Theory.provability_comparison_le_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : { Γ := Σ, rank := 0 + 1 }-Relation T.ProvabilityComparisonLE

instance for definability tactic

noncomputable def PointwiseComposition.FFL.FirstOrder.Theory.provabilityComparisonLT {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Σ₁.Semisentence 2

The provability Comparison LT construction in FFL.FirstOrder.Theory.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Theory.provability_comparison_lt_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Σ₁-Relation T.ProvabilityComparisonLT via T.provabilityComparisonLT

instance PointwiseComposition.FFL.FirstOrder.Theory.provability_comparison_lt_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Σ₁-Relation T.ProvabilityComparisonLT

instance PointwiseComposition.FFL.FirstOrder.Theory.provability_comparison_lt_definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : { Γ := Σ, rank := 0 + 1 }-Relation T.ProvabilityComparisonLT

instance for definability tactic

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.le_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ ψ : V} : T.ProvabilityComparisonLT φ ψ → T.ProvabilityComparisonLE φ ψ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.le_to_provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ ψ : V} : T.ProvabilityComparisonLE φ ψ → Provable T φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.le_trans {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ ψ χ : V} : T.ProvabilityComparisonLE φ ψ → T.ProvabilityComparisonLE ψ χ → T.ProvabilityComparisonLE φ χ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.le_antisymm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ ψ : V} : T.ProvabilityComparisonLE φ ψ → T.ProvabilityComparisonLE ψ φ → φ = ψ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.iff_le_refl_provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : T.ProvabilityComparisonLE φ φ ↔ Provable T φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.lt_irrefl {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : ¬T.ProvabilityComparisonLT φ φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.lt_trans {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ ψ χ : V} : T.ProvabilityComparisonLT φ ψ → T.ProvabilityComparisonLT ψ χ → T.ProvabilityComparisonLT φ χ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.not_lt_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ ψ : V} : T.ProvabilityComparisonLE φ ψ → ¬T.ProvabilityComparisonLT ψ φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ProvabilityComparison.find_minimal_proof_fintype {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {ι : Type u_2} [Finite ι] (φ : ι → V) {i : ι} (H : Provable T (φ i)) : ∃ (j : ι), ∀ (k : ι), T.ProvabilityComparisonLE (φ j) (φ k)