diff --git a/Foundation.lean b/Foundation.lean index b6a8753d1..b236d4b74 100644 --- a/Foundation.lean +++ b/Foundation.lean @@ -494,6 +494,18 @@ public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Tra1 public import Foundation.Propositional.Kripke2.Hilbert.F_Ser public import Foundation.Propositional.Kripke2.Hilbert.F_Sym public import Foundation.Propositional.Kripke2.Hilbert.F_Tra1 +public import Foundation.Propositional.Kripke3.Axiom.Dummett +public import Foundation.Propositional.Kripke3.Axiom.KreiselPutnam +public import Foundation.Propositional.Kripke3.Axiom.LEM +public import Foundation.Propositional.Kripke3.Axiom.Tra +public import Foundation.Propositional.Kripke3.Axiom.WLEM +public import Foundation.Propositional.Kripke3.Basic +public import Foundation.Propositional.Kripke3.Logic.Cl +public import Foundation.Propositional.Kripke3.Logic.Int.Completeness +public import Foundation.Propositional.Kripke3.Logic.Int.DP +public import Foundation.Propositional.Kripke3.Logic.KC +public import Foundation.Propositional.Kripke3.Logic.KreiselPutnam +public import Foundation.Propositional.Kripke3.Logic.LC public import Foundation.Propositional.Logic.Basic public import Foundation.Propositional.Logic.Letterless_Int_Cl public import Foundation.Propositional.Logic.PostComplete diff --git a/Foundation/Propositional/ConsistentTableau.lean b/Foundation/Propositional/ConsistentTableau.lean index cd834094b..9b8028e59 100644 --- a/Foundation/Propositional/ConsistentTableau.lean +++ b/Foundation/Propositional/ConsistentTableau.lean @@ -3,37 +3,46 @@ module public import Foundation.Propositional.Formula.Basic public import Foundation.Propositional.Entailment.Cl.Basic public import Foundation.Vorspiel.Set.Basic +public import Foundation.Propositional.Entailment.Corsi @[expose] public section namespace LO.Propositional -open Entailment FiniteContext +open Entailment open Formula variable {α : Type*} variable {S} [Entailment S (Formula α)] variable {𝓢 : S} -def Tableau (α : Type u) := Set (Formula α) × Set (Formula α) +structure Tableau (α : Type u) where + Γ : Set (Formula α) + Δ : Set (Formula α) namespace Tableau +instance : HasSubset (Tableau α) := ⟨λ t₁ t₂ => t₁.Γ ⊆ t₂.Γ ∧ t₁.Δ ⊆ t₂.Δ⟩ + +def insert₁ (φ : Formula α) (t : Tableau α) : Tableau α := ⟨insert φ t.Γ, t.Δ⟩ +def insert₂ (φ : Formula α) (t : Tableau α) : Tableau α := ⟨t.Γ, insert φ t.Δ⟩ + variable {φ ψ: Formula α} {T U : FormulaSet α} {t u : Tableau α} -abbrev Consistent (𝓢 : S) (t : Tableau α) := ∀ {Γ Δ : Finset (Formula α)}, (↑Γ ⊆ t.1) → (↑Δ ⊆ t.2) → 𝓢 ⊬ (Γ.conj) 🡒 (Δ.disj) +@[grind] +def Consistent (𝓢 : S) (t : Tableau α) := ∀ {Γ Δ : Finset (Formula α)}, (↑Γ ⊆ t.Γ) → (↑Δ ⊆ t.Δ) → 𝓢 ⊬ (Γ.conj) 🡒 (Δ.disj) abbrev Inconsistent (𝓢 : S) (t : Tableau α) := ¬Consistent 𝓢 t +lemma iff_inconsistent : Inconsistent 𝓢 t ↔ ∃ Γ Δ : Finset (Formula α), (↑Γ ⊆ t.Γ) ∧ (↑Δ ⊆ t.Δ) ∧ 𝓢 ⊢ (Γ.conj) 🡒 (Δ.disj) := by grind; -instance : HasSubset (Tableau α) := ⟨λ t₁ t₂ => t₁.1 ⊆ t₂.1 ∧ t₁.2 ⊆ t₂.2⟩ -@[simp] lemma subset_def {t₁ t₂ : Tableau α} : t₁ ⊆ t₂ ↔ t₁.1 ⊆ t₂.1 ∧ t₁.2 ⊆ t₂.2 := by rfl +@[simp] lemma subset_def {t₁ t₂ : Tableau α} : t₁ ⊆ t₂ ↔ t₁.Γ ⊆ t₂.Γ ∧ t₁.Δ ⊆ t₂.Δ := by rfl -@[simp] lemma equality_def {t₁ t₂ : Tableau α} : t₁ = t₂ ↔ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2 := by +@[simp] lemma equality_def {t₁ t₂ : Tableau α} : t₁ = t₂ ↔ t₁.Γ = t₂.Γ ∧ t₁.Δ = t₂.Δ := by constructor; . intro h; cases h; simp; . rintro ⟨h₁, h₂⟩; cases t₁; cases t₂; simp_all; -lemma not_mem₂ (hCon : t.Consistent 𝓢) {Γ : Finset (Formula α)} (hΓ : ∀ φ ∈ Γ, φ ∈ t.1) (h : 𝓢 ⊢ Γ.conj 🡒 ψ) : ψ ∉ t.2 := by +lemma not_mem₂ (hCon : t.Consistent 𝓢) {Γ : Finset (Formula α)} (hΓ : ∀ φ ∈ Γ, φ ∈ t.Γ) (h : 𝓢 ⊢ Γ.conj 🡒 ψ) : ψ ∉ t.Δ := by by_contra hC; have : 𝓢 ⊢ Γ.conj 🡒 (Finset.disj {ψ}) := by simpa; have : 𝓢 ⊬ Γ.conj 🡒 (Finset.disj {ψ}) := hCon (by aesop) (by aesop); @@ -41,145 +50,113 @@ lemma not_mem₂ (hCon : t.Consistent 𝓢) {Γ : Finset (Formula α)} (hΓ : section -variable [Entailment.Int 𝓢] +variable [Entailment.VF 𝓢] +open Entailment.Corsi -lemma disjoint_of_consistent (hCon : t.Consistent 𝓢) : Disjoint t.1 t.2 := by +lemma disjoint_of_consistent (hCon : t.Consistent 𝓢) : Disjoint t.Γ t.Δ := by by_contra h; obtain ⟨T, hp₁, hp₂, hp⟩ := by simpa [Disjoint] using h; obtain ⟨φ, hp⟩ := Set.nonempty_def.mp $ Set.nonempty_iff_ne_empty.mpr hp; - have : 𝓢 ⊬ (Finset.conj {φ}) 🡒 (Finset.disj {φ}) := hCon - (by simp_all only [Finset.coe_singleton, Set.singleton_subset_iff]; apply hp₁; assumption) - (by simp_all only [Finset.coe_singleton, Set.singleton_subset_iff]; apply hp₂; assumption); + have : 𝓢 ⊬ (Finset.conj {φ}) 🡒 (Finset.disj {φ}) := hCon (by grind) (by grind); replace this : 𝓢 ⊬ φ 🡒 φ := by simpa using this; - have : 𝓢 ⊢ φ 🡒 φ := C!_id; + have : 𝓢 ⊢ φ 🡒 φ := impId; contradiction; variable [DecidableEq α] lemma iff_consistent_insert₁ - : Tableau.Consistent 𝓢 ((insert φ T), U) ↔ ∀ {Γ Δ : Finset (Formula α)}, (↑Γ ⊆ T) → (↑Δ ⊆ U) → 𝓢 ⊬ φ ⋏ Γ.conj 🡒 Δ.disj := by + : (t.insert₁ φ).Consistent 𝓢 ↔ ∀ {Γ Δ : Finset (Formula α)}, (↑Γ ⊆ t.Γ) → (↑Δ ⊆ t.Δ) → 𝓢 ⊬ (insert φ Γ).conj 🡒 Δ.disj := by constructor; . intro h Γ Δ hΓ hΔ; by_contra hC; apply h (Γ := insert φ Γ) (Δ := Δ) ?_ hΔ; - . exact C!_trans (by simp) hC; + . assumption; . simp only [Finset.coe_insert]; apply Set.insert_subset_insert; exact hΓ; . intro h Γ Δ hΓ hΔ; by_contra hC; - simp_all only; apply h (Γ := Γ.erase φ) (Δ := Δ) (by simpa) hΔ; - refine C!_trans ?_ hC; - . exact C!_trans CKFConjinsertFConj! $ CFConj_FConj!_of_subset $ Finset.insert_erase_subset φ Γ + exact ruleI (CFConjFConj_of_subset (by grind)) hC; -lemma iff_not_consistent_insert₁ : ¬Tableau.Consistent 𝓢 ((insert φ T), U) ↔ ∃ Γ Δ : Finset (Formula α), (↑Γ ⊆ T) ∧ (↑Δ ⊆ U) ∧ 𝓢 ⊢ φ ⋏ Γ.conj 🡒 Δ.disj := by - constructor; - . contrapose!; apply iff_consistent_insert₁.mpr; - . contrapose!; apply iff_consistent_insert₁.mp; +lemma iff_not_consistent_insert₁ : (t.insert₁ φ).Inconsistent 𝓢 ↔ ∃ Γ Δ : Finset (Formula α), (↑Γ ⊆ t.Γ) ∧ (↑Δ ⊆ t.Δ) ∧ 𝓢 ⊢ (insert φ Γ).conj 🡒 Δ.disj := by + apply Iff.trans iff_consistent_insert₁.not + grind; -lemma iff_consistent_insert₂ : Tableau.Consistent 𝓢 (T, (insert φ U)) ↔ ∀ {Γ Δ : Finset (Formula α)}, (↑Γ ⊆ T) → (↑Δ ⊆ U) → 𝓢 ⊬ Γ.conj 🡒 φ ⋎ Δ.disj := by +lemma iff_consistent_insert₂ : (t.insert₂ φ).Consistent 𝓢 ↔ ∀ {Γ Δ : Finset (Formula α)}, (↑Γ ⊆ t.Γ) → (↑Δ ⊆ t.Δ) → 𝓢 ⊬ Γ.conj 🡒 (insert φ Δ).disj := by constructor; . intro h Γ Δ hΓ hΔ; by_contra hC; apply h (Γ := Γ) (Δ := insert φ Δ) hΓ ?_; - . exact C!_trans hC $ by simp; + . assumption; . simp only [Finset.coe_insert]; apply Set.insert_subset_insert; exact hΔ; . intro h Γ Δ hΓ hΔ; by_contra hC; apply h (Γ := Γ) (Δ := Δ.erase φ) hΓ (by simpa); - exact C!_trans hC $ by - refine C!_trans ?_ $ CinsertFDisjAFDisj! (𝓢 := 𝓢) (Γ := Δ.erase φ); - apply CDisj₂Disj₂_of_subset; - simp only [Finset.mem_toList, Finset.mem_insert, Finset.mem_erase, ne_eq]; - tauto; + apply ruleI hC; + apply CFDisjFDisj_of_subset; + grind; -lemma iff_not_consistent_insert₂ : ¬Tableau.Consistent 𝓢 (T, (insert φ U)) ↔ ∃ Γ Δ : Finset (Formula α), (↑Γ ⊆ T) ∧ (↑Δ ⊆ U) ∧ 𝓢 ⊢ Γ.conj 🡒 φ ⋎ Δ.disj := by - constructor; - . contrapose!; apply iff_consistent_insert₂.mpr; - . contrapose!; apply iff_consistent_insert₂.mp; +lemma iff_not_consistent_insert₂ : (t.insert₂ φ).Inconsistent 𝓢 ↔ ∃ Γ Δ : Finset (Formula α), (↑Γ ⊆ t.Γ) ∧ (↑Δ ⊆ t.Δ) ∧ 𝓢 ⊢ Γ.conj 🡒 (insert φ Δ).disj := by + apply Iff.trans iff_consistent_insert₂.not; + grind; section Consistent variable {t : Tableau α} -lemma consistent_either (hCon : t.Consistent 𝓢) (φ : Formula α) : Tableau.Consistent 𝓢 ((insert φ t.1), t.2) ∨ Tableau.Consistent 𝓢 (t.1, (insert φ t.2)) := by - by_contra hC; - push_neg at hC; - have ⟨hC₁, hC₂⟩ := hC; - - obtain ⟨Γ₁, Δ₁, hΓ₁, hΔ₁, h₁⟩ := iff_not_consistent_insert₁.mp hC₁; - replace h₁ := left_K!_symm h₁; - - obtain ⟨Γ₂, Δ₂, hΓ₂, hΔ₂, h₂⟩ := iff_not_consistent_insert₂.mp hC₂; +lemma consistent_either (hCon : t.Consistent 𝓢) (φ : Formula α) + : Tableau.Consistent 𝓢 (t.insert₁ φ) ∨ Tableau.Consistent 𝓢 (t.insert₂ φ) := by + by_contra! hC; + have ⟨h₁, h₂⟩ := hC; + obtain ⟨Γ₁, Δ₁, hΓ₁, hΔ₁, h₁⟩ := iff_not_consistent_insert₁.mp h₁; + obtain ⟨Γ₂, Δ₂, hΓ₂, hΔ₂, h₂⟩ := iff_not_consistent_insert₂.mp h₂; apply @hCon (Γ := Γ₁ ∪ Γ₂) (Δ := Δ₁ ∪ Δ₂) ?_ ?_; - . exact C!_trans (C!_trans (by simp) (cut! h₁ h₂)) (by simp); + . replace h₁ : 𝓢 ⊢ φ ⋏ Γ₁.conj 🡒 Δ₁.disj := ruleI insert_FConj h₁; + replace h₂ : 𝓢 ⊢ Γ₂.conj 🡒 φ ⋎ Δ₂.disj := by + apply ruleI; + . exact h₂; + . sorry; + sorry; . simp only [Finset.coe_union, Set.union_subset_iff]; tauto; . simp only [Finset.coe_union, Set.union_subset_iff]; tauto; - -- have : 𝓢 ⊢ ⋀(Γ₁ ++ Γ₂) 🡒 ⋁(Δ₁ ++ Δ₂) := C!_trans (K!_left EConj₂AppendKConj₂Conj₂!) $ C!_trans (cut! h₁ h₂) (K!_right EDisj₂AppendADisj₂Disj₂!); - end Consistent end -abbrev Saturated (t : Tableau α) := ∀ φ : Formula α, φ ∈ t.1 ∨ φ ∈ t.2 + +@[grind] +def Saturated (t : Tableau α) := ∀ φ : Formula α, φ ∈ t.Γ ∨ φ ∈ t.Δ section Saturated -variable [Entailment.Int 𝓢] +variable [Entailment.VF 𝓢] variable {t : Tableau α} -lemma mem₂_of_not_mem₁ (hMat : Saturated t) : φ ∉ t.1 → φ ∈ t.2 := by - intro h; - cases (hMat φ) with - | inl h' => exact absurd h' h; - | inr _ => assumption; - -lemma mem₁_of_not_mem₂ (hMat : Saturated t) : φ ∉ t.2 → φ ∈ t.1 := by - intro h; - cases (hMat φ) with - | inl _ => assumption; - | inr h' => exact absurd h' h; +lemma mem₂_of_notMem₁_of_saturated (hMat : Saturated t) : φ ∉ t.Γ → φ ∈ t.Δ := by grind; +lemma mem₁_of_notMem₂_of_saturated (hMat : Saturated t) : φ ∉ t.Δ → φ ∈ t.Γ := by grind; -lemma not_mem₁_iff_mem₂ (hCon : t.Consistent 𝓢) (hMat : Saturated t) : φ ∉ t.1 ↔ φ ∈ t.2 := by +@[grind .] +lemma iff_mem₁_notMem₂_of_consistent_saturated (hCon : t.Consistent 𝓢) (hSat : Saturated t) : φ ∈ t.Γ ↔ φ ∉ t.Δ := by constructor; - . apply mem₂_of_not_mem₁ hMat; - . apply Set.disjoint_right.mp $ disjoint_of_consistent hCon; + . apply Set.disjoint_right.mp $ Disjoint.symm $ disjoint_of_consistent hCon; + . apply mem₁_of_notMem₂_of_saturated hSat; -lemma not_mem₂_iff_mem₁ (hCon : t.Consistent 𝓢) (hMat : Saturated t) : φ ∉ t.2 ↔ φ ∈ t.1 := by - constructor; - . apply mem₁_of_not_mem₂ hMat; - . apply Set.disjoint_left.mp $ disjoint_of_consistent hCon; - -lemma saturated_duality - {t₁ t₂ : Tableau α} - (ct₁ : t₁.Consistent 𝓢) (ct₂ : t₂.Consistent 𝓢) - (st₁ : Saturated t₁) (st₂ : Saturated t₂) - : t₁.1 = t₂.1 ↔ t₁.2 = t₂.2 := by +@[grind .] +lemma iff_mem₂_notMem₁_of_consistent_saturated (hCon : t.Consistent 𝓢) (hSat : Saturated t) : φ ∈ t.Δ ↔ φ ∉ t.Γ := by constructor; - . intro h; - apply Set.eq_of_subset_of_subset; - . intro φ hp; - apply not_mem₁_iff_mem₂ ct₂ st₂ |>.mp; rw [←h]; - apply not_mem₁_iff_mem₂ ct₁ st₁ |>.mpr hp; - . intro φ hp; - apply not_mem₁_iff_mem₂ ct₁ st₁ |>.mp; rw [h]; - apply not_mem₁_iff_mem₂ ct₂ st₂ |>.mpr hp; - . intro h; - apply Set.eq_of_subset_of_subset; - . intro φ hp; - apply not_mem₂_iff_mem₁ ct₂ st₂ |>.mp; rw [←h]; - apply not_mem₂_iff_mem₁ ct₁ st₁ |>.mpr hp; - . intro φ hp; - apply not_mem₂_iff_mem₁ ct₁ st₁ |>.mp; rw [h]; - apply not_mem₂_iff_mem₁ ct₂ st₂ |>.mpr hp; + . apply Set.disjoint_left.mp $ Disjoint.symm $ disjoint_of_consistent hCon; + . apply mem₂_of_notMem₁_of_saturated hSat; + +lemma saturated_duality {t₁ t₂ : Tableau α} (ct₁ : t₁.Consistent 𝓢) (ct₂ : t₂.Consistent 𝓢) (st₁ : Saturated t₁) (st₂ : Saturated t₂) : + t₁.Γ = t₂.Γ ↔ t₁.Δ = t₂.Δ := by grind; end Saturated -lemma emptyset_consistent [Entailment.Int 𝓢] [DecidableEq α] [H_consis : Entailment.Consistent 𝓢] : Consistent 𝓢 ⟨∅, ∅⟩ := by +lemma emptyset_consistent [Entailment.VF 𝓢] [DecidableEq α] [H_consis : Entailment.Consistent 𝓢] : Consistent 𝓢 ⟨∅, ∅⟩ := by intro Γ Δ hΓ hΔ; by_contra hC; obtain ⟨ψ, hψ⟩ := H_consis.exists_unprovable; @@ -187,7 +164,7 @@ lemma emptyset_consistent [Entailment.Int 𝓢] [DecidableEq α] [H_consis : Ent simp only [Set.subset_empty_iff, Finset.coe_eq_empty] at hΓ hΔ; subst hΓ hΔ; simp only [Finset.conj_empty, Finset.disj_empty] at hC; - exact of_O! (hC ⨀ C!_id); + exact Corsi.of_O (hC ⨀ (by simp)); section lindenbaum @@ -197,7 +174,7 @@ variable {t : Tableau α} open Classical open Encodable -noncomputable def lindenbaum_next (φ : Formula α) (t : Tableau α) : Tableau α := if Tableau.Consistent 𝓢 (insert φ t.1, t.2) then (insert φ t.1, t.2) else (t.1, insert φ t.2) +noncomputable def lindenbaum_next (φ : Formula α) (t : Tableau α) : Tableau α := if Tableau.Consistent 𝓢 (t.insert₁ φ) then (t.insert₁ φ) else (t.insert₂ φ) noncomputable def lindenbaum_next_indexed [Encodable α] (t : Tableau α) : ℕ → Tableau α | 0 => t @@ -207,14 +184,14 @@ noncomputable def lindenbaum_next_indexed [Encodable α] (t : Tableau α) : ℕ | none => lindenbaum_next_indexed t i local notation:max t"[" i "]" => lindenbaum_next_indexed 𝓢 t i -def lindenbaum_maximal [Encodable α] (t : Tableau α) : Tableau α := (⋃ i, t[i].1, ⋃ i, t[i].2) +def lindenbaum_maximal [Encodable α] (t : Tableau α) : Tableau α := ⟨⋃ i, t[i].1, ⋃ i, t[i].2⟩ local notation:max t"∞" => lindenbaum_maximal 𝓢 t @[simp] lemma lindenbaum_next_indexed_zero [Encodable α] {t : Tableau α} : (t.lindenbaum_next_indexed 𝓢 0) = t := by simp [lindenbaum_next_indexed] variable {𝓢} -lemma next_parametericConsistent [Entailment.Int 𝓢] (consistent : t.Consistent 𝓢) (φ : Formula α) : (t.lindenbaum_next 𝓢 φ).Consistent 𝓢 := by +lemma next_parametericConsistent [Entailment.VF 𝓢] (consistent : t.Consistent 𝓢) (φ : Formula α) : (t.lindenbaum_next 𝓢 φ).Consistent 𝓢 := by dsimp [lindenbaum_next]; split; . simpa; @@ -224,7 +201,7 @@ lemma next_parametericConsistent [Entailment.Int 𝓢] (consistent : t.Consisten variable [Encodable α] -lemma lindenbaum_next_indexed_parametricConsistent_succ [Entailment.Int 𝓢] {i : ℕ} : Consistent 𝓢 t[i] → Consistent 𝓢 t[i + 1] := by +lemma lindenbaum_next_indexed_parametricConsistent_succ [Entailment.VF 𝓢] {i : ℕ} : Consistent 𝓢 t[i] → Consistent 𝓢 t[i + 1] := by dsimp [lindenbaum_next_indexed]; split; . intro h; @@ -238,7 +215,7 @@ lemma mem_lindenbaum_next_indexed (t) (φ : Formula α) : φ ∈ t[(encode φ) + . left; tauto; . right; tauto; -lemma lindenbaum_next_indexed_parametricConsistent [Entailment.Int 𝓢] (consistent : t.Consistent 𝓢) (i : ℕ) : t[i].Consistent 𝓢 := by +lemma lindenbaum_next_indexed_parametricConsistent [Entailment.VF 𝓢] (consistent : t.Consistent 𝓢) (i : ℕ) : t[i].Consistent 𝓢 := by induction i with | zero => simpa; | succ i ih => apply lindenbaum_next_indexed_parametricConsistent_succ; assumption; @@ -309,7 +286,7 @@ lemma exists_finset_lindenbaum_index₂ {Δ : Finset _} (hΓ : ↑Δ ⊆ ⋃ i, apply hΔ; simpa; -lemma exists_parametricConsistent_saturated_tableau [Entailment.Int 𝓢] (hCon : t.Consistent 𝓢) : ∃ u, t ⊆ u ∧ (Tableau.Consistent 𝓢 u) ∧ (Saturated u) := by +lemma exists_parametricConsistent_saturated_tableau [Entailment.VF 𝓢] (hCon : t.Consistent 𝓢) : ∃ u, t ⊆ u ∧ (Tableau.Consistent 𝓢 u) ∧ (Saturated u) := by use t∞; refine ⟨?subset, ?consistent, ?saturated⟩; case subset => constructor <;> apply Set.subset_iUnion_of_subset 0 (by simp); @@ -338,45 +315,42 @@ end Tableau open Tableau -def SaturatedConsistentTableau (𝓢 : S) := {t : Tableau α // Saturated t ∧ t.Consistent 𝓢} +@[ext] +structure SaturatedConsistentTableau (𝓢 : S) extends Tableau α where + saturated : Saturated toTableau + consistent : Consistent 𝓢 toTableau namespace SaturatedConsistentTableau -lemma consistent (t : SaturatedConsistentTableau 𝓢) : Consistent 𝓢 t.1 := t.2.2 - -lemma saturated (t : SaturatedConsistentTableau 𝓢) : Saturated t.1 := t.2.1 - variable {t₀ : Tableau α} {φ ψ : Formula α} -lemma lindenbaum [Entailment.Int 𝓢] [Encodable α] (hCon : t₀.Consistent 𝓢) : ∃ (t : SaturatedConsistentTableau 𝓢), t₀ ⊆ t.1 := by +attribute [simp, grind .] saturated consistent + +lemma lindenbaum [Entailment.VF 𝓢] [Encodable α] (hCon : t₀.Consistent 𝓢) : ∃ (t : SaturatedConsistentTableau 𝓢), t₀ ⊆ t.toTableau := by obtain ⟨t, ht, hCon, hMax⟩ := Tableau.lindenbaum hCon; exact ⟨⟨t, hMax, hCon⟩, ht⟩; -instance [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] [DecidableEq α] [Encodable α] : Nonempty (SaturatedConsistentTableau 𝓢) := ⟨lindenbaum Tableau.emptyset_consistent |>.choose⟩ +instance [Entailment.Consistent 𝓢] [Entailment.VF 𝓢] [DecidableEq α] [Encodable α] : Nonempty (SaturatedConsistentTableau 𝓢) := ⟨lindenbaum Tableau.emptyset_consistent |>.choose⟩ variable {t t₁ t₂ : SaturatedConsistentTableau 𝓢} -lemma not_mem₂ {Γ : Finset (Formula α)} (hΓ : ↑Γ ⊆ t.1.1) (h : 𝓢 ⊢ Γ.conj 🡒 ψ) : ψ ∉ t.1.2 := t.1.not_mem₂ t.consistent hΓ h - -variable [Entailment.Int 𝓢] +lemma not_mem₂ {Γ : Finset (Formula α)} (hΓ : ↑Γ ⊆ t.Γ) (h : 𝓢 ⊢ Γ.conj 🡒 ψ) : ψ ∉ t.Δ := t.toTableau.not_mem₂ t.consistent hΓ h -@[simp] lemma disjoint : Disjoint t.1.1 t.1.2 := t.1.disjoint_of_consistent t.2.2 +variable [Entailment.VF 𝓢] -lemma iff_not_mem₁_mem₂ : φ ∉ t.1.1 ↔ φ ∈ t.1.2 := Tableau.not_mem₁_iff_mem₂ t.consistent t.saturated +@[simp, grind .] lemma disjoint : Disjoint t.Γ t.Δ := t.toTableau.disjoint_of_consistent t.consistent -lemma iff_not_mem₂_mem₁ : φ ∉ t.1.2 ↔ φ ∈ t.1.1 := Tableau.not_mem₂_iff_mem₁ t.consistent t.saturated +lemma iff_mem₁_notMem₂ : φ ∈ t.Γ ↔ φ ∉ t.Δ := t.toTableau.iff_mem₁_notMem₂_of_consistent_saturated t.consistent t.saturated +lemma iff_mem₂_notMem₁ : φ ∈ t.Δ ↔ φ ∉ t.Γ := t.toTableau.iff_mem₂_notMem₁_of_consistent_saturated t.consistent t.saturated -lemma saturated_duality: t₁.1.1 = t₂.1.1 ↔ t₁.1.2 = t₂.1.2 := Tableau.saturated_duality t₁.consistent t₂.consistent t₁.saturated t₂.saturated +attribute [grind =_] iff_mem₁_notMem₂ iff_mem₂_notMem₁ -lemma equality_of₁ (e₁ : t₁.1.1 = t₂.1.1) : t₁ = t₂ := by - have e := Tableau.equality_def.mpr ⟨e₁, (saturated_duality.mp e₁)⟩; - calc - t₁ = ⟨t₁.1, t₁.saturated, t₁.consistent⟩ := by rfl; - _ = ⟨t₂.1, t₂.saturated, t₂.consistent⟩ := by simp [e]; - _ = t₂ := by rfl; +@[grind =] lemma saturated_duality: t₁.Γ = t₂.Γ ↔ t₁.Δ = t₂.Δ := Tableau.saturated_duality t₁.consistent t₂.consistent t₁.saturated t₂.saturated -lemma equality_of₂ (e₂ : t₁.1.2 = t₂.1.2) : t₁ = t₂ := equality_of₁ $ saturated_duality.mpr e₂ +@[grind <=] lemma equality_of₁ (e₁ : t₁.Γ = t₂.Γ) : t₁ = t₂ := by ext <;> grind; +@[grind <=] lemma equality_of₂ (e₂ : t₁.Δ = t₂.Δ) : t₁ = t₂ := by ext <;> grind; +/- section variable [DecidableEq α] [Encodable α] @@ -424,60 +398,66 @@ lemma iff_provable_mem₁ : 𝓢 ⊢ φ ↔ ∀ t : SaturatedConsistentTableau exact Context.emptyPrf! $ iff_provable_include₁.mpr $ by tauto; end +-/ section Saturated -lemma mdp_mem₁_provable (h : 𝓢 ⊢ φ 🡒 ψ) (hp₁ : φ ∈ t.1.1) : ψ ∈ t.1.1 := by - apply iff_not_mem₂_mem₁.mp; +lemma imp_closed₁ (h : 𝓢 ⊢ φ 🡒 ψ) (hp₁ : φ ∈ t.1.1) : ψ ∈ t.1.1 := by by_contra hq₂; - apply by simpa using t.consistent (Γ := {φ}) (Δ := {ψ}) (by simpa) (by simpa); - exact h; + apply t.consistent (Γ := {φ}) (Δ := {ψ}); + . grind; + . grind; + . simpa; -lemma mdp_mem₂_provable (h : 𝓢 ⊢ φ 🡒 ψ) (hp₁ : ψ ∈ t.1.2) : φ ∈ t.1.2 := by - by_contra hq₂; - have := iff_not_mem₂_mem₁.mpr $ mdp_mem₁_provable h $ iff_not_mem₂_mem₁.mp hq₂; - contradiction; +lemma imp_closed₂ (h : 𝓢 ⊢ φ 🡒 ψ) (hp₂ : ψ ∈ t.1.2) : φ ∈ t.1.2 := by + contrapose! hp₂; + grind [imp_closed₁ h]; -@[simp] lemma mem₁_verum : ⊤ ∈ t.1.1 := by - apply iff_not_mem₂_mem₁.mp; +@[simp, grind .] +lemma mem₁_verum : ⊤ ∈ t.Γ := by by_contra hC; - apply by simpa using t.consistent (Γ := ∅) (Δ := {⊤}) (by simp) (by simpa); - simp; + apply t.consistent (Γ := ∅) (Δ := {⊤}); + . grind; + . grind; + . simp; -@[simp] lemma not_mem₁_falsum : ⊥ ∉ t.1.1 := by +@[simp, grind .] +lemma notMem₁_falsum : ⊥ ∉ t.Γ := by by_contra hC; - have : 𝓢 ⊬ ⊥ 🡒 ⊥ := by simpa using t.consistent (Γ := {⊥}) (Δ := ∅) (by simpa) (by simp); - apply this; - simp; + apply t.consistent (Γ := {⊥}) (Δ := ∅); + . grind; + . grind; + . simp; -@[simp] lemma mem₂_falsum : ⊥ ∈ t.1.2 := iff_not_mem₁_mem₂.mp not_mem₁_falsum +@[simp, grind .] +lemma mem₂_falsum : ⊥ ∈ t.Δ := by grind; -lemma mem₁_of_provable : 𝓢 ⊢ φ → φ ∈ t.1.1 := by +lemma mem₁_of_provable (t : SaturatedConsistentTableau 𝓢) : 𝓢 ⊢ φ → φ ∈ t.Γ := by intro h; - exact mdp_mem₁_provable (C!_of_conseq! h) mem₁_verum; + apply imp_closed₁ (φ := ⊤); + . apply Corsi.af h; + . grind; -lemma mdp_mem₁ [DecidableEq α] (h : φ 🡒 ψ ∈ t.1.1) (hp : φ ∈ t.1.1) : ψ ∈ t.1.1 := by - apply iff_not_mem₂_mem₁.mp; - by_contra hC; - apply t.consistent (Γ := {φ, φ 🡒 ψ}) (Δ := {ψ}) ?_ (by simpa); - . apply CFConj_CDisj!_of_innerMDP (φ := φ) (ψ := ψ) <;> simp; - . simp only [Finset.coe_insert, Finset.coe_singleton]; - apply Set.doubleton_subset.mpr; - tauto; +open Entailment.Corsi -lemma iff_mem₁_and [DecidableEq α] : φ ⋏ ψ ∈ t.1.1 ↔ φ ∈ t.1.1 ∧ ψ ∈ t.1.1 := by +@[grind =>] +lemma iff_mem₁_and [DecidableEq α] : φ ⋏ ψ ∈ t.Γ ↔ φ ∈ t.Γ ∧ ψ ∈ t.Γ := by constructor; - . intro h; constructor <;> exact mdp_mem₁_provable (by simp) h + . intro h; constructor <;> exact imp_closed₁ (by simp) h . rintro ⟨hp, hq⟩; - apply iff_not_mem₂_mem₁.mp; by_contra hC; - apply t.consistent (Γ := {φ, ψ}) (Δ := {φ ⋏ ψ}) ?_ (by simp_all); - . apply CFConj_CDisj!_of_K_intro (φ := φ) (ψ := ψ) <;> simp; - . simp only [Finset.coe_insert, Finset.coe_singleton]; - apply Set.doubleton_subset.mpr; - tauto; + apply t.consistent (Γ := {φ, ψ}) (Δ := {φ ⋏ ψ}); + . grind; + . grind; + . rw [Finset.disj_singleton]; + apply ruleC <;> exact mem_fconj (by simp); -lemma iff_mem₁_conj₂ [DecidableEq α] {Γ : List (Formula α)} : ⋀Γ ∈ t.1.1 ↔ ∀ φ ∈ Γ, φ ∈ t.1.1 := by +@[grind =>] +lemma iff_mem₂_and [DecidableEq α] : φ ⋏ ψ ∈ t.Δ ↔ φ ∈ t.Δ ∨ ψ ∈ t.Δ := by grind; + +attribute [grind =] List.conj₂_nil List.conj₂_singleton List.conj₂_cons_nonempty + +lemma iff_mem₁_conj₂ [DecidableEq α] {Γ : List (Formula α)} : ⋀Γ ∈ t.Γ ↔ ∀ φ ∈ Γ, φ ∈ t.Γ := by induction Γ using List.induction_with_singleton with | hcons φ Γ Γ_nil ih => simp only [(List.conj₂_cons_nonempty Γ_nil), List.mem_cons]; @@ -487,59 +467,26 @@ lemma iff_mem₁_conj₂ [DecidableEq α] {Γ : List (Formula α)} : ⋀Γ ∈ t . exact ih.mp (iff_mem₁_and.mp h |>.2) _ hp; . intro h; apply iff_mem₁_and.mpr; - simp_all; + grind; | _ => simp; -lemma iff_mem₁_fconj [DecidableEq α] {Γ : Finset (Formula α)} : Γ.conj ∈ t.1.1 ↔ ↑Γ ⊆ t.1.1 := by - constructor; - . intro h φ hφ; - apply iff_mem₁_conj₂ (Γ := Γ.toList) (t := t) |>.mp; - . apply mdp_mem₁_provable ?_ h; simp; - . simpa; - . intro h; - apply mdp_mem₁_provable ?_ $ iff_mem₁_conj₂ (Γ := Γ.toList) (t := t) |>.mpr $ by - intro φ hφ; - apply h; - simp_all; - simp; +lemma iff_mem₁_fconj [DecidableEq α] {Γ : Finset (Formula α)} : Γ.conj ∈ t.Γ ↔ ↑Γ ⊆ t.Γ := by + apply Iff.trans iff_mem₁_conj₂; + grind [Finset.mem_toList]; -private lemma of_mem₁_or [DecidableEq α] : φ ⋎ ψ ∈ t.1.1 → (φ ∈ t.1.1 ∨ ψ ∈ t.1.1) := by - intro h; - by_contra hC; push_neg at hC; - apply t.consistent (Γ := {φ ⋎ ψ}) (Δ := {φ, ψ}) (by simp_all) ?_; - . apply CFConj_CDisj!_of_A (φ := φ) (ψ := ψ) <;> simp; - . simp only [Finset.coe_insert, Finset.coe_singleton]; - apply Set.doubleton_subset.mpr; - constructor; - . exact iff_not_mem₁_mem₂.mp hC.1; - . exact iff_not_mem₁_mem₂.mp hC.2; - -private lemma of_mem₂_or : φ ⋎ ψ ∈ t.1.2 → φ ∈ t.1.2 ∧ ψ ∈ t.1.2 := by - contrapose; - suffices (φ ∉ t.1.2 ∨ ψ ∉ t.1.2) → φ ⋎ ψ ∉ t.1.2 by tauto; - rintro (hφ | hψ); - . apply iff_not_mem₂_mem₁.mpr; - exact mdp_mem₁_provable or₁! $ iff_not_mem₂_mem₁.mp hφ; - . apply iff_not_mem₂_mem₁.mpr; - exact mdp_mem₁_provable or₂! $ iff_not_mem₂_mem₁.mp hψ; - -lemma iff_mem₁_or [DecidableEq α] : φ ⋎ ψ ∈ t.1.1 ↔ φ ∈ t.1.1 ∨ ψ ∈ t.1.1 := by +@[grind =>] +lemma iff_mem₁_or [DecidableEq α] : φ ⋎ ψ ∈ t.Γ ↔ φ ∈ t.Γ ∨ ψ ∈ t.Γ := by constructor; - . apply of_mem₁_or; . intro h; - cases h with - | inl h => exact mdp_mem₁_provable or₁! h; - | inr h => exact mdp_mem₁_provable or₂! h; + by_contra! hC; + apply t.consistent (Γ := {φ ⋎ ψ}) (Δ := {φ, ψ}) (by simp_all); + . grind; + . rw [Finset.conj_singleton]; + apply ruleD <;> apply mem_fdisj (by simp); + . rintro (h | h) <;> apply imp_closed₁ (by simp) h; -lemma iff_mem₂_or [DecidableEq α] : φ ⋎ ψ ∈ t.1.2 ↔ φ ∈ t.1.2 ∧ ψ ∈ t.1.2 := by - constructor; - . apply of_mem₂_or; - . contrapose; - push_neg; - intro hφψ hφ; - rcases iff_mem₁_or.mp $ iff_not_mem₂_mem₁.mp hφψ with (hφ | hψ); - . have := iff_not_mem₂_mem₁.mpr hφ; contradiction; - . exact iff_not_mem₂_mem₁.mpr hψ; +@[grind =>] +lemma iff_mem₂_or [DecidableEq α] : φ ⋎ ψ ∈ t.Δ ↔ φ ∈ t.Δ ∧ ψ ∈ t.Δ := by grind; lemma iff_mem₂_disj [DecidableEq α] {Γ : List (Formula α)} : ⋁Γ ∈ t.1.2 ↔ ∀ φ ∈ Γ, φ ∈ t.1.2 := by induction Γ using List.induction_with_singleton with @@ -555,87 +502,41 @@ lemma iff_mem₂_disj [DecidableEq α] {Γ : List (Formula α)} : ⋁Γ ∈ t.1. | _ => simp; lemma iff_mem₂_fdisj [DecidableEq α] {Γ : Finset (Formula α)} : Γ.disj ∈ t.1.2 ↔ ↑Γ ⊆ t.1.2 := by - apply Iff.trans $ show Γ.disj ∈ t.1.2 ↔ ⋁Γ.toList ∈ t.1.2 by constructor <;> apply mdp_mem₂_provable $ by simp; apply Iff.trans iff_mem₂_disj; - simp_all only [Finset.mem_toList]; - rfl; + grind [Finset.mem_toList] -lemma of_mem₁_imp [DecidableEq α] : φ 🡒 ψ ∈ t.1.1 → (φ ∈ t.1.2 ∨ ψ ∈ t.1.1) := by - intro h; +@[grind =>] +lemma of_mem₁_imp [DecidableEq α] [HasAxiomRfl 𝓢] (h : φ 🡒 ψ ∈ t.Γ) (hp : φ ∈ t.Γ) : ψ ∈ t.Γ := by by_contra hC; - push_neg at hC; - exact hC.2 $ mdp_mem₁ h $ iff_not_mem₂_mem₁.mp hC.1 + apply t.consistent (Γ := {φ, φ 🡒 ψ}) (Δ := {ψ}); + . grind; + . grind; + . rw [Finset.disj_singleton]; + apply ruleI (ψ := φ ⋏ (φ 🡒 ψ)); + . apply ruleC <;> exact mem_fconj (by simp); + . simp; -lemma of_mem₁_imp' [DecidableEq α] : φ 🡒 ψ ∈ t.1.1 → (φ ∈ t.1.1 → ψ ∈ t.1.1) := by - intro h h₁; - apply or_iff_not_imp_left.mp $ of_mem₁_imp h; - apply iff_not_mem₂_mem₁.mpr h₁; +lemma of_mem₁_imp' [DecidableEq α] [HasAxiomRfl 𝓢] : φ 🡒 ψ ∈ t.1.1 → (φ ∈ t.1.2 ∨ ψ ∈ t.1.1) := by grind [of_mem₁_imp]; -lemma of_mem₁_neg [DecidableEq α] (h : ∼φ ∈ t.1.1) : φ ∈ t.1.2 := by - rcases of_mem₁_imp h with (hC | hC); - . assumption; - . exfalso; - exact SaturatedConsistentTableau.not_mem₁_falsum hC; -lemma of_mem₁_neg' [DecidableEq α] (h : ∼φ ∈ t.1.1) : φ ∉ t.1.1 := by - apply iff_not_mem₁_mem₂.mpr; - apply of_mem₁_neg h; +@[grind =>] +lemma of_mem₁_neg [DecidableEq α] [HasAxiomRfl 𝓢] (h : ∼φ ∈ t.1.1) : φ ∉ t.1.1 := by grind [of_mem₁_imp]; -private lemma of_mem₂_imp [DecidableEq α] [Encodable α] [Entailment.Cl 𝓢] : φ 🡒 ψ ∈ t.1.2 → (φ ∈ t.1.1 ∧ ψ ∈ t.1.2) := by - intro h; - by_contra hC; - replace hC := not_and_or.mp hC; - rcases hC with (hφ | hψ); - . have : φ ⋎ (φ 🡒 ψ) ∈ t.1.1 := iff_provable_mem₁.mp (A!_replace_right lem! CNC!) t; - rcases iff_mem₁_or.mp this with (_ | _); - . contradiction; - . have := iff_not_mem₁_mem₂.mpr h; - contradiction; - . have : ψ 🡒 (φ 🡒 ψ) ∈ t.1.1 := iff_provable_mem₁.mp implyK! t; - have : φ 🡒 ψ ∉ t.1.2 := iff_not_mem₂_mem₁.mpr $ mdp_mem₁ this (iff_not_mem₂_mem₁.mp hψ); - contradiction; +lemma of_mem₁_neg' [DecidableEq α] [HasAxiomRfl 𝓢] (h : ∼φ ∈ t.1.1) : φ ∈ t.1.2 := by grind; -lemma iff_mem₁_imp [DecidableEq α] [Encodable α] [Entailment.Cl 𝓢] : φ 🡒 ψ ∈ t.1.1 ↔ (φ ∈ t.1.2 ∨ ψ ∈ t.1.1) := by - constructor; - . apply of_mem₁_imp; - . contrapose; - push_neg; - intro hφψ; - rcases of_mem₂_imp $ iff_not_mem₁_mem₂.mp hφψ with ⟨hφ, hψ⟩; - constructor; - . exact iff_not_mem₂_mem₁.mpr hφ; - . exact iff_not_mem₁_mem₂.mpr hψ; -lemma iff_mem₂_imp [DecidableEq α] [Encodable α] [Entailment.Cl 𝓢] : φ 🡒 ψ ∈ t.1.2 ↔ (φ ∈ t.1.1 ∧ ψ ∈ t.1.2) := by - constructor; - . apply of_mem₂_imp; - . contrapose; - push_neg; - intro hφψ hφ; - rcases of_mem₁_imp $ iff_not_mem₂_mem₁.mp hφψ with (hφ | hψ); - . have := iff_not_mem₁_mem₂.mpr hφ; contradiction; - . exact iff_not_mem₂_mem₁.mpr hψ; - -lemma not_mem₁_neg_of_mem₁ [DecidableEq α] : φ ∈ t.1.1 → ∼φ ∉ t.1.1 := by - intro hp; - by_contra hnp; - have := iff_mem₁_and.mpr ⟨hp, hnp⟩; - have : ⊥ ∈ t.1.1 := mdp_mem₁_provable CKNO! this; - have : ⊥ ∉ t.1.1 := not_mem₁_falsum - contradiction; - -lemma mem₂_neg_of_mem₁ [DecidableEq α] : φ ∈ t.1.1 → ∼φ ∈ t.1.2 := by +private lemma of_mem₂_imp [DecidableEq α] [Encodable α] [HasAxiomRfl 𝓢] [Entailment.Cl 𝓢] : φ 🡒 ψ ∈ t.1.2 → (φ ∈ t.1.1 ∧ ψ ∈ t.1.2) := by intro h; - exact iff_not_mem₁_mem₂ (φ := ∼φ) (t := t) |>.mp $ not_mem₁_neg_of_mem₁ h; + set_option push_neg.use_distrib true in by_contra! hC; + rcases hC with (hφ | hψ); + . rcases iff_mem₁_or.mp (mem₁_of_provable t (show 𝓢 ⊢ φ ⋎ (φ 🡒 ψ) by sorry)) with (_ | _) <;> grind; + . exact (iff_mem₁_notMem₂.mp $ of_mem₁_imp (mem₁_of_provable t (by sorry)) $ iff_mem₁_notMem₂.mpr hψ) h; -lemma mdp₁_mem [DecidableEq α] (hp : φ ∈ t.1.1) (h : φ 🡒 ψ ∈ t.1.1) : ψ ∈ t.1.1 := by - apply iff_not_mem₂_mem₁.mp; - by_contra hC; - apply t.consistent (Γ := {φ, φ 🡒 ψ}) (Δ := {ψ}) ?_ (by simpa); - . apply CFConj_CDisj!_of_innerMDP (φ := φ) (ψ := ψ) <;> simp; - . simp only [Finset.coe_insert, Finset.coe_singleton]; - apply Set.doubleton_subset.mpr; - constructor <;> assumption; +lemma iff_mem₁_imp [DecidableEq α] [Encodable α] [HasAxiomRfl 𝓢] [Entailment.Cl 𝓢] : φ 🡒 ψ ∈ t.1.1 ↔ (φ ∈ t.1.2 ∨ ψ ∈ t.1.1) := by + grind only [of_mem₁_imp, of_mem₂_imp, iff_mem₂_notMem₁, iff_mem₁_notMem₂]; + +lemma iff_mem₂_imp [DecidableEq α] [Encodable α] [HasAxiomRfl 𝓢] [Entailment.Cl 𝓢] : φ 🡒 ψ ∈ t.1.2 ↔ (φ ∈ t.1.1 ∧ ψ ∈ t.1.2) := by + grind only [of_mem₁_imp, of_mem₂_imp, iff_mem₂_notMem₁, iff_mem₁_notMem₂]; end Saturated diff --git a/Foundation/Propositional/Entailment/Corsi/VF.lean b/Foundation/Propositional/Entailment/Corsi/VF.lean index dc3577085..28037978b 100644 --- a/Foundation/Propositional/Entailment/Corsi/VF.lean +++ b/Foundation/Propositional/Entailment/Corsi/VF.lean @@ -124,7 +124,6 @@ lemma ruleC_fconj' {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢ simpa; - lemma mem_lconj₂ {Γ : List F} (h : φ ∈ Γ) : 𝓢 ⊢ ⋀Γ 🡒 φ := by induction Γ using List.induction_with_singleton with | hcons ψ Δ he ih => @@ -191,6 +190,10 @@ lemma mem_ldisj₂ {Γ : List F} (h : ψ ∈ Γ) : 𝓢 ⊢ ψ 🡒 Γ.disj₂ : exact orIntroR; | _ => simp_all; +lemma mem_fdisj {Γ : Finset F} (h : ψ ∈ Γ) : 𝓢 ⊢ ψ 🡒 Γ.disj := by + apply mem_ldisj₂; + simpa using h; + lemma mem_fdisj' {Γ : Finset ι} (Φ : ι → F) (hΦ : ∃ i ∈ Γ, Φ i = ψ) : 𝓢 ⊢ ψ 🡒 ⩖ i ∈ Γ, Φ i := by apply mem_ldisj₂; simpa; @@ -212,6 +215,26 @@ lemma ruleD_fdisj' {Γ : Finset ι} (Φ : ι → F) (h : ∀ i ∈ Γ, 𝓢 ⊢ simpa; +lemma CLDisj₂Disj₂_of_provable {Γ : List F} (h : ∀ γ ∈ Γ, 𝓢 ⊢ γ 🡒 δ) : 𝓢 ⊢ Γ.disj₂ 🡒 δ := by + induction Γ using List.induction_with_singleton with + | hnil => simp only [List.disj₂_nil, Entailment.efq!]; + | hsingle φ => apply h; simp; + | hcons ψ Δ he ih => + simp only [List.disj₂_cons_nonempty he]; + simp only [List.mem_cons, forall_eq_or_imp] at h; + apply ruleD; + . apply h.1; + . apply ih h.2; + +lemma CLDisj₂Disj₂_of_subset {Γ Δ : List F} (h : ∀ φ, φ ∈ Γ → φ ∈ Δ) : 𝓢 ⊢ Γ.disj₂ 🡒 Δ.disj₂ := by + apply CLDisj₂Disj₂_of_provable; + intro γ hγ; + apply mem_ldisj₂ $ h _ hγ; + +lemma CFDisjFDisj_of_subset {Γ Δ : Finset F} (h : Γ ⊆ Δ) : 𝓢 ⊢ Γ.disj 🡒 Δ.disj := by + apply CLDisj₂Disj₂_of_subset; + simpa; + variable [Entailment.Disjunctive 𝓢] [Entailment.Consistent 𝓢] diff --git a/Foundation/Propositional/Kripke/AxiomDummett.lean b/Foundation/Propositional/Kripke/AxiomDummett.lean index 4278a2f90..a38b280be 100644 --- a/Foundation/Propositional/Kripke/AxiomDummett.lean +++ b/Foundation/Propositional/Kripke/AxiomDummett.lean @@ -102,5 +102,7 @@ end canonicality end Kripke + + end LO.Propositional end diff --git a/Foundation/Propositional/Kripke3/Axiom/Dummett.lean b/Foundation/Propositional/Kripke3/Axiom/Dummett.lean new file mode 100644 index 000000000..9b8c034c7 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Axiom/Dummett.lean @@ -0,0 +1,96 @@ +module + +public import Foundation.Propositional.Kripke3.Basic +public import Foundation.Vorspiel.Rel.Connected +public import Foundation.Propositional.Kripke3.Logic.Int.Completeness + +@[expose] public section + +namespace LO.Propositional + +variable {κ α : Type*} [Nonempty κ] + +namespace KripkeModel + +variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α} + +lemma validates_axiomDummett [IsPiecewiseStronglyConnected M.rel] : M ⊧ (Axioms.Dummett φ ψ) := by + have : PiecewiseStronglyConnected M.rel := IsPiecewiseStronglyConnected.ps_connected; + contrapose! this; + obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this; + replace h := forces_or.not.mp h; + push_neg at h; + rcases h with ⟨h₁, h₂⟩; + + replace h₁ := forces_imp.not.mp h₁; + push_neg at h₁; + obtain ⟨y, Rxy, hyφ, hyψ⟩ := h₁; + + replace h₂ := forces_imp.not.mp h₂; + push_neg at h₂; + obtain ⟨z, Rxz, hzψ, hzφ⟩ := h₂; + + dsimp [PiecewiseStronglyConnected] + push_neg; + use x, y, z; + refine ⟨Rxy, Rxz, ?_⟩; + . set_option push_neg.use_distrib true in by_contra! hC; + rcases hC with (Ryz | Rzy); + . apply hzφ $ M.formula_persistency hyφ Ryz; + . apply hyψ $ M.formula_persistency hzψ Rzy; + +variable [DecidableEq α] +lemma isPiecewiseStronglyConvergent_of_validates_axiomDummett + (a b : α) (hab : a ≠ b := by trivial) + [Std.Refl K] + (h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.Dummett #a #b)) + : IsPiecewiseStronglyConvergent K := by + constructor; + rintro x y z Rxy Rxz; + have := (h $ (λ {p v} => if p = a then K y v else if p = b then K z v else True)) x; + rw [forces_or] at this; + rcases this with (hi | hi); + . simp only [forces_imp, forces_atom, ↓reduceIte, hab.symm] at hi; + use y; + constructor; + . apply Std.Refl.refl; + . apply hi; + . assumption; + . apply Std.Refl.refl; + . use z; + simp only [forces_imp, forces_atom, hab.symm, ↓reduceIte] at hi; + constructor; + . apply hi z Rxz; + exact Std.Refl.refl z; + . apply Std.Refl.refl; + +end KripkeModel + + + +section + +variable {S} [Entailment S (Formula ℕ)] +variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] + +open Formula.Kripke +open LO.Entailment + LO.Entailment.FiniteContext +open canonicalKripkeModel +open SaturatedConsistentTableau +open Classical + +instance [Entailment.HasAxiomDummett 𝓢] : IsPiecewiseStronglyConnected (canonicalKripkeModel 𝓢).rel := by + constructor; + rintro x y z Rxy Rxz; + by_contra!; + obtain ⟨φ, hφy, hφz⟩ := Set.not_subset.mp this.1; + obtain ⟨ψ, hψz, hψy⟩ := Set.not_subset.mp this.2; + rcases (show φ 🡒 ψ ∈ x.1.1 ∨ ψ 🡒 φ ∈ x.1.1 by exact iff_mem₁_or.mp $ mem₁_of_provable dummett!) with (hφψx | hψφx); + . exact hψy $ mdp₁_mem hφy (Rxy hφψx); + . exact hφz $ mdp₁_mem hψz (Rxz hψφx); + +end + +end LO.Propositional +end diff --git a/Foundation/Propositional/Kripke3/Axiom/KreiselPutnam.lean b/Foundation/Propositional/Kripke3/Axiom/KreiselPutnam.lean new file mode 100644 index 000000000..b64c82628 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Axiom/KreiselPutnam.lean @@ -0,0 +1,237 @@ +module + +public import Foundation.Propositional.Kripke3.Basic +public import Foundation.Vorspiel.Rel.Euclidean +public import Foundation.Propositional.Entailment.KreiselPutnam +public import Foundation.Propositional.Kripke3.Logic.Int.Completeness + +@[expose] public section + +namespace LO.Propositional + +variable {κ α : Type*} [Nonempty κ] + +namespace KripkeModel + +class KreiselPutnam (M : KripkeModel κ α) extends M.Intuitionistic where + kreisel_putnam : + ∀ x y z : M.world, + (x ≺ y ∧ x ≺ z ∧ ¬y ≺ z ∧ ¬z ≺ y) → + (∃ u, x ≺ u ∧ u ≺ y ∧ u ≺ z ∧ (∀ v, u ≺ v → ∃ w, v ≺ w ∧ (y ≺ w ∨ z ≺ w))) + +export KreiselPutnam (kreisel_putnam) + +variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α} + +lemma validates_axiomKreiselPutnam_of_satisfiesKreiselPutnamCondition + [M.KreiselPutnam] : M ⊧ (Axioms.KreiselPutnam φ ψ χ) := by + intro x y Rxy h₁; + apply forces_or.mpr; + by_contra! hC; + obtain ⟨h₂, h₃⟩ := hC; + + replace h₂ := forces_imp.not.mp h₂; + push_neg at h₂; + obtain ⟨z₁, Ryz₁, ⟨hz₁φ, hz₁ψ⟩⟩ := h₂; + + replace h₃ := forces_imp.not.mp h₃; + push_neg at h₃; + obtain ⟨z₂, Ryz₂, ⟨hz₂φ, hz₂ψ⟩⟩ := h₃; + + obtain ⟨u, Ryu, ⟨Ruz₁, Ruz₂, h⟩⟩ := M.kreisel_putnam y z₁ z₂ ⟨ + Ryz₁, Ryz₂, + by + rcases forces_or.mp $ h₁ _ Ryz₁ hz₁φ with (h | h); + . exfalso; exact hz₁ψ h; + . by_contra hC; exact hz₂ψ $ M.formula_persistency h hC; + , + by + rcases forces_or.mp $ h₁ _ Ryz₂ hz₂φ with (h | h); + . by_contra hC; exact hz₁ψ $ M.formula_persistency h hC; + . exfalso; exact hz₂ψ h; + ⟩; + have : ¬u ⊩ (∼φ) := by + by_contra hC; + rcases forces_or.mp $ h₁ _ Ryu hC with (h | h); + . apply hz₁ψ $ M.formula_persistency h Ruz₁; + . apply hz₂ψ $ M.formula_persistency h Ruz₂; + replace this := forces_neg.not.mp this; + push_neg at this; + obtain ⟨v, Ruv, hv⟩ := this; + + rcases h v Ruv with ⟨w, Rvw, (Rz₁w | Rz₂w)⟩ + . apply (forces_neg.mp $ M.formula_persistency hz₁φ Rz₁w) w $ Std.Refl.refl w; + exact M.formula_persistency hv Rvw; + . apply (forces_neg.mp $ M.formula_persistency hz₂φ Rz₂w) w $ Std.Refl.refl w; + exact M.formula_persistency hv Rvw; + +end KripkeModel + +section + +variable {S} [Entailment S (Formula ℕ)] +variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] + +open Formula.Kripke +open LO.Entailment + LO.Entailment.FiniteContext +open canonicalKripkeModel +open SaturatedConsistentTableau +open Classical + +instance [Entailment.HasAxiomKreiselPutnam 𝓢] : (canonicalKripkeModel 𝓢).KreiselPutnam := by + constructor; + rintro x y z ⟨Rxy, Rxz, nRyz, nRzy⟩; + let ΓNyz := { φ | ∼φ ∈ (y.1.1 ∩ z.1.1)}.image (∼·); + obtain ⟨u, hu₁, hu₂⟩ := lindenbaum (𝓢 := 𝓢) (t₀ := ⟨x.1.1 ∪ ΓNyz, y.1.2 ∪ z.1.2⟩) $ by + show Tableau.Consistent 𝓢 (x.1.1 ∪ ΓNyz, y.1.2 ∪ z.1.2); + rintro Γ Δ hΓ hΔ; + by_contra hC; + let Γx := { φ ∈ Γ | φ ∈ x.1.1}; + let Γ₁ := { φ ∈ Γ | φ ∈ ΓNyz }; + let Γ₂ := Γ₁.preimage (∼·) $ by simp [Set.InjOn]; + let Δy := { φ ∈ Δ | φ ∈ y.1.2}; + let Δz := { φ ∈ Δ | φ ∈ z.1.2}; + replace hC : 𝓢 ⊢ (Γx ∪ Γ₁).conj 🡒 (Δy ∪ Δz).disj := C!_replace ?_ ?_ hC; + . replace hC : 𝓢 ⊢ Γx.conj ⋏ Γ₁.conj 🡒 Δy.disj ⋎ Δz.disj := C!_replace CKFconjFconjUnion! CFdisjUnionAFdisj hC; + generalize eδy : Δy.disj = δy at hC; + generalize eδz : Δz.disj = δz at hC; + replace hC : ↑Γx *⊢[𝓢] ∼(Γ₂.disj) 🡒 δy ⋎ δz := C!_trans ?_ $ FConj_DT.mp $ CK!_iff_CC!.mp hC; + . generalize eγ : Γ₂.disj = γ at hC; + replace hC : ↑Γx *⊢[𝓢] (∼γ 🡒 δy) ⋎ (∼γ 🡒 δz) := kreiselputnam'! hC; + replace hC : ∼γ 🡒 δy ∈ x.1.1 ∨ ∼γ 🡒 δz ∈ x.1.1 := iff_mem₁_or.mp $ iff_provable_include₁.mp hC x ?_; + . rcases hC with h | h; + . apply iff_not_mem₂_mem₁.mpr $ of_mem₁_imp' (Rxy h) ?_ + . subst eδy; + apply iff_mem₂_fdisj.mpr; + intro φ hφ; + simp only [Finset.coe_filter, Set.mem_setOf_eq, Δy] at hφ; + exact hφ.2; + . subst eγ; + apply mdp_mem₁_provable (φ := Γ₁.conj) ?_ ?_; + . apply C!_trans ?_ CFconjNNFconj!; + apply CFConj_FConj!_of_subset; + intro φ; + simp only [Finset.mem_image, Finset.mem_preimage, Finset.mem_filter, forall_exists_index, and_imp, Γ₁, Γ₂]; + rintro _ _ _ rfl; + tauto; + . apply iff_mem₁_fconj.mpr; + intro φ; + simp only [Set.mem_inter_iff, Set.mem_image, Set.mem_setOf_eq, Finset.coe_filter, and_imp, forall_exists_index, Γ₁, ΓNyz]; + rintro _ _ _ _ rfl; + assumption; + . apply iff_not_mem₂_mem₁.mpr $ of_mem₁_imp' (Rxz h) ?_ + . subst eδz; + apply iff_mem₂_fdisj.mpr; + intro φ hφ; + simp only [Finset.coe_filter, Set.mem_setOf_eq, Δz] at hφ; + exact hφ.2; + . subst eγ; + apply mdp_mem₁_provable (φ := Γ₁.conj) ?_ ?_; + . apply C!_trans ?_ CFconjNNFconj!; + apply CFConj_FConj!_of_subset; + intro φ; + simp only [Finset.mem_image, Finset.mem_preimage, Finset.mem_filter, forall_exists_index, and_imp, Γ₁, Γ₂]; + rintro _ _ _ rfl; + tauto; + . apply iff_mem₁_fconj.mpr; + intro φ; + simp only [Set.mem_inter_iff, Set.mem_image, Set.mem_setOf_eq, Finset.coe_filter, and_imp, forall_exists_index, Γ₁, ΓNyz]; + rintro _ _ _ _ rfl; + assumption; + . intro φ hφ; + simp only [Finset.coe_filter, Set.mem_setOf_eq, Γx] at hφ; + exact hφ.2; + . apply Context.of!; + apply right_Fconj!_intro; + simp only [Set.mem_inter_iff, Set.mem_image, Set.mem_setOf_eq, Finset.mem_filter, and_imp, forall_exists_index, Γ₁, Γ₂, ΓNyz]; + rintro _ hψ ψ hψ₁ hψ₂ rfl; + apply C!_trans CNFdisjFconj!; + apply left_Fconj!_intro; + suffices ∼ψ ∈ Γ ∧ ∼ψ ∈ y.1.1 ∧ ∼ψ ∈ z.1.1 by simpa [Γ₁, Γ₂] using this; + tauto; + . apply CFConj_FConj!_of_subset; + intro φ hφ; + simp only [Finset.mem_union, Finset.mem_filter, Γx, Γ₁]; + rcases hΓ hφ with h | h <;> tauto; + . apply CFDisjFDisj_of_subset; + intro φ hφ; + simp only [Finset.mem_union, Finset.mem_filter, Δy, Δz]; + rcases hΔ hφ with h | h <;> tauto; + replace hu₁ := Set.union_subset_iff.mp hu₁; + replace hu₂ := Set.union_subset_iff.mp hu₂; + use u; + refine ⟨?_, ?_, ?_, ?_⟩; + . exact hu₁.1; + . apply canonicalKripkeModel.def_rel₂.mpr; exact hu₂ |>.1; + . apply canonicalKripkeModel.def_rel₂.mpr; exact hu₂ |>.2; + . intro v Ruv; + by_contra! hC; + obtain ⟨γ₁, hγ₁₁, hγ₁₂⟩ : ∃ γ₁ ∈ v.1.1, ∼γ₁ ∈ y.1.1 := by + have : Tableau.Inconsistent 𝓢 ⟨y.1.1 ∪ v.1.1, ∅⟩ := by + by_contra hconsis; + obtain ⟨t, ht⟩ := lindenbaum hconsis; + apply hC t ?_ |>.1; + . exact Set.union_subset_iff.mp (Tableau.subset_def.mp ht |>.1) |>.1; + . exact Set.union_subset_iff.mp (Tableau.subset_def.mp ht |>.1) |>.2; + dsimp [Tableau.Inconsistent, Tableau.Consistent] at this; + push_neg at this; + obtain ⟨Γ, Δ, hΓ, hΔ, hΓΔ⟩ := this; + simp only [Set.subset_empty_iff, Finset.coe_eq_empty] at hΔ; + subst hΔ; + simp only [Finset.disj_empty] at hΓΔ; + use ({ φ ∈ Γ | φ ∈ v.1.1}).conj; + constructor; + . apply iff_mem₁_fconj.mpr; + intro; + simp; + . apply iff_provable_include₁_finset (Γ := {x ∈ Γ | x ∈ y.1.1}) |>.mp ?_ y ?_; + . apply N!_iff_CO!.mpr; + apply FConj_DT'.mpr; + apply Context.weakening! ?_ (FConj_DT.mp hΓΔ); + intro φ hφ; + simp only [Finset.coe_union, Finset.coe_filter, Set.mem_union, Set.mem_setOf_eq]; + rcases hΓ hφ with _ | _ <;> tauto; + . intro; + simp; + obtain ⟨γ₂, hγ₂₁, hγ₂₂⟩ : ∃ γ₂ ∈ v.1.1, ∼γ₂ ∈ z.1.1 := by + have : Tableau.Inconsistent 𝓢 ⟨z.1.1 ∪ v.1.1, ∅⟩ := by + by_contra hconsis; + obtain ⟨t, ht⟩ := lindenbaum hconsis; + apply hC t ?_ |>.2; + . exact Set.union_subset_iff.mp (Tableau.subset_def.mp ht |>.1) |>.1; + . exact Set.union_subset_iff.mp (Tableau.subset_def.mp ht |>.1) |>.2; + dsimp [Tableau.Inconsistent, Tableau.Consistent] at this; + push_neg at this; + obtain ⟨Γ, Δ, hΓ, hΔ, hΓΔ⟩ := this; + simp only [Set.subset_empty_iff, Finset.coe_eq_empty] at hΔ; + subst hΔ; + simp only [Finset.disj_empty] at hΓΔ; + use ({ φ ∈ Γ | φ ∈ v.1.1}).conj; + constructor; + . apply iff_mem₁_fconj.mpr; + intro; + simp; + . apply iff_provable_include₁_finset (Γ := {x ∈ Γ | x ∈ z.1.1}) |>.mp ?_ z ?_; + . apply N!_iff_CO!.mpr; + apply FConj_DT'.mpr; + apply Context.weakening! ?_ (FConj_DT.mp hΓΔ); + intro φ hφ; + simp only [Finset.coe_union, Finset.coe_filter, Set.mem_union, Set.mem_setOf_eq]; + rcases hΓ hφ with _ | _ <;> tauto; + . intro; + simp; + have : ∼(γ₁ ⋏ γ₂) ∈ v.1.1 := Ruv $ hu₁.2 $ by + simp only [Set.mem_inter_iff, Set.mem_image, Set.mem_setOf_eq, Formula.neg_inj, exists_eq_right, ΓNyz]; + constructor <;> + . apply mdp_mem₁_provable CANNNK!; + apply iff_mem₁_or.mpr; + tauto; + apply of_mem₁_neg' this; + apply iff_mem₁_and.mpr; + tauto; + +end + +end LO.Propositional +end diff --git a/Foundation/Propositional/Kripke3/Axiom/LEM.lean b/Foundation/Propositional/Kripke3/Axiom/LEM.lean new file mode 100644 index 000000000..ab1ff8676 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Axiom/LEM.lean @@ -0,0 +1,84 @@ +module + +public import Foundation.Propositional.Kripke3.Basic +public import Foundation.Vorspiel.Rel.Euclidean +public import Foundation.Propositional.Kripke3.Logic.Int.Completeness + +@[expose] public section + +namespace LO.Propositional + +variable {κ α : Type*} [Nonempty κ] + +namespace KripkeModel + +variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α} + +lemma validates_axiomLEM_of_isSymmetric [Std.Symm M.rel] : M ⊧ (Axioms.LEM φ) := by + have : Symmetric M.rel := Std.Symm.symm; + contrapose! this; + obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this; + + replace h := forces_or.not.mp h; + push_neg at h; + rcases h with ⟨h₁, h₂⟩; + + replace h₂ := forces_neg.not.mp h₂; + push_neg at h₂; + obtain ⟨y, Rxy, hy⟩ := h₂; + + dsimp [Symmetric] + push_neg; + use x, y; + constructor; + . assumption; + . contrapose! h₁; + apply M.formula_persistency hy h₁; + +lemma validates_axiomLEM_of_isRightEuclidean [IsRightEuclidean M.rel] : M ⊧ (Axioms.LEM φ) := validates_axiomLEM_of_isSymmetric + +lemma isRightEuclidean_of_validates_axiomLEM [Std.Refl K] [IsTrans _ K] + (h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.LEM #a)) + : IsRightEuclidean K := by + constructor; + rintro x y z Rxy Rxz; + have := h (λ {p v} => K y v) x; + rcases this with (hi | hi); + . apply IsTrans.trans y x z hi Rxz; + . exfalso; + apply forces_neg.mp hi y Rxy; + apply Std.Refl.refl; + +end KripkeModel + +section + +variable {S} [Entailment S (Formula ℕ)] +variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] + +open Formula.Kripke +open LO.Entailment + LO.Entailment.FiniteContext +open canonicalKripkeModel +open SaturatedConsistentTableau +open Classical + +instance [Entailment.HasAxiomLEM 𝓢] : IsRightEuclidean (canonicalKripkeModel 𝓢).rel := by + constructor; + intro x y z Rxy; + contrapose!; + rintro nRyz; + obtain ⟨φ, hφy, hφz⟩ := Set.not_subset.mp nRyz; + apply Set.not_subset.mpr; + use φ; + constructor; + . rcases (show φ ∈ x.1.1 ∨ ∼φ ∈ x.1.1 by exact iff_mem₁_or.mp $ mem₁_of_provable (by simp)) with h | h; + . assumption; + . have : φ ∉ y.1.1 := of_mem₁_neg' $ Rxy h; + contradiction; + . assumption; + +end + +end LO.Propositional +end diff --git a/Foundation/Propositional/Kripke3/Axiom/Tra.lean b/Foundation/Propositional/Kripke3/Axiom/Tra.lean new file mode 100644 index 000000000..4741f7170 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Axiom/Tra.lean @@ -0,0 +1,30 @@ +module + +public import Foundation.Propositional.Kripke3.Basic + +@[expose] public section + +namespace LO.Propositional + +variable {κ α : Type*} [Nonempty κ] + +namespace KripkeModel + +variable {M : KripkeModel κ α} [IsTrans _ M.rel] + {φ ψ χ : Formula α} + +@[simp, grind .] +lemma validates_axiomTra₁ : M ⊧ Axioms.Tra1 φ ψ χ := + fun _ y _ hyφψ z Ryz _ w Rzw hzφ => + hyφψ w (IsTrans.trans y z w Ryz Rzw) hzφ + +@[simp, grind .] +lemma validates_axiomTra₂ : M ⊧ Axioms.Tra2 φ ψ χ := + fun _ y _ hyφψ z Ryz hzψχ w Rzw hwφ => + hzψχ w Rzw $ hyφψ w (IsTrans.trans y z w Ryz Rzw) hwφ + +end KripkeModel + +end LO.Propositional + +end diff --git a/Foundation/Propositional/Kripke3/Axiom/WLEM.lean b/Foundation/Propositional/Kripke3/Axiom/WLEM.lean new file mode 100644 index 000000000..3138eec30 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Axiom/WLEM.lean @@ -0,0 +1,115 @@ +module + +public import Foundation.Propositional.Kripke3.Basic +public import Foundation.Propositional.Kripke3.Logic.Int.Completeness +public import Foundation.Vorspiel.Rel.Convergent + +@[expose] public section + +namespace LO.Propositional + +variable {κ α : Type*} [Nonempty κ] + +namespace KripkeModel + +variable {M : KripkeModel κ α} [M.Intuitionistic] {φ ψ χ : Formula α} + +lemma validates_axiomWLEM [IsPiecewiseStronglyConvergent M.rel] : M ⊧ (Axioms.WLEM φ) := by + have : PiecewiseStronglyConvergent M.rel := IsPiecewiseStronglyConvergent.ps_convergent; + contrapose! this; + obtain ⟨x, h⟩ := exists_world_notForces_of_notValidates this; + + replace h := forces_or.not.mp h; + push_neg at h; + rcases h with ⟨h₁, h₂⟩; + + replace h₁ := forces_neg.not.mp h₁; + push_neg at h₁; + obtain ⟨y, Rxy, hy⟩ := h₁; + + replace h₂ := forces_neg.not.mp h₂; + push_neg at h₂; + obtain ⟨z, Rxz, hz⟩ := h₂; + + dsimp [PiecewiseStronglyConvergent] + push_neg; + use x, y, z; + refine ⟨Rxy, Rxz, ?_⟩; + . intro u Ryu; + by_contra Rzu; + exact hz u Rzu $ M.formula_persistency hy Ryu; + +lemma isPiecewiseStronglyConvergent_of_validates_axiomWLEM [Std.Refl K] + (h : ∀ V, letI M : KripkeModel κ α := ⟨K, V⟩; M ⊧ (Axioms.WLEM #a)) + : IsPiecewiseStronglyConvergent K := by + constructor; + rintro x y z Rxy Rxz; + have := (h $ (λ {p v} => K y v)) x; + rw [forces_or] at this; + rcases this with (hi | hi); + . exfalso; + simp only [forces_neg, ForcingRelation.NotForces, forces_atom] at hi; + apply hi y Rxy $ Std.Refl.refl y; + . simp only [forces_neg, ForcingRelation.NotForces, forces_atom] at hi; + push_neg at hi; + obtain ⟨w, Rzw, Ryw⟩ := hi z Rxz; + use w; + +end KripkeModel + + +section + +variable {S} [Entailment S (Formula ℕ)] +variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] + +open Formula.Kripke +open LO.Entailment + LO.Entailment.FiniteContext +open canonicalKripkeModel +open SaturatedConsistentTableau +open Classical + +instance [Entailment.HasAxiomWLEM 𝓢] : IsPiecewiseStronglyConvergent (canonicalKripkeModel 𝓢).rel := by + constructor; + rintro x y z Rxy Rxz; + obtain ⟨w, hw⟩ := lindenbaum (𝓢 := 𝓢) $ by + show Tableau.Consistent 𝓢 (y.1.1 ∪ z.1.1, ∅); + rintro Γ Δ hΓ hΔ h; + replace hΓ : (SetLike.coe Γ) ⊆ (↑y.1.1 ∪ ↑z.1.1) := by grind; + replace hΔ : Δ = ∅ := by simpa using hΔ; + subst hΔ; + + let Θx := { φ ∈ Γ | (φ ∈ y.1.1 ∧ φ ∈ x.1.1) ∨ (φ ∈ z.1.1 ∧ φ ∈ x.1.1) }; + let Θy := { φ ∈ Γ | φ ∈ y.1.1 ∧ φ ∉ x.1.1 }; + let Θz := { φ ∈ Γ | φ ∈ z.1.1 ∧ φ ∉ x.1.1 }; + + simp only [Finset.disj_empty] at h; + replace : [Θx.conj] ⊢[𝓢] ∼∼Θz.conj 🡒 ∼Θy.conj := contra! $ FiniteContext.deductInv'! $ by + apply FConj_DT.mpr; + apply FConj_DT'.mpr; + apply FConj_DT'.mpr; + apply mdp! $ Context.of! h; + apply FConj_DT.mp; + apply CFConj_FConj!_of_subset; + intro φ hφ; + rcases hΓ hφ with h | h <;> + . dsimp [Θx, Θy, Θz]; + grind; + + have h_Θx_x : Θx.conj ∈ x.1.1 := iff_mem₁_fconj.mpr $ by intro; grind only [Finset.mem_coe, Finset.mem_filter]; + have h_Θz_z : Θz.conj ∈ z.1.1 := iff_mem₁_fconj.mpr $ by intro; grind only [Finset.mem_coe, Finset.mem_filter]; + have nh_nΘz_z : ∼Θz.conj ∉ z.1.1 := not_mem₁_neg_of_mem₁ h_Θz_z; + have nh_nΘz_x : ∼Θz.conj ∉ x.1.1 := Set.notMem_subset Rxz nh_nΘz_z; + have h_nnΘz_x : ∼∼Θz.conj ∈ x.1.1 := or_iff_not_imp_left.mp (iff_mem₁_or.mp $ mem₁_of_provable $ wlem!) nh_nΘz_x; + have h_nΘy_y : ∼Θy.conj ∈ y.1.1 := Rxy $ mdp₁_mem h_nnΘz_x $ mdp_mem₁_provable this h_Θx_x; + have nh_nΘy_y : ∼Θy.conj ∉ y.1.1 := not_mem₁_neg_of_mem₁ $ iff_mem₁_fconj.mpr $ by intro; grind only [Finset.mem_coe, Finset.mem_filter]; + contradiction; + use w; + simpa using hw; + +end + +end LO.Propositional + +end diff --git a/Foundation/Propositional/Kripke3/Basic.lean b/Foundation/Propositional/Kripke3/Basic.lean new file mode 100644 index 000000000..a549c7721 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Basic.lean @@ -0,0 +1,237 @@ +module + +public import Foundation.Propositional.Logic.Basic +public import Foundation.Propositional.Entailment.Corsi.Basic +public import Foundation.Vorspiel.Rel.Basic +public import Foundation.Logic.ForcingRelation + +@[expose] public section + +variable {κ α : Type*} [Nonempty κ] + +namespace LO.Propositional + +open Entailment + +structure KripkeModel (κ : Type*) [Nonempty κ] (α : Type*) where + frame : Rel κ κ + val : α → κ → Prop + +namespace KripkeModel + +abbrev world (_ : KripkeModel κ α) := κ + +variable {M : KripkeModel κ α} {x y z : M.world} {a : α} {φ ψ χ : Formula α} {n m : ℕ} + +abbrev rel : Rel M.world M.world := M.frame +infix:45 " ≺ " => rel + +abbrev relInv (x y : M.world) := M.frame y x +infix:45 " ≻ " => relInv + +abbrev relItr (n : ℕ) : Rel M.world M.world := M.frame.Iterate n +notation x:45 " ≺^[" n:0 "] " y:46 => relItr n x y + +-- instance : CoeSort (KripkeModel κ α) (Type*) := ⟨λ M => M.world⟩ +instance : CoeFun (KripkeModel κ α) (λ M => α → M.world → Prop) := ⟨fun M => M.val⟩ + +section Forces + + +@[grind] +def Forces (M : KripkeModel κ α) (x : M.world) : Formula α → Prop + | .atom a => M a x + | ⊥ => False + | φ ⋏ ψ => Forces M x φ ∧ Forces M x ψ + | φ ⋎ ψ => Forces M x φ ∨ Forces M x ψ + | φ 🡒 ψ => ∀ y : M.world, x ≺ y → (Forces M y φ → Forces M y ψ) + +instance : ForcingRelation M.world (Formula α) where + Forces := Forces M + +@[grind =] lemma forces_atom : x ⊩ (.atom a) ↔ M a x := by tauto +@[simp, grind .] lemma forces_falsum : x ⊮ ⊥ := by tauto; +@[simp, grind .] lemma forces_verum : x ⊩ ⊤ := by tauto; +@[grind =] lemma forces_and : x ⊩ φ ⋏ ψ ↔ x ⊩ φ ∧ x ⊩ ψ := by rfl; +@[grind =] lemma forces_or : x ⊩ φ ⋎ ψ ↔ x ⊩ φ ∨ x ⊩ ψ := by rfl; +@[grind =] lemma forces_imp : x ⊩ φ 🡒 ψ ↔ ∀ y : M.world, x ≺ y → (y ⊩ φ → y ⊩ ψ) := by rfl; + +@[grind =] +lemma forces_neg : x ⊩ ∼φ ↔ ∀ y, x ≺ y → (y ⊮ φ) := by + simp [Formula.neg_def, forces_imp, ForcingRelation.NotForces]; + +instance : ForcingRelation.BasicSemantics M.world where + verum {_} := forces_verum + falsum {_} := forces_falsum + and {_ _ _} := forces_and + or {_ _ _} := forces_or + + +@[grind =] +lemma forces_lconj {l : List _} : x ⊩ l.conj ↔ ∀ φ ∈ l, x ⊩ φ := by + induction l <;> + grind [List.conj_cons, List.conj_nil]; + +@[grind =] +lemma forces_lconj₂ {l : List _} : x ⊩ ⋀l ↔ ∀ φ ∈ l, x ⊩ φ := by + induction l using List.induction_with_singleton <;> + grind [List.conj₂_nil, List.conj₂_cons_nonempty, List.conj₂_singleton] + +@[grind =] +lemma forces_lconj' {l : List β} {ι : β → Formula α} : x ⊩ l.conj' ι ↔ ∀ i ∈ l, x ⊩ (ι i) := by + grind [List.conj']; + +@[grind =] +lemma forces_fconj {s : Finset _} : x ⊩ s.conj ↔ ∀ φ ∈ s, x ⊩ φ := by + apply Iff.trans forces_lconj₂; + simp; + +@[grind =] +lemma forces_fconj' {s : Finset β} {ι : β → Formula α} : x ⊩ s.conj' ι ↔ ∀ i ∈ s, x ⊩ (ι i) := by + apply Iff.trans forces_lconj'; + simp; + + +@[grind =] +lemma forces_ldisj {l : List _} : x ⊩ l.disj ↔ ∃ φ ∈ l, x ⊩ φ := by + induction l <;> + grind [List.disj_cons, List.disj_nil]; + +@[grind =] +lemma forces_ldisj₂ {l : List _} : x ⊩ ⋁l ↔ ∃ φ ∈ l, x ⊩ φ := by + induction l using List.induction_with_singleton <;> + grind [List.disj₂_nil, List.disj₂_cons_nonempty, List.disj₂_singleton] + +@[grind =] +lemma forces_ldisj' {l : List β} {ι : β → Formula α} : x ⊩ l.disj' ι ↔ ∃ i ∈ l, x ⊩ (ι i) := by + grind [List.disj'] + +@[grind =] +lemma forces_fdisj {s : Finset _} : x ⊩ s.disj ↔ ∃ φ ∈ s, x ⊩ φ := by + apply Iff.trans forces_ldisj₂; + simp; + +@[grind =] +lemma forces_fdisj' {s : Finset β} {ι : β → Formula α} : x ⊩ s.disj' ι ↔ ∃ i ∈ s, x ⊩ (ι i) := by + apply Iff.trans forces_ldisj'; + simp; + +end Forces + + +section Models + +variable {M : KripkeModel κ α} {φ ψ χ : Formula α} + +instance : Semantics (KripkeModel κ α) (Formula α) := ⟨λ M φ => M.world ∀⊩ φ⟩ + +@[grind =] +lemma iff_validates_forall_forces : M ⊧ φ ↔ ∀ x : M.world, x ⊩ φ := by rfl +alias ⟨forallforces_of_validates, validates_of_forall_forces⟩ := iff_validates_forall_forces + +@[grind =] +lemma iff_notValidates_exists_world_notForces : M ⊭ φ ↔ ∃ x : M.world, x ⊮ φ := by + simp [Semantics.Models, Semantics.NotModels]; +alias ⟨exists_world_notForces_of_notValidates, notValidates_of_exists_world_notForces⟩ := iff_notValidates_exists_world_notForces + + +lemma validates_verum : M ⊧ ⊤ := ForcingRelation.AllForces.verum +instance : Semantics.Top (KripkeModel κ α) := ⟨λ _ => validates_verum⟩ + +lemma validates_falsum : M ⊭ ⊥ := by + have : Inhabited M.world := Inhabited.mk $ Nonempty.some inferInstance; + apply ForcingRelation.AllForces.falsum +instance : Semantics.Bot (KripkeModel κ α) := ⟨λ _ => validates_falsum⟩ + +@[grind =] +lemma validates_and : M ⊧ (φ ⋏ ψ) ↔ M ⊧ φ ∧ M ⊧ ψ := ForcingRelation.AllForces.and +instance : Semantics.And (KripkeModel κ α) := ⟨validates_and⟩ + +lemma validates_andElim₁ : M ⊧ Axioms.AndElim₁ φ ψ := by intro x; grind; +lemma validates_andElim₂ : M ⊧ Axioms.AndElim₂ φ ψ := by intro x; grind; +lemma validates_orInst₁ : M ⊧ Axioms.OrInst₁ φ ψ := by intro x; grind; +lemma validates_orInst₂ : M ⊧ Axioms.OrInst₂ φ ψ := by intro x; grind; +lemma validates_efq : M ⊧ Axioms.EFQ φ := by intro x; grind; + +lemma validates_distributeAndOr : M ⊧ Axioms.DistributeAndOr φ ψ χ := by + rintro x y Rxy ⟨hφ, (hψ | hχ)⟩ + . left; constructor <;> assumption; + . right; constructor <;> assumption; + +lemma validates_axiomD : M ⊧ Axioms.D φ ψ χ := by + rintro x y Rxy ⟨h₁, h₂⟩ z Ryz (hφ | hψ); + . apply h₁ <;> assumption; + . apply h₂ <;> assumption; + +lemma validates_axiomI : M ⊧ Axioms.I φ ψ χ := by + rintro x y Rxy ⟨h₁, h₂⟩ z Ryz h₃; + exact h₂ z Ryz $ h₁ z Ryz h₃; + +lemma validates_impId : M ⊧ Axioms.ImpId φ := by rintro x y Rxy hφ; assumption; + +attribute [grind .] + validates_verum + validates_falsum + validates_and + validates_andElim₁ + validates_andElim₂ + validates_orInst₁ + validates_orInst₂ + validates_efq + validates_distributeAndOr + validates_axiomD + validates_axiomI + validates_impId + +@[grind <=] +lemma validates_ruleC (hφ : M ⊧ φ) (hψ : M ⊧ ψ) : M ⊧ φ ⋏ ψ := fun x ↦ ⟨hφ x, hψ x⟩ + +@[grind <=] +lemma validates_afortiori (h : M ⊧ φ) : M ⊧ ψ 🡒 φ := fun _ y _ _ ↦ h y + +end Models + + +section + +class Persistent (M : KripkeModel κ α) : Prop where + atom_persistency : ∀ {x y : M.world} {a : α}, x ⊩ (.atom a) → x ≺ y → y ⊩ (.atom a) +export Persistent (atom_persistency) + +lemma formula_persistency [Persistent M] [IsTrans _ M.rel] {x y : M.world} {φ : Formula α} (hxφ : x ⊩ φ) (Rxy : x ≺ y) : y ⊩ φ := by + induction φ with + | hatom => apply atom_persistency hxφ Rxy; + | himp φ ψ ihφ ihψ => + intro z Ryz hzφ; + apply hxφ z $ IsTrans.trans _ _ _ Rxy Ryz; + apply hzφ; + | _ => grind; + +@[grind .] +lemma validates_implyK [Persistent M] [IsTrans _ M.rel] : M ⊧ φ 🡒 ψ 🡒 φ := by + intro x y Rxy hφ z Ryz hψ; + apply formula_persistency hφ Ryz; + +@[grind .] +lemma validates_implyS [IsTrans _ M.rel] [Std.Refl M.rel] : M ⊧ Axioms.ImplyS φ ψ χ := by + rintro x y Rxy hφψχ z Ryz hφψ w Rzw hφ; + have Ryw : y ≺ w := IsTrans.trans _ _ _ Ryz Rzw; + have Rww : w ≺ w := Std.Refl.refl _; + exact hφψχ _ Ryw hφ _ Rww (hφψ _ Rzw hφ); + +lemma validates_mdp_of_reflexive [Std.Refl M.rel] (hφψ : M ⊧ φ 🡒 ψ) (hφ : M ⊧ φ) : M ⊧ ψ := by + intro x; + apply hφψ x; + . apply Std.Refl.refl; + . apply hφ; + +class Intuitionistic (M : KripkeModel κ α) extends Std.Refl M.rel, IsTrans _ M.rel, Persistent M + +end + +end KripkeModel + + +end LO.Propositional + +end diff --git a/Foundation/Propositional/Kripke3/Logic/Cl.lean b/Foundation/Propositional/Kripke3/Logic/Cl.lean new file mode 100644 index 000000000..af3e7176d --- /dev/null +++ b/Foundation/Propositional/Kripke3/Logic/Cl.lean @@ -0,0 +1,33 @@ +module + +public import Foundation.Propositional.Kripke3.Axiom.LEM + +@[expose] public section + +namespace LO.Propositional + +open LO.Entailment +open SaturatedConsistentTableau +open KripkeModel + +namespace Cl + +variable [Consistent (Propositional.Cl)] + +theorem provable_of_forall_connected_model_validates + : (∀ {κ : Type 0}, [Nonempty κ] → ∀ M : KripkeModel κ ℕ, [M.Intuitionistic] → [IsRightEuclidean M.rel] → M ⊧ φ) → (Propositional.Cl) ⊢ φ + := fun h ↦ canonicalKripkeModel.iff_validates_provable.mp $ h _ + +lemma exists_connected_model_of_unprovable (h : (Propositional.Cl) ⊬ φ) + : ∃ κ : Type 0, ∃ _ : Nonempty κ, ∃ M : KripkeModel κ ℕ, ∃ _ : M.Intuitionistic, ∃ _ : IsRightEuclidean M.rel, ∃ w : M.world, w ⊮ φ := by + contrapose! h; + apply provable_of_forall_connected_model_validates; + apply h; + +end Cl + + +end LO.Propositional + + +end diff --git a/Foundation/Propositional/Kripke3/Logic/Int/Completeness.lean b/Foundation/Propositional/Kripke3/Logic/Int/Completeness.lean new file mode 100644 index 000000000..0b393c4ad --- /dev/null +++ b/Foundation/Propositional/Kripke3/Logic/Int/Completeness.lean @@ -0,0 +1,153 @@ +module + +public import Foundation.Propositional.Kripke3.Basic +public import Foundation.Propositional.ConsistentTableau +public import Foundation.Propositional.Entailment.Minimal.Basic +public import Foundation.Propositional.Kripke.Basic +public import Foundation.Propositional.Hilbert.Standard.Basic + +@[expose] public section + +namespace LO.Propositional + +variable [Encodable α] [DecidableEq α] + +variable {S} [Entailment S (Formula α)] +variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] + +open LO.Entailment +open SaturatedConsistentTableau +open KripkeModel + +def canonicalKripkeModel (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] + : KripkeModel (SaturatedConsistentTableau 𝓢) α where + frame t₁ t₂ := t₁.1.1 ⊆ t₂.1.1 + val a t := (#a) ∈ t.1.1 + +instance : KripkeModel.Intuitionistic (canonicalKripkeModel 𝓢) where + refl := by tauto_set; + trans := by tauto_set; + atom_persistency := by tauto; + +namespace canonicalKripkeModel + +variable {x y t t₁ t₂ : (canonicalKripkeModel 𝓢).world} {φ ψ : Formula α} + +lemma def_rel₁ : x ≺ y ↔ x.1.1 ⊆ y.1.1 := by simp [canonicalKripkeModel]; + +lemma def_rel₂ : x ≺ y ↔ y.1.2 ⊆ x.1.2 := by + constructor; + . intro h φ; + contrapose!; + simp only [iff_not_mem₂_mem₁] + apply h; + . intro h φ; + contrapose!; + simp only [iff_not_mem₁_mem₂] + apply h; + +lemma truthlemma : t ⊩ φ ↔ φ ∈ t.1.1 := by + induction φ generalizing t with + | hatom => tauto; + | hfalsum => simp [not_mem₁_falsum]; + | hand φ ψ ihp ihq => simp [SaturatedConsistentTableau.iff_mem₁_and, *]; + | hor φ ψ ihp ihq => simp [SaturatedConsistentTableau.iff_mem₁_or, *]; + | himp φ ψ ihp ihq => + constructor; + . contrapose!; + intro h; + replace h := iff_not_mem₁_mem₂.mp h; + obtain ⟨t', ⟨h, _⟩⟩ := lindenbaum (𝓢 := 𝓢) (t₀ := (insert φ t.1.1, {ψ})) $ by + intro Γ Δ hΓ hΔ; + by_contra hC; + apply t.consistent (Γ := Γ.erase φ) (Δ := {φ 🡒 ψ}) ?_ ?_; + . simp only [Finset.disj_singleton]; + apply FConj_DT.mpr; + apply Context.deduct! + replace hC := Context.weakening! (Δ := insert φ Γ) (by simp) $ FConj_DT.mp hC; + rcases Set.subset_singleton_iff_eq.mp hΔ with (hΔ | hΔ); + . simp only [Finset.coe_eq_empty] at hΔ; + subst hΔ; + simp only [Finset.disj_empty, Finset.coe_erase, Set.insert_diff_singleton] at hC ⊢; + exact of_O! hC; + . simp only [Finset.coe_eq_singleton] at hΔ; + subst hΔ; + simpa using hC; + . simpa using Set.iff_subset_insert_subset_diff.mp hΓ; + . simpa; + have ⟨_, _⟩ := Set.insert_subset_iff.mp h; + apply forces_imp.not.mpr; + push_neg; + use t'; + refine ⟨?_, ?_, ?_⟩; + . assumption; + . apply ihp.mpr; + assumption; + . apply ihq.not.mpr; + apply iff_not_mem₁_mem₂.mpr; + simp_all only [Set.singleton_subset_iff]; + . intro h t' htt' hp; + replace hp := ihp.mp hp; + have hpq := htt' h; + apply ihq.mpr; + apply iff_not_mem₂_mem₁.mp; + apply not_mem₂ (Γ := {φ, φ 🡒 ψ}); + . simp only [Finset.coe_insert, Finset.coe_singleton]; + apply Set.doubleton_subset.mpr; + tauto; + . suffices 𝓢 ⊢ Finset.conj {φ, φ 🡒 ψ} 🡒 Finset.disj {ψ} by simpa; + apply Entailment.CFConj_CDisj!_of_innerMDP (φ := φ) (ψ := ψ) <;> simp; + +lemma iff_validates_provable : (canonicalKripkeModel 𝓢) ⊧ φ ↔ 𝓢 ⊢ φ := by + constructor; + . contrapose!; + intro h; + obtain ⟨t', ht'⟩ := lindenbaum $ by + show Tableau.Consistent 𝓢 (∅, {φ}); + simp only [Tableau.Consistent]; + rintro Γ Δ hΓ hΔ; + by_contra hC; + apply h; + rcases Set.subset_singleton_iff_eq.mp hΔ with (hΔ | hΔ); + . simp only [Set.subset_empty_iff, Finset.coe_eq_empty] at hΓ hΔ; + subst hΓ hΔ; + simp only [Finset.conj_empty, Finset.disj_empty] at hC; + exact of_O! $ hC ⨀ verum!; + . simp only [Set.subset_empty_iff, Finset.coe_eq_empty, Finset.coe_eq_singleton] at hΓ hΔ; + subst hΓ hΔ; + simp only [Finset.conj_empty, Finset.disj_singleton] at hC; + exact hC ⨀ verum!;; + apply KripkeModel.notValidates_of_exists_world_notForces + use t'; + apply truthlemma.not.mpr; + apply iff_not_mem₁_mem₂.mpr; + simp_all; + . intro h t; + suffices φ ∈ t.1.1 by exact truthlemma.mpr this; + exact mem₁_of_provable h; + +end canonicalKripkeModel + + + +namespace Int + +variable [Consistent (Propositional.Int)] + +theorem provable_of_forall_model_validates + : (∀ {κ : Type 0}, [Nonempty κ] → ∀ M : KripkeModel κ ℕ, [M.Intuitionistic] → M ⊧ φ) → (Propositional.Int) ⊢ φ + := fun h ↦ canonicalKripkeModel.iff_validates_provable.mp $ h _ + +lemma exists_model_of_unprovable (h : (Propositional.Int) ⊬ φ) + : ∃ κ : Type 0, ∃ _ : Nonempty κ, ∃ M : KripkeModel κ ℕ, ∃ _ : M.Intuitionistic, ∃ w : M.world, w ⊮ φ := by + contrapose! h; + apply provable_of_forall_model_validates; + apply h; + +end Int + + +end LO.Propositional + + +end diff --git a/Foundation/Propositional/Kripke3/Logic/Int/DP.lean b/Foundation/Propositional/Kripke3/Logic/Int/DP.lean new file mode 100644 index 000000000..6b2a3fb66 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Logic/Int/DP.lean @@ -0,0 +1,126 @@ +module + +public import Foundation.Propositional.Kripke3.Logic.Int.Completeness + +@[expose] public section + +namespace LO.Propositional + +open Kripke +open Formula.Kripke + +namespace Int + +variable {κ₁ κ₂ : Type*} [Nonempty κ₁] [Nonempty κ₂] + {M₁ : KripkeModel κ₁ ℕ} {M₂ : KripkeModel κ₂ ℕ} [M₁.Intuitionistic] [M₂.Intuitionistic] + {w₁ : M₁.world} {w₂ : M₂.world} + {φ ψ : Formula ℕ} + +abbrev countermodelDP + (M₁ : KripkeModel κ₁ α) [M₁.Intuitionistic] + (M₂ : KripkeModel κ₂ α) [M₂.Intuitionistic] + (w₁ : M₁.world) (w₂ : M₂.world) + : KripkeModel (Unit ⊕ κ₁ ⊕ κ₂) α where + frame x y := + match x, y with + | (Sum.inl _), (Sum.inl _) => True + | (Sum.inl _), (Sum.inr $ Sum.inl y) => M₁.rel w₁ y + | (Sum.inl _), (Sum.inr $ Sum.inr y) => M₂.rel w₂ y + | (Sum.inr $ Sum.inl x), (Sum.inr $ Sum.inl y) => M₁.rel x y + | (Sum.inr $ Sum.inr x), (Sum.inr $ Sum.inr y) => M₂.rel x y + | _, _ => False + val a w := + match w with + | Sum.inr $ Sum.inl w => M₁ a w + | Sum.inr $ Sum.inr w => M₂ a w + | _ => False + +instance : (countermodelDP M₁ M₂ w₁ w₂).Intuitionistic where + refl x := by + match x with + | (Sum.inl _) => trivial + | (Sum.inr $ Sum.inl x) => exact Std.Refl.refl x + | (Sum.inr $ Sum.inr x) => exact Std.Refl.refl x + trans := by + simp only [ + countermodelDP, KripkeModel.rel, Sum.forall, forall_const, imp_self, + implies_true, true_and, IsEmpty.forall_iff, and_true, and_self, imp_false + ]; + refine ⟨?_, ?_, ?_⟩; + . constructor; + . apply Trans.trans; + . apply Trans.trans; + . apply Trans.trans; + . apply Trans.trans; + atom_persistency := by + simp only [ + countermodelDP, KripkeModel.rel, KripkeModel.forces_atom, Sum.forall, + imp_false, not_true_eq_false, implies_true, IsEmpty.forall_iff, and_self, + not_false_eq_true, true_and, and_true, + ]; + constructor <;> apply KripkeModel.Persistent.atom_persistency; + +lemma counterexampleDPModel.forces_left {x : M₁.world} : + x ⊩ φ ↔ ((countermodelDP M₁ M₂ w₁ w₂).Forces (Sum.inr $ Sum.inl x) φ) := by + induction φ generalizing x with + | himp φ ψ ihφ ihψ => + constructor; + . intro hφψ y; + match y with + | (Sum.inl _) | (Sum.inr $ Sum.inr y) => simp [countermodelDP] + | (Sum.inr $ Sum.inl y) => grind [hφψ y]; + . intro h y Rxy hφ; + exact ihψ.mpr $ h (Sum.inr $ Sum.inl y) Rxy $ ihφ.mp $ hφ; + | hatom => simp [KripkeModel.Forces, KripkeModel.forces_atom] + | _ => simp_all [KripkeModel.Forces]; + +lemma counterexampleDPModel.forces_right {x : M₂.world} : + x ⊩ φ ↔ ((countermodelDP M₁ M₂ w₁ w₂).Forces (Sum.inr $ Sum.inr x) φ) := by + induction φ generalizing x with + | himp φ ψ ihφ ihψ => + constructor; + . intro hφψ y; + match y with + | (Sum.inl _) | (Sum.inr $ Sum.inl y) => simp [countermodelDP] + | (Sum.inr $ Sum.inr y) => grind [hφψ y]; + . intro h y Rxy hφ; + exact ihψ.mpr $ h (Sum.inr $ Sum.inr y) Rxy $ ihφ.mp $ hφ; + | hatom => simp [KripkeModel.Forces, KripkeModel.forces_atom] + | _ => simp_all [KripkeModel.Forces]; + +variable [Entailment.Consistent (Propositional.Int)] + +theorem disjunctive : Propositional.Int ⊢ φ ⋎ ψ → Propositional.Int ⊢ φ ∨ Propositional.Int ⊢ ψ := by + contrapose!; + rintro ⟨hnφ, hnψ⟩; + obtain ⟨_, _, M₁, _, w₁, h₁⟩ := exists_model_of_unprovable hnφ; + obtain ⟨_, _, M₂, _, w₂, h₂⟩ := exists_model_of_unprovable hnψ; + + suffices ∃ κ : Type 0, ∃ _ : Nonempty κ, ∃ M : KripkeModel κ ℕ, ∃ w : M.world, w ⊮ φ ⋎ ψ by sorry; + let M := countermodelDP M₁ M₂ w₁ w₂; + have : M.Intuitionistic := by infer_instance; + have : IsTrans _ M.rel := by sorry; + + refine ⟨_, _, M, Sum.inl (), ?_⟩ + apply M.forces_or.not.mpr; + push_neg; + constructor; + . contrapose! h₁; + exact counterexampleDPModel.forces_left.mpr $ by + show M.Forces (Sum.inr $ Sum.inl w₁) φ; + apply M.formula_persistency h₁; + apply Std.Refl.refl; + . contrapose! h₂; + exact counterexampleDPModel.forces_right.mpr $ by + show M.Forces (Sum.inr $ Sum.inr w₂) ψ; + apply M.formula_persistency h₂; + apply Std.Refl.refl; + +instance : Entailment.Disjunctive Propositional.Int := ⟨disjunctive⟩ + +end Int + + +end LO.Propositional + +end diff --git a/Foundation/Propositional/Kripke3/Logic/KC.lean b/Foundation/Propositional/Kripke3/Logic/KC.lean new file mode 100644 index 000000000..83c709890 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Logic/KC.lean @@ -0,0 +1,33 @@ +module + +public import Foundation.Propositional.Kripke3.Axiom.WLEM + +@[expose] public section + +namespace LO.Propositional + +open LO.Entailment +open SaturatedConsistentTableau +open KripkeModel + +namespace KC + +variable [Consistent (Propositional.KC)] + +theorem provable_of_forall_convergent_model_validates + : (∀ {κ : Type 0}, [Nonempty κ] → ∀ M : KripkeModel κ ℕ, [M.Intuitionistic] → [IsPiecewiseStronglyConvergent M.rel] → M ⊧ φ) → (Propositional.KC) ⊢ φ + := fun h ↦ canonicalKripkeModel.iff_validates_provable.mp $ h _ + +lemma exists_convergent_model_of_unprovable (h : (Propositional.KC) ⊬ φ) + : ∃ κ : Type 0, ∃ _ : Nonempty κ, ∃ M : KripkeModel κ ℕ, ∃ _ : M.Intuitionistic, ∃ _ : IsPiecewiseStronglyConvergent M.rel, ∃ w : M.world, w ⊮ φ := by + contrapose! h; + apply provable_of_forall_convergent_model_validates; + apply h; + +end KC + + +end LO.Propositional + + +end diff --git a/Foundation/Propositional/Kripke3/Logic/KreiselPutnam.lean b/Foundation/Propositional/Kripke3/Logic/KreiselPutnam.lean new file mode 100644 index 000000000..dcfb033a6 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Logic/KreiselPutnam.lean @@ -0,0 +1,33 @@ +module + +public import Foundation.Propositional.Kripke3.Axiom.KreiselPutnam + +@[expose] public section + +namespace LO.Propositional + +open LO.Entailment +open SaturatedConsistentTableau +open KripkeModel + +namespace KreiselPutnam + +variable [Consistent (Propositional.KreiselPutnam)] + +theorem provable_of_forall_kreisel_putnam_model_validates + : (∀ {κ : Type 0}, [Nonempty κ] → ∀ M : KripkeModel κ ℕ, [M.KreiselPutnam] → M ⊧ φ) → (Propositional.KreiselPutnam) ⊢ φ + := fun h ↦ canonicalKripkeModel.iff_validates_provable.mp $ h _ + +lemma exists_kreisel_putnam_model_of_unprovable (h : (Propositional.KreiselPutnam) ⊬ φ) + : ∃ κ : Type 0, ∃ _ : Nonempty κ, ∃ M : KripkeModel κ ℕ, ∃ _ : M.KreiselPutnam, ∃ w : M.world, w ⊮ φ := by + contrapose! h; + apply provable_of_forall_kreisel_putnam_model_validates; + apply h; + +end KreiselPutnam + + +end LO.Propositional + + +end diff --git a/Foundation/Propositional/Kripke3/Logic/LC.lean b/Foundation/Propositional/Kripke3/Logic/LC.lean new file mode 100644 index 000000000..1ccf6a573 --- /dev/null +++ b/Foundation/Propositional/Kripke3/Logic/LC.lean @@ -0,0 +1,33 @@ +module + +public import Foundation.Propositional.Kripke3.Axiom.Dummett + +@[expose] public section + +namespace LO.Propositional + +open LO.Entailment +open SaturatedConsistentTableau +open KripkeModel + +namespace LC + +variable [Consistent (Propositional.LC)] + +theorem provable_of_forall_connected_model_validates + : (∀ {κ : Type 0}, [Nonempty κ] → ∀ M : KripkeModel κ ℕ, [M.Intuitionistic] → [IsPiecewiseStronglyConnected M.rel] → M ⊧ φ) → (Propositional.LC) ⊢ φ + := fun h ↦ canonicalKripkeModel.iff_validates_provable.mp $ h _ + +lemma exists_connected_model_of_unprovable (h : (Propositional.LC) ⊬ φ) + : ∃ κ : Type 0, ∃ _ : Nonempty κ, ∃ M : KripkeModel κ ℕ, ∃ _ : M.Intuitionistic, ∃ _ : IsPiecewiseStronglyConnected M.rel, ∃ w : M.world, w ⊮ φ := by + contrapose! h; + apply provable_of_forall_connected_model_validates; + apply h; + +end LC + + +end LO.Propositional + + +end