@@ -17,60 +17,99 @@ variable {L : Language} [L.Encodable] [L.LORDefinable]
1717
1818variable (T : Theory L) [T.Δ₁]
1919
20- def _root_.LO.FirstOrder.Theory.ProvabilityComparison (φ ψ : V) : Prop :=
20+ def _root_.LO.FirstOrder.Theory.ProvabilityComparisonLE (φ ψ : V) : Prop :=
2121 ∃ b, T.Proof b φ ∧ ∀ b' < b, ¬T.Proof b' ψ
2222
23+ def _root_.LO.FirstOrder.Theory.ProvabilityComparisonLT (φ ψ : V) : Prop :=
24+ ∃ b, T.Proof b φ ∧ ∀ b' ≤ b, ¬T.Proof b' ψ
25+
2326section
2427
25- noncomputable def _root_.LO.FirstOrder.Theory.provabilityComparison : 𝚺₁.Semisentence 2 := .mkSigma
28+ noncomputable def _root_.LO.FirstOrder.Theory.provabilityComparisonLE : 𝚺₁.Semisentence 2 := .mkSigma
2629 “φ ψ. ∃ b, !T.proof.sigma b φ ∧ ∀ b' < b, ¬!T.proof.pi b' ψ”
2730
28- instance _root_.LO.FirstOrder.Theory.provability_comparison_defined :
29- 𝚺₁-Relation[V] T.ProvabilityComparison via T.provabilityComparison := .mk fun v ↦ by
30- simp [Theory.provabilityComparison, Theory.ProvabilityComparison]
31+ instance _root_.LO.FirstOrder.Theory.provability_comparison_le_defined :
32+ 𝚺₁-Relation[V] T.ProvabilityComparisonLE via T.provabilityComparisonLE := .mk fun v ↦ by
33+ simp [Theory.provabilityComparisonLE, Theory.ProvabilityComparisonLE]
34+
35+ instance _root_.LO.FirstOrder.Theory.provability_comparison_le_definable : 𝚺₁-Relation[V] T.ProvabilityComparisonLE :=
36+ T.provability_comparison_le_defined.to_definable
37+
38+ /-- instance for definability tactic -/
39+ instance _root_.LO.FirstOrder.Theory.provability_comparison_le_definable' :
40+ 𝚺-[0 + 1 ]-Relation[V] T.ProvabilityComparisonLE := T.provability_comparison_le_definable
41+
3142
32- instance _root_.LO.FirstOrder.Theory.provability_comparison_definable : 𝚺₁-Relation[V] T.ProvabilityComparison :=
33- T.provability_comparison_defined.to_definable
43+ noncomputable def _root_.LO.FirstOrder.Theory.provabilityComparisonLT : 𝚺₁.Semisentence 2 := .mkSigma
44+ “φ ψ. ∃ b, !T.proof.sigma b φ ∧ ∀ b' <⁺ b, ¬!T.proof.pi b' ψ”
3445
35- /-- instance for definability tactic-/
36- instance _root_.LO.FirstOrder.Theory.provability_comparison_definable' :
37- 𝚺-[0 + 1 ]-Relation[V] T.ProvabilityComparison := T.provability_comparison_definable
46+ instance _root_.LO.FirstOrder.Theory.provability_comparison_lt_defined :
47+ 𝚺₁-Relation[V] T.ProvabilityComparisonLT via T.provabilityComparisonLT := .mk fun v ↦ by
48+ simp [Theory.provabilityComparisonLT, Theory.ProvabilityComparisonLT]
49+
50+ instance _root_.LO.FirstOrder.Theory.provability_comparison_lt_definable : 𝚺₁-Relation[V] T.ProvabilityComparisonLT :=
51+ T.provability_comparison_lt_defined.to_definable
52+
53+ /-- instance for definability tactic -/
54+ instance _root_.LO.FirstOrder.Theory.provability_comparison_lt_definable' :
55+ 𝚺-[0 + 1 ]-Relation[V] T.ProvabilityComparisonLT := T.provability_comparison_lt_definable
3856
3957end
4058
41- variable {T}
59+ variable {T : Theory L} [T.Δ₁]
4260
4361namespace ProvabilityComparison
4462
45- variable {φ ψ : V}
63+ variable {φ ψ χ : V}
4664
47- lemma to_provable : T.ProvabilityComparison φ ψ → T.Provable φ := by rintro ⟨b, hb, _⟩; exact ⟨b, hb⟩
65+ local infixl :50 " ≼"
66+ local infixl :50 " ≺"
67+ local prefix :50 " □"
4868
49- lemma refl_iff_provable : T.ProvabilityComparison φ φ ↔ T.Provable φ := by
50- constructor
51- · exact to_provable
52- · rintro ⟨b, hb⟩
53- have : ∃ b, T.Proof b φ ∧ ∀ z < b, ¬T.Proof z φ :=
54- InductionOnHierarchy.least_number_sigma 𝚺 1 (P := (T.Proof · φ)) ( by definability) hb
55- rcases this with ⟨b, bd, h⟩
56- exact ⟨b, bd , h⟩
69+ @[grind =>]
70+ lemma le_of_lt : φ ≺ ψ → φ ≼ ψ := by rintro ⟨b, _⟩; exact ⟨b, by grind⟩
71+
72+ @[grind =>]
73+ lemma le_to_provable : φ ≼ ψ → □φ := by rintro ⟨ b, hb, _⟩; exact ⟨b, by grind⟩
74+
75+ @[grind =>]
76+ lemma le_trans : φ ≼ ψ → ψ ≼ χ → φ ≼ χ := by rintro ⟨b, hb , h⟩ ⟨d, hd, H⟩; use b; grind;
5777
58- lemma antisymm : T.ProvabilityComparison φ ψ → T.ProvabilityComparison ψ φ → φ = ψ := by
78+ @[grind =>]
79+ lemma le_antisymm : φ ≼ ψ → ψ ≼ φ → φ = ψ := by
5980 rintro ⟨b, hb, Hb⟩ ⟨d, hd, Hd⟩
6081 have : b = d := by
6182 by_contra ne
6283 wlog lt : b < d
63- · have : b ≤ d := le_of_not_gt <| this d hd Hd b hb Hb (Ne.symm ne)
64- have : d ≤ b := le_of_not_gt lt
65- have : b = d := le_antisymm (by assumption) (by assumption)
66- contradiction
84+ · grind;
6785 have : ¬T.Proof b φ := Hd b lt
6886 contradiction
6987 have : ({φ} : V) = {ψ} := by simp [←hb.1 , ←hd.1 , this ]
7088 simpa using this
7189
72- lemma find_minimal_proof_fintype [Fintype ι] (φ : ι → V) (H : T.Provable (φ i)) :
73- ∃ j, ∀ k, T.ProvabilityComparison (φ j) (φ k) := by
90+
91+ lemma iff_le_refl_provable : φ ≼ φ ↔ □φ := by
92+ constructor
93+ · exact le_to_provable
94+ · rintro ⟨b, hb⟩
95+ have : ∃ b, T.Proof b φ ∧ ∀ z < b, ¬T.Proof z φ :=
96+ InductionOnHierarchy.least_number_sigma 𝚺 1 (P := (T.Proof · φ)) (by definability) hb
97+ rcases this with ⟨b, bd, h⟩
98+ exact ⟨b, bd, h⟩
99+
100+ @[grind .]
101+ lemma lt_irrefl : ¬φ ≺ φ := by rintro ⟨b, hb, h⟩; have : ¬T.Proof b φ := h b (by simp); contradiction
102+
103+ @[grind =>]
104+ lemma lt_trans : φ ≺ ψ → ψ ≺ χ → φ ≺ χ := by rintro ⟨b, hb, h⟩ ⟨d, hd, H⟩; use b; grind;
105+
106+
107+ @[grind =>]
108+ lemma not_lt_of_le : φ ≼ ψ → ¬ψ ≺ φ := by grind;
109+
110+
111+ lemma find_minimal_proof_fintype [Fintype ι] (φ : ι → V) (H : □(φ i)) :
112+ ∃ j, ∀ k, (φ j) ≼ (φ k) := by
74113 rcases show ∃ dᵢ, T.Proof dᵢ (φ i)from H with ⟨dᵢ, Hdᵢ⟩
75114 have : ∃ z, (∃ j, T.Proof z (φ j)) ∧ ∀ w < z, ∀ x, ¬T.Proof w (φ x) := by
76115 simpa using
0 commit comments