Skip to content

Commit bec4d81

Browse files
SnO2WMaNSnO2WMaN
committed
wip
1 parent a45ba64 commit bec4d81

4 files changed

Lines changed: 505 additions & 0 deletions

File tree

‎VeryWeakSubintuitionistic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,5 +12,6 @@ public import VeryWeakSubintuitionistic.Propositional.Kripke.Basic
1212
public import VeryWeakSubintuitionistic.Propositional.Proof.Basic
1313
public import VeryWeakSubintuitionistic.Propositional.Proof.Int
1414
public import VeryWeakSubintuitionistic.Propositional.Proof.VF
15+
public import VeryWeakSubintuitionistic.Propositional.Proof.VFR
1516
public import VeryWeakSubintuitionistic.Propositional.Slash
1617
public import VeryWeakSubintuitionistic.Propositional.Syntax

‎VeryWeakSubintuitionistic/Propositional/FMT/Ros.lean‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
module
2+
3+
public import VeryWeakSubintuitionistic.Propositional.FMT.Completeness
4+
5+
@[expose] public section
6+
7+
namespace FMTSemantics
8+
9+
variable {F : Frame κ α} {A B C : Formula α}
10+
11+
class Frame.Rosser (F : Frame κ α) : Prop where
12+
ros : ∀ x A B, ∃ z : F.World, x ≺[B 🡒 A] z
13+
14+
lemma frameValid_ros [F.Rosser] (hA : F ⊨ ∼A) (hB : F ⊨ B) : F ⊨ ∼(B 🡒 A) := by
15+
intro V x y Rxy hBA;
16+
obtain ⟨z, _⟩ := Frame.Rosser.ros y A B;
17+
apply hA V F.root z (by grind);
18+
apply hBA;
19+
. assumption;
20+
. apply hB;
21+
22+
open Classical
23+
open ProvableVF
24+
open SaturatedConsistentTableau
25+
26+
noncomputable def countermodelRos (Λ : Axioms α) (A) [Λ.ConsistentVF] [Λ.DisjunctiveVF] : Model (SaturatedConsistentTableau Λ A) α where
27+
Val a T := (ha : #a ∈ scope Λ A) → ⟨#a, ha⟩ ∈ T.ant
28+
Rel' B T₁ T₂ :=
29+
match B with
30+
| (C 🡒 D) => (h : C 🡒 D ∈ scope Λ A) → ⟨C 🡒 D, h⟩ ∈ T₁.con ∨ ⟨C, (by grind)⟩ ∈ T₂.con ∨ ⟨D, (by grind)⟩ ∈ T₂.ant
31+
| _ => True
32+
root' := SaturatedConsistentTableau.lindenbaum (countermodel.rootSeed Λ A) (countermodel.rootSeed_consistent)
33+
root_rooted' := by
34+
intro B T;
35+
split;
36+
. rename_i B C D;
37+
intro h;
38+
by_contra!;
39+
rcases this with ⟨hCD, hC, hD⟩;
40+
apply hCD;
41+
apply lindenbaum_subset_con;
42+
grind;
43+
. trivial;
44+
45+
variable {Λ : Axioms α} [Λ.ConsistentVF] [Λ.DisjunctiveVF]
46+
47+
lemma countermodelRos_Rosser : (countermodelRos Λ A).Rosser := by
48+
constructor;
49+
intro T B C;
50+
wlog _ : C 🡒 B ∈ scope Λ A;
51+
. use T;
52+
intro h;
53+
contradiction;
54+
sorry;
55+
56+
end FMTSemantics
57+
58+
end

‎VeryWeakSubintuitionistic/Propositional/Proof/VFR/Basic.lean‎

Lines changed: 273 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,273 @@
1+
module
2+
3+
public import VeryWeakSubintuitionistic.Propositional.Proof.Basic
4+
5+
@[expose] public section
6+
7+
variable {α : Type*}
8+
9+
inductive ProofVFR (Λ : Axioms α) : Formula α → Type _
10+
| axm {A} : A ∈ Λ → ProofVFR Λ A
11+
| andElimL {A B} : ProofVFR Λ $ (A ⋏ B) 🡒 A
12+
| andElimR {A B} : ProofVFR Λ $ (A ⋏ B) 🡒 B
13+
| orIntroL {A B} : ProofVFR Λ $ A 🡒 (A ⋎ B)
14+
| orIntroR {A B} : ProofVFR Λ $ B 🡒 (A ⋎ B)
15+
| distributeAndOr {A B C} : ProofVFR Λ $ (A ⋏ (B ⋎ C)) 🡒 ((A ⋏ B) ⋎ (A ⋏ C))
16+
| impId {A} : ProofVFR Λ $ A 🡒 A
17+
| efq {A} : ProofVFR Λ $ ⊥ 🡒 A
18+
| mdp {A B} : ProofVFR Λ (A 🡒 B) → ProofVFR Λ A → ProofVFR Λ B
19+
| af {A B} : ProofVFR Λ A → ProofVFR Λ (B 🡒 A)
20+
| ruleC {A B C} : ProofVFR Λ (A 🡒 B) → ProofVFR Λ (A 🡒 C) → ProofVFR Λ (A 🡒 (B ⋏ C))
21+
| ruleD {A B C} : ProofVFR Λ (A 🡒 C) → ProofVFR Λ (B 🡒 C) → ProofVFR Λ ((A ⋎ B) 🡒 C)
22+
| ruleI {A B C} : ProofVFR Λ (A 🡒 B) → ProofVFR Λ (B 🡒 C) → ProofVFR Λ (A 🡒 C)
23+
| ros {A B} : ProofVFR Λ (∼A) → ProofVFR Λ B → ProofVFR Λ (∼(B 🡒 A))
24+
25+
infix:25 " ⊢ᴿ! " => ProofVFR
26+
27+
namespace ProofVFR
28+
29+
variable {Λ Λ₁ Λ₂ : Axioms α} {A B C : Formula α}
30+
31+
def andComm : Λ ⊢ᴿ! (A ⋏ B) 🡒 (B ⋏ A) := ruleC andElimR andElimL
32+
def orComm : Λ ⊢ᴿ! (A ⋎ B) 🡒 (B ⋎ A) := ruleD orIntroR orIntroL
33+
34+
def distributeOrAnd : Λ ⊢ᴿ! ((A ⋎ B) ⋏ (A ⋎ C)) 🡒 (A ⋎ (B ⋏ C)) := by
35+
letI D := A ⋎ (B ⋏ C);
36+
haveI P₁ : Λ ⊢ᴿ! ((A ⋎ B) ⋏ A) 🡒 D := ruleI andElimR orIntroL
37+
haveI P₂ : Λ ⊢ᴿ! ((A ⋎ B) ⋏ C) 🡒 ((C ⋏ A) ⋎ (C ⋏ B)) := ruleI andComm distributeAndOr
38+
haveI P₃ : Λ ⊢ᴿ! (C ⋏ A) 🡒 D := ruleI andElimR orIntroL;
39+
haveI P₄ : Λ ⊢ᴿ! (C ⋏ B) 🡒 D := ruleI andComm orIntroR;
40+
haveI P₅ : Λ ⊢ᴿ! ((C ⋏ A) ⋎ (C ⋏ B)) 🡒 D := ruleD P₃ P₄;
41+
haveI P₆ : Λ ⊢ᴿ! ((A ⋎ B) ⋏ C) 🡒 D := ruleI P₂ P₅;
42+
haveI P₇ : Λ ⊢ᴿ! ((A ⋎ B) ⋏ A ⋎ (A ⋎ B) ⋏ C) 🡒 D := ruleD P₁ P₆;
43+
exact ruleI distributeAndOr P₇;
44+
45+
def verum : Λ ⊢ᴿ! ⊤ := impId
46+
47+
def orIntroRuleL : Λ ⊢ᴿ! A → Λ ⊢ᴿ! (A ⋎ B) := λ h => mdp orIntroL h
48+
def orIntroRuleR : Λ ⊢ᴿ! B → Λ ⊢ᴿ! (A ⋎ B) := λ h => mdp orIntroR h
49+
50+
def andIntro : Λ ⊢ᴿ! A → Λ ⊢ᴿ! B → Λ ⊢ᴿ! A ⋏ B := λ h₁ h₂ => mdp (ruleC (af h₁) (af h₂)) (verum)
51+
52+
noncomputable def ofSubsetAxm (hsub : Λ₁ ⊆ Λ₂) : Λ₁ ⊢ᴿ! A → Λ₂ ⊢ᴿ! A := λ h => by
53+
induction h with
54+
| axm h₁ => exact axm (hsub h₁)
55+
| andElimL => exact andElimL
56+
| andElimR => exact andElimR
57+
| orIntroL => exact orIntroL
58+
| orIntroR => exact orIntroR
59+
| distributeAndOr => exact distributeAndOr
60+
| impId => exact impId
61+
| efq => exact efq
62+
| mdp _ _ ihAB ihA => exact mdp ihAB ihA
63+
| af _ ihA => exact af ihA
64+
| ruleC _ _ ihAB ihAC => exact ruleC ihAB ihAC
65+
| ruleD _ _ ihAC ihBC => exact ruleD ihAC ihBC
66+
| ruleI _ _ ihAB ihBC => exact ruleI ihAB ihBC
67+
| ros _ _ ihA ihB => exact ros ihA ihB
68+
69+
end ProofVFR
70+
71+
72+
abbrev ProvableVFR (Λ : Axioms α) (A : Formula α) : Prop := Nonempty (Λ ⊢ᴿ! A)
73+
infix:25 " ⊢ᴿ " => ProvableVFR
74+
75+
abbrev UnprovableVFR (Λ : Axioms α) (A : Formula α) : Prop := ¬(Λ ⊢ᴿ A)
76+
infix:25 " ⊬ᴿ " => UnprovableVFR
77+
78+
namespace ProvableVFR
79+
80+
variable {Λ : Axioms α} {A B C : Formula α}
81+
82+
@[grind =>] lemma axm : A ∈ Λ → Λ ⊢ᴿ A := λ h => ⟨ProofVFR.axm h⟩
83+
@[simp, grind .] lemma andElimL : Λ ⊢ᴿ (A ⋏ B) 🡒 A := ⟨ProofVFR.andElimL⟩
84+
@[simp, grind .] lemma andElimR : Λ ⊢ᴿ (A ⋏ B) 🡒 B := ⟨ProofVFR.andElimR⟩
85+
@[simp, grind .] lemma orIntroL : Λ ⊢ᴿ A 🡒 (A ⋎ B) := ⟨ProofVFR.orIntroL⟩
86+
@[simp, grind .] lemma orIntroR : Λ ⊢ᴿ B 🡒 (A ⋎ B) := ⟨ProofVFR.orIntroR⟩
87+
@[simp, grind .] lemma distributeAndOr : Λ ⊢ᴿ (A ⋏ (B ⋎ C)) 🡒 ((A ⋏ B) ⋎ (A ⋏ C)) := ⟨ProofVFR.distributeAndOr⟩
88+
@[simp, grind .] lemma impId : Λ ⊢ᴿ A 🡒 A := ⟨ProofVFR.impId⟩
89+
@[simp, grind .] lemma efq : Λ ⊢ᴿ ⊥ 🡒 A := ⟨ProofVFR.efq⟩
90+
@[simp, grind .] lemma verum : Λ ⊢ᴿ ⊤ := ⟨ProofVFR.verum⟩
91+
@[grind =>] lemma mdp : Λ ⊢ᴿ A 🡒 B → Λ ⊢ᴿ A → Λ ⊢ᴿ B := λ ⟨h₁⟩ ⟨h₂⟩ => ⟨ProofVFR.mdp h₁ h₂⟩
92+
@[grind <=] lemma af : Λ ⊢ᴿ A → Λ ⊢ᴿ B 🡒 A := λ ⟨h⟩ => ⟨ProofVFR.af h⟩
93+
@[grind <=] lemma ruleC : Λ ⊢ᴿ A 🡒 B → Λ ⊢ᴿ A 🡒 C → Λ ⊢ᴿ A 🡒 (B ⋏ C) := λ ⟨h₁⟩ ⟨h₂⟩ => ⟨ProofVFR.ruleC h₁ h₂⟩
94+
@[grind <=] lemma ruleD : Λ ⊢ᴿ A 🡒 C → Λ ⊢ᴿ B 🡒 C → Λ ⊢ᴿ (A ⋎ B) 🡒 C := λ ⟨h₁⟩ ⟨h₂⟩ => ⟨ProofVFR.ruleD h₁ h₂⟩
95+
@[grind =>] lemma ruleI : Λ ⊢ᴿ A 🡒 B → Λ ⊢ᴿ B 🡒 C → Λ ⊢ᴿ A 🡒 C := λ ⟨h₁⟩ ⟨h₂⟩ => ⟨ProofVFR.ruleI h₁ h₂⟩
96+
@[grind <=] lemma ros : Λ ⊢ᴿ ∼A → Λ ⊢ᴿ B → Λ ⊢ᴿ ∼(B 🡒 A) := λ ⟨h₁⟩ ⟨h₂⟩ => ⟨ProofVFR.ros h₁ h₂⟩
97+
98+
@[grind <=] lemma orIntroRuleL : Λ ⊢ᴿ A → Λ ⊢ᴿ (A ⋎ B) := λ h => mdp orIntroL h
99+
@[grind <=] lemma orIntroRuleR : Λ ⊢ᴿ B → Λ ⊢ᴿ (A ⋎ B) := λ h => mdp orIntroR h
100+
@[grind <=] lemma andIntro : Λ ⊢ᴿ A → Λ ⊢ᴿ B → Λ ⊢ᴿ A ⋏ B := λ ⟨h₁⟩ ⟨h₂⟩ => ⟨ProofVFR.andIntro h₁ h₂⟩
101+
102+
lemma ofSubsetAxm (hsub : Λ₁ ⊆ Λ₂) : Λ₁ ⊢ᴿ A → Λ₂ ⊢ᴿ A := λ ⟨h⟩ => ⟨ProofVFR.ofSubsetAxm hsub h⟩
103+
lemma ofEmpty : ∅ ⊢ᴿ A → Λ ⊢ᴿ A := ofSubsetAxm (by grind)
104+
105+
lemma ruleI₃ : Λ ⊢ᴿ A 🡒 B → Λ ⊢ᴿ B 🡒 C → Λ ⊢ᴿ C 🡒 D → Λ ⊢ᴿ A 🡒 D := by
106+
intro hAB hBC hCD;
107+
exact ruleI (ruleI hAB hBC) hCD;
108+
109+
lemma distributeOrAnd : Λ ⊢ᴿ ((A ⋎ B) ⋏ (A ⋎ C)) 🡒 (A ⋎ (B ⋏ C)) := ⟨ProofVFR.distributeOrAnd⟩
110+
111+
lemma replaceAnd₂ (h : Λ ⊢ᴿ B 🡒 C) : Λ ⊢ᴿ (A ⋏ B) 🡒 (A ⋏ C) := by
112+
apply ruleC;
113+
. exact andElimL;
114+
. exact ruleI andElimR h;
115+
116+
lemma replaceOr₂ (h : Λ ⊢ᴿ B 🡒 C) : Λ ⊢ᴿ (A ⋎ B) 🡒 (A ⋎ C) := by
117+
apply ruleD;
118+
. exact orIntroL;
119+
. exact ruleI h orIntroR;
120+
121+
122+
@[grind <=]
123+
lemma lconj_of_mem {X : List (Formula α)} (h : A ∈ X) : Λ ⊢ᴿ ⋀X 🡒 A := by
124+
match X with
125+
| [] => grind;
126+
| [B] => grind;
127+
| B :: C :: X =>
128+
simp_all only [List.mem_cons, Formula.lconj];
129+
rcases h with (rfl | rfl | h);
130+
. exact andElimL;
131+
. exact ruleI andElimR (lconj_of_mem (by grind));
132+
. exact ruleI andElimR (lconj_of_mem (by grind));
133+
134+
@[grind <=]
135+
lemma sconj_of_mem {X : Finset (Formula α)} (h : A ∈ X) : Λ ⊢ᴿ ⋀X 🡒 A := lconj_of_mem (by simpa)
136+
137+
138+
@[grind <=]
139+
lemma ldisj_of_mem {X : List (Formula α)} (h : A ∈ X) : Λ ⊢ᴿ A 🡒 ⋁X := by
140+
match X with
141+
| [] => grind;
142+
| [B] => grind;
143+
| B :: C :: X =>
144+
simp_all only [List.mem_cons, Formula.ldisj];
145+
rcases h with (rfl | rfl | h);
146+
. exact orIntroL;
147+
. exact ruleI (ldisj_of_mem (by grind)) orIntroR;
148+
. exact ruleI (ldisj_of_mem (by grind)) orIntroR;
149+
150+
@[grind <=]
151+
lemma sdisj_of_mem {X : Finset (Formula α)} (h : A ∈ X) : Λ ⊢ᴿ A 🡒 ⋁X := ldisj_of_mem (by simpa)
152+
153+
154+
lemma ldisj_insert {X : List (Formula α)} {A} : Λ ⊢ᴿ ⋁(A :: X) 🡒 (⋁X ⋎ A) := by
155+
match X with
156+
| [] | [B] => grind;
157+
| B :: X => apply ruleD <;> simp;
158+
159+
lemma ldisj_of_subset {X Y : List (Formula α)} (h : X ⊆ Y) : Λ ⊢ᴿ ⋁X 🡒 ⋁Y := by
160+
match X with
161+
| [] => grind;
162+
| [B] => grind;
163+
| B :: X =>
164+
simp_all only [List.cons_subset];
165+
rcases h with ⟨hB, hXY⟩;
166+
apply ruleI;
167+
. exact ldisj_insert;
168+
. apply ruleD;
169+
. exact ldisj_of_subset hXY;
170+
. exact ldisj_of_mem hB;
171+
172+
lemma sdisj_of_subset {X Y : Finset (Formula α)} (h : X ⊆ Y) : Λ ⊢ᴿ ⋁X 🡒 ⋁Y := ldisj_of_subset $ by intro A; simpa using @h A;
173+
174+
lemma sdisj_insert [DecidableEq α] {X : Finset (Formula α)} : Λ ⊢ᴿ ⋁(insert A X) 🡒 (⋁X ⋎ A) := by
175+
apply ruleI ?_ ldisj_insert;
176+
apply ldisj_of_subset;
177+
intro B;
178+
simp;
179+
180+
181+
lemma lconj_insert {X : List (Formula α)} {A} : Λ ⊢ᴿ (⋀X ⋏ A) 🡒 ⋀(A :: X) := by
182+
match X with
183+
| [] | [B] => grind;
184+
| B :: X => apply ruleC <;> simp;
185+
186+
lemma lconj_of_subset {X Y : List (Formula α)} (h : X ⊆ Y) : Λ ⊢ᴿ ⋀Y 🡒 ⋀X := by
187+
match X with
188+
| [] => grind;
189+
| [B] => grind;
190+
| B :: X =>
191+
simp_all only [List.cons_subset];
192+
rcases h with ⟨hB, hXY⟩;
193+
apply ruleI;
194+
. apply ruleC;
195+
. exact lconj_of_subset hXY;
196+
. exact lconj_of_mem hB;
197+
. apply lconj_insert;
198+
199+
lemma sconj_of_subset {X Y : Finset (Formula α)} (h : X ⊆ Y) : Λ ⊢ᴿ ⋀Y 🡒 ⋀X := lconj_of_subset $ by intro A; simpa using @h A;
200+
201+
lemma sconj_insert [DecidableEq α] {X : Finset (Formula α)} : Λ ⊢ᴿ (⋀X ⋏ A) 🡒 ⋀(insert A X) := by
202+
apply ruleI lconj_insert;
203+
apply lconj_of_subset;
204+
intro B;
205+
simp;
206+
207+
208+
@[induction_eliminator]
209+
protected lemma rec_provable
210+
{motive : (A : Formula α) → (Λ ⊢ᴿ A) → Prop}
211+
(axm : ∀ {A}, (h : A ∈ Λ) → motive A (axm h))
212+
(mdp : ∀ {A B}, {hAB : Λ ⊢ᴿ A 🡒 B} → {hA : Λ ⊢ᴿ A} → (motive (A 🡒 B) hAB) → (motive A hA) → (motive B (mdp hAB hA)))
213+
(af : ∀ {A B}, {hA : Λ ⊢ᴿ A} → (motive A hA) → (motive (B 🡒 A) (af hA)))
214+
(ruleC : ∀ {A B C}, {hAB : Λ ⊢ᴿ A 🡒 B} → {hAC : Λ ⊢ᴿ A 🡒 C} → (motive (A 🡒 B) hAB) → (motive (A 🡒 C) hAC) → (motive (A 🡒 (B ⋏ C)) (ruleC hAB hAC)))
215+
(ruleD : ∀ {A B C}, {hAC : Λ ⊢ᴿ A 🡒 C} → {hBC : Λ ⊢ᴿ B 🡒 C} → (motive (A 🡒 C) hAC) → (motive (B 🡒 C) hBC) → (motive ((A ⋎ B) 🡒 C) (ruleD hAC hBC)))
216+
(ruleI : ∀ {A B C}, {hAB : Λ ⊢ᴿ A 🡒 B} → {hBC : Λ ⊢ᴿ B 🡒 C} → (motive (A 🡒 B) hAB) → (motive (B 🡒 C) hBC) → (motive (A 🡒 C) (ruleI hAB hBC)))
217+
(ros : ∀ {A B}, {hA : Λ ⊢ᴿ ∼A} → {hB : Λ ⊢ᴿ B} → (motive (∼A) hA) → (motive B hB) → (motive (∼(B 🡒 A)) (ros hA hB)))
218+
(distributeAndOr : ∀ {A B C : Formula α}, (motive ((A ⋏ (B ⋎ C)) 🡒 ((A ⋏ B) ⋎ (A ⋏ C))) distributeAndOr))
219+
(impId : ∀ {A}, (motive (A 🡒 A) impId))
220+
(andElimL : ∀ {A B}, (motive ((A ⋏ B) 🡒 A) andElimL))
221+
(andElimR : ∀ {A B}, (motive ((A ⋏ B) 🡒 B) andElimR))
222+
(orIntroL : ∀ {A B}, (motive (A 🡒 (A ⋎ B)) orIntroL))
223+
(orIntroR : ∀ {A B}, (motive (B 🡒 (A ⋎ B)) orIntroR))
224+
(efq : ∀ {A}, (motive (⊥ 🡒 A) efq))
225+
: ∀ {A}, (d : Λ ⊢ᴿ A) → motive A d := by rintro A ⟨d⟩; induction d <;> grind;
226+
227+
end ProvableVFR
228+
229+
230+
231+
class Axioms.ConsistentVFR (Λ : Axioms α) : Prop where
232+
unprovable_bot : Λ ⊬ᴿ ⊥
233+
234+
namespace ProvableVFR
235+
236+
export Axioms.ConsistentVFR (unprovable_bot)
237+
attribute [simp, grind .] unprovable_bot
238+
239+
end ProvableVFR
240+
241+
242+
243+
section Disjunctive
244+
245+
class Axioms.DisjunctiveVFR (Λ : Axioms α) : Prop where
246+
disjunctive : ∀ {A B}, (Λ ⊢ᴿ (A ⋎ B)) → (Λ ⊢ᴿ A) ∨ (Λ ⊢ᴿ B)
247+
248+
namespace ProvableVFR
249+
250+
export Axioms.DisjunctiveVFR (disjunctive)
251+
252+
variable {Λ : Axioms α} [Axioms.DisjunctiveVFR Λ] {A B C : Formula α}
253+
254+
lemma ldisj_disjunctive {l : List _} (hl : l ≠ []) : Λ ⊢ᴿ ⋁l → ∃ B ∈ l, Λ ⊢ᴿ B := by
255+
match l with
256+
| [] => contradiction
257+
| [A] => intro _; use A; simpa;
258+
| A :: B :: l =>
259+
intro hAB;
260+
rcases disjunctive hAB with hA | hB;
261+
. use A;
262+
grind;
263+
. obtain ⟨C, hC⟩ := ldisj_disjunctive (by grind) hB;
264+
use C;
265+
grind;
266+
267+
lemma sdisj_disjunctive {s : Finset _} (hs : s ≠ ∅) : Λ ⊢ᴿ ⋁s → ∃ B ∈ s, Λ ⊢ᴿ B := by
268+
intro h;
269+
simpa using ldisj_disjunctive (by simpa) h;
270+
271+
end ProvableVFR
272+
273+
end Disjunctive

0 commit comments

Comments
 (0)