Skip to content

Commit 51eba23

Browse files
SnO2WMaNSnO2WMaN
authored
refactor(Propositional): Redesign Hilbert Systems (#812)
1 parent fd11f33 commit 51eba23

94 files changed

Lines changed: 2533 additions & 3953 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Foundation.lean‎

Lines changed: 38 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -358,10 +358,8 @@ public import Foundation.Modal.Maximal.Basic
358358
public import Foundation.Modal.Maximal.Makinson
359359
public import Foundation.Modal.Maximal.Unprovability
360360
public import Foundation.Modal.MaximalConsistentSet
361-
public import Foundation.Modal.ModalCompanion
362361
public import Foundation.Modal.ModalCompanion.Corsi
363362
public import Foundation.Modal.ModalCompanion.Corsi.VF
364-
public import Foundation.Modal.ModalCompanion.Standard
365363
public import Foundation.Modal.ModalCompanion.Standard.Basic
366364
public import Foundation.Modal.ModalCompanion.Standard.Cl
367365
public import Foundation.Modal.ModalCompanion.Standard.Int
@@ -417,11 +415,11 @@ public import Foundation.Modal.PLoN.Logic
417415
public import Foundation.Modal.PLoN.Logic.N
418416
public import Foundation.Modal.Tableau
419417
public import Foundation.Modal.VanBentham.StandardTranslation
420-
public import Foundation.Propositional.ClassicalSemantics.Basic
421-
public import Foundation.Propositional.ClassicalSemantics.Hilbert
422-
public import Foundation.Propositional.ClassicalSemantics.NNFormula
423-
public import Foundation.Propositional.ClassicalSemantics.Tait
424-
public import Foundation.Propositional.ClassicalSemantics.ZeroSubst
418+
public import Foundation.Propositional.Boolean.Basic
419+
public import Foundation.Propositional.Boolean.Hilbert
420+
public import Foundation.Propositional.Boolean.NNFormula
421+
public import Foundation.Propositional.Boolean.Tait
422+
public import Foundation.Propositional.Boolean.ZeroSubst
425423
public import Foundation.Propositional.ConsistentTableau
426424
public import Foundation.Propositional.Decidable
427425
public import Foundation.Propositional.Dialectica.Basic
@@ -444,29 +442,23 @@ public import Foundation.Propositional.Entailment.KreiselPutnam
444442
public import Foundation.Propositional.Entailment.LC
445443
public import Foundation.Propositional.Entailment.Minimal.Basic
446444
public import Foundation.Propositional.Entailment.Scott
447-
public import Foundation.Propositional.FMT.AxiomSer
445+
public import Foundation.Propositional.FMT.Axiom.Ser
448446
public import Foundation.Propositional.FMT.Basic
449447
public import Foundation.Propositional.FMT.Completeness
450-
public import Foundation.Propositional.FMT.Hilbert
451-
public import Foundation.Propositional.FMT.Logic
452-
public import Foundation.Propositional.FMT.Logic.VF
453-
public import Foundation.Propositional.FMT.Logic.VF_Ser
448+
public import Foundation.Propositional.FMT.Hilbert.Basic
449+
public import Foundation.Propositional.FMT.Hilbert.VF
450+
public import Foundation.Propositional.FMT.Hilbert.VF_Ser
454451
public import Foundation.Propositional.Formula.Basic
455452
public import Foundation.Propositional.Formula.NNFormula
456453
public import Foundation.Propositional.Heyting.Semantics
457-
public import Foundation.Propositional.Hilbert.Axiom
458-
public import Foundation.Propositional.Hilbert.F
459454
public import Foundation.Propositional.Hilbert.F.Basic
460455
public import Foundation.Propositional.Hilbert.F.Deduction
461456
public import Foundation.Propositional.Hilbert.F.Disjunctive
462457
public import Foundation.Propositional.Hilbert.F_WF
463-
public import Foundation.Propositional.Hilbert.Standard
464-
public import Foundation.Propositional.Hilbert.Standard.Basic
465-
public import Foundation.Propositional.Hilbert.Standard.Glivenko
466-
public import Foundation.Propositional.Hilbert.VF
458+
public import Foundation.Propositional.Hilbert.Minimal.Basic
459+
public import Foundation.Propositional.Hilbert.Minimal.Glivenko
467460
public import Foundation.Propositional.Hilbert.VF.Basic
468461
public import Foundation.Propositional.Hilbert.VF.Disjunctive
469-
public import Foundation.Propositional.Hilbert.WF
470462
public import Foundation.Propositional.Hilbert.WF.Basic
471463
public import Foundation.Propositional.Hilbert.WF_VF
472464
public import Foundation.Propositional.Kripke.AxiomDummett
@@ -476,43 +468,40 @@ public import Foundation.Propositional.Kripke.AxiomWLEM
476468
public import Foundation.Propositional.Kripke.Basic
477469
public import Foundation.Propositional.Kripke.Completeness
478470
public import Foundation.Propositional.Kripke.Filtration
479-
public import Foundation.Propositional.Kripke.Hilbert
480-
public import Foundation.Propositional.Kripke.Logic.Cl
481-
public import Foundation.Propositional.Kripke.Logic.Int
482-
public import Foundation.Propositional.Kripke.Logic.KC
483-
public import Foundation.Propositional.Kripke.Logic.KreiselPutnam
484-
public import Foundation.Propositional.Kripke.Logic.LC
471+
public import Foundation.Propositional.Kripke.Hilbert.Basic
472+
public import Foundation.Propositional.Kripke.Hilbert.Cl
473+
public import Foundation.Propositional.Kripke.Hilbert.Int.Basic
474+
public import Foundation.Propositional.Kripke.Hilbert.Int.DP
475+
public import Foundation.Propositional.Kripke.Hilbert.KC
476+
public import Foundation.Propositional.Kripke.Hilbert.KreiselPutnam
477+
public import Foundation.Propositional.Kripke.Hilbert.LC
485478
public import Foundation.Propositional.Kripke.Preservation
486479
public import Foundation.Propositional.Kripke.Rooted
487-
public import Foundation.Propositional.Kripke2.AxiomCorfl
488-
public import Foundation.Propositional.Kripke2.AxiomHrd
489-
public import Foundation.Propositional.Kripke2.AxiomPCon
490-
public import Foundation.Propositional.Kripke2.AxiomPSCon
491-
public import Foundation.Propositional.Kripke2.AxiomRfl
492-
public import Foundation.Propositional.Kripke2.AxiomSer
493-
public import Foundation.Propositional.Kripke2.AxiomSym
494-
public import Foundation.Propositional.Kripke2.AxiomTra
480+
public import Foundation.Propositional.Kripke2.Axiom.Corfl
481+
public import Foundation.Propositional.Kripke2.Axiom.Hrd
482+
public import Foundation.Propositional.Kripke2.Axiom.PCon
483+
public import Foundation.Propositional.Kripke2.Axiom.PSCon
484+
public import Foundation.Propositional.Kripke2.Axiom.Rfl
485+
public import Foundation.Propositional.Kripke2.Axiom.Ser
486+
public import Foundation.Propositional.Kripke2.Axiom.Sym
487+
public import Foundation.Propositional.Kripke2.Axiom.Tra
495488
public import Foundation.Propositional.Kripke2.Basic
496-
public import Foundation.Propositional.Kripke2.FTheory
497-
public import Foundation.Propositional.Kripke2.Hilbert
498-
public import Foundation.Propositional.Kripke2.Logic
499-
public import Foundation.Propositional.Kripke2.Logic.F
500-
public import Foundation.Propositional.Kripke2.Logic.F_Rfl
501-
public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Sym
502-
public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1
503-
public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1_Hrd
504-
public import Foundation.Propositional.Kripke2.Logic.F_Ser
505-
public import Foundation.Propositional.Kripke2.Logic.F_Sym
506-
public import Foundation.Propositional.Kripke2.Logic.F_Tra1
507-
public import Foundation.Propositional.Kripke2.Logic.F_Tra1_Hrd
489+
public import Foundation.Propositional.Kripke2.Hilbert.Basic
490+
public import Foundation.Propositional.Kripke2.Hilbert.F
491+
public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl
492+
public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Sym
493+
public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Tra1
494+
public import Foundation.Propositional.Kripke2.Hilbert.F_Ser
495+
public import Foundation.Propositional.Kripke2.Hilbert.F_Sym
496+
public import Foundation.Propositional.Kripke2.Hilbert.F_Tra1
508497
public import Foundation.Propositional.Logic.Basic
509498
public import Foundation.Propositional.Logic.Letterless_Int_Cl
510499
public import Foundation.Propositional.Logic.PostComplete
511-
public import Foundation.Propositional.Logic.Slash
500+
public import Foundation.Propositional.Logic.Superintuitionistic
512501
public import Foundation.Propositional.Neighborhood.NB.Basic
513-
public import Foundation.Propositional.Neighborhood.NB.Hilbert
514-
public import Foundation.Propositional.Neighborhood.NB.Logic
515-
public import Foundation.Propositional.Neighborhood.NB.Logic.WF
502+
public import Foundation.Propositional.Neighborhood.NB.Hilbert.Basic
503+
public import Foundation.Propositional.Neighborhood.NB.Hilbert.WF
504+
public import Foundation.Propositional.Slash
516505
public import Foundation.Propositional.Tait.Calculus
517506
public import Foundation.Propositional.Translation
518507
public import Foundation.ProvabilityLogic.Arithmetic

‎Foundation/Modal/Logic/GL/Independency.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,8 @@ lemma unprovable_notbox : Modal.GL ⊬ ∼□φ := by
2929
by_contra hC;
3030
have : Modal.GL ⊢ ∼□φ 🡒 ∼□⊥ := contra! (imply_box_distribute'! efq!)
3131
have : Modal.GL ⊢ ∼□⊥ := this ⨀ hC;
32-
have : Propositional.Cl ⊢ (⊥ 🡒 ⊥) 🡒 ⊥ := GL.provable_verTranslated_Cl this;
33-
have := Propositional.Cl.soundness this (λ _ => False);
32+
have : ∼∼⊥ ∈ Propositional.Cl := GL.provable_verTranslated_Cl this;
33+
have := Hilbert.Cl.soundness this (λ _ => False);
3434
tauto;
3535

3636
lemma unprovable_independency : Modal.GL ⊬ independency φ := by

‎Foundation/Modal/Maximal/Basic.lean‎

Lines changed: 18 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module
22

3-
public import Foundation.Propositional.ClassicalSemantics.Hilbert
3+
public import Foundation.Propositional.Boolean.Hilbert
44
public import Foundation.Modal.Hilbert.Normal.Basic
55

66
@[expose] public section
@@ -34,6 +34,7 @@ lemma toIP : φᵀ.toPropFormula = φᵀ := by
3434

3535
end trivTranslate
3636

37+
3738
@[grind]
3839
def verTranslate : Formula α → Formula α
3940
| atom a => atom a
@@ -66,11 +67,11 @@ open Formula (trivTranslate verTranslate)
6667

6768
variable {φ : Modal.Formula ℕ}
6869

69-
lemma Hilbert.Normal.provable_of_classical_provable {Ax : Axiom ℕ} {φ : Propositional.Formula ℕ} : Propositional.Cl ⊢ φ → (Hilbert.Normal Ax ⊢ φ.toModalFormula) := by
70-
intro h;
71-
induction h using Propositional.Hilbert.Standard.rec! with
72-
| axm _ h => rcases h with (rfl | rfl) <;> simp;
73-
| mdp ihφψ ihφ => exact ihφψ ⨀ ihφ;
70+
lemma Hilbert.Normal.provable_of_classical_provable {Ax : Axiom ℕ} {φ : Propositional.Formula ℕ} : φ ∈ Propositional.Cl → (Hilbert.Normal Ax ⊢ φ.toModalFormula) := by
71+
rintro ⟨h⟩;
72+
induction h with
73+
| axm h => rcases h with (⟨_, rfl⟩ | ⟨_, rfl⟩) <;> simp;
74+
| mdp _ _ ihφψ ihφ => exact ihφψ ⨀ ihφ;
7475
| _ => dsimp [Propositional.Formula.toModalFormula]; simp;
7576

7677

@@ -86,26 +87,23 @@ lemma iff_trivTranslated : Modal.Triv ⊢ φ 🡘 φᵀ := by
8687
| _ => apply E!_id
8788

8889
@[grind =]
89-
lemma iff_provable_Cl : Modal.Triv ⊢ φ ↔ Propositional.Cl ⊢ φᵀ.toPropFormula := by
90+
lemma iff_provable_Cl : Modal.Triv ⊢ φ ↔ φᵀ.toPropFormula ∈ Propositional.Cl := by
91+
rw [←Propositional.Hilbert.iff_mem_logic_provable];
9092
constructor;
9193
. intro h;
9294
induction h using Hilbert.Normal.rec! with
9395
| axm s a =>
9496
rcases a with (rfl | rfl | rfl) <;> simp [trivTranslate, Formula.toPropFormula];
95-
| mdp ih₁ ih₂ =>
96-
dsimp [trivTranslate] at ih₁ ih₂;
97-
exact ih₁ ⨀ ih₂;
97+
| mdp ih₁ ih₂ => exact ih₁ ⨀ ih₂;
9898
| nec ih => exact ih;
99-
| _ =>
100-
dsimp [trivTranslate, Formula.toPropFormula];
101-
cl_prover;
99+
| _ => dsimp [trivTranslate, Formula.toPropFormula]; cl_prover;
102100
. intro h;
103101
have d₁ : Modal.Triv ⊢ φᵀ 🡒 φ := K!_right iff_trivTranslated;
104-
have d₂ : Modal.Triv ⊢ φᵀ := by simpa only [trivTranslate.toIP] using Hilbert.Normal.provable_of_classical_provable h;
102+
have d₂ : Modal.Triv ⊢ φᵀ := by simpa using Hilbert.Normal.provable_of_classical_provable h;
105103
exact d₁ ⨀ d₂;
106104

107105
@[grind =]
108-
lemma iff_tautology : Modal.Triv ⊢ φ ↔ φᵀ.toPropFormula.Tautology := by grind;
106+
lemma iff_tautology : Modal.Triv ⊢ φ ↔ φᵀ.toPropFormula.IsTautology := by grind;
109107

110108
end Triv
111109

@@ -122,25 +120,22 @@ lemma iff_verTranslated : Modal.Ver ⊢ φ 🡘 φⱽ := by
122120
| _ => apply E!_id
123121

124122
@[grind =]
125-
lemma iff_provable_Cl : Modal.Ver ⊢ φ ↔ Propositional.Cl ⊢ φⱽ.toPropFormula := by
123+
lemma iff_provable_Cl : Modal.Ver ⊢ φ ↔ φⱽ.toPropFormula ∈ Propositional.Cl := by
124+
rw [←Propositional.Hilbert.iff_mem_logic_provable];
126125
constructor;
127126
. intro h;
128127
induction h using Hilbert.Normal.rec! with
129128
| axm s a =>
130129
rcases a with (rfl | rfl | rfl) <;> simp [verTranslate, Formula.toPropFormula];
131-
| mdp ih₁ ih₂ =>
132-
dsimp [verTranslate] at ih₁ ih₂;
133-
exact ih₁ ⨀ ih₂;
134-
| _ =>
135-
dsimp [verTranslate, Formula.toPropFormula];
136-
cl_prover;
130+
| mdp ih₁ ih₂ => exact ih₁ ⨀ ih₂;
131+
| _ => dsimp [verTranslate, Formula.toPropFormula]; cl_prover;
137132
. intro h;
138133
have d₁ : Modal.Ver ⊢ φⱽ 🡒 φ := K!_right iff_verTranslated;
139134
have d₂ : Modal.Ver ⊢ φⱽ := by simpa using Hilbert.Normal.provable_of_classical_provable h;
140135
exact d₁ ⨀ d₂;
141136

142137
@[grind =]
143-
lemma iff_tautology : Modal.Ver ⊢ φ ↔ φⱽ.toPropFormula.Tautology := by grind;
138+
lemma iff_tautology : Modal.Ver ⊢ φ ↔ φⱽ.toPropFormula.IsTautology := by grind;
144139

145140
end Ver
146141

‎Foundation/Modal/Maximal/Makinson.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ public import Foundation.Modal.Hilbert.NNFormula
44
public import Foundation.Modal.Maximal.Basic
55
public import Foundation.Modal.Logic.SumNormal
66
public import Foundation.Modal.Kripke.Logic.Ver
7-
public import Foundation.Propositional.ClassicalSemantics.ZeroSubst
7+
public import Foundation.Propositional.Boolean.ZeroSubst
88

99
@[expose] public section
1010

@@ -75,7 +75,7 @@ open LO.Entailment LO.Entailment.FiniteContext LO.Modal.Entailment
7575
open Formula
7676
open Propositional
7777

78-
variable {v : ClassicalSemantics.Valuation ℕ}
78+
variable {v : Boolean.Valuation ℕ}
7979

8080
lemma KD_provability_of_classical_satisfiability (hl : φ.Letterless) :
8181
(v ⊧ (φᵀ.toPropFormula) → Modal.KD ⊢ φ) ∧
@@ -92,7 +92,7 @@ lemma KD_provability_of_classical_satisfiability (hl : φ.Letterless) :
9292
. exact C_of_N $ ihφ (by grind) |>.2 hφ;
9393
. exact C!_of_conseq! $ ihψ (by grind) |>.1 hψ;
9494
. intro h;
95-
simp only [trivTranslate, toPropFormula, Semantics.Models, Formula.ClassicalSemantics.val] at h;
95+
simp only [trivTranslate, toPropFormula, Semantics.Models, Formula.Boolean.val] at h;
9696
push_neg at h;
9797
rcases h with ⟨hφ, hψ⟩;
9898
replace hφ := ihφ (by grind) |>.1 hφ;
@@ -115,14 +115,14 @@ lemma KD_provability_of_classical_satisfiability (hl : φ.Letterless) :
115115
lemma provable_KD_of_classical_satisfiability (hl : φ.Letterless) : (v ⊧ φᵀ.toPropFormula) → Modal.KD ⊢ φ :=
116116
KD_provability_of_classical_satisfiability hl |>.1
117117

118-
lemma provable_KD_of_classical_tautology (hl : φ.Letterless) (h : (Semantics.Valid (ClassicalSemantics.Valuation ℕ) (φᵀ.toPropFormula)))
118+
lemma provable_KD_of_classical_tautology (hl : φ.Letterless) (h : (Semantics.Valid (Boolean.Valuation ℕ) (φᵀ.toPropFormula)))
119119
: Modal.KD ⊢ φ := provable_KD_of_classical_satisfiability hl (h (λ _ => True))
120120

121121
lemma provable_not_KD_of_classical_unsatisfiable (hl : φ.Letterless) : (¬(v ⊧ φᵀ.toPropFormula)) → Modal.KD ⊢ ∼φ :=
122122
KD_provability_of_classical_satisfiability hl |>.2
123123

124124
private lemma subset_Triv_of_KD_subset.lemma₁
125-
{φ : Modal.Formula α} {s : Propositional.ZeroSubstitution _} {v : ClassicalSemantics.Valuation α} :
125+
{φ : Modal.Formula α} {s : Propositional.ZeroSubstitution _} {v : Boolean.Valuation α} :
126126
v ⊧ (((φᵀ.toPropFormula)⟦s.1⟧)) ↔
127127
v ⊧ ((φ⟦(s : Modal.ZeroSubstitution _).1⟧)ᵀ.toPropFormula)
128128
:= by
@@ -136,8 +136,8 @@ private lemma subset_Triv_of_KD_subset.lemma₁
136136
| _ => simp_all [trivTranslate, toPropFormula];
137137

138138
lemma subset_Triv_of_KD_subset.lemma₂ {φ : Modal.Formula α} {s : Propositional.ZeroSubstitution _} :
139-
(∼((φᵀ.toPropFormula)⟦s.1⟧)).Tautology ↔
140-
((∼φ⟦(s : Modal.ZeroSubstitution _).1⟧)ᵀ.toPropFormula).Tautology
139+
(∼((φᵀ.toPropFormula)⟦s.1⟧)).IsTautology ↔
140+
((∼φ⟦(s : Modal.ZeroSubstitution _).1⟧)ᵀ.toPropFormula).IsTautology
141141
:= by
142142
constructor;
143143
. intro h v hφ;
@@ -149,10 +149,10 @@ lemma subset_Triv_of_KD_subset.lemma₂ {φ : Modal.Formula α} {s : Proposition
149149
theorem subset_Triv_of_KD_subset [Modal.KD ⪯ L] : L ⪯ Modal.Triv := by
150150
by_contra! hC;
151151
obtain ⟨φ, hφ₁, hφ₂⟩ := not_weakerThan_iff.mp hC;
152-
replace hφ₂ := (not_imp_not.mpr Propositional.Cl.completeness) $ Modal.Triv.iff_provable_Cl.not.mp $ hφ₂;
153-
obtain ⟨s, h⟩ := ClassicalSemantics.exists_neg_zeroSubst_of_not_tautology hφ₂;
152+
replace hφ₂ := (not_imp_not.mpr Hilbert.Cl.completeness) $ Modal.Triv.iff_provable_Cl.not.mp $ hφ₂;
153+
obtain ⟨s, h⟩ := Boolean.exists_neg_zeroSubst_of_not_tautology hφ₂;
154154
let ψ := φ⟦(s : Modal.ZeroSubstitution _).1⟧;
155-
have : Semantics.Valid (ClassicalSemantics.Valuation ℕ) (∼(ψᵀ.toPropFormula)) := subset_Triv_of_KD_subset.lemma₂.mp h;
155+
have : Semantics.Valid (Boolean.Valuation ℕ) (∼(ψᵀ.toPropFormula)) := subset_Triv_of_KD_subset.lemma₂.mp h;
156156
have : Modal.KD ⊢ ∼ψ := provable_not_KD_of_classical_unsatisfiable Formula.letterless_zeroSubst
157157
$ Semantics.Not.models_not.mp
158158
$ this (λ _ => True);

‎Foundation/Modal/Maximal/Unprovability.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ end Ver
3838

3939
namespace K4
4040

41-
lemma provable_trivTranslated_Cl : Modal.K4 ⊢ φ → Propositional.Cl ⊢ φᵀ.toPropFormula := by
41+
lemma provable_trivTranslated_Cl : Modal.K4 ⊢ φ → φᵀ.toPropFormula ∈ Propositional.Cl := by
4242
intro h;
4343
apply Triv.iff_provable_Cl.mp;
4444
apply WeakerThan.pbl h;
@@ -64,7 +64,8 @@ instance : Modal.K4 ⪱ Modal.GL := by
6464

6565
namespace GL
6666

67-
lemma provable_verTranslated_Cl : Modal.GL ⊢ φ → Propositional.Cl ⊢ φⱽ.toPropFormula := by
67+
lemma provable_verTranslated_Cl : Modal.GL ⊢ φ → φⱽ.toPropFormula ∈ Propositional.Cl := by
68+
rw [←Propositional.Hilbert.iff_mem_logic_provable];
6869
intro h;
6970
induction h using Hilbert.Normal.rec! with
7071
| axm _ a =>

‎Foundation/Modal/ModalCompanion.lean‎

Lines changed: 0 additions & 6 deletions
This file was deleted.

‎Foundation/Modal/ModalCompanion/Corsi/VF.lean‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,7 @@ module
22

33
public import Foundation.Modal.PLoN.Logic.N
44
public import Foundation.Modal.Logic.SumNormal
5-
public import Foundation.Propositional.FMT.Logic
6-
public import Foundation.Propositional.Kripke.Logic.Cl
5+
public import Foundation.Propositional.FMT.Hilbert.VF
76

87
@[expose] public section
98

@@ -118,10 +117,10 @@ lemma provable_gödelWeakTranslated_of_provable_VF.lemma {M : PLoN.Model} {w : M
118117
| _ => dsimp [Formula.PLoN.Forces]; grind;
119118

120119
open provable_gödelWeakTranslated_of_provable_VF in
121-
lemma provable_gödelWeakTranslated_of_provable_VF : Propositional.VF ⊢ φ → Modal.N ⊢ φᶜ := by
120+
lemma provable_gödelWeakTranslated_of_provable_VF : φ ∈ Propositional.VF → Modal.N ⊢ φᶜ := by
122121
contrapose!;
123122
intro h;
124-
apply Propositional.VF.FMT.sound.not_provable_of_countermodel;
123+
apply HilbertVF.VF.soundFMT.not_provable_of_countermodel;
125124
apply Propositional.FMT.not_validOnFrameClass_of_exists_model_world;
126125
obtain ⟨M, w, _, hφ⟩ := Modal.PLoN.exists_model_world_of_not_validOnFrameClass $ Modal.N.PLoN.complete.exists_countermodel_of_not_provable h;
127126
use lemma.translate M, .inr w;
@@ -162,10 +161,10 @@ lemma provable_VF_of_provable_gödelWeakTranslated.lemma {M : FMT.Model} {w : M.
162161
| _ => dsimp [Formula.PLoN.Forces]; grind;
163162

164163
open provable_VF_of_provable_gödelWeakTranslated in
165-
lemma provable_VF_Ser_of_provable_gödelWeakTranslated : Modal.NP ⊢ φᶜ → Propositional.VF ⊢ φ := by
164+
lemma provable_VF_Ser_of_provable_gödelWeakTranslated : Modal.NP ⊢ φᶜ → φ ∈ Propositional.VF := by
166165
contrapose!;
167166
intro h;
168-
obtain ⟨M, x, _, H⟩ := Propositional.FMT.exists_model_world_of_not_validOnFrameClass $ Propositional.VF.FMT.complete.exists_countermodel_of_not_provable h;
167+
obtain ⟨M, x, _, H⟩ := Propositional.FMT.exists_model_world_of_not_validOnFrameClass $ HilbertVF.VF.completeFMT.exists_countermodel_of_not_provable h;
169168
apply Modal.NP.PLoN.sound.not_provable_of_countermodel;
170169
apply Modal.PLoN.not_validOnFrameClass_of_exists_model_world;
171170
use lemma.translate M, x;
@@ -174,7 +173,7 @@ lemma provable_VF_Ser_of_provable_gödelWeakTranslated : Modal.NP ⊢ φᶜ →
174173
. apply lemma.not.mpr H;
175174

176175
lemma VF_modal_companion_TFAE : [
177-
Propositional.VF ⊢ φ,
176+
φ ∈ Propositional.VF,
178177
Modal.N ⊢ φᶜ,
179178
Modal.NP ⊢ φᶜ
180179
].TFAE := by

‎Foundation/Modal/ModalCompanion/Standard.lean‎

Lines changed: 0 additions & 11 deletions
This file was deleted.

0 commit comments

Comments
 (0)