Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@iehality
iehality committed Jul 24, 2024
1 parent 71d6e97 commit 37ff63b
Show file tree
Hide file tree
Showing 4 changed files with 125 additions and 17 deletions.
78 changes: 65 additions & 13 deletions Arithmetization/ISigmaOne/Metamath/FormalizedSigmaOneCompleteness.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,33 @@ def toNumVec {n} (e : Fin n → V) : (Language.codeIn ℒₒᵣ V).TSemitermVec

@[simp] lemma toNumVec_nth {n} (e : Fin n → V) (i : Fin n) : (toNumVec e).nth i = ↑(e i) := by ext; simp [toNumVec]

@[simp] lemma toNumVec_val_nth {n} (e : Fin n → V) (i : Fin n) : (toNumVec e).val.[i] = numeral (e i) := by simp [toNumVec]

/-- TODO: move-/
@[simp] lemma coe_coe_lt {n} (i : Fin n) : (i : V) < (n : V) :=
calc (i : V) < (i : V) + (n - i : V) := by simp
_ = (n : V) := by simp

@[simp] lemma cast_substs_numVec (p : Semisentence ℒₒᵣ (n + 1)) :
((.cast (V := V) (n := ↑(n + 1)) (n' := ↑n + 1) ⌜Rew.embₙ.hom p⌝ (by simp)) ^/[(toNumVec e).q.substs (typedNumeral 0 x).sing]) =
⌜Rew.embₙ.hom p⌝ ^/[toNumVec (x :> e)] := by
have : (toNumVec e).q.substs (typedNumeral 0 x).sing = x ∷ᵗ toNumVec e := by
ext; simp
apply nth_ext' ((↑n : V) + 1)
(by rw [len_termSubstVec]; simpa using (toNumVec e).prop.qVec)
(by simp [←(toNumVec e).prop.1])
intro i hi
rw [nth_termSubstVec (by simpa using (toNumVec e).prop.qVec) hi]
rcases zero_or_succ i with (rfl | ⟨i, rfl⟩)
· simp [Language.qVec]
· simp only [Language.qVec, nth_cons_succ, Language.TSemitermVec.prop]
rcases eq_fin_of_lt_nat (by simpa using hi) with ⟨i, rfl⟩
rw [nth_termBShiftVec (by simp)]
simp; exact coe_coe_lt (V := V) i
rw [this]
ext; simp [toNumVec]


namespace TProof

open Language.Theory.TProof System
Expand Down Expand Up @@ -80,9 +107,11 @@ open FirstOrder.Arith

theorem boldSigma₁Complete : ∀ {n} {σ : Semisentence ℒₒᵣ n},
Hierarchy 𝚺 1 σ → ∀ {e}, Semiformula.Evalbm V e σ → T ⊢! ⌜Rew.embₙ.hom σ⌝^/[toNumVec e]
| _, _, Hierarchy.verum _ _ _, _, h => by simp
| _, _, Hierarchy.falsum _ _ _, _, h => by simp at h
| _, _, Hierarchy.rel _ _ Language.Eq.eq v, e, h => by { simp [Rew.rel]; sorry }
| _, _, Hierarchy.verum _ _ _, _, h => by simp only [LogicalConnective.HomClass.map_top,
Semiformula.codeIn'_verum, Language.TSemiformula.substs_verum, Language.TSemiformula.neg_verum,
Language.TSemiformula.neg_falsum, verum!, dne'!]
| _, _, Hierarchy.falsum _ _ _, _, h => by sorry
| _, _, Hierarchy.rel _ _ Language.Eq.eq v, e, h => by sorry
| _, _, Hierarchy.nrel _ _ Language.Eq.eq v, e, h => by sorry
| _, _, Hierarchy.rel _ _ Language.LT.lt v, e, h => by sorry
| _, _, Hierarchy.nrel _ _ Language.LT.lt v, e, h => by sorry
Expand All @@ -94,17 +123,40 @@ theorem boldSigma₁Complete : ∀ {n} {σ : Semisentence ℒₒᵣ n},
rcases this with (h | h)
· simpa using or₁'! (boldSigma₁Complete hp h)
· simpa using or₂'! (boldSigma₁Complete hq h)
| _, _, Hierarchy.ball pt hp, e, h => by {
| _, _, Hierarchy.ball (p := p) pt hp, e, h => by
rcases Rew.positive_iff.mp pt with ⟨t, rfl⟩
have := termEqComplete T e t
simp [←Rew.emb_bShift_term]
sorry


}
| _, _, Hierarchy.bex pt hp, e, h => by sorry
| _, _, Hierarchy.sigma (p := p) hp, e, h => by sorry
| _, _, Hierarchy.ex hp, e, h => by sorry
simp only [Rew.ball, Rew.q_emb, Rew.hom_finitary2, Rew.emb_bvar, ← Rew.emb_bShift_term,
Semiformula.codeIn'_ball, substs_ball]
apply ball_replace! T _ _ _ ⨀ (eq_symm! T _ _ ⨀ termEq_complete! T e t) ⨀ ?_
apply ball_intro!
intro x hx
suffices T ⊢! ⌜Rew.embₙ.hom p⌝^/[toNumVec (x :> e)] by
simpa [Language.TSemifromula.substs_substs]
have : Semiformula.Evalbm V (x :> e) p := by
simp at h; exact h x hx
exact boldSigma₁Complete hp this
| _, _, Hierarchy.bex (p := p) (t := t) pt hp, e, h => by
rcases Rew.positive_iff.mp pt with ⟨t, rfl⟩
simp only [Rew.bex, Rew.q_emb, Rew.hom_finitary2, Rew.emb_bvar, ← Rew.emb_bShift_term,
Semiformula.codeIn'_bex, substs_bex]
apply bex_replace! T _ _ _ ⨀ (eq_symm! T _ _ ⨀ termEq_complete! T e t) ⨀ ?_
have : ∃ x < t.valbm V e, Semiformula.Evalbm V (x :> e) p := by simpa using h
rcases this with ⟨x, hx, Hx⟩
apply bex_intro! T _ _ hx
simpa [Language.TSemifromula.substs_substs] using boldSigma₁Complete hp Hx
| _, _, Hierarchy.sigma (p := p) hp, e, h => by
have hp : Hierarchy 𝚺 1 p := hp.accum _
simp only [Rew.ex, Rew.q_emb, Semiformula.codeIn'_ex, Language.TSemiformula.substs_ex]
have : ∃ x, Semiformula.Evalbm V (x :> e) p := by simpa using h
rcases this with ⟨x, hx⟩
apply ex! x
simpa [Language.TSemifromula.substs_substs] using boldSigma₁Complete hp hx
| _, _, Hierarchy.ex (p := p) hp, e, h => by
simp only [Rew.ex, Rew.q_emb, Semiformula.codeIn'_ex, Language.TSemiformula.substs_ex]
have : ∃ x, Semiformula.Evalbm V (x :> e) p := by simpa using h
rcases this with ⟨x, hx⟩
apply ex! x
simpa [Language.TSemifromula.substs_substs] using boldSigma₁Complete hp hx

end TProof

Expand Down
3 changes: 3 additions & 0 deletions Arithmetization/ISigmaOne/Metamath/Formula/Typed.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,9 @@ scoped instance : LogicalConnective (L.TSemiformula n) where

def Language.TSemiformula.cast (p : L.TSemiformula n) (eq : n = n' := by simp) : L.TSemiformula n' := eq ▸ p

@[simp] lemma Language.TSemiformula.val_cast (p : L.TSemiformula n) (eq : n = n') :
(p.cast eq).val = p.val := by rcases eq; simp [Language.TSemiformula.cast]

def Language.TSemiformula.all (p : L.TSemiformula (n + 1)) : L.TSemiformula n := ⟨^∀[n] p.val, by simp⟩

def Language.TSemiformula.ex (p : L.TSemiformula (n + 1)) : L.TSemiformula n := ⟨^∃[n] p.val, by simp⟩
Expand Down
42 changes: 40 additions & 2 deletions Arithmetization/ISigmaOne/Metamath/Proof/R.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,24 +61,32 @@ def eqRefl (t : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t =' t := by
have : T ⊢ (#'0 =' #'0).all := byAxm EQTheory.refl
simpa [Language.TSemiformula.substs₁] using specialize this t

lemma eq_refl! (t : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t =' t := ⟨eqRefl T t⟩

def eqSymm (t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₁ := by
have : T ⊢ (#'1 =' #'0 ⟶ #'0 =' #'1).all.all := byAxm EQTheory.symm
have := by simpa using specialize this t₁
simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this t₂

lemma eq_symm! (t₁ t₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₁ := ⟨eqSymm T t₁ t₂⟩

def eqTrans (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := by
have : T ⊢ (#'2 =' #'1 ⟶ #'1 =' #'0 ⟶ #'2 =' #'0).all.all.all := byAxm EQTheory.trans
have := by simpa using specialize this t₁
have := by simpa using specialize this t₂
simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this t₃

lemma eq_trans! (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ t₂ =' t₃ ⟶ t₁ =' t₃ := ⟨eqTrans T t₁ t₂ t₃⟩

noncomputable def replace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) :
T ⊢ t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := by
have : T ⊢ (#'1 =' #'0 ⟶ p^/[(#'1).sing] ⟶ p^/[(#'0).sing]).all.all := byAxm <| EQTheory.replace p
have := by simpa using specialize this t
simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁,
Language.TSemifromula.substs_substs] using specialize this u

lemma replace! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t =' u ⟶ p^/[t.sing] ⟶ p^/[u.sing] := ⟨replace T p t u⟩

noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := by
apply deduct'
apply deduct
Expand All @@ -94,6 +102,8 @@ noncomputable def addExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t
simpa using this
exact of (Γ := Γ) this ⨀ bu ⨀ b

lemma add_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ + u₁) =' (t₂ + u₂) := ⟨addExt T t₁ t₂ u₁ u₂⟩

noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := by
apply deduct'
apply deduct
Expand All @@ -109,6 +119,8 @@ noncomputable def mulExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t
simpa using this
exact of (Γ := Γ) this ⨀ bu ⨀ b

lemma mul_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ (t₁ * u₁) =' (t₂ * u₂) := ⟨mulExt T t₁ t₂ u₁ u₂⟩

noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := by
apply deduct'
apply deduct
Expand All @@ -126,22 +138,36 @@ noncomputable def ltExt (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢ t
simpa using this
exact of (Γ := Γ) this ⨀ bu ⨀ b

lemma lt_ext! (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.TTerm) : T ⊢! t₁ =' t₂ ⟶ u₁ =' u₂ ⟶ t₁ <' u₁ ⟶ t₂ <' u₂ := ⟨ltExt T t₁ t₂ u₁ u₂⟩

noncomputable def ballReplace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) :
T ⊢ t =' u ⟶ p.ball t ⟶ p.ball u := by
simpa [Language.TSemifromula.substs_substs] using replace T ((p^/[(#'0).sing]).ball #'0) t u

lemma ball_replace! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) :
T ⊢! t =' u ⟶ p.ball t ⟶ p.ball u := ⟨ballReplace T p t u⟩

noncomputable def bexReplace (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) :
T ⊢ t =' u ⟶ p.bex t ⟶ p.bex u := by
simpa [Language.TSemifromula.substs_substs] using replace T ((p^/[(#'0).sing]).bex #'0) t u

lemma bex_replace! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.TTerm) :
T ⊢! t =' u ⟶ p.bex t ⟶ p.bex u := ⟨bexReplace T p t u⟩

variable [R₀Theory T]

def addComplete (n m : V) : T ⊢ (↑n + ↑m) =' ↑(n + m) := byAxm (R₀Theory.add n m)

lemma add_complete! (n m : V) : T ⊢! (↑n + ↑m) =' ↑(n + m) := ⟨addComplete T n m⟩

def mulComplete (n m : V) : T ⊢ (↑n * ↑m) =' ↑(n * m) := byAxm (R₀Theory.mul n m)

lemma mul_complete! (n m : V) : T ⊢! (↑n * ↑m) =' ↑(n * m) := ⟨mulComplete T n m⟩

def neComplete {n m : V} (h : n ≠ m) : T ⊢ ↑n ≠' ↑m := byAxm (R₀Theory.ne h)

lemma ne_complete! {n m : V} (h : n ≠ m) : T ⊢! ↑n ≠' ↑m := ⟨neComplete T h⟩

def ltNumeral (t : ⌜ℒₒᵣ⌝.TTerm) (n : V) : T ⊢ t <' ↑n ⟷ (tSubstItr t.sing (#'1 =' #'0) n).disj := by
have : T ⊢ (#'0 <' ↑n ⟷ (tSubstItr (#'0).sing (#'1 =' #'0) n).disj).all := byAxm (R₀Theory.ltNumeral n)
simpa [Language.TSemitermVec.q_of_pos, Language.TSemiformula.substs₁] using specialize this t
Expand All @@ -155,6 +181,8 @@ def ltComplete {n m : V} (h : n < m) : T ⊢ ↑n <' ↑m := by
apply disj (i := m - (n + 1)) _ (by simpa using sub_succ_lt_self (by simp [h]))
simpa [nth_tSubstItr', h] using eqRefl T ↑n

lemma lt_complete! {n m : V} (h : n < m) : T ⊢! ↑n <' ↑m := ⟨ltComplete T h⟩

noncomputable def nltComplete {n m : V} (h : m ≤ n) : T ⊢ ↑n ≮' ↑m := by
have : T ⊢ ↑n ≮' ↑m ⟷ (tSubstItr (↑n : ⌜ℒₒᵣ⌝.TTerm).sing (#'1 ≠' #'0) m).conj := by
simpa using negReplaceIff' <| ltNumeral T n m
Expand All @@ -165,6 +193,8 @@ noncomputable def nltComplete {n m : V} (h : m ≤ n) : T ⊢ ↑n ≮' ↑m :=
have : n ≠ i := Ne.symm <| ne_of_lt <| lt_of_lt_of_le hi h
simpa [nth_tSubstItr', hi] using neComplete T this

lemma nlt_complete {n m : V} (h : m ≤ n) : T ⊢! ↑n ≮' ↑m := ⟨nltComplete T h⟩

noncomputable def ballIntro (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V)
(bs : ∀ i < n, T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) :
T ⊢ p.ball ↑n := by
Expand All @@ -184,12 +214,20 @@ noncomputable def ballIntro (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V)
exact of (replace T p.shift ↑i &'0) ⨀ e ⨀ of this
exact orReplaceLeft' this (andRight (nltNumeral T (&'0) n))

lemma ball_intro! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V)
(bs : ∀ i < n, T ⊢! p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) :
T ⊢! p.ball ↑n := ⟨ballIntro T p n fun i hi ↦ (bs i hi).get⟩

noncomputable def bexIntro (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V) {i}
(hi : i < n) (bs : T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) :
(hi : i < n) (b : T ⊢ p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) :
T ⊢ p.bex ↑n := by
apply ex i
suffices T ⊢ i <' n ⋏ p^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing] by simpa
exact System.andIntro (ltComplete T hi) bs
exact System.andIntro (ltComplete T hi) b

lemma bex_intro! (p : ⌜ℒₒᵣ⌝.TSemiformula (0 + 1)) (n : V) {i}
(hi : i < n) (b : T ⊢! p ^/[(i : ⌜ℒₒᵣ⌝.TTerm).sing]) :
T ⊢! p.bex ↑n := ⟨bexIntro T p n hi b.get⟩

end TProof

Expand Down
19 changes: 17 additions & 2 deletions Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -339,10 +339,15 @@ instance : System.Classical T where

def exIntro (p : L.TSemiformula (0 + 1)) (t : L.TTerm) (b : T ⊢ p.substs₁ t) : T ⊢ p.ex := TDerivation.ex t b

lemma ex_intro! (p : L.TSemiformula (0 + 1)) (t : L.TTerm) (b : T ⊢! p.substs₁ t) : T ⊢! p.ex := ⟨exIntro _ t b.get⟩

def specialize {p : L.TSemiformula (0 + 1)} (b : T ⊢ p.all) (t : L.TTerm) : T ⊢ p.substs₁ t := TDerivation.specialize b t

def conj (ps : L.TSemiformulaVec 0) (ds : ∀ i, (hi : i < len ps.val) → T ⊢ ps.nth i hi) : T ⊢ ps.conj :=
TDerivation.conj ps ds
lemma specialize! {p : L.TSemiformula (0 + 1)} (b : T ⊢! p.all) (t : L.TTerm) : T ⊢! p.substs₁ t := ⟨TDerivation.specialize b.get t⟩

def conj (ps : L.TSemiformulaVec 0) (ds : ∀ i, (hi : i < len ps.val) → T ⊢ ps.nth i hi) : T ⊢ ps.conj := TDerivation.conj ps ds

lemma conj! (ps : L.TSemiformulaVec 0) (ds : ∀ i, (hi : i < len ps.val) → T ⊢! ps.nth i hi) : T ⊢! ps.conj := ⟨conj ps fun i hi ↦ (ds i hi).get⟩

def conj' (ps : L.TSemiformulaVec 0) (ds : ∀ i, (hi : i < len ps.val) → T ⊢ ps.nth (len ps.val - (i + 1)) (sub_succ_lt_self hi)) : T ⊢ ps.conj :=
TDerivation.conj ps <| fun i hi ↦ by
Expand All @@ -357,8 +362,12 @@ def disj (ps : L.TSemiformulaVec 0) {i} (hi : i < len ps.val) (d : T ⊢ ps.nth

def shift {p : L.TFormula} (d : T ⊢ p) : T ⊢ p.shift := by simpa using TDerivation.shift d

lemma shift! {p : L.TFormula} (d : T ⊢! p) : T ⊢! p.shift := ⟨by simpa using TDerivation.shift d.get⟩

def all {p : L.TSemiformula (0 + 1)} (dp : T ⊢ p.free) : T ⊢ p.all := TDerivation.all (by simpa using dp)

lemma all! {p : L.TSemiformula (0 + 1)} (dp : T ⊢! p.free) : T ⊢! p.all := ⟨all dp.get⟩

def generalizeAux {C : L.TFormula} {p : L.TSemiformula (0 + 1)} (dp : T ⊢ C.shift ⟶ p.free) : T ⊢ C ⟶ p.all := by
rw [TSemiformula.imp_def] at dp ⊢
apply TDerivation.or
Expand All @@ -378,6 +387,8 @@ def generalize {Γ} {p : L.TSemiformula (0 + 1)} (d : Γ.map .shift ⊢[T] p.fre
apply generalizeAux
simpa [conj_shift] using System.FiniteContext.toDef d

lemma generalize! {Γ} {p : L.TSemiformula (0 + 1)} (d : Γ.map .shift ⊢[T]! p.free) : Γ ⊢[T]! p.all := ⟨generalize d.get⟩

def specializeWithCtxAux {C : L.TFormula} {p : L.TSemiformula (0 + 1)} (d : T ⊢ C ⟶ p.all) (t : L.TTerm) : T ⊢ C ⟶ p.substs₁ t := by
rw [TSemiformula.imp_def] at d ⊢
apply TDerivation.or
Expand All @@ -387,8 +398,12 @@ def specializeWithCtxAux {C : L.TFormula} {p : L.TSemiformula (0 + 1)} (d : T

def specializeWithCtx {Γ} {p : L.TSemiformula (0 + 1)} (d : Γ ⊢[T] p.all) (t) : Γ ⊢[T] p.substs₁ t := specializeWithCtxAux d t

lemma specialize_with_ctx! {Γ} {p : L.TSemiformula (0 + 1)} (d : Γ ⊢[T]! p.all) (t) : Γ ⊢[T]! p.substs₁ t := ⟨specializeWithCtx d.get t⟩

def ex {p : L.TSemiformula (0 + 1)} (t) (dp : T ⊢ p.substs₁ t) : T ⊢ p.ex := TDerivation.ex t (by simpa using dp)

lemma ex! {p : L.TSemiformula (0 + 1)} (t) (dp : T ⊢! p.substs₁ t) : T ⊢! p.ex := ⟨ex t dp.get⟩

end Language.Theory.TProof

end typed_derivation

0 comments on commit 37ff63b

Please sign in to comment.