Witness comparisons of provability

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

Equations

• T.ProvabilityComparisonLE φ ψ = ∃ (b : V), LO.FirstOrder.Arithmetic.Bootstrapping.Proof T b φ ∧ ∀ b' < b, ¬LO.FirstOrder.Arithmetic.Bootstrapping.Proof T b' ψ

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

Equations

• T.ProvabilityComparisonLT φ ψ = ∃ (b : V), LO.FirstOrder.Arithmetic.Bootstrapping.Proof T b φ ∧ ∀ b' ≤ b, ¬LO.FirstOrder.Arithmetic.Bootstrapping.Proof T b' ψ

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

Equations

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

instance LO.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 LO.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 LO.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 LO.FirstOrder.Theory.provabilityComparisonLT {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚺₁.Semisentence 2

Equations

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

instance LO.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 LO.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 LO.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 LO.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 LO.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 LO.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 LO.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 LO.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 LO.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 LO.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 LO.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 LO.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} {i : ι} [Fintype ι] (φ : ι → V) (H : Provable T (φ i)) : ∃ (j : ι), ∀ (k : ι), T.ProvabilityComparisonLE (φ j) (φ k)