import Logic.Syntax
import Kripke.Frame
universe u
abbrev Semantics := Kripke.Frame
namespace Kripke
open Syntax
open Pf
def soundness {W : Type u}[Frame W] {Γ : Ctxt}{tm : Tm} : Pf Γ tm → Entails W Γ tm
| Pf.assume => by
apply Semantics.assumption
| Pf.wk h pf => by
exact Semantics.wk (Γ := _) (Δ := _) (t := _) h (soundness pf)
| Pf.and_I p q => by
apply Semantics.and_Ia
apply soundness p
apply soundness q
| Pf.and_E₁ p => by
apply Semantics.and_E₁a
apply soundness p
| Pf.and_E₂ p => by
apply Semantics.and_E₂a
apply soundness p
| or_I₁ p => by
apply Semantics.or_I₁
apply soundness p
| or_I₂ q => by
apply Semantics.or_I₂
apply soundness q
| or_E p_or_q c_ass_p c_ass_q => by
apply Semantics.or_EaW : Type uaW : Type uaW : Type u
apply soundness p_or_qaW : Type u
apply soundness c_ass_p
apply soundness c_ass_q
| Pf.imp_I p => by
apply Semantics.imp_I
apply soundness p
| Pf.imp_E p q => by
apply Semantics.imp_Eaa
apply soundness p
apply soundness q
| Pf.tt_I => fun _ _ => trivial
| Pf.ff_E p => by
exact Semantics.ff_E (Γ := _) (p := _) (soundness p)
section Consistency
namespace Consistency
open Triv
end Consistency
end Consistency
section ExcludedMiddle
namespace ExcludedMiddle
/-- A Kripke frame that refutes the Law of Excluded Middle.
w1 [P]
/
/
w0 []
\
\
w2 [¬P]
-/
inductive EMFrame where
| w0 | w1 | w2
instance : LE EMFrame where
le x y := match x, y with
| .w0, _ => True
| .w1, .w1 => True
| .w2, .w2 => True
| _, _ => False
instance : Preorder EMFrame where
le_refl x := by cases xw0w1w2 <;>w0w1w2 simp [LE.le]
le_trans x y z := by
cases x <;> cases y <;> cases zw2.w2.w0w2.w2.w1w2.w2.w2 <;>w0.w0.w0w0.w0.w1w0.w0.w2w0.w1.w0w0.w1.w1w0.w1.w2w0.w2.w0w0.w2.w1w0.w2.w2w1.w0.w0w1.w0.w1w1.w0.w2w1.w1.w0w1.w1.w1w1.w1.w2w1.w2.w0w1.w2.w1w1.w2.w2w2.w0.w0w2.w0.w1w2.w0.w2w2.w1.w0w2.w1.w1w2.w1.w2w2.w2.w0w2.w2.w1w2.w2.w2 simp [LE.le]
instance : Frame EMFrame where
val w i := match w, i with
| .w1, 0 => True
| _, _ => False
le_val := by⊢ ∀ {w w' : EMFrame} {i : ℕ},
w ≤ w' →
(match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False
intro w w'⊢ ∀ {i : ℕ},
w ≤ w' →
(match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False i⊢ w ≤ w' →
(match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False hle⊢ (match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False hval
cases ww0w1w2 <;>w0w1w2 cases w'w2.w0w2.w1w2.w2 <;>w0.w0w0.w1w0.w2w1.w0w1.w1w1.w2w2.w0w2.w1w2.w2 simp [LE.le] at *
exact hval
open Tm
open EMFrame
theorem em_not_provable : ¬ Pf [] (var 0 ∨ (var 0 ⇒ ff)) := by
intro h
-- EM for P := var 0, is neither probable nor refutable at w0
let EM_pf_at_w := soundness (W := EMFrame) h w0 (by simp [all_at_world])
simp [at_world] at EM_pf_at_w
rcases EM_pf_at_w with pf_p | pf_not_p
· -- case 1: w0 forced at p,
-- But by def of val it is not forced here
simp [Frame.val] at pf_p
· -- Case 2: w0 forces p -> ⊥
-- At every world accessible from w0, if p is true, then ⊥ is true.
-- But w1 is accessible from w0, and p is true at w1 while ⊥ is never true.
have w0_le_w1 : w0 ≤ w1 := by simp [LE.le]
have p_at_w1 : at_world w1 (var 0) := by simp [at_world, Frame.val]
exact pf_not_p w1 w0_le_w1 p_at_w1
end ExcludedMiddle
end ExcludedMiddle
end Kripke