add(Incompleteness): Add LT version WitnessComparison (#780)

Author: SnO2WMaN

Foundation/FirstOrder/Incompleteness/RosserProvability.lean

@@ -15,12 +15,12 @@ variable {L : Language} [L.Encodable] [L.LORDefinable]
 
 variable (T : Theory L) [T.Δ₁]
 
-def _root_.LO.FirstOrder.Theory.RosserProvable (φ : V) : Prop := T.ProvabilityComparison φ (neg L φ)
+def _root_.LO.FirstOrder.Theory.RosserProvable (φ : V) : Prop := T.ProvabilityComparisonLE φ (neg L φ)
 
 section
 
 noncomputable def _root_.LO.FirstOrder.Theory.rosserProvable : 𝚺₁.Semisentence 1 := .mkSigma
-  “φ. ∃ nφ, !(negGraph L) nφ φ ∧ !T.provabilityComparison φ nφ”
+  “φ. ∃ nφ, !(negGraph L) nφ φ ∧ !T.provabilityComparisonLE φ nφ”
 
 instance _root_.LO.FirstOrder.Theory.RosserProvable_defined :
     𝚺₁-Predicate (T.RosserProvable : V → Prop) via T.rosserProvable := .mk fun v ↦ by
@@ -35,10 +35,10 @@ end
 
 variable {T}
 
-lemma rosser_quote {φ : SyntacticFormula L} : T.RosserProvable (V := V) ⌜φ⌝ ↔ T.ProvabilityComparison (V := V) ⌜φ⌝ ⌜∼φ⌝ := by
+lemma rosser_quote {φ : SyntacticFormula L} : T.RosserProvable (V := V) ⌜φ⌝ ↔ T.ProvabilityComparisonLE (V := V) ⌜φ⌝ ⌜∼φ⌝ := by
   simp [Theory.RosserProvable, Semiformula.quote_def]
 
-lemma rosser_quote₀ {φ : Sentence L} : T.RosserProvable (V := V) ⌜φ⌝ ↔ T.ProvabilityComparison (V := V) ⌜φ⌝ ⌜∼φ⌝ := by
+lemma rosser_quote₀ {φ : Sentence L} : T.RosserProvable (V := V) ⌜φ⌝ ↔ T.ProvabilityComparisonLE (V := V) ⌜φ⌝ ⌜∼φ⌝ := by
   simpa [Sentence.quote_def] using rosser_quote
 
 lemma rosser_quote_def {φ : SyntacticFormula L} :
@@ -47,7 +47,7 @@ lemma rosser_quote_def {φ : SyntacticFormula L} :
 lemma rosser_quote_def₀ {φ : Sentence L} :
     T.RosserProvable (V := V) ⌜φ⌝ ↔ ∃ b : V, T.Proof b ⌜φ⌝ ∧ ∀ b' < b, ¬T.Proof b' ⌜∼φ⌝ := by simpa [Sentence.quote_def] using rosser_quote
 
-def RosserProvable.to_provable {φ : V} : T.RosserProvable φ → T.Provable φ := ProvabilityComparison.to_provable
+def RosserProvable.to_provable {φ : V} : T.RosserProvable φ → T.Provable φ := ProvabilityComparison.le_to_provable
 
 lemma provable_of_standard_proof {n : ℕ} {φ : Sentence L} : T.Proof (n : V) ⌜φ⌝ → T ⊢ φ := fun h ↦ by
   have : T.Proof n ⌜φ⌝ ↔ T.Proof (↑n : V) ⌜φ⌝ := by
@@ -81,10 +81,7 @@ def not_rosserProvable [Entailment.Consistent T] {φ : Sentence L} : T ⊢ ∼φ
   let n : ℕ := ⌜h.get⌝
   have hn : T.Proof (↑n : V) ⌜∼φ⌝ := by simp [n, coe_quote_proof_eq]
   rcases rosser_quote₀.mp r with ⟨b, hb, Hb⟩
-  have : b ≤ n := by
-    by_contra A
-    have : ¬T.Proof (↑n : V) ⌜∼φ⌝ := Hb n (lt_of_not_ge A)
-    contradiction
+  have : b ≤ n := by grind;
   rcases eq_nat_of_le_nat this with ⟨b, rfl⟩
   have : T ⊢ φ := provable_of_standard_proof hb
   have : Entailment.Inconsistent T := Entailment.inconsistent_of_provable_of_unprovable this h

Foundation/FirstOrder/Incompleteness/WitnessComparison.lean

@@ -17,60 +17,99 @@ variable {L : Language} [L.Encodable] [L.LORDefinable]
 
 variable (T : Theory L) [T.Δ₁]
 
-def _root_.LO.FirstOrder.Theory.ProvabilityComparison (φ ψ : V) : Prop :=
+def _root_.LO.FirstOrder.Theory.ProvabilityComparisonLE (φ ψ : V) : Prop :=
   ∃ b, T.Proof b φ ∧ ∀ b' < b, ¬T.Proof b' ψ
 
+def _root_.LO.FirstOrder.Theory.ProvabilityComparisonLT (φ ψ : V) : Prop :=
+  ∃ b, T.Proof b φ ∧ ∀ b' ≤ b, ¬T.Proof b' ψ
+
 section
 
-noncomputable def _root_.LO.FirstOrder.Theory.provabilityComparison : 𝚺₁.Semisentence 2 := .mkSigma
+noncomputable def _root_.LO.FirstOrder.Theory.provabilityComparisonLE : 𝚺₁.Semisentence 2 := .mkSigma
   “φ ψ. ∃ b, !T.proof.sigma b φ ∧ ∀ b' < b, ¬!T.proof.pi b' ψ”
 
-instance _root_.LO.FirstOrder.Theory.provability_comparison_defined :
-    𝚺₁-Relation[V] T.ProvabilityComparison via T.provabilityComparison := .mk fun v ↦ by
-  simp [Theory.provabilityComparison, Theory.ProvabilityComparison]
+instance _root_.LO.FirstOrder.Theory.provability_comparison_le_defined :
+    𝚺₁-Relation[V] T.ProvabilityComparisonLE via T.provabilityComparisonLE := .mk fun v ↦ by
+  simp [Theory.provabilityComparisonLE, Theory.ProvabilityComparisonLE]
+
+instance _root_.LO.FirstOrder.Theory.provability_comparison_le_definable : 𝚺₁-Relation[V] T.ProvabilityComparisonLE :=
+  T.provability_comparison_le_defined.to_definable
+
+/-- instance for definability tactic -/
+instance _root_.LO.FirstOrder.Theory.provability_comparison_le_definable' :
+    𝚺-[0 + 1]-Relation[V] T.ProvabilityComparisonLE := T.provability_comparison_le_definable
+
 
-instance _root_.LO.FirstOrder.Theory.provability_comparison_definable : 𝚺₁-Relation[V] T.ProvabilityComparison :=
-  T.provability_comparison_defined.to_definable
+noncomputable def _root_.LO.FirstOrder.Theory.provabilityComparisonLT : 𝚺₁.Semisentence 2 := .mkSigma
+  “φ ψ. ∃ b, !T.proof.sigma b φ ∧ ∀ b' <⁺ b, ¬!T.proof.pi b' ψ”
 
-/-- instance for definability tactic-/
-instance _root_.LO.FirstOrder.Theory.provability_comparison_definable' :
-    𝚺-[0 + 1]-Relation[V] T.ProvabilityComparison := T.provability_comparison_definable
+instance _root_.LO.FirstOrder.Theory.provability_comparison_lt_defined :
+    𝚺₁-Relation[V] T.ProvabilityComparisonLT via T.provabilityComparisonLT := .mk fun v ↦ by
+  simp [Theory.provabilityComparisonLT, Theory.ProvabilityComparisonLT]
+
+instance _root_.LO.FirstOrder.Theory.provability_comparison_lt_definable : 𝚺₁-Relation[V] T.ProvabilityComparisonLT :=
+  T.provability_comparison_lt_defined.to_definable
+
+/-- instance for definability tactic -/
+instance _root_.LO.FirstOrder.Theory.provability_comparison_lt_definable' :
+    𝚺-[0 + 1]-Relation[V] T.ProvabilityComparisonLT := T.provability_comparison_lt_definable
 
 end
 
-variable {T}
+variable {T : Theory L} [T.Δ₁]
 
 namespace ProvabilityComparison
 
-variable {φ ψ : V}
+variable {φ ψ χ : V}
 
-lemma to_provable : T.ProvabilityComparison φ ψ → T.Provable φ := by rintro ⟨b, hb, _⟩; exact ⟨b, hb⟩
+local infixl:50 "≼" => T.ProvabilityComparisonLE
+local infixl:50 "≺" => T.ProvabilityComparisonLT
+local prefix:50 "□" => T.Provable
 
-lemma refl_iff_provable : T.ProvabilityComparison φ φ ↔ T.Provable φ := by
-  constructor
-  · exact to_provable
-  · rintro ⟨b, hb⟩
-    have : ∃ b, T.Proof b φ ∧ ∀ z < b, ¬T.Proof z φ :=
-      InductionOnHierarchy.least_number_sigma 𝚺 1 (P := (T.Proof · φ)) (by definability) hb
-    rcases this with ⟨b, bd, h⟩
-    exact ⟨b, bd, h⟩
+@[grind =>]
+lemma le_of_lt : φ ≺ ψ → φ ≼ ψ := by rintro ⟨b, _⟩; exact ⟨b, by grind⟩
+
+@[grind =>]
+lemma le_to_provable : φ ≼ ψ → □φ := by rintro ⟨b, hb, _⟩; exact ⟨b, by grind⟩
+
+@[grind =>]
+lemma le_trans : φ ≼ ψ → ψ ≼ χ → φ ≼ χ := by rintro ⟨b, hb, h⟩ ⟨d, hd, H⟩; use b; grind;
 
-lemma antisymm : T.ProvabilityComparison φ ψ → T.ProvabilityComparison ψ φ → φ = ψ := by
+@[grind =>]
+lemma le_antisymm : φ ≼ ψ → ψ ≼ φ → φ = ψ := by
   rintro ⟨b, hb, Hb⟩ ⟨d, hd, Hd⟩
   have : b = d := by
     by_contra ne
     wlog lt : b < d
-    · have : b ≤ d := le_of_not_gt <| this d hd Hd b hb Hb (Ne.symm ne)
-      have : d ≤ b := le_of_not_gt lt
-      have : b = d := le_antisymm (by assumption) (by assumption)
-      contradiction
+    · grind;
     have : ¬T.Proof b φ := Hd b lt
     contradiction
   have : ({φ} : V) = {ψ} := by simp [←hb.1, ←hd.1, this]
   simpa using this
 
-lemma find_minimal_proof_fintype [Fintype ι] (φ : ι → V) (H : T.Provable (φ i)) :
-    ∃ j, ∀ k, T.ProvabilityComparison (φ j) (φ k) := by
+
+lemma iff_le_refl_provable : φ ≼ φ ↔ □φ := by
+  constructor
+  · exact le_to_provable
+  · rintro ⟨b, hb⟩
+    have : ∃ b, T.Proof b φ ∧ ∀ z < b, ¬T.Proof z φ :=
+      InductionOnHierarchy.least_number_sigma 𝚺 1 (P := (T.Proof · φ)) (by definability) hb
+    rcases this with ⟨b, bd, h⟩
+    exact ⟨b, bd, h⟩
+
+@[grind .]
+lemma lt_irrefl : ¬φ ≺ φ := by rintro ⟨b, hb, h⟩; have : ¬T.Proof b φ := h b (by simp); contradiction
+
+@[grind =>]
+lemma lt_trans : φ ≺ ψ → ψ ≺ χ → φ ≺ χ := by rintro ⟨b, hb, h⟩ ⟨d, hd, H⟩; use b; grind;
+
+
+@[grind =>]
+lemma not_lt_of_le : φ ≼ ψ → ¬ψ ≺ φ := by grind;
+
+
+lemma find_minimal_proof_fintype [Fintype ι] (φ : ι → V) (H : □(φ i)) :
+    ∃ j, ∀ k, (φ j) ≼ (φ k) := by
   rcases show ∃ dᵢ, T.Proof dᵢ (φ i)from H with ⟨dᵢ, Hdᵢ⟩
   have : ∃ z, (∃ j, T.Proof z (φ j)) ∧ ∀ w < z, ∀ x, ¬T.Proof w (φ x) := by
     simpa using

Foundation/ProvabilityLogic/SolovaySentences.lean

@@ -144,16 +144,16 @@ section model
 
 variable (T) {V : Type*} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁]
 
-def NegativeSuccessor (φ ψ : V) : Prop := T.ProvabilityComparison (neg ℒₒᵣ φ) (neg ℒₒᵣ ψ)
+def NegativeSuccessor (φ ψ : V) : Prop := T.ProvabilityComparisonLE (neg ℒₒᵣ φ) (neg ℒₒᵣ ψ)
 
-lemma NegativeSuccessor.quote_iff_provabilityComparison {φ ψ : Sentence ℒₒᵣ} :
-    NegativeSuccessor (V := V) T ⌜φ⌝ ⌜ψ⌝ ↔ T.ProvabilityComparison (V := V) ⌜∼φ⌝ ⌜∼ψ⌝ := by
+lemma NegativeSuccessor.quote_iff_provabilityComparisonLE {φ ψ : Sentence ℒₒᵣ} :
+    NegativeSuccessor (V := V) T ⌜φ⌝ ⌜ψ⌝ ↔ T.ProvabilityComparisonLE (V := V) ⌜∼φ⌝ ⌜∼ψ⌝ := by
   simp [NegativeSuccessor, Sentence.quote_def, Semiformula.quote_def]
 
 section
 
 def negativeSuccessor : 𝚺₁.Semisentence 2 := .mkSigma
-  “φ ψ. ∃ nφ, ∃ nψ, !(negGraph ℒₒᵣ) nφ φ ∧ !(negGraph ℒₒᵣ) nψ ψ ∧ !T.provabilityComparison nφ nψ”
+  “φ ψ. ∃ nφ, ∃ nψ, !(negGraph ℒₒᵣ) nφ φ ∧ !(negGraph ℒₒᵣ) nψ ψ ∧ !T.provabilityComparisonLE nφ nψ”
 
 instance negativeSuccessor_defined : 𝚺₁-Relation[V] NegativeSuccessor T via (negativeSuccessor T) := .mk fun v ↦ by
   simp [negativeSuccessor, NegativeSuccessor]
@@ -367,9 +367,9 @@ private lemma Solovay.exclusive.comparable {i₁ i₂ : F} {ε₁ ε₂ : List F
       rcases hji₁ε₂ with ⟨η₁, η₂, rfl⟩
       have Θε₂ : ΘChain T V (η₁ ++ j :: i₁ :: η₂) := by simpa using Θε₂
       exact ΘChain.cons_cons_iff'.mp (ΘChain.append_iff.mp Θε₂).2 |>.1
-    have : ∀ k, i₁ ≺ k → T.ProvabilityComparison (V := V) ⌜∼T.solovay j⌝ ⌜∼T.solovay k⌝ := by
-      simpa [NegativeSuccessor.quote_iff_provabilityComparison] using ΘChain.cons_cons_iff.mp this
-    exact (ProvabilityComparison.refl_iff_provable (L := ℒₒᵣ)).mp (this j hij₁)
+    have : ∀ k, i₁ ≺ k → T.ProvabilityComparisonLE (V := V) ⌜∼T.solovay j⌝ ⌜∼T.solovay k⌝ := by
+      simpa [NegativeSuccessor.quote_iff_provabilityComparisonLE] using ΘChain.cons_cons_iff.mp this
+    exact (ProvabilityComparison.iff_le_refl_provable (L := ℒₒᵣ)).mp (this j hij₁)
   contradiction
 
 /-- Condition 1.-/
@@ -399,15 +399,15 @@ lemma Solovay.exclusive {i₁ i₂ : F} (ne : i₁ ≠ i₂) : T.Solovay V i₁
     rcases hj₂ with ⟨_, rfl⟩
     have : ΘChain T V ([j₂] ++ k :: ε) := (ΘChain.append_iff.mp Θε₂).2
     simpa using (ΘChain.append_iff.mp this).1
-  have P₁ : T.ProvabilityComparison (V := V) ⌜∼T.solovay j₁⌝ ⌜∼T.solovay j₂⌝ := by
-    simpa [NegativeSuccessor.quote_iff_provabilityComparison] using
+  have P₁ : T.ProvabilityComparisonLE (V := V) ⌜∼T.solovay j₁⌝ ⌜∼T.solovay j₂⌝ := by
+    simpa [NegativeSuccessor.quote_iff_provabilityComparisonLE] using
       ΘChain.doubleton_iff.mp C₁ j₂
         (cε₂.rel_of_infix _ _ <| List.infix_iff_prefix_suffix.mpr ⟨j₂ :: k :: ε, by simp, hj₂⟩)
-  have P₂ : T.ProvabilityComparison (V := V) ⌜∼T.solovay j₂⌝ ⌜∼T.solovay j₁⌝ := by
-    simpa [NegativeSuccessor.quote_iff_provabilityComparison] using
+  have P₂ : T.ProvabilityComparisonLE (V := V) ⌜∼T.solovay j₂⌝ ⌜∼T.solovay j₁⌝ := by
+    simpa [NegativeSuccessor.quote_iff_provabilityComparisonLE] using
       ΘChain.doubleton_iff.mp C₂ j₁
         (cε₁.rel_of_infix _ _ <| List.infix_iff_prefix_suffix.mpr ⟨j₁ :: k :: ε, by simp, hj₁⟩)
-  have : j₁ = j₂ := by simpa using ProvabilityComparison.antisymm (V := V) P₁ P₂
+  have : j₁ = j₂ := by simpa using ProvabilityComparison.le_antisymm (V := V) P₁ P₂
   contradiction
 
 /-- Condition 2.-/
@@ -419,9 +419,9 @@ lemma Solovay.refute (ne : F.root.1 ≠ i) : T.Solovay V i → T.Provable (⌜
   rcases show Θ T V i from h.1 with ⟨ε, hε, cε⟩
   rcases List.ChainI.prec_exists_of_ne hε (Ne.symm ne) with ⟨ε', i', hii', rfl, hε'⟩
   have : ∀ k, i' ≺ k → NegativeSuccessor T ⌜T.solovay i⌝ ⌜T.solovay k⌝ := (ΘChain.cons_cons_iff.mp cε).2
-  have : T.ProvabilityComparison (V := V) ⌜∼T.solovay i⌝ ⌜∼T.solovay i⌝ := by
-    simpa [NegativeSuccessor.quote_iff_provabilityComparison] using this i hii'
-  exact (ProvabilityComparison.refl_iff_provable (T := T)).mp this
+  have : T.ProvabilityComparisonLE (V := V) ⌜∼T.solovay i⌝ ⌜∼T.solovay i⌝ := by
+    simpa [NegativeSuccessor.quote_iff_provabilityComparisonLE] using this i hii'
+  exact (ProvabilityComparison.iff_le_refl_provable (T := T)).mp this
 
 lemma Θ.disjunction (i : F) : Θ T V i → T.Solovay V i ∨ ∃ j, i ≺ j ∧ T.Solovay V j := by
   have : IsConverseWellFounded F (· ≺ ·) := inferInstance
@@ -430,7 +430,7 @@ lemma Θ.disjunction (i : F) : Θ T V i → T.Solovay V i ∨ ∃ j, i ≺ j ∧
   by_cases hS : T.Solovay V i
   · left; exact hS
   · right
-    have : ∃ j, i ≺ j ∧ ∀ k, i ≺ k → T.ProvabilityComparison (V := V) ⌜∼T.solovay j⌝ ⌜∼T.solovay k⌝ := by
+    have : ∃ j, i ≺ j ∧ ∀ k, i ≺ k → T.ProvabilityComparisonLE (V := V) ⌜∼T.solovay j⌝ ⌜∼T.solovay k⌝ := by
       have : ∃ j, i ≺ j ∧ T.Provable (⌜∼T.solovay j⌝ : V) := by
         have : Θ T V i → ∃ x, i ≺ x ∧ T.Provable (⌜∼T.solovay x⌝ : V) := by
           simpa [Theory.ConsistentWith.quote_iff, Theory.Solovay] using hS
@@ -445,7 +445,7 @@ lemma Θ.disjunction (i : F) : Θ T V i → T.Solovay V i ∨ ∃ j, i ≺ j ∧
       exact ⟨
         j :: ε,
         hε.cons hij,
-        cε.cons_of hε (by simpa [NegativeSuccessor.quote_iff_provabilityComparison]) hij⟩
+        cε.cons_of hε (by simpa [NegativeSuccessor.quote_iff_provabilityComparisonLE]) hij⟩
     have : T.Solovay V j ∨ ∃ k, j ≺ k ∧ T.Solovay V k := ih j hij this
     rcases this with (hSj | ⟨k, hjk, hSk⟩)
     · exact ⟨j, hij, hSj⟩