From 8ba6a6a57314adf4321729050d56dc13523700a4 Mon Sep 17 00:00:00 2001 From: twwar Date: Tue, 23 Sep 2025 15:33:25 +0200 Subject: [PATCH 01/12] nj defs basic --- Cslib/Logics/IPL/NJ/Basic.lean | 331 +++++++++++++++++++++++++++++++++ Cslib/Logics/IPL/NJ/Defs.lean | 303 ++++++++++++++++++++++++++++++ 2 files changed, 634 insertions(+) create mode 100644 Cslib/Logics/IPL/NJ/Basic.lean create mode 100644 Cslib/Logics/IPL/NJ/Defs.lean diff --git a/Cslib/Logics/IPL/NJ/Basic.lean b/Cslib/Logics/IPL/NJ/Basic.lean new file mode 100644 index 00000000..8e3304fe --- /dev/null +++ b/Cslib/Logics/IPL/NJ/Basic.lean @@ -0,0 +1,331 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ +import Cslib.Logics.IPL.NJ.Defs + +/-! # Elementary derivations and equivalences in NJ -/ + +variable {Atom : Type u} [DecidableEq Atom] + +namespace IPL + +open Proposition + +namespace NJ + +open Derivation + +/-! +### Negation theorems + +The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. +-/ + +/-- Double negation introduction -/ +def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, impl (impl A B) B⟩ := by + apply implI (A := A.impl B) + apply implE (A := A) <;> exact ax' (by grind) + +theorem Derivable.dni {A B : Proposition Atom} : Derivable ⟨{A},impl (impl A B) B⟩ := + ⟨Derivation.dni⟩ + +/-- The double negation of excluded-middle, or in minimal-logic-style ⊢ (A ∨ (A → B)) → B → B. -/ +def Derivation.notNotLEM {A B : Proposition Atom} : + Derivation ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := by + apply implI + rw [insert_empty_eq] + apply implE (A := A.disj (A.impl B)) (ax' <| by grind) + apply disjI₂ + apply implI + apply implE (A := A.disj (A.impl B)) (ax' <| by grind) + apply disjI₁ + apply ax' <| by grind + +theorem Derivable.not_not_lem {A B : Proposition Atom} : + Derivable ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := ⟨Derivation.notNotLEM⟩ + +/-- Triple negation elimination -/ +def Derivation.tne {A B : Proposition Atom} : + Derivation ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := by + apply implI + apply implE (A := (A.impl B).impl B) (ax' <| by grind) + exact Derivation.dni.weak' (Γ := {A}) (by grind) + +theorem Derivable.tne {A B : Proposition Atom} : + Derivable ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := ⟨Derivation.tne⟩ + +def tneEquiv {A B : Proposition Atom} : + Proposition.equiv (A.impl B) (((A.impl B).impl B).impl B) := ⟨Derivation.dni, Derivation.tne⟩ + +theorem tne_equivalent {A B : Proposition Atom} : + Proposition.Equiv (A.impl B) (((A.impl B).impl B).impl B) := ⟨Derivable.dni, Derivable.tne⟩ + +/-- Modus tollens -/ +def Derivation.modusTollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) + (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B.impl C) Γ, A.impl C⟩ := by + apply implI + apply implE (A := B) + · exact ax' (by grind) + · exact D.weak' (h := by grind) + +theorem Derivable.modus_tollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) + (h : Derivable ⟨insert A Γ, B⟩) : Derivable ⟨insert (B.impl C) Γ, A.impl C⟩ := + let ⟨D⟩ := h; ⟨D.modusTollens C⟩ + +/-! +### De Morgan laws + +The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. +-/ + +/-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ +def disjImpOfConjImps {A B C : Proposition Atom} : + Derivation ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := by + apply implI + apply disjE (A := A) (B := B) + · apply ax + · apply implE (A := A) + · apply conjE₁ (B := B.impl C) + exact ax' (by grind) + · apply ax + · apply implE (A := B) + · apply conjE₂ (A := A.impl C) + exact ax' (by grind) + · apply ax + +/-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ +theorem disj_imp_of_conj_imps {A B C : Proposition Atom} : + Derivable ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := ⟨disjImpOfConjImps⟩ + +/-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ +def conjImpsOfDisjImp {A B C : Proposition Atom} : + Derivation ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := by + apply conjI + · apply implI + apply implE (A := A.disj B) + · exact ax' (by grind) + · apply disjI₁ + apply ax + · apply implI + apply implE (A := A.disj B) + · exact ax' (by grind) + · apply disjI₂ + apply ax + +/-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ +theorem conj_imps_of_disj_imp {A B C : Proposition Atom} : + Derivable ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := ⟨conjImpsOfDisjImp⟩ + +def disjImpConjImpsEquiv {A B C : Proposition Atom} : + Proposition.equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := + ⟨conjImpsOfDisjImp, disjImpOfConjImps⟩ + +theorem disj_imp_conj_imps_equivalent {A B C : Proposition Atom} : + Proposition.Equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := + ⟨conj_imps_of_disj_imp, disj_imp_of_conj_imps⟩ + +/-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ +def conjImpOfDisjImps {A B C : Proposition Atom} : + Derivation ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := by + apply implI + apply disjE (A := A.impl C) (B := B.impl C) + · exact ax' (by grind) + · apply implE (A := A) + · apply ax + · apply conjE₁ (B := B) + exact ax' (by grind) + · apply implE (A := B) + · apply ax + · apply conjE₂ (A := A) + exact ax' (by grind) + +/-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ +theorem conj_imp_of_disj_imps {A B C : Proposition Atom} : + Derivable ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := ⟨conjImpOfDisjImps⟩ + +/-! ### Further equivalences and implications -/ + +/-- Equivalence of A → (B → C) and (A ∧ B) → C -/ +def curryEquiv {A B C : Proposition Atom} : + Proposition.equiv (A.impl (B.impl C)) (impl (A.conj B) C) := by + constructor + · apply implI + apply implE (A := B) + · apply implE (A := A) + · exact ax' (by grind) + · apply conjE₁ (B := B) + exact ax' (by grind) + · apply conjE₂ (A := A) + exact ax' (by grind) + · apply implI + apply implI + apply implE (A := A.conj B) + · exact ax' (by grind) + · apply conjI <;> exact ax' (by grind) + +/-- Equivalence of A → (B → C) and (A ∧ B) → C -/ +theorem curry_equiv {A B C : Proposition Atom} : + Proposition.Equiv (A.impl (B.impl C)) (impl (A.conj B) C) := ⟨⟨curryEquiv.1⟩, ⟨curryEquiv.2⟩⟩ + +/-- A ∧ B ⊢ B ∧ A -/ +def conjCommDer {A B : Proposition Atom} : Derivation ⟨{A.conj B}, B.conj A⟩ := by + apply conjI + · apply conjE₂ (A := A) + exact ax' (by grind) + · apply conjE₁ (B := B) + exact ax' (by grind) + +/-- Equivalence of A ∧ B and B ∧ A -/ +def conjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.conj B) (B.conj A) := + ⟨conjCommDer, conjCommDer⟩ + +/-- Equivalence of A ∧ B and B ∧ A -/ +theorem conj_comm_equiv {A B : Proposition Atom} : Proposition.Equiv (A.conj B) (B.conj A) := + ⟨⟨conjCommDer⟩, ⟨conjCommDer⟩⟩ + +/-- Equivalence of A ∧ A and A -/ +def conjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.conj A) A := by + constructor + · apply conjE₁ (B := A) + exact ax' (by grind) + · apply conjI <;> exact ax' (by grind) + +/-- Equivalence of A ∧ A and A -/ +theorem conj_idem_equiv {A : Proposition Atom} : Proposition.Equiv (A.conj A) A := + ⟨⟨conjIdemEquiv.1⟩, ⟨conjIdemEquiv.2⟩⟩ + +/-- A ∨ B ⊢ B ∨ A -/ +def disjCommDer {A B : Proposition Atom} : Derivation ⟨{A.disj B}, B.disj A⟩ := by + apply disjE (A := A) (B := B) + · exact ax' (by grind) + · apply disjI₂ + exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∨ B and B ∨ A -/ +def disjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.disj B) (B.disj A) := + ⟨disjCommDer, disjCommDer⟩ + +/-- Equivalence of A ∨ B and B ∨ A -/ +theorem disj_comm_equiv {A B : Proposition Atom} : Proposition.Equiv (A.disj B) (B.disj A) := + ⟨⟨disjCommDer⟩, ⟨disjCommDer⟩⟩ + +/-- Equivalence of A ∨ A and A -/ +def disjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.disj A) A := by + constructor + · apply disjE (A := A) (B := A) <;> exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∨ A and A -/ +theorem disj_idem_equiv {A : Proposition Atom} : Proposition.Equiv (A.disj A) A := + ⟨⟨disjIdemEquiv.1⟩, ⟨disjIdemEquiv.2⟩⟩ + +/-- Equivalence of A → (A → B) and A → B -/ +def implIdemEquiv {A B : Proposition Atom} : + Proposition.equiv (A.impl <| A.impl B) (A.impl B) := by + constructor + · apply implI + apply implE (A := A) + · apply implE (A := A) + · exact ax' (by grind) + · exact ax' (by grind) + · exact ax' (by grind) + · apply implI + exact ax' (by grind) + +/-- Equivalence of A → (A → B) and A → B -/ +theorem impl_idem_equiv {A B : Proposition Atom} : + Proposition.Equiv (A.impl <| A.impl B) (A.impl B) := ⟨⟨implIdemEquiv.1⟩, ⟨implIdemEquiv.2⟩⟩ + +/-- A → (B → C) ⊢ B → (A → C) -/ +def implSwapDer {A B C : Proposition Atom} : + Derivation ⟨{A.impl <| B.impl C}, B.impl (A.impl C)⟩ := by + apply implI + apply implI + apply implE (A := B) + · apply implE (A := A) <;> exact ax' (by grind) + · exact ax' (by grind) + +/-- Equivalence of A → (B → C) and B → (A → C) -/ +def implSwapEquiv {A B C : Proposition Atom} : + Proposition.equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := ⟨implSwapDer, implSwapDer⟩ + +/-- A → (B → C) ⊢ (A → B) → (A → C) -/ +def implImplDistrib {A B C : Proposition Atom} : + Derivation ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := by + apply implI + apply implI + apply implE (A := B) <;> apply implE (A := A) <;> exact ax' (by grind) + +theorem impl_impl_distrib {A B C : Proposition Atom} : + Derivable ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := ⟨implImplDistrib⟩ + +/-- Equivalence of A → (B → C) and B → (A → C) -/ +theorem impl_swap_equiv {A B C : Proposition Atom} : + Proposition.Equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := ⟨⟨implSwapDer⟩, ⟨implSwapDer⟩⟩ + +/-- Equivalence of A ∧ (A ∨ B) and A -/ +def absorbConjDisj {A B : Proposition Atom} : Proposition.equiv (A.conj <| (A.disj B)) A := by + constructor + · apply conjE₁ (B := (A.disj B)) + exact ax' (by grind) + · apply conjI + · exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∧ (A ∨ B) and A -/ +theorem absorb_conj_disj {A B : Proposition Atom} : Proposition.Equiv (A.conj <| (A.disj B)) A := + ⟨⟨absorbConjDisj.1⟩, ⟨absorbConjDisj.2⟩⟩ + +/-- Equivalence of A ∨ (A ∧ B) and A -/ +def absorbDisjConj {A B : Proposition Atom} : Proposition.equiv (A.disj <| A.conj B) A := by + constructor + · apply disjE (A := A) (B := A.conj B) + · exact ax' (by grind) + · exact ax' (by grind) + · apply conjE₁ (B := B) + exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∨ (A ∧ B) and A -/ +theorem absorb_disj_conj {A B : Proposition Atom} : Proposition.Equiv (A.disj <| A.conj B) A := + ⟨⟨absorbDisjConj.1⟩, ⟨absorbDisjConj.2⟩⟩ + +/-- Falsum is absorbing for conjunction -/ +def botConjAbsorb {A : Proposition Atom} : Proposition.equiv (A.conj bot) bot := by + constructor + · apply conjE₂ (A := A) + exact ax' (by grind) + · apply conjI + · apply botE + exact ax' (by grind) + · exact ax' (by grind) + +/-- Falsum is absorbing for conjunction -/ +theorem bot_conj_absorb {A : Proposition Atom} : Proposition.Equiv (A.conj bot) bot := + ⟨⟨botConjAbsorb.1⟩, ⟨botConjAbsorb.2⟩⟩ + +/-- Falsum is neutral for disjunction -/ +def botDisjNeutral {A : Proposition Atom} : Proposition.equiv (A.disj bot) A := by + constructor + · apply disjE (A := A) (B := bot) + · exact ax' (by grind) + · exact ax' (by grind) + · apply botE + exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Falsum is neutral for disjunction -/ +theorem bot_disj_neutral {A : Proposition Atom} : Proposition.Equiv (A.disj bot) A := + ⟨⟨botDisjNeutral.1⟩, ⟨botDisjNeutral.2⟩⟩ + +end NJ + +end IPL diff --git a/Cslib/Logics/IPL/NJ/Defs.lean b/Cslib/Logics/IPL/NJ/Defs.lean new file mode 100644 index 00000000..5fb59a43 --- /dev/null +++ b/Cslib/Logics/IPL/NJ/Defs.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ +import Mathlib.Data.Finset.Insert +import Mathlib.Data.Finset.SDiff + +/-! +# Gentzen's NJ + +Natural deduction for intuitionistic propositional logic. + +## Main definitions + +- `Proposition` : a type of propositions with atoms in a given type. +- `Derivation` : natural deduction derivation, done in "sequent style", ie with explicit +hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit weakening +and exchange, and the axiom rule derives `{A} ∪ Γ ⊢ A` for any context `Γ`, allowing weakening to +be a derived rule. +- `Derivable` : defined as `Nonempty (Derivation S)`. +- `Proposition.equiv` and `Proposition.Equiv` : `Type`- and `Prop`-valued equivalence of +propositions. + +## Main results + +- `Derivation.weak` : weakening as a derived rule. +- `Derivation.subs` : substituting a derivation for a hypothesis. +- `equiv_equivalence` : equivalence of propositions is an equivalence. + +## References + +- Dag Prawitz, *Natural Deduction: a proof-theoretical study*. +- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely +presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*. +(Suggestions of better references welcome!) +-/ + +universe u + +variable {Atom : Type u} [DecidableEq Atom] + +namespace IPL + +/-- Propositions. We view negation as a defined connective ~A := A → ⊥ -/ +inductive Proposition (Atom : Type u) : Type u where + /-- Propositional atoms -/ + | atom (x : Atom) + /-- Falsum -/ + | bot + /-- Conjunction -/ + | conj (a b : Proposition Atom) + /-- Disjunction -/ + | disj (a b : Proposition Atom) + /-- Implication -/ + | impl (a b : Proposition Atom) +deriving DecidableEq, BEq + +namespace NJ + +open Proposition + +/-- Contexts are finsets of propositions. -/ +abbrev Ctx (Atom) := Finset (Proposition Atom) + +/-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ +abbrev Sequent (Atom) := Ctx Atom × Proposition Atom + +/-- A derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ. -/ +inductive Derivation : Sequent Atom → Type _ where + /-- Axiom (or assumption) -/ + | ax (Γ : Ctx Atom) (A : Proposition Atom) : Derivation ⟨insert A Γ, A⟩ + /-- Falsum elimination (ex falso quodlibet) -/ + | botE {Γ : Ctx Atom} (A : Proposition Atom) : Derivation ⟨Γ, bot⟩ → Derivation ⟨Γ, A⟩ + /-- Conjunction introduction -/ + | conjI {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, conj A B⟩ + /-- Conjunction elimination left -/ + | conjE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, A⟩ + /-- Conjunction elimination right -/ + | conjE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, B⟩ + /-- Disjunction introduction left -/ + | disjI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, disj A B⟩ + /-- Disjunction introduction right -/ + | disjI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, disj A B⟩ + /-- Disjunction elimination -/ + | disjE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation ⟨Γ, disj A B⟩ → + Derivation ⟨insert A Γ, C⟩ → Derivation ⟨insert B Γ, C⟩ → Derivation ⟨Γ, C⟩ + /-- Implication introduction -/ + | implI {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation ⟨insert A Γ, B⟩ → Derivation ⟨Γ, impl A B⟩ + /-- Implication elimination -/ + | implE {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation ⟨Γ, impl A B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ + +/-- A sequent is derivable if it has a derivation. -/ +def Derivable (S : Sequent Atom) := Nonempty (Derivation S) + +/-- A proposition is derivable if it has a derivation from the empty context. -/ +def Proposition.PDerivable (A : Proposition Atom) := Nonempty (Derivation ⟨∅,A⟩) + +/-- An equivalence between A and B is a derivation of B from A and vice-versa. -/ +def Proposition.equiv (A B : Proposition Atom) := Derivation ⟨{A},B⟩ × Derivation ⟨{B},A⟩ + +/-- Two propositions A and B are equivalent if B can be derived from A and vice-versa. -/ +def Proposition.Equiv (A B : Proposition Atom) := Derivable ⟨{A},B⟩ ∧ Derivable ⟨{B},A⟩ + +open Derivation + +/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ +def Proposition.top : Proposition Atom := impl bot bot + +def derivationTop : Derivation (Atom := Atom) ⟨∅,Proposition.top⟩ := by + apply implI + exact ax (Atom := Atom) ∅ bot + +theorem top_derivable : Proposition.PDerivable (Atom := Atom) Proposition.top := ⟨derivationTop⟩ + +/-! ### Common proof patterns -/ + +/-- A convenient reformulation of the axiom rule. -/ +def Derivation.ax' {Γ : Ctx Atom} {A : Proposition Atom} (h : A ∈ Γ) : Derivation ⟨Γ,A⟩ := by + have : Γ = insert A Γ := by grind + rw [this] + apply ax + +/-- Weakening is a derived rule. -/ +def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) + (D : Derivation ⟨Γ, A⟩) : Derivation ⟨Γ ∪ Δ, A⟩ := by + match D with + | ax Γ A => + rw [Finset.insert_union A Γ Δ] + exact ax (Γ ∪ Δ) A + | botE A D => exact botE A <| D.weak Δ + | conjI D D' => exact conjI (D.weak Δ) (D'.weak Δ) + | conjE₁ D => exact conjE₁ <| D.weak Δ + | conjE₂ D => exact conjE₂ <| D.weak Δ + | disjI₁ D => exact disjI₁ <| D.weak Δ + | disjI₂ D => exact disjI₂ <| D.weak Δ + | @disjE _ _ _ A B _ D D' D'' => + apply disjE (D.weak Δ) + · rw [←Finset.insert_union A Γ Δ]; exact D'.weak Δ + · rw [←Finset.insert_union B Γ Δ]; exact D''.weak Δ + | @implI _ _ A B Γ D => + apply implI + rw [←Finset.insert_union A Γ Δ]; exact D.weak Δ + | implE D D' => exact implE (D.weak Δ) (D'.weak Δ) + +theorem Derivable.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) + (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Γ ∪ Δ, A⟩ := by + let ⟨D⟩ := h + exact ⟨D.weak Δ⟩ + +def Derivation.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h : Γ ⊆ Δ) (D : Derivation ⟨Γ, A⟩) : + Derivation ⟨Δ, A⟩ := Finset.union_sdiff_of_subset h ▸ D.weak (Δ \ Γ) + +theorem Derivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) + (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Δ, A⟩ := by + let ⟨D⟩ := h + exact ⟨D.weak' h_ext⟩ + +/-- Substitution of a derivation `E` for one of the hypotheses in the context `Gamma` of `D`. -/ +def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} + (D : Derivation ⟨Γ, B⟩) (E : Derivation ⟨Δ, A⟩) : Derivation ⟨(Γ \ {A}) ∪ Δ, B⟩ := by + match D with + | ax _ _ => + by_cases B = A + case pos h => + rw [h, Finset.union_comm] + exact E.weak _ + case neg h => + have : B ∉ ({A} : Finset (Proposition Atom)) := Finset.notMem_singleton.mpr h + rw [Finset.insert_sdiff_of_notMem (h := this)] + exact (ax _ B).weak _ + | botE _ D => exact botE B <| D.subs E + | conjI D D' => exact conjI (D.subs E) (D'.subs E) + | conjE₁ D => exact conjE₁ <| D.subs E + | conjE₂ D => exact conjE₂ <| D.subs E + | disjI₁ D => exact disjI₁ <| D.subs E + | disjI₂ D => exact disjI₂ <| D.subs E + | @disjE _ _ _ C C' B D D' D'' => + apply disjE (D.subs E) + · by_cases C = A + case pos h => + rw [h] at D' ⊢ + have : insert A ((Γ \ {A}) ∪ Δ) = (insert A Γ) ∪ Δ := by grind + rw [this] + exact D'.weak _ + case neg h => + have : insert C ((Γ \ {A}) ∪ Δ) = ((insert C Γ) \ {A}) ∪ Δ := by grind + rw [this] + exact D'.subs E + · by_cases C' = A + case pos h => + rw [h] at D'' ⊢ + have : insert A ((Γ \ {A}) ∪ Δ) = (insert A Γ) ∪ Δ := by grind + rw [this] + exact D''.weak _ + case neg h => + have : insert C' ((Γ \ {A}) ∪ Δ) = ((insert C' Γ) \ {A}) ∪ Δ := by grind + rw [this] + exact D''.subs E + | @implI _ _ A' B _ D => + apply implI + by_cases A' = A + case pos h => + rw [h] at D ⊢ + have : insert A (Γ \ {A} ∪ Δ) = insert A Γ ∪ Δ := by grind + rw [this] + exact D.weak Δ + case neg h => + have : insert A' ((Γ \ {A}) ∪ Δ) = ((insert A' Γ) \ {A}) ∪ Δ := by grind + rw [this] + exact D.subs E + | implE D D' => exact implE (D.subs E) (D'.subs E) + +theorem Derivable.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} + (h₁ : Derivable ⟨Γ, B⟩) (h₂ : Derivable ⟨Δ, A⟩) : Derivable ⟨(Γ \ {A}) ∪ Δ, B⟩ := + let ⟨D⟩ := h₁; let ⟨E⟩ := h₂; ⟨D.subs E⟩ + +def Derivation.subs' {Γ : Ctx Atom} {A B : Proposition Atom} + (D : Derivation ⟨{A}, B⟩) (E : Derivation ⟨Γ, A⟩) : Derivation ⟨Γ, B⟩ := by + have : Γ = ({A} \ {A}) ∪ Γ := by grind + rw [this] + exact D.subs E + +theorem Derivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} + (h : Derivable ⟨{A}, B⟩) (h' : Derivable ⟨Γ, A⟩) : Derivable ⟨Γ, B⟩ := + let ⟨D⟩ := h; let ⟨E⟩ := h'; ⟨D.subs' E⟩ + +/-! ### Properties of NJ-equivalence -/ + +theorem Proposition.derivable_iff_equiv_top (A : Proposition Atom) : + PDerivable A ↔ Proposition.Equiv A top := by + constructor <;> intro h + · constructor + · exact ⟨derivationTop.weak' (Δ := {A}) (by grind)⟩ + · let ⟨D⟩ := h + exact ⟨D.weak' (Δ := {Proposition.top}) (by grind)⟩ + · let ⟨D⟩ := h.2 + exact ⟨D.subs' derivationTop⟩ + +/-- Change the conclusion along an equivalence. -/ +def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) : + Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ := e.1.subs' + +theorem equivalent_derivability (Γ : Ctx Atom) {A B : Proposition Atom} (h : Proposition.Equiv A B) + : Derivable ⟨Γ, A⟩ ↔ Derivable ⟨Γ, B⟩ := ⟨h.1.subs', h.2.subs'⟩ + +/-- Replace a hypothesis along an equivalence. -/ +def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) + (C : Proposition Atom) (D : Derivation ⟨insert A Γ, C⟩) : Derivation ⟨insert B Γ, C⟩ := by + have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind + rw [this] + refine D.subs ?_ + exact e.2.weak' (by grind) + +theorem equivalent_hypotheses (Γ : Ctx Atom) {A B : Proposition Atom} (h : Proposition.Equiv A B) + (C : Proposition Atom) : Derivable ⟨insert A Γ, C⟩ ↔ Derivable ⟨insert B Γ, C⟩ := by + let ⟨⟨D⟩, ⟨D'⟩⟩ := h + constructor + · intro ⟨DA⟩ + have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind + rw [this] + refine ⟨DA.subs ?_⟩ + exact D'.weak' (by grind) + · intro ⟨DB⟩ + have : insert A Γ = (insert B Γ \ {B}) ∪ (insert A Γ) := by grind + rw [this] + refine ⟨DB.subs ?_⟩ + exact D.weak' (by grind) + +def reflEquiv (A : Proposition Atom) : Proposition.equiv A A := + let D : Derivation ⟨{A},A⟩ := ax' <| by grind; + ⟨D,D⟩ + +def commEquiv {A B : Proposition Atom} (e : Proposition.equiv A B) : Proposition.equiv B A := + ⟨e.2, e.1⟩ + +def transEquiv {A B C : Proposition Atom} (e : Proposition.Equiv A B) (e' : Proposition.Equiv B C) : + Proposition.Equiv A C := ⟨e'.1.subs' e.1, e.2.subs' e'.2⟩ + +theorem equivalent_refl (A : Proposition Atom) : Proposition.Equiv A A := by + have : Derivable ⟨{A},A⟩ := ⟨ax' <| by grind⟩ + grind [Proposition.Equiv] + +theorem equivalent_comm {A B : Proposition Atom} : + Proposition.Equiv A B → Proposition.Equiv B A := by grind [Proposition.Equiv] + +theorem equivalent_trans {A B C : Proposition Atom} : + Proposition.Equiv A B → Proposition.Equiv B C → Proposition.Equiv A C := by + grind [Proposition.Equiv, Derivable.subs'] + +/-- Equivalence is indeed an equivalence relation. -/ +theorem equiv_equivalence : Equivalence (Proposition.Equiv (Atom := Atom)) := + ⟨equivalent_refl, equivalent_comm, equivalent_trans⟩ + +protected def propositionSetoid : Setoid (Proposition Atom) := + ⟨Proposition.Equiv, equiv_equivalence⟩ + +end NJ + +end IPL From 4ea136d5ae4ebc7d81cde1197c4f5e0e3c213d11 Mon Sep 17 00:00:00 2001 From: twwar Date: Tue, 23 Sep 2025 16:18:06 +0200 Subject: [PATCH 02/12] typo --- Cslib/Logics/IPL/NJ/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Logics/IPL/NJ/Defs.lean b/Cslib/Logics/IPL/NJ/Defs.lean index 5fb59a43..05c3aa75 100644 --- a/Cslib/Logics/IPL/NJ/Defs.lean +++ b/Cslib/Logics/IPL/NJ/Defs.lean @@ -15,7 +15,7 @@ Natural deduction for intuitionistic propositional logic. - `Proposition` : a type of propositions with atoms in a given type. - `Derivation` : natural deduction derivation, done in "sequent style", ie with explicit -hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit weakening +hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit contraction and exchange, and the axiom rule derives `{A} ∪ Γ ⊢ A` for any context `Γ`, allowing weakening to be a derived rule. - `Derivable` : defined as `Nonempty (Derivation S)`. From 86bb320197caaaaec11edc7b7df9195f60000c47 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 1 Oct 2025 11:24:30 +0200 Subject: [PATCH 03/12] avoid tactics for data --- Cslib/Logics/IPL/NJ/Basic.lean | 85 ++++++++++++++++------------------ Cslib/Logics/IPL/NJ/Defs.lean | 47 ++++++++----------- 2 files changed, 59 insertions(+), 73 deletions(-) diff --git a/Cslib/Logics/IPL/NJ/Basic.lean b/Cslib/Logics/IPL/NJ/Basic.lean index 8e3304fe..c8a0441c 100644 --- a/Cslib/Logics/IPL/NJ/Basic.lean +++ b/Cslib/Logics/IPL/NJ/Basic.lean @@ -24,34 +24,33 @@ The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := i -/ /-- Double negation introduction -/ -def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, impl (impl A B) B⟩ := by - apply implI (A := A.impl B) - apply implE (A := A) <;> exact ax' (by grind) +def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, impl (impl A B) B⟩ := + implI (A := A.impl B) _ <| + implE (A := A) (ax' (by grind)) (ax' (by grind)) theorem Derivable.dni {A B : Proposition Atom} : Derivable ⟨{A},impl (impl A B) B⟩ := ⟨Derivation.dni⟩ /-- The double negation of excluded-middle, or in minimal-logic-style ⊢ (A ∨ (A → B)) → B → B. -/ def Derivation.notNotLEM {A B : Proposition Atom} : - Derivation ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := by - apply implI - rw [insert_empty_eq] - apply implE (A := A.disj (A.impl B)) (ax' <| by grind) - apply disjI₂ - apply implI - apply implE (A := A.disj (A.impl B)) (ax' <| by grind) - apply disjI₁ - apply ax' <| by grind + Derivation ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := + implI _ <| + implE (A := A.disj (A.impl B)) (ax' <| by grind) <| + disjI₂ <| + implI _ <| + implE (A := A.disj (A.impl B)) (ax' <| by grind) <| + disjI₁ <| + ax' <| by grind theorem Derivable.not_not_lem {A B : Proposition Atom} : Derivable ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := ⟨Derivation.notNotLEM⟩ /-- Triple negation elimination -/ def Derivation.tne {A B : Proposition Atom} : - Derivation ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := by - apply implI - apply implE (A := (A.impl B).impl B) (ax' <| by grind) - exact Derivation.dni.weak' (Γ := {A}) (by grind) + Derivation ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := + implI _ <| + implE (A := (A.impl B).impl B) (ax' <| by grind) <| + Derivation.dni.weak' (Γ := {A}) (by grind) theorem Derivable.tne {A B : Proposition Atom} : Derivable ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := ⟨Derivation.tne⟩ @@ -64,11 +63,11 @@ theorem tne_equivalent {A B : Proposition Atom} : /-- Modus tollens -/ def Derivation.modusTollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) - (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B.impl C) Γ, A.impl C⟩ := by - apply implI - apply implE (A := B) - · exact ax' (by grind) - · exact D.weak' (h := by grind) + (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B.impl C) Γ, A.impl C⟩ := + implI _ <| + implE (A := B) + (ax' (by grind)) + (D.weak' (h := by grind)) theorem Derivable.modus_tollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) (h : Derivable ⟨insert A Γ, B⟩) : Derivable ⟨insert (B.impl C) Γ, A.impl C⟩ := @@ -82,18 +81,16 @@ The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := i /-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ def disjImpOfConjImps {A B C : Proposition Atom} : - Derivation ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := by - apply implI - apply disjE (A := A) (B := B) - · apply ax - · apply implE (A := A) - · apply conjE₁ (B := B.impl C) - exact ax' (by grind) - · apply ax - · apply implE (A := B) - · apply conjE₂ (A := A.impl C) - exact ax' (by grind) - · apply ax + Derivation ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := + implI _ <| + disjE (A := A) (B := B) + (ax _ _) + (implE (A := A) + (conjE₁ (B := B.impl C) (ax' <| by grind)) + (ax _ _)) + (implE (A := B) + (conjE₂ (A := A.impl C) (ax' (by grind))) + (ax _ _)) /-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ theorem disj_imp_of_conj_imps {A B C : Proposition Atom} : @@ -101,18 +98,16 @@ theorem disj_imp_of_conj_imps {A B C : Proposition Atom} : /-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ def conjImpsOfDisjImp {A B C : Proposition Atom} : - Derivation ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := by - apply conjI - · apply implI - apply implE (A := A.disj B) - · exact ax' (by grind) - · apply disjI₁ - apply ax - · apply implI - apply implE (A := A.disj B) - · exact ax' (by grind) - · apply disjI₂ - apply ax + Derivation ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := + conjI + (implI {impl (disj A B) C} <| + implE (A := A.disj B) (B := C) + (ax' (by grind)) + (disjI₁ (ax _ _))) + (implI {impl (disj A B) C} <| + implE (A := A.disj B) (B := C) + (ax' (by grind)) + (disjI₂ (ax _ _))) /-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ theorem conj_imps_of_disj_imp {A B C : Proposition Atom} : diff --git a/Cslib/Logics/IPL/NJ/Defs.lean b/Cslib/Logics/IPL/NJ/Defs.lean index 05c3aa75..45c539c2 100644 --- a/Cslib/Logics/IPL/NJ/Defs.lean +++ b/Cslib/Logics/IPL/NJ/Defs.lean @@ -110,9 +110,8 @@ open Derivation /-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ def Proposition.top : Proposition Atom := impl bot bot -def derivationTop : Derivation (Atom := Atom) ⟨∅,Proposition.top⟩ := by - apply implI - exact ax (Atom := Atom) ∅ bot +def derivationTop : Derivation (Atom := Atom) ⟨∅, Proposition.top⟩ := + implI ∅ <| ax (Atom := Atom) ∅ bot theorem top_derivable : Proposition.PDerivable (Atom := Atom) Proposition.top := ⟨derivationTop⟩ @@ -125,26 +124,21 @@ def Derivation.ax' {Γ : Ctx Atom} {A : Proposition Atom} (h : A ∈ Γ) : Deriv apply ax /-- Weakening is a derived rule. -/ -def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) - (D : Derivation ⟨Γ, A⟩) : Derivation ⟨Γ ∪ Δ, A⟩ := by - match D with - | ax Γ A => - rw [Finset.insert_union A Γ Δ] - exact ax (Γ ∪ Δ) A - | botE A D => exact botE A <| D.weak Δ - | conjI D D' => exact conjI (D.weak Δ) (D'.weak Δ) - | conjE₁ D => exact conjE₁ <| D.weak Δ - | conjE₂ D => exact conjE₂ <| D.weak Δ - | disjI₁ D => exact disjI₁ <| D.weak Δ - | disjI₂ D => exact disjI₂ <| D.weak Δ +def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) : + (D : Derivation ⟨Γ, A⟩) → Derivation ⟨Γ ∪ Δ, A⟩ + | ax Γ A => (Finset.insert_union A Γ Δ) ▸ ax (Γ ∪ Δ) A + | botE A D => botE A <| D.weak Δ + | conjI D D' => conjI (D.weak Δ) (D'.weak Δ) + | conjE₁ D => conjE₁ <| D.weak Δ + | conjE₂ D => conjE₂ <| D.weak Δ + | disjI₁ D => disjI₁ <| D.weak Δ + | disjI₂ D => disjI₂ <| D.weak Δ | @disjE _ _ _ A B _ D D' D'' => - apply disjE (D.weak Δ) - · rw [←Finset.insert_union A Γ Δ]; exact D'.weak Δ - · rw [←Finset.insert_union B Γ Δ]; exact D''.weak Δ - | @implI _ _ A B Γ D => - apply implI - rw [←Finset.insert_union A Γ Δ]; exact D.weak Δ - | implE D D' => exact implE (D.weak Δ) (D'.weak Δ) + disjE (D.weak Δ) + ((Finset.insert_union A Γ Δ) ▸ D'.weak Δ) + ((Finset.insert_union B Γ Δ) ▸ D''.weak Δ) + | @implI _ _ A B Γ D => implI (Γ ∪ Δ) <| (Finset.insert_union A Γ Δ) ▸ D.weak Δ + | implE D D' => implE (D.weak Δ) (D'.weak Δ) theorem Derivable.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Γ ∪ Δ, A⟩ := by @@ -155,11 +149,9 @@ def Derivation.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h : Γ ⊆ Δ) ( Derivation ⟨Δ, A⟩ := Finset.union_sdiff_of_subset h ▸ D.weak (Δ \ Γ) theorem Derivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) - (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Δ, A⟩ := by - let ⟨D⟩ := h - exact ⟨D.weak' h_ext⟩ + (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Δ, A⟩ := let ⟨D⟩ := h; ⟨D.weak' h_ext⟩ -/-- Substitution of a derivation `E` for one of the hypotheses in the context `Gamma` of `D`. -/ +/-- Substitution of a derivation `E` for one of the hypotheses in the context `Γ` of `D`. -/ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} (D : Derivation ⟨Γ, B⟩) (E : Derivation ⟨Δ, A⟩) : Derivation ⟨(Γ \ {A}) ∪ Δ, B⟩ := by match D with @@ -169,8 +161,7 @@ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} rw [h, Finset.union_comm] exact E.weak _ case neg h => - have : B ∉ ({A} : Finset (Proposition Atom)) := Finset.notMem_singleton.mpr h - rw [Finset.insert_sdiff_of_notMem (h := this)] + rw [Finset.insert_sdiff_of_notMem (h := Finset.notMem_singleton.mpr h)] exact (ax _ B).weak _ | botE _ D => exact botE B <| D.subs E | conjI D D' => exact conjI (D.subs E) (D'.subs E) From c3378c4bca080df1811fffe5a60b42f6caed6ab3 Mon Sep 17 00:00:00 2001 From: twwar Date: Fri, 3 Oct 2025 15:31:18 +0200 Subject: [PATCH 04/12] conditional derivability --- Cslib/Logics/IPL/NJ/Defs.lean | 245 +++++++++++++++++++++++++++------- 1 file changed, 194 insertions(+), 51 deletions(-) diff --git a/Cslib/Logics/IPL/NJ/Defs.lean b/Cslib/Logics/IPL/NJ/Defs.lean index 45c539c2..b6a5ed23 100644 --- a/Cslib/Logics/IPL/NJ/Defs.lean +++ b/Cslib/Logics/IPL/NJ/Defs.lean @@ -63,6 +63,11 @@ open Proposition /-- Contexts are finsets of propositions. -/ abbrev Ctx (Atom) := Finset (Proposition Atom) +/-- Theories are abitrary sets of propositions. -/ +abbrev Theory (Atom) := Set (Proposition Atom) + +abbrev Theory.empty (Atom) : Theory (Atom) := ∅ + /-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ abbrev Sequent (Atom) := Ctx Atom × Proposition Atom @@ -93,17 +98,40 @@ inductive Derivation : Sequent Atom → Type _ where | implE {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, impl A B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ +inductive Theory.Derivable (T : Theory Atom) (A : Proposition Atom) : Prop + | der (Γ : Ctx Atom) (hΓ : ↑Γ ⊆ T) (D : Derivation ⟨Γ, A⟩) : T.Derivable A + +theorem Theory.Derivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (A : Proposition Atom) : + T.Derivable A → T'.Derivable A + | .der Γ hΓ D => ⟨Γ, fun ⦃_⦄ a_1 => hT (hΓ a_1), D⟩ + /-- A sequent is derivable if it has a derivation. -/ -def Derivable (S : Sequent Atom) := Nonempty (Derivation S) +abbrev Theory.SDerivable (T : Theory Atom) (S : Sequent Atom) := Theory.Derivable (T ∪ ↑S.1) S.2 + +theorem Theory.SDerivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (S : Sequent Atom) : + T.SDerivable S → T'.SDerivable S + | .der Γ hΓ D => ⟨Γ, by grind, D⟩ /-- A proposition is derivable if it has a derivation from the empty context. -/ -def Proposition.PDerivable (A : Proposition Atom) := Nonempty (Derivation ⟨∅,A⟩) +abbrev Derivable : Proposition Atom → Prop := Theory.empty Atom |>.Derivable + +abbrev SDerivable : Sequent Atom → Prop := Theory.empty Atom |>.SDerivable + +theorem Derivable_iff (A : Proposition Atom) : Derivable A ↔ Nonempty (Derivation ⟨∅, A⟩) := by + constructor + · intro ⟨Γ, hΓ, D⟩ + exact Finset.eq_empty_of_forall_notMem hΓ ▸ ⟨D⟩ + · intro ⟨D⟩ + refine ⟨∅, by simp, D⟩ /-- An equivalence between A and B is a derivation of B from A and vice-versa. -/ def Proposition.equiv (A B : Proposition Atom) := Derivation ⟨{A},B⟩ × Derivation ⟨{B},A⟩ +def Theory.Equiv (T : Theory Atom) (A B : Proposition Atom) := + T.Derivable (A.impl B) ∧ T.Derivable (B.impl A) + /-- Two propositions A and B are equivalent if B can be derived from A and vice-versa. -/ -def Proposition.Equiv (A B : Proposition Atom) := Derivable ⟨{A},B⟩ ∧ Derivable ⟨{B},A⟩ +abbrev Equiv : Proposition Atom → Proposition Atom → Prop := Theory.empty Atom |>.Equiv open Derivation @@ -113,7 +141,11 @@ def Proposition.top : Proposition Atom := impl bot bot def derivationTop : Derivation (Atom := Atom) ⟨∅, Proposition.top⟩ := implI ∅ <| ax (Atom := Atom) ∅ bot -theorem top_derivable : Proposition.PDerivable (Atom := Atom) Proposition.top := ⟨derivationTop⟩ +theorem Theory.top_derivable (T : Theory Atom) : T.Derivable Proposition.top := by + refine ⟨∅, by simp, derivationTop⟩ + +theorem top_derivable : Derivable (Atom := Atom) Proposition.top := + Theory.top_derivable (Theory.empty Atom) /-! ### Common proof patterns -/ @@ -140,16 +172,32 @@ def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) : | @implI _ _ A B Γ D => implI (Γ ∪ Δ) <| (Finset.insert_union A Γ Δ) ▸ D.weak Δ | implE D D' => implE (D.weak Δ) (D'.weak Δ) -theorem Derivable.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) - (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Γ ∪ Δ, A⟩ := by - let ⟨D⟩ := h - exact ⟨D.weak Δ⟩ - def Derivation.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h : Γ ⊆ Δ) (D : Derivation ⟨Γ, A⟩) : Derivation ⟨Δ, A⟩ := Finset.union_sdiff_of_subset h ▸ D.weak (Δ \ Γ) -theorem Derivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) - (h : Derivable ⟨Γ, A⟩) : Derivable ⟨Δ, A⟩ := let ⟨D⟩ := h; ⟨D.weak' h_ext⟩ +lemma sDerivable_iff (S : Sequent Atom) : SDerivable S ↔ Nonempty (Derivation S) := by + constructor + · intro ⟨Γ, hΓ, D⟩ + refine ⟨D.weak' ?_⟩ + simpa using hΓ + · intro ⟨D⟩ + refine ⟨S.1, by simp, D⟩ + +theorem Theory.SDerivable.sequent_weak (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} : + T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ ∪ Δ, A⟩ + | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind + +theorem Theory.SDerivable.sequent_weak' (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} + (h_ext : Γ ⊆ Δ) : T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Δ, A⟩ + | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind + +theorem SDerivable.weak {Γ Δ : Ctx Atom} {A : Proposition Atom} (_ : SDerivable ⟨Γ, A⟩) : + SDerivable ⟨Γ ∪ Δ, A⟩ := by + apply Theory.SDerivable.sequent_weak; assumption + +theorem SDerivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) + (_ : SDerivable ⟨Γ, A⟩) : SDerivable ⟨Δ, A⟩ := by + apply Theory.SDerivable.sequent_weak' <;> assumption /-- Substitution of a derivation `E` for one of the hypotheses in the context `Γ` of `D`. -/ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} @@ -205,9 +253,10 @@ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} exact D.subs E | implE D D' => exact implE (D.subs E) (D'.subs E) -theorem Derivable.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} - (h₁ : Derivable ⟨Γ, B⟩) (h₂ : Derivable ⟨Δ, A⟩) : Derivable ⟨(Γ \ {A}) ∪ Δ, B⟩ := - let ⟨D⟩ := h₁; let ⟨E⟩ := h₂; ⟨D.subs E⟩ +theorem Theory.SDerivable.subs {T : Theory Atom} {Γ Δ : Ctx Atom} {A B : Proposition Atom} : + T.SDerivable ⟨Γ, B⟩ → T.SDerivable ⟨Δ, A⟩ → T.SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ + | .der Γ' hΓ' D, .der Δ' hΔ' E => + ⟨Γ' \ {A} ∪ Δ', by grind [Finset.coe_union, Finset.coe_sdiff], D.subs E⟩ def Derivation.subs' {Γ : Ctx Atom} {A B : Proposition Atom} (D : Derivation ⟨{A}, B⟩) (E : Derivation ⟨Γ, A⟩) : Derivation ⟨Γ, B⟩ := by @@ -215,28 +264,116 @@ def Derivation.subs' {Γ : Ctx Atom} {A B : Proposition Atom} rw [this] exact D.subs E -theorem Derivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} - (h : Derivable ⟨{A}, B⟩) (h' : Derivable ⟨Γ, A⟩) : Derivable ⟨Γ, B⟩ := - let ⟨D⟩ := h; let ⟨E⟩ := h'; ⟨D.subs' E⟩ +theorem Theory.SDerivable.subs' {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : + T.Derivable (A.impl B) → T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ, B⟩ + | ⟨Δ, hΔ, E⟩, ⟨Γ', hΓ', D⟩ => by + refine ⟨Δ ∪ Γ', by grind, ?_⟩ + apply implE (A := A) + · exact E.weak' (by grind) + · exact D.weak' (by grind) + +theorem SDerivable.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} : + SDerivable ⟨Γ, B⟩ → SDerivable ⟨Δ, A⟩ → SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ := Theory.SDerivable.subs + +theorem SDerivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} : + (h : Derivable (A.impl B)) → (h' : SDerivable ⟨Γ, A⟩) → SDerivable ⟨Γ, B⟩ := + Theory.SDerivable.subs' + +/-! ### Inference rules for derivability -/ + +theorem Theory.Derivable.ax' {T : Theory Atom} {A : Proposition Atom} (h : A ∈ T) : + T.Derivable A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ + +theorem Theory.Derivable.botE {T : Theory Atom} (A : Proposition Atom) : + T.Derivable Proposition.bot → T.Derivable A + | ⟨Γ, h, D⟩ => ⟨Γ, h, Derivation.botE A D⟩ + +theorem Theory.Derivable.conjI {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable A → T.Derivable B → T.Derivable (A.conj B) + | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => + ⟨Γ ∪ Γ', by grind, Derivation.conjI (D.weak' (by grind)) (D'.weak' (by grind))⟩ + +theorem Theory.Derivable.conjE₁ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable (A.conj B) → T.Derivable A + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₁⟩ + +theorem Theory.Derivable.conjE₂ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable (A.conj B) → T.Derivable B + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₂⟩ + +theorem Theory.Derivable.disjI₁ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable A → T.Derivable (A.disj B) + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₁⟩ + +theorem Theory.Derivable.disjI₂ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable B → T.Derivable (A.disj B) + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₂⟩ + +theorem Theory.Derivable.disjE {T : Theory Atom} {A B C : Proposition Atom} : + T.Derivable (A.disj B) → T.Derivable (A.impl C) → T.Derivable (B.impl C) → T.Derivable C + | ⟨Γ, h, D⟩, ⟨Δ₁, h₁, E₁⟩, ⟨Δ₂, h₂, E₂⟩ => by + refine ⟨Γ ∪ Δ₁ ∪ Δ₂, by grind, ?_⟩ + apply Derivation.disjE (A := A) (B := B) + · exact D.weak' (by grind) + · apply Derivation.implE (A := A) + · exact E₁.weak' (by grind) + · exact Derivation.ax' (by grind) + · apply Derivation.implE (A := B) + · exact E₂.weak' (by grind) + · exact Derivation.ax' (by grind) + +theorem Theory.Derivable.implE {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable (A.impl B) → T.Derivable A → T.Derivable B + | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by + refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ + exact Derivation.implE (A := A) (D₁.weak' (by grind)) (D₂.weak' (by grind)) + +theorem Theory.Derivable.trans {T : Theory Atom} {A B C : Proposition Atom} : + T.Derivable (A.impl B) → T.Derivable (B.impl C) → T.Derivable (A.impl C) + | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by + refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ + apply implI + apply Derivation.implE (A := B) + · exact D₂.weak' (by grind) + · apply Derivation.implE (A := A) + · exact D₁.weak' (by grind) + · exact Derivation.ax' (by grind) /-! ### Properties of NJ-equivalence -/ -theorem Proposition.derivable_iff_equiv_top (A : Proposition Atom) : - PDerivable A ↔ Proposition.Equiv A top := by +theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition Atom) : + T.Derivable A ↔ T.Equiv A top := by constructor <;> intro h · constructor - · exact ⟨derivationTop.weak' (Δ := {A}) (by grind)⟩ - · let ⟨D⟩ := h - exact ⟨D.weak' (Δ := {Proposition.top}) (by grind)⟩ - · let ⟨D⟩ := h.2 - exact ⟨D.subs' derivationTop⟩ + · refine ⟨∅, by grind, ?_⟩ + exact implI (A := A) (B := Proposition.top) ∅ <| derivationTop.weak' (by grind) + · let ⟨Γ, hΓ, D⟩ := h + refine ⟨Γ, by grind, ?_⟩ + refine implI Γ <| D.weak' (by grind) + · let ⟨Γ, hΓ, D⟩ := h.2 + refine ⟨Γ, by grind, ?_⟩ + exact implE (A := Proposition.top) D <| derivationTop.weak' (by grind) /-- Change the conclusion along an equivalence. -/ def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ := e.1.subs' -theorem equivalent_derivability (Γ : Ctx Atom) {A B : Proposition Atom} (h : Proposition.Equiv A B) - : Derivable ⟨Γ, A⟩ ↔ Derivable ⟨Γ, B⟩ := ⟨h.1.subs', h.2.subs'⟩ +theorem Theory.equivalent_sDerivable_conclusion {T : Theory Atom} (Γ : Ctx Atom) + {A B : Proposition Atom} (h : T.Equiv A B) : T.SDerivable ⟨Γ, A⟩ ↔ T.SDerivable ⟨Γ, B⟩ := by + let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h + constructor <;> intro ⟨Γ', hΓ, D⟩ + · refine ⟨Γ₁ ∪ Γ', by grind, ?_⟩ + apply implE (A := A) + · exact D₁.weak' (by grind) + · exact D.weak' (by grind) + · refine ⟨Γ₂ ∪ Γ', by grind, ?_⟩ + apply implE (A := B) + · exact D₂.weak' (by grind) + · exact D.weak' (by grind) + +theorem equivalent_sDerivable_conclusion (Γ : Ctx Atom) {A B : Proposition Atom} (h : Equiv A B) : + SDerivable ⟨Γ, A⟩ ↔ SDerivable ⟨Γ, B⟩ := + (Theory.empty Atom).equivalent_sDerivable_conclusion Γ h /-- Replace a hypothesis along an equivalence. -/ def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) @@ -246,20 +383,25 @@ def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition refine D.subs ?_ exact e.2.weak' (by grind) -theorem equivalent_hypotheses (Γ : Ctx Atom) {A B : Proposition Atom} (h : Proposition.Equiv A B) - (C : Proposition Atom) : Derivable ⟨insert A Γ, C⟩ ↔ Derivable ⟨insert B Γ, C⟩ := by - let ⟨⟨D⟩, ⟨D'⟩⟩ := h - constructor - · intro ⟨DA⟩ - have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind +theorem equivalent_hypotheses {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} + (h : T.Equiv A B) (C : Proposition Atom) : + T.SDerivable ⟨insert A Γ, C⟩ ↔ T.SDerivable ⟨insert B Γ, C⟩ := by + let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h + constructor <;> intro h' + · have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind rw [this] - refine ⟨DA.subs ?_⟩ - exact D'.weak' (by grind) - · intro ⟨DB⟩ - have : insert A Γ = (insert B Γ \ {B}) ∪ (insert A Γ) := by grind + apply Theory.SDerivable.subs h' + refine ⟨insert B Γ₁ ∪ Γ₂, by grind, ?_⟩ + apply implE (A := B) + · exact D₂.weak' (by grind) + · exact ax' (by grind) + · have : insert A Γ = (insert B Γ \ {B}) ∪ (insert A Γ) := by grind rw [this] - refine ⟨DB.subs ?_⟩ - exact D.weak' (by grind) + apply Theory.SDerivable.subs h' + refine ⟨insert A Γ₂ ∪ Γ₁, by grind, ?_⟩ + apply implE (A := A) + · exact D₁.weak' (by grind) + · exact ax' (by grind) def reflEquiv (A : Proposition Atom) : Proposition.equiv A A := let D : Derivation ⟨{A},A⟩ := ax' <| by grind; @@ -268,26 +410,27 @@ def reflEquiv (A : Proposition Atom) : Proposition.equiv A A := def commEquiv {A B : Proposition Atom} (e : Proposition.equiv A B) : Proposition.equiv B A := ⟨e.2, e.1⟩ -def transEquiv {A B C : Proposition Atom} (e : Proposition.Equiv A B) (e' : Proposition.Equiv B C) : - Proposition.Equiv A C := ⟨e'.1.subs' e.1, e.2.subs' e'.2⟩ +def transEquiv {A B C : Proposition Atom} (eAB : Proposition.equiv A B) + (eBC : Proposition.equiv B C) : Proposition.equiv A C := + ⟨mapEquivConclusion _ eBC eAB.1, mapEquivConclusion _ (commEquiv eAB) eBC.2⟩ -theorem equivalent_refl (A : Proposition Atom) : Proposition.Equiv A A := by - have : Derivable ⟨{A},A⟩ := ⟨ax' <| by grind⟩ - grind [Proposition.Equiv] +theorem equivalent_refl {T : Theory Atom} (A : Proposition Atom) : T.Equiv A A := by + have : T.Derivable (A.impl A) := by refine ⟨∅, by grind, ?_⟩; apply implI; exact ax' (by grind) + grind [Theory.Equiv] -theorem equivalent_comm {A B : Proposition Atom} : - Proposition.Equiv A B → Proposition.Equiv B A := by grind [Proposition.Equiv] +theorem equivalent_comm {T : Theory Atom} {A B : Proposition Atom} : + T.Equiv A B → T.Equiv B A := by grind [Theory.Equiv] -theorem equivalent_trans {A B C : Proposition Atom} : - Proposition.Equiv A B → Proposition.Equiv B C → Proposition.Equiv A C := by - grind [Proposition.Equiv, Derivable.subs'] +theorem equivalent_trans {T : Theory Atom} {A B C : Proposition Atom} : + T.Equiv A B → T.Equiv B C → T.Equiv A C + | ⟨AB, BA⟩, ⟨BC, CB⟩ => ⟨AB.trans BC, CB.trans BA⟩ /-- Equivalence is indeed an equivalence relation. -/ -theorem equiv_equivalence : Equivalence (Proposition.Equiv (Atom := Atom)) := +theorem Theory.equiv_equivalence (T : Theory Atom) : Equivalence (T.Equiv (Atom := Atom)) := ⟨equivalent_refl, equivalent_comm, equivalent_trans⟩ -protected def propositionSetoid : Setoid (Proposition Atom) := - ⟨Proposition.Equiv, equiv_equivalence⟩ +protected def Theory.propositionSetoid (T : Theory Atom) : Setoid (Proposition Atom) := + ⟨T.Equiv, T.equiv_equivalence⟩ end NJ From a98f065549900737739891b19c947046cebbb642 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 4 Oct 2025 16:42:26 +0200 Subject: [PATCH 05/12] fix theorems --- Cslib/Logics/IPL/NJ/Basic.lean | 700 ++++++++++++++++++------------ Cslib/Logics/IPL/NJ/Defs.lean | 437 ------------------- Cslib/Logics/IPL/NJ/Theorems.lean | 331 ++++++++++++++ 3 files changed, 743 insertions(+), 725 deletions(-) delete mode 100644 Cslib/Logics/IPL/NJ/Defs.lean create mode 100644 Cslib/Logics/IPL/NJ/Theorems.lean diff --git a/Cslib/Logics/IPL/NJ/Basic.lean b/Cslib/Logics/IPL/NJ/Basic.lean index c8a0441c..13504e4d 100644 --- a/Cslib/Logics/IPL/NJ/Basic.lean +++ b/Cslib/Logics/IPL/NJ/Basic.lean @@ -3,323 +3,447 @@ Copyright (c) 2025 Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Logics.IPL.NJ.Defs +import Mathlib.Data.Finset.Insert +import Mathlib.Data.Finset.SDiff -/-! # Elementary derivations and equivalences in NJ -/ +/-! +# Gentzen's NJ + +Natural deduction for intuitionistic propositional logic. + +## Main definitions + +- `Proposition` : a type of propositions with atoms in a given type. +- `Derivation` : natural deduction derivation, done in "sequent style", ie with explicit +hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit contraction +and exchange, and the axiom rule derives `{A} ∪ Γ ⊢ A` for any context `Γ`, allowing weakening to +be a derived rule. +- `Derivable` : defined as `Nonempty (Derivation S)`. +- `Proposition.equiv` and `Proposition.Equiv` : `Type`- and `Prop`-valued equivalence of +propositions. + +## Main results + +- `Derivation.weak` : weakening as a derived rule. +- `Derivation.subs` : substituting a derivation for a hypothesis. +- `equiv_equivalence` : equivalence of propositions is an equivalence. + +## References + +- Dag Prawitz, *Natural Deduction: a proof-theoretical study*. +- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely +presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*. +(Suggestions of better references welcome!) +-/ + +universe u variable {Atom : Type u} [DecidableEq Atom] namespace IPL -open Proposition +/-- Propositions. We view negation as a defined connective ~A := A → ⊥ -/ +inductive Proposition (Atom : Type u) : Type u where + /-- Propositional atoms -/ + | atom (x : Atom) + /-- Falsum -/ + | bot + /-- Conjunction -/ + | conj (a b : Proposition Atom) + /-- Disjunction -/ + | disj (a b : Proposition Atom) + /-- Implication -/ + | impl (a b : Proposition Atom) +deriving DecidableEq, BEq namespace NJ -open Derivation +open Proposition -/-! -### Negation theorems +/-- Contexts are finsets of propositions. -/ +abbrev Ctx (Atom) := Finset (Proposition Atom) + +/-- Theories are abitrary sets of propositions. -/ +abbrev Theory (Atom) := Set (Proposition Atom) + +abbrev Theory.empty (Atom) : Theory (Atom) := ∅ + +/-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ +abbrev Sequent (Atom) := Ctx Atom × Proposition Atom + +/-- A derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ. -/ +inductive Derivation : Sequent Atom → Type _ where + /-- Axiom (or assumption) -/ + | ax (Γ : Ctx Atom) (A : Proposition Atom) : Derivation ⟨insert A Γ, A⟩ + /-- Falsum elimination (ex falso quodlibet) -/ + | botE {Γ : Ctx Atom} (A : Proposition Atom) : Derivation ⟨Γ, bot⟩ → Derivation ⟨Γ, A⟩ + /-- Conjunction introduction -/ + | conjI {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, conj A B⟩ + /-- Conjunction elimination left -/ + | conjE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, A⟩ + /-- Conjunction elimination right -/ + | conjE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, B⟩ + /-- Disjunction introduction left -/ + | disjI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, disj A B⟩ + /-- Disjunction introduction right -/ + | disjI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, disj A B⟩ + /-- Disjunction elimination -/ + | disjE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation ⟨Γ, disj A B⟩ → + Derivation ⟨insert A Γ, C⟩ → Derivation ⟨insert B Γ, C⟩ → Derivation ⟨Γ, C⟩ + /-- Implication introduction -/ + | implI {A B : Proposition Atom} (Γ : Ctx Atom) : + Derivation ⟨insert A Γ, B⟩ → Derivation ⟨Γ, impl A B⟩ + /-- Implication elimination -/ + | implE {Γ : Ctx Atom} {A B : Proposition Atom} : + Derivation ⟨Γ, impl A B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ + +inductive Theory.Derivable (T : Theory Atom) (A : Proposition Atom) : Prop + | der (Γ : Ctx Atom) (hΓ : ↑Γ ⊆ T) (D : Derivation ⟨Γ, A⟩) : T.Derivable A + +theorem Theory.Derivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (A : Proposition Atom) : + T.Derivable A → T'.Derivable A + | .der Γ hΓ D => ⟨Γ, fun ⦃_⦄ a_1 => hT (hΓ a_1), D⟩ + +/-- A sequent is derivable if it has a derivation. -/ +abbrev Theory.SDerivable (T : Theory Atom) (S : Sequent Atom) := Theory.Derivable (T ∪ ↑S.1) S.2 + +theorem Theory.SDerivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (S : Sequent Atom) : + T.SDerivable S → T'.SDerivable S + | .der Γ hΓ D => ⟨Γ, by grind, D⟩ + +/-- A proposition is derivable if it has a derivation from the empty context. -/ +abbrev Derivable : Proposition Atom → Prop := Theory.empty Atom |>.Derivable + +abbrev SDerivable : Sequent Atom → Prop := Theory.empty Atom |>.SDerivable + +theorem derivable_iff {A : Proposition Atom} : Derivable A ↔ Nonempty (Derivation ⟨∅, A⟩) := by + constructor + · intro ⟨Γ, hΓ, D⟩ + exact Finset.eq_empty_of_forall_notMem hΓ ▸ ⟨D⟩ + · intro ⟨D⟩ + refine ⟨∅, by simp, D⟩ -The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. --/ +/-- An equivalence between A and B is a derivation of B from A and vice-versa. -/ +def Proposition.equiv (A B : Proposition Atom) := Derivation ⟨{A},B⟩ × Derivation ⟨{B},A⟩ -/-- Double negation introduction -/ -def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, impl (impl A B) B⟩ := - implI (A := A.impl B) _ <| - implE (A := A) (ax' (by grind)) (ax' (by grind)) - -theorem Derivable.dni {A B : Proposition Atom} : Derivable ⟨{A},impl (impl A B) B⟩ := - ⟨Derivation.dni⟩ - -/-- The double negation of excluded-middle, or in minimal-logic-style ⊢ (A ∨ (A → B)) → B → B. -/ -def Derivation.notNotLEM {A B : Proposition Atom} : - Derivation ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := - implI _ <| - implE (A := A.disj (A.impl B)) (ax' <| by grind) <| - disjI₂ <| - implI _ <| - implE (A := A.disj (A.impl B)) (ax' <| by grind) <| - disjI₁ <| - ax' <| by grind - -theorem Derivable.not_not_lem {A B : Proposition Atom} : - Derivable ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := ⟨Derivation.notNotLEM⟩ - -/-- Triple negation elimination -/ -def Derivation.tne {A B : Proposition Atom} : - Derivation ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := - implI _ <| - implE (A := (A.impl B).impl B) (ax' <| by grind) <| - Derivation.dni.weak' (Γ := {A}) (by grind) - -theorem Derivable.tne {A B : Proposition Atom} : - Derivable ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := ⟨Derivation.tne⟩ - -def tneEquiv {A B : Proposition Atom} : - Proposition.equiv (A.impl B) (((A.impl B).impl B).impl B) := ⟨Derivation.dni, Derivation.tne⟩ - -theorem tne_equivalent {A B : Proposition Atom} : - Proposition.Equiv (A.impl B) (((A.impl B).impl B).impl B) := ⟨Derivable.dni, Derivable.tne⟩ - -/-- Modus tollens -/ -def Derivation.modusTollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) - (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B.impl C) Γ, A.impl C⟩ := - implI _ <| - implE (A := B) - (ax' (by grind)) - (D.weak' (h := by grind)) - -theorem Derivable.modus_tollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) - (h : Derivable ⟨insert A Γ, B⟩) : Derivable ⟨insert (B.impl C) Γ, A.impl C⟩ := - let ⟨D⟩ := h; ⟨D.modusTollens C⟩ +def Theory.Equiv (T : Theory Atom) (A B : Proposition Atom) := + T.Derivable (A.impl B) ∧ T.Derivable (B.impl A) -/-! -### De Morgan laws +/-- Two propositions A and B are equivalent if B can be derived from A and vice-versa. -/ +abbrev Equiv : Proposition Atom → Proposition Atom → Prop := Theory.empty Atom |>.Equiv -The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. --/ +open Derivation -/-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ -def disjImpOfConjImps {A B C : Proposition Atom} : - Derivation ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := - implI _ <| - disjE (A := A) (B := B) - (ax _ _) - (implE (A := A) - (conjE₁ (B := B.impl C) (ax' <| by grind)) - (ax _ _)) - (implE (A := B) - (conjE₂ (A := A.impl C) (ax' (by grind))) - (ax _ _)) - -/-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ -theorem disj_imp_of_conj_imps {A B C : Proposition Atom} : - Derivable ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := ⟨disjImpOfConjImps⟩ - -/-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ -def conjImpsOfDisjImp {A B C : Proposition Atom} : - Derivation ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := - conjI - (implI {impl (disj A B) C} <| - implE (A := A.disj B) (B := C) - (ax' (by grind)) - (disjI₁ (ax _ _))) - (implI {impl (disj A B) C} <| - implE (A := A.disj B) (B := C) - (ax' (by grind)) - (disjI₂ (ax _ _))) - -/-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ -theorem conj_imps_of_disj_imp {A B C : Proposition Atom} : - Derivable ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := ⟨conjImpsOfDisjImp⟩ - -def disjImpConjImpsEquiv {A B C : Proposition Atom} : - Proposition.equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := - ⟨conjImpsOfDisjImp, disjImpOfConjImps⟩ - -theorem disj_imp_conj_imps_equivalent {A B C : Proposition Atom} : - Proposition.Equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := - ⟨conj_imps_of_disj_imp, disj_imp_of_conj_imps⟩ - -/-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ -def conjImpOfDisjImps {A B C : Proposition Atom} : - Derivation ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := by - apply implI - apply disjE (A := A.impl C) (B := B.impl C) - · exact ax' (by grind) - · apply implE (A := A) - · apply ax - · apply conjE₁ (B := B) - exact ax' (by grind) - · apply implE (A := B) - · apply ax - · apply conjE₂ (A := A) - exact ax' (by grind) - -/-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ -theorem conj_imp_of_disj_imps {A B C : Proposition Atom} : - Derivable ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := ⟨conjImpOfDisjImps⟩ - -/-! ### Further equivalences and implications -/ - -/-- Equivalence of A → (B → C) and (A ∧ B) → C -/ -def curryEquiv {A B C : Proposition Atom} : - Proposition.equiv (A.impl (B.impl C)) (impl (A.conj B) C) := by +/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ +def Proposition.top : Proposition Atom := impl bot bot + +def derivationTop : Derivation (Atom := Atom) ⟨∅, Proposition.top⟩ := + implI ∅ <| ax (Atom := Atom) ∅ bot + +theorem Theory.top_derivable (T : Theory Atom) : T.Derivable Proposition.top := by + refine ⟨∅, by simp, derivationTop⟩ + +theorem top_derivable : Derivable (Atom := Atom) Proposition.top := + Theory.top_derivable (Theory.empty Atom) + +/-! ### Common proof patterns -/ + +/-- A convenient reformulation of the axiom rule. -/ +def Derivation.ax' {Γ : Ctx Atom} {A : Proposition Atom} (h : A ∈ Γ) : Derivation ⟨Γ,A⟩ := by + have : Γ = insert A Γ := by grind + rw [this] + apply ax + +/-- Weakening is a derived rule. -/ +def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) : + (D : Derivation ⟨Γ, A⟩) → Derivation ⟨Γ ∪ Δ, A⟩ + | ax Γ A => (Finset.insert_union A Γ Δ) ▸ ax (Γ ∪ Δ) A + | botE A D => botE A <| D.weak Δ + | conjI D D' => conjI (D.weak Δ) (D'.weak Δ) + | conjE₁ D => conjE₁ <| D.weak Δ + | conjE₂ D => conjE₂ <| D.weak Δ + | disjI₁ D => disjI₁ <| D.weak Δ + | disjI₂ D => disjI₂ <| D.weak Δ + | @disjE _ _ _ A B _ D D' D'' => + disjE (D.weak Δ) + ((Finset.insert_union A Γ Δ) ▸ D'.weak Δ) + ((Finset.insert_union B Γ Δ) ▸ D''.weak Δ) + | @implI _ _ A B Γ D => implI (Γ ∪ Δ) <| (Finset.insert_union A Γ Δ) ▸ D.weak Δ + | implE D D' => implE (D.weak Δ) (D'.weak Δ) + +def Derivation.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h : Γ ⊆ Δ) (D : Derivation ⟨Γ, A⟩) : + Derivation ⟨Δ, A⟩ := Finset.union_sdiff_of_subset h ▸ D.weak (Δ \ Γ) + +theorem sDerivable_iff {S : Sequent Atom} : SDerivable S ↔ Nonempty (Derivation S) := by constructor - · apply implI - apply implE (A := B) - · apply implE (A := A) - · exact ax' (by grind) - · apply conjE₁ (B := B) - exact ax' (by grind) - · apply conjE₂ (A := A) - exact ax' (by grind) - · apply implI + · intro ⟨Γ, hΓ, D⟩ + refine ⟨D.weak' ?_⟩ + simpa using hΓ + · intro ⟨D⟩ + refine ⟨S.1, by simp, D⟩ + +theorem Theory.SDerivable.sequent_weak (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} : + T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ ∪ Δ, A⟩ + | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind + +theorem Theory.SDerivable.sequent_weak' (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} + (h_ext : Γ ⊆ Δ) : T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Δ, A⟩ + | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind + +theorem SDerivable.weak {Γ Δ : Ctx Atom} {A : Proposition Atom} (_ : SDerivable ⟨Γ, A⟩) : + SDerivable ⟨Γ ∪ Δ, A⟩ := by + apply Theory.SDerivable.sequent_weak; assumption + +theorem SDerivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) + (_ : SDerivable ⟨Γ, A⟩) : SDerivable ⟨Δ, A⟩ := by + apply Theory.SDerivable.sequent_weak' <;> assumption + +/-- Substitution of a derivation `E` for one of the hypotheses in the context `Γ` of `D`. -/ +def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} + (D : Derivation ⟨Γ, B⟩) (E : Derivation ⟨Δ, A⟩) : Derivation ⟨(Γ \ {A}) ∪ Δ, B⟩ := by + match D with + | ax _ _ => + by_cases B = A + case pos h => + rw [h, Finset.union_comm] + exact E.weak _ + case neg h => + rw [Finset.insert_sdiff_of_notMem (h := Finset.notMem_singleton.mpr h)] + exact (ax _ B).weak _ + | botE _ D => exact botE B <| D.subs E + | conjI D D' => exact conjI (D.subs E) (D'.subs E) + | conjE₁ D => exact conjE₁ <| D.subs E + | conjE₂ D => exact conjE₂ <| D.subs E + | disjI₁ D => exact disjI₁ <| D.subs E + | disjI₂ D => exact disjI₂ <| D.subs E + | @disjE _ _ _ C C' B D D' D'' => + apply disjE (D.subs E) + · by_cases C = A + case pos h => + rw [h] at D' ⊢ + have : insert A ((Γ \ {A}) ∪ Δ) = (insert A Γ) ∪ Δ := by grind + rw [this] + exact D'.weak _ + case neg h => + have : insert C ((Γ \ {A}) ∪ Δ) = ((insert C Γ) \ {A}) ∪ Δ := by grind + rw [this] + exact D'.subs E + · by_cases C' = A + case pos h => + rw [h] at D'' ⊢ + have : insert A ((Γ \ {A}) ∪ Δ) = (insert A Γ) ∪ Δ := by grind + rw [this] + exact D''.weak _ + case neg h => + have : insert C' ((Γ \ {A}) ∪ Δ) = ((insert C' Γ) \ {A}) ∪ Δ := by grind + rw [this] + exact D''.subs E + | @implI _ _ A' B _ D => apply implI - apply implE (A := A.conj B) - · exact ax' (by grind) - · apply conjI <;> exact ax' (by grind) - -/-- Equivalence of A → (B → C) and (A ∧ B) → C -/ -theorem curry_equiv {A B C : Proposition Atom} : - Proposition.Equiv (A.impl (B.impl C)) (impl (A.conj B) C) := ⟨⟨curryEquiv.1⟩, ⟨curryEquiv.2⟩⟩ - -/-- A ∧ B ⊢ B ∧ A -/ -def conjCommDer {A B : Proposition Atom} : Derivation ⟨{A.conj B}, B.conj A⟩ := by - apply conjI - · apply conjE₂ (A := A) - exact ax' (by grind) - · apply conjE₁ (B := B) - exact ax' (by grind) - -/-- Equivalence of A ∧ B and B ∧ A -/ -def conjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.conj B) (B.conj A) := - ⟨conjCommDer, conjCommDer⟩ - -/-- Equivalence of A ∧ B and B ∧ A -/ -theorem conj_comm_equiv {A B : Proposition Atom} : Proposition.Equiv (A.conj B) (B.conj A) := - ⟨⟨conjCommDer⟩, ⟨conjCommDer⟩⟩ - -/-- Equivalence of A ∧ A and A -/ -def conjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.conj A) A := by - constructor - · apply conjE₁ (B := A) - exact ax' (by grind) - · apply conjI <;> exact ax' (by grind) - -/-- Equivalence of A ∧ A and A -/ -theorem conj_idem_equiv {A : Proposition Atom} : Proposition.Equiv (A.conj A) A := - ⟨⟨conjIdemEquiv.1⟩, ⟨conjIdemEquiv.2⟩⟩ - -/-- A ∨ B ⊢ B ∨ A -/ -def disjCommDer {A B : Proposition Atom} : Derivation ⟨{A.disj B}, B.disj A⟩ := by - apply disjE (A := A) (B := B) - · exact ax' (by grind) - · apply disjI₂ - exact ax' (by grind) - · apply disjI₁ - exact ax' (by grind) - -/-- Equivalence of A ∨ B and B ∨ A -/ -def disjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.disj B) (B.disj A) := - ⟨disjCommDer, disjCommDer⟩ - -/-- Equivalence of A ∨ B and B ∨ A -/ -theorem disj_comm_equiv {A B : Proposition Atom} : Proposition.Equiv (A.disj B) (B.disj A) := - ⟨⟨disjCommDer⟩, ⟨disjCommDer⟩⟩ - -/-- Equivalence of A ∨ A and A -/ -def disjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.disj A) A := by - constructor - · apply disjE (A := A) (B := A) <;> exact ax' (by grind) - · apply disjI₁ - exact ax' (by grind) + by_cases A' = A + case pos h => + rw [h] at D ⊢ + have : insert A (Γ \ {A} ∪ Δ) = insert A Γ ∪ Δ := by grind + rw [this] + exact D.weak Δ + case neg h => + have : insert A' ((Γ \ {A}) ∪ Δ) = ((insert A' Γ) \ {A}) ∪ Δ := by grind + rw [this] + exact D.subs E + | implE D D' => exact implE (D.subs E) (D'.subs E) + +theorem Theory.SDerivable.subs {T : Theory Atom} {Γ Δ : Ctx Atom} {A B : Proposition Atom} : + T.SDerivable ⟨Γ, B⟩ → T.SDerivable ⟨Δ, A⟩ → T.SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ + | .der Γ' hΓ' D, .der Δ' hΔ' E => + ⟨Γ' \ {A} ∪ Δ', by grind [Finset.coe_union, Finset.coe_sdiff], D.subs E⟩ + +def Derivation.subs' {Γ : Ctx Atom} {A B : Proposition Atom} + (D : Derivation ⟨{A}, B⟩) (E : Derivation ⟨Γ, A⟩) : Derivation ⟨Γ, B⟩ := by + have : Γ = ({A} \ {A}) ∪ Γ := by grind + rw [this] + exact D.subs E + +theorem Theory.SDerivable.subs' {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : + T.Derivable (A.impl B) → T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ, B⟩ + | ⟨Δ, hΔ, E⟩, ⟨Γ', hΓ', D⟩ => by + refine ⟨Δ ∪ Γ', by grind, ?_⟩ + apply implE (A := A) + · exact E.weak' (by grind) + · exact D.weak' (by grind) + +theorem SDerivable.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} : + SDerivable ⟨Γ, B⟩ → SDerivable ⟨Δ, A⟩ → SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ := Theory.SDerivable.subs + +theorem SDerivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} : + (h : Derivable (A.impl B)) → (h' : SDerivable ⟨Γ, A⟩) → SDerivable ⟨Γ, B⟩ := + Theory.SDerivable.subs' + +/-! ### Inference rules for derivability -/ + +theorem Theory.Derivable.ax' {T : Theory Atom} {A : Proposition Atom} (h : A ∈ T) : + T.Derivable A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ + +theorem Theory.Derivable.botE {T : Theory Atom} (A : Proposition Atom) : + T.Derivable Proposition.bot → T.Derivable A + | ⟨Γ, h, D⟩ => ⟨Γ, h, Derivation.botE A D⟩ + +theorem Theory.Derivable.conjI {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable A → T.Derivable B → T.Derivable (A.conj B) + | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => + ⟨Γ ∪ Γ', by grind, Derivation.conjI (D.weak' (by grind)) (D'.weak' (by grind))⟩ + +theorem Theory.Derivable.conjE₁ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable (A.conj B) → T.Derivable A + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₁⟩ + +theorem Theory.Derivable.conjE₂ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable (A.conj B) → T.Derivable B + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₂⟩ + +theorem Theory.Derivable.disjI₁ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable A → T.Derivable (A.disj B) + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₁⟩ + +theorem Theory.Derivable.disjI₂ {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable B → T.Derivable (A.disj B) + | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₂⟩ + +theorem Theory.Derivable.disjE {T : Theory Atom} {A B C : Proposition Atom} : + T.Derivable (A.disj B) → T.Derivable (A.impl C) → T.Derivable (B.impl C) → T.Derivable C + | ⟨Γ, h, D⟩, ⟨Δ₁, h₁, E₁⟩, ⟨Δ₂, h₂, E₂⟩ => by + refine ⟨Γ ∪ Δ₁ ∪ Δ₂, by grind, ?_⟩ + apply Derivation.disjE (A := A) (B := B) + · exact D.weak' (by grind) + · apply Derivation.implE (A := A) + · exact E₁.weak' (by grind) + · exact Derivation.ax' (by grind) + · apply Derivation.implE (A := B) + · exact E₂.weak' (by grind) + · exact Derivation.ax' (by grind) + +theorem Theory.Derivable.implE {T : Theory Atom} {A B : Proposition Atom} : + T.Derivable (A.impl B) → T.Derivable A → T.Derivable B + | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by + refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ + exact Derivation.implE (A := A) (D₁.weak' (by grind)) (D₂.weak' (by grind)) + +theorem Theory.Derivable.trans {T : Theory Atom} {A B C : Proposition Atom} : + T.Derivable (A.impl B) → T.Derivable (B.impl C) → T.Derivable (A.impl C) + | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by + refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ + apply implI + apply Derivation.implE (A := B) + · exact D₂.weak' (by grind) + · apply Derivation.implE (A := A) + · exact D₁.weak' (by grind) + · exact Derivation.ax' (by grind) -/-- Equivalence of A ∨ A and A -/ -theorem disj_idem_equiv {A : Proposition Atom} : Proposition.Equiv (A.disj A) A := - ⟨⟨disjIdemEquiv.1⟩, ⟨disjIdemEquiv.2⟩⟩ +/-! ### Properties of NJ-equivalence -/ -/-- Equivalence of A → (A → B) and A → B -/ -def implIdemEquiv {A B : Proposition Atom} : - Proposition.equiv (A.impl <| A.impl B) (A.impl B) := by +theorem equiv_iff {A B : Proposition Atom} : Equiv A B ↔ Nonempty (Proposition.equiv A B) := by constructor - · apply implI + · intro ⟨hAB, hBA⟩ + let ⟨DAB⟩ := derivable_iff.mp hAB + let ⟨DBA⟩ := derivable_iff.mp hBA + refine ⟨?_,?_⟩ + · refine Derivation.implE (DAB.weak' (by grind)) (ax' <| by grind) + · refine Derivation.implE (DBA.weak' (by grind)) (ax' <| by grind) + · intro ⟨DAB, DBA⟩ + refine ⟨?_,?_⟩ + all_goals apply derivable_iff.mpr; constructor; apply implI; assumption + + +theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition Atom) : + T.Derivable A ↔ T.Equiv A top := by + constructor <;> intro h + · constructor + · refine ⟨∅, by grind, ?_⟩ + exact implI (A := A) (B := Proposition.top) ∅ <| derivationTop.weak' (by grind) + · let ⟨Γ, hΓ, D⟩ := h + refine ⟨Γ, by grind, ?_⟩ + refine implI Γ <| D.weak' (by grind) + · let ⟨Γ, hΓ, D⟩ := h.2 + refine ⟨Γ, by grind, ?_⟩ + exact implE (A := Proposition.top) D <| derivationTop.weak' (by grind) + +/-- Change the conclusion along an equivalence. -/ +def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) : + Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ := e.1.subs' + +theorem Theory.equivalent_sDerivable_conclusion {T : Theory Atom} (Γ : Ctx Atom) + {A B : Proposition Atom} (h : T.Equiv A B) : T.SDerivable ⟨Γ, A⟩ ↔ T.SDerivable ⟨Γ, B⟩ := by + let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h + constructor <;> intro ⟨Γ', hΓ, D⟩ + · refine ⟨Γ₁ ∪ Γ', by grind, ?_⟩ apply implE (A := A) - · apply implE (A := A) - · exact ax' (by grind) - · exact ax' (by grind) + · exact D₁.weak' (by grind) + · exact D.weak' (by grind) + · refine ⟨Γ₂ ∪ Γ', by grind, ?_⟩ + apply implE (A := B) + · exact D₂.weak' (by grind) + · exact D.weak' (by grind) + +theorem equivalent_sDerivable_conclusion (Γ : Ctx Atom) {A B : Proposition Atom} (h : Equiv A B) : + SDerivable ⟨Γ, A⟩ ↔ SDerivable ⟨Γ, B⟩ := + (Theory.empty Atom).equivalent_sDerivable_conclusion Γ h + +/-- Replace a hypothesis along an equivalence. -/ +def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) + (C : Proposition Atom) (D : Derivation ⟨insert A Γ, C⟩) : Derivation ⟨insert B Γ, C⟩ := by + have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind + rw [this] + refine D.subs ?_ + exact e.2.weak' (by grind) + +theorem equivalent_hypotheses {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} + (h : T.Equiv A B) (C : Proposition Atom) : + T.SDerivable ⟨insert A Γ, C⟩ ↔ T.SDerivable ⟨insert B Γ, C⟩ := by + let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h + constructor <;> intro h' + · have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind + rw [this] + apply Theory.SDerivable.subs h' + refine ⟨insert B Γ₁ ∪ Γ₂, by grind, ?_⟩ + apply implE (A := B) + · exact D₂.weak' (by grind) · exact ax' (by grind) - · apply implI - exact ax' (by grind) - -/-- Equivalence of A → (A → B) and A → B -/ -theorem impl_idem_equiv {A B : Proposition Atom} : - Proposition.Equiv (A.impl <| A.impl B) (A.impl B) := ⟨⟨implIdemEquiv.1⟩, ⟨implIdemEquiv.2⟩⟩ - -/-- A → (B → C) ⊢ B → (A → C) -/ -def implSwapDer {A B C : Proposition Atom} : - Derivation ⟨{A.impl <| B.impl C}, B.impl (A.impl C)⟩ := by - apply implI - apply implI - apply implE (A := B) - · apply implE (A := A) <;> exact ax' (by grind) - · exact ax' (by grind) - -/-- Equivalence of A → (B → C) and B → (A → C) -/ -def implSwapEquiv {A B C : Proposition Atom} : - Proposition.equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := ⟨implSwapDer, implSwapDer⟩ - -/-- A → (B → C) ⊢ (A → B) → (A → C) -/ -def implImplDistrib {A B C : Proposition Atom} : - Derivation ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := by - apply implI - apply implI - apply implE (A := B) <;> apply implE (A := A) <;> exact ax' (by grind) - -theorem impl_impl_distrib {A B C : Proposition Atom} : - Derivable ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := ⟨implImplDistrib⟩ - -/-- Equivalence of A → (B → C) and B → (A → C) -/ -theorem impl_swap_equiv {A B C : Proposition Atom} : - Proposition.Equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := ⟨⟨implSwapDer⟩, ⟨implSwapDer⟩⟩ - -/-- Equivalence of A ∧ (A ∨ B) and A -/ -def absorbConjDisj {A B : Proposition Atom} : Proposition.equiv (A.conj <| (A.disj B)) A := by - constructor - · apply conjE₁ (B := (A.disj B)) - exact ax' (by grind) - · apply conjI + · have : insert A Γ = (insert B Γ \ {B}) ∪ (insert A Γ) := by grind + rw [this] + apply Theory.SDerivable.subs h' + refine ⟨insert A Γ₂ ∪ Γ₁, by grind, ?_⟩ + apply implE (A := A) + · exact D₁.weak' (by grind) · exact ax' (by grind) - · apply disjI₁ - exact ax' (by grind) -/-- Equivalence of A ∧ (A ∨ B) and A -/ -theorem absorb_conj_disj {A B : Proposition Atom} : Proposition.Equiv (A.conj <| (A.disj B)) A := - ⟨⟨absorbConjDisj.1⟩, ⟨absorbConjDisj.2⟩⟩ +def reflEquiv (A : Proposition Atom) : Proposition.equiv A A := + let D : Derivation ⟨{A},A⟩ := ax' <| by grind; + ⟨D,D⟩ -/-- Equivalence of A ∨ (A ∧ B) and A -/ -def absorbDisjConj {A B : Proposition Atom} : Proposition.equiv (A.disj <| A.conj B) A := by - constructor - · apply disjE (A := A) (B := A.conj B) - · exact ax' (by grind) - · exact ax' (by grind) - · apply conjE₁ (B := B) - exact ax' (by grind) - · apply disjI₁ - exact ax' (by grind) +def commEquiv {A B : Proposition Atom} (e : Proposition.equiv A B) : Proposition.equiv B A := + ⟨e.2, e.1⟩ -/-- Equivalence of A ∨ (A ∧ B) and A -/ -theorem absorb_disj_conj {A B : Proposition Atom} : Proposition.Equiv (A.disj <| A.conj B) A := - ⟨⟨absorbDisjConj.1⟩, ⟨absorbDisjConj.2⟩⟩ +def transEquiv {A B C : Proposition Atom} (eAB : Proposition.equiv A B) + (eBC : Proposition.equiv B C) : Proposition.equiv A C := + ⟨mapEquivConclusion _ eBC eAB.1, mapEquivConclusion _ (commEquiv eAB) eBC.2⟩ -/-- Falsum is absorbing for conjunction -/ -def botConjAbsorb {A : Proposition Atom} : Proposition.equiv (A.conj bot) bot := by - constructor - · apply conjE₂ (A := A) - exact ax' (by grind) - · apply conjI - · apply botE - exact ax' (by grind) - · exact ax' (by grind) +theorem equivalent_refl {T : Theory Atom} (A : Proposition Atom) : T.Equiv A A := by + have : T.Derivable (A.impl A) := by refine ⟨∅, by grind, ?_⟩; apply implI; exact ax' (by grind) + grind [Theory.Equiv] -/-- Falsum is absorbing for conjunction -/ -theorem bot_conj_absorb {A : Proposition Atom} : Proposition.Equiv (A.conj bot) bot := - ⟨⟨botConjAbsorb.1⟩, ⟨botConjAbsorb.2⟩⟩ +theorem equivalent_comm {T : Theory Atom} {A B : Proposition Atom} : + T.Equiv A B → T.Equiv B A := by grind [Theory.Equiv] -/-- Falsum is neutral for disjunction -/ -def botDisjNeutral {A : Proposition Atom} : Proposition.equiv (A.disj bot) A := by - constructor - · apply disjE (A := A) (B := bot) - · exact ax' (by grind) - · exact ax' (by grind) - · apply botE - exact ax' (by grind) - · apply disjI₁ - exact ax' (by grind) - -/-- Falsum is neutral for disjunction -/ -theorem bot_disj_neutral {A : Proposition Atom} : Proposition.Equiv (A.disj bot) A := - ⟨⟨botDisjNeutral.1⟩, ⟨botDisjNeutral.2⟩⟩ +theorem equivalent_trans {T : Theory Atom} {A B C : Proposition Atom} : + T.Equiv A B → T.Equiv B C → T.Equiv A C + | ⟨AB, BA⟩, ⟨BC, CB⟩ => ⟨AB.trans BC, CB.trans BA⟩ + +/-- Equivalence is indeed an equivalence relation. -/ +theorem Theory.equiv_equivalence (T : Theory Atom) : Equivalence (T.Equiv (Atom := Atom)) := + ⟨equivalent_refl, equivalent_comm, equivalent_trans⟩ + +protected def Theory.propositionSetoid (T : Theory Atom) : Setoid (Proposition Atom) := + ⟨T.Equiv, T.equiv_equivalence⟩ end NJ diff --git a/Cslib/Logics/IPL/NJ/Defs.lean b/Cslib/Logics/IPL/NJ/Defs.lean deleted file mode 100644 index b6a5ed23..00000000 --- a/Cslib/Logics/IPL/NJ/Defs.lean +++ /dev/null @@ -1,437 +0,0 @@ -/- -Copyright (c) 2025 Thomas Waring. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Thomas Waring --/ -import Mathlib.Data.Finset.Insert -import Mathlib.Data.Finset.SDiff - -/-! -# Gentzen's NJ - -Natural deduction for intuitionistic propositional logic. - -## Main definitions - -- `Proposition` : a type of propositions with atoms in a given type. -- `Derivation` : natural deduction derivation, done in "sequent style", ie with explicit -hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit contraction -and exchange, and the axiom rule derives `{A} ∪ Γ ⊢ A` for any context `Γ`, allowing weakening to -be a derived rule. -- `Derivable` : defined as `Nonempty (Derivation S)`. -- `Proposition.equiv` and `Proposition.Equiv` : `Type`- and `Prop`-valued equivalence of -propositions. - -## Main results - -- `Derivation.weak` : weakening as a derived rule. -- `Derivation.subs` : substituting a derivation for a hypothesis. -- `equiv_equivalence` : equivalence of propositions is an equivalence. - -## References - -- Dag Prawitz, *Natural Deduction: a proof-theoretical study*. -- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely -presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*. -(Suggestions of better references welcome!) --/ - -universe u - -variable {Atom : Type u} [DecidableEq Atom] - -namespace IPL - -/-- Propositions. We view negation as a defined connective ~A := A → ⊥ -/ -inductive Proposition (Atom : Type u) : Type u where - /-- Propositional atoms -/ - | atom (x : Atom) - /-- Falsum -/ - | bot - /-- Conjunction -/ - | conj (a b : Proposition Atom) - /-- Disjunction -/ - | disj (a b : Proposition Atom) - /-- Implication -/ - | impl (a b : Proposition Atom) -deriving DecidableEq, BEq - -namespace NJ - -open Proposition - -/-- Contexts are finsets of propositions. -/ -abbrev Ctx (Atom) := Finset (Proposition Atom) - -/-- Theories are abitrary sets of propositions. -/ -abbrev Theory (Atom) := Set (Proposition Atom) - -abbrev Theory.empty (Atom) : Theory (Atom) := ∅ - -/-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ -abbrev Sequent (Atom) := Ctx Atom × Proposition Atom - -/-- A derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ. -/ -inductive Derivation : Sequent Atom → Type _ where - /-- Axiom (or assumption) -/ - | ax (Γ : Ctx Atom) (A : Proposition Atom) : Derivation ⟨insert A Γ, A⟩ - /-- Falsum elimination (ex falso quodlibet) -/ - | botE {Γ : Ctx Atom} (A : Proposition Atom) : Derivation ⟨Γ, bot⟩ → Derivation ⟨Γ, A⟩ - /-- Conjunction introduction -/ - | conjI {Γ : Ctx Atom} {A B : Proposition Atom} : - Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, conj A B⟩ - /-- Conjunction elimination left -/ - | conjE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, A⟩ - /-- Conjunction elimination right -/ - | conjE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, B⟩ - /-- Disjunction introduction left -/ - | disjI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, disj A B⟩ - /-- Disjunction introduction right -/ - | disjI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, disj A B⟩ - /-- Disjunction elimination -/ - | disjE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation ⟨Γ, disj A B⟩ → - Derivation ⟨insert A Γ, C⟩ → Derivation ⟨insert B Γ, C⟩ → Derivation ⟨Γ, C⟩ - /-- Implication introduction -/ - | implI {A B : Proposition Atom} (Γ : Ctx Atom) : - Derivation ⟨insert A Γ, B⟩ → Derivation ⟨Γ, impl A B⟩ - /-- Implication elimination -/ - | implE {Γ : Ctx Atom} {A B : Proposition Atom} : - Derivation ⟨Γ, impl A B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ - -inductive Theory.Derivable (T : Theory Atom) (A : Proposition Atom) : Prop - | der (Γ : Ctx Atom) (hΓ : ↑Γ ⊆ T) (D : Derivation ⟨Γ, A⟩) : T.Derivable A - -theorem Theory.Derivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (A : Proposition Atom) : - T.Derivable A → T'.Derivable A - | .der Γ hΓ D => ⟨Γ, fun ⦃_⦄ a_1 => hT (hΓ a_1), D⟩ - -/-- A sequent is derivable if it has a derivation. -/ -abbrev Theory.SDerivable (T : Theory Atom) (S : Sequent Atom) := Theory.Derivable (T ∪ ↑S.1) S.2 - -theorem Theory.SDerivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (S : Sequent Atom) : - T.SDerivable S → T'.SDerivable S - | .der Γ hΓ D => ⟨Γ, by grind, D⟩ - -/-- A proposition is derivable if it has a derivation from the empty context. -/ -abbrev Derivable : Proposition Atom → Prop := Theory.empty Atom |>.Derivable - -abbrev SDerivable : Sequent Atom → Prop := Theory.empty Atom |>.SDerivable - -theorem Derivable_iff (A : Proposition Atom) : Derivable A ↔ Nonempty (Derivation ⟨∅, A⟩) := by - constructor - · intro ⟨Γ, hΓ, D⟩ - exact Finset.eq_empty_of_forall_notMem hΓ ▸ ⟨D⟩ - · intro ⟨D⟩ - refine ⟨∅, by simp, D⟩ - -/-- An equivalence between A and B is a derivation of B from A and vice-versa. -/ -def Proposition.equiv (A B : Proposition Atom) := Derivation ⟨{A},B⟩ × Derivation ⟨{B},A⟩ - -def Theory.Equiv (T : Theory Atom) (A B : Proposition Atom) := - T.Derivable (A.impl B) ∧ T.Derivable (B.impl A) - -/-- Two propositions A and B are equivalent if B can be derived from A and vice-versa. -/ -abbrev Equiv : Proposition Atom → Proposition Atom → Prop := Theory.empty Atom |>.Equiv - -open Derivation - -/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ -def Proposition.top : Proposition Atom := impl bot bot - -def derivationTop : Derivation (Atom := Atom) ⟨∅, Proposition.top⟩ := - implI ∅ <| ax (Atom := Atom) ∅ bot - -theorem Theory.top_derivable (T : Theory Atom) : T.Derivable Proposition.top := by - refine ⟨∅, by simp, derivationTop⟩ - -theorem top_derivable : Derivable (Atom := Atom) Proposition.top := - Theory.top_derivable (Theory.empty Atom) - -/-! ### Common proof patterns -/ - -/-- A convenient reformulation of the axiom rule. -/ -def Derivation.ax' {Γ : Ctx Atom} {A : Proposition Atom} (h : A ∈ Γ) : Derivation ⟨Γ,A⟩ := by - have : Γ = insert A Γ := by grind - rw [this] - apply ax - -/-- Weakening is a derived rule. -/ -def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) : - (D : Derivation ⟨Γ, A⟩) → Derivation ⟨Γ ∪ Δ, A⟩ - | ax Γ A => (Finset.insert_union A Γ Δ) ▸ ax (Γ ∪ Δ) A - | botE A D => botE A <| D.weak Δ - | conjI D D' => conjI (D.weak Δ) (D'.weak Δ) - | conjE₁ D => conjE₁ <| D.weak Δ - | conjE₂ D => conjE₂ <| D.weak Δ - | disjI₁ D => disjI₁ <| D.weak Δ - | disjI₂ D => disjI₂ <| D.weak Δ - | @disjE _ _ _ A B _ D D' D'' => - disjE (D.weak Δ) - ((Finset.insert_union A Γ Δ) ▸ D'.weak Δ) - ((Finset.insert_union B Γ Δ) ▸ D''.weak Δ) - | @implI _ _ A B Γ D => implI (Γ ∪ Δ) <| (Finset.insert_union A Γ Δ) ▸ D.weak Δ - | implE D D' => implE (D.weak Δ) (D'.weak Δ) - -def Derivation.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h : Γ ⊆ Δ) (D : Derivation ⟨Γ, A⟩) : - Derivation ⟨Δ, A⟩ := Finset.union_sdiff_of_subset h ▸ D.weak (Δ \ Γ) - -lemma sDerivable_iff (S : Sequent Atom) : SDerivable S ↔ Nonempty (Derivation S) := by - constructor - · intro ⟨Γ, hΓ, D⟩ - refine ⟨D.weak' ?_⟩ - simpa using hΓ - · intro ⟨D⟩ - refine ⟨S.1, by simp, D⟩ - -theorem Theory.SDerivable.sequent_weak (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} : - T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ ∪ Δ, A⟩ - | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind - -theorem Theory.SDerivable.sequent_weak' (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} - (h_ext : Γ ⊆ Δ) : T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Δ, A⟩ - | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind - -theorem SDerivable.weak {Γ Δ : Ctx Atom} {A : Proposition Atom} (_ : SDerivable ⟨Γ, A⟩) : - SDerivable ⟨Γ ∪ Δ, A⟩ := by - apply Theory.SDerivable.sequent_weak; assumption - -theorem SDerivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) - (_ : SDerivable ⟨Γ, A⟩) : SDerivable ⟨Δ, A⟩ := by - apply Theory.SDerivable.sequent_weak' <;> assumption - -/-- Substitution of a derivation `E` for one of the hypotheses in the context `Γ` of `D`. -/ -def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} - (D : Derivation ⟨Γ, B⟩) (E : Derivation ⟨Δ, A⟩) : Derivation ⟨(Γ \ {A}) ∪ Δ, B⟩ := by - match D with - | ax _ _ => - by_cases B = A - case pos h => - rw [h, Finset.union_comm] - exact E.weak _ - case neg h => - rw [Finset.insert_sdiff_of_notMem (h := Finset.notMem_singleton.mpr h)] - exact (ax _ B).weak _ - | botE _ D => exact botE B <| D.subs E - | conjI D D' => exact conjI (D.subs E) (D'.subs E) - | conjE₁ D => exact conjE₁ <| D.subs E - | conjE₂ D => exact conjE₂ <| D.subs E - | disjI₁ D => exact disjI₁ <| D.subs E - | disjI₂ D => exact disjI₂ <| D.subs E - | @disjE _ _ _ C C' B D D' D'' => - apply disjE (D.subs E) - · by_cases C = A - case pos h => - rw [h] at D' ⊢ - have : insert A ((Γ \ {A}) ∪ Δ) = (insert A Γ) ∪ Δ := by grind - rw [this] - exact D'.weak _ - case neg h => - have : insert C ((Γ \ {A}) ∪ Δ) = ((insert C Γ) \ {A}) ∪ Δ := by grind - rw [this] - exact D'.subs E - · by_cases C' = A - case pos h => - rw [h] at D'' ⊢ - have : insert A ((Γ \ {A}) ∪ Δ) = (insert A Γ) ∪ Δ := by grind - rw [this] - exact D''.weak _ - case neg h => - have : insert C' ((Γ \ {A}) ∪ Δ) = ((insert C' Γ) \ {A}) ∪ Δ := by grind - rw [this] - exact D''.subs E - | @implI _ _ A' B _ D => - apply implI - by_cases A' = A - case pos h => - rw [h] at D ⊢ - have : insert A (Γ \ {A} ∪ Δ) = insert A Γ ∪ Δ := by grind - rw [this] - exact D.weak Δ - case neg h => - have : insert A' ((Γ \ {A}) ∪ Δ) = ((insert A' Γ) \ {A}) ∪ Δ := by grind - rw [this] - exact D.subs E - | implE D D' => exact implE (D.subs E) (D'.subs E) - -theorem Theory.SDerivable.subs {T : Theory Atom} {Γ Δ : Ctx Atom} {A B : Proposition Atom} : - T.SDerivable ⟨Γ, B⟩ → T.SDerivable ⟨Δ, A⟩ → T.SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ - | .der Γ' hΓ' D, .der Δ' hΔ' E => - ⟨Γ' \ {A} ∪ Δ', by grind [Finset.coe_union, Finset.coe_sdiff], D.subs E⟩ - -def Derivation.subs' {Γ : Ctx Atom} {A B : Proposition Atom} - (D : Derivation ⟨{A}, B⟩) (E : Derivation ⟨Γ, A⟩) : Derivation ⟨Γ, B⟩ := by - have : Γ = ({A} \ {A}) ∪ Γ := by grind - rw [this] - exact D.subs E - -theorem Theory.SDerivable.subs' {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : - T.Derivable (A.impl B) → T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ, B⟩ - | ⟨Δ, hΔ, E⟩, ⟨Γ', hΓ', D⟩ => by - refine ⟨Δ ∪ Γ', by grind, ?_⟩ - apply implE (A := A) - · exact E.weak' (by grind) - · exact D.weak' (by grind) - -theorem SDerivable.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} : - SDerivable ⟨Γ, B⟩ → SDerivable ⟨Δ, A⟩ → SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ := Theory.SDerivable.subs - -theorem SDerivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} : - (h : Derivable (A.impl B)) → (h' : SDerivable ⟨Γ, A⟩) → SDerivable ⟨Γ, B⟩ := - Theory.SDerivable.subs' - -/-! ### Inference rules for derivability -/ - -theorem Theory.Derivable.ax' {T : Theory Atom} {A : Proposition Atom} (h : A ∈ T) : - T.Derivable A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ - -theorem Theory.Derivable.botE {T : Theory Atom} (A : Proposition Atom) : - T.Derivable Proposition.bot → T.Derivable A - | ⟨Γ, h, D⟩ => ⟨Γ, h, Derivation.botE A D⟩ - -theorem Theory.Derivable.conjI {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable A → T.Derivable B → T.Derivable (A.conj B) - | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => - ⟨Γ ∪ Γ', by grind, Derivation.conjI (D.weak' (by grind)) (D'.weak' (by grind))⟩ - -theorem Theory.Derivable.conjE₁ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable (A.conj B) → T.Derivable A - | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₁⟩ - -theorem Theory.Derivable.conjE₂ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable (A.conj B) → T.Derivable B - | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₂⟩ - -theorem Theory.Derivable.disjI₁ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable A → T.Derivable (A.disj B) - | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₁⟩ - -theorem Theory.Derivable.disjI₂ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable B → T.Derivable (A.disj B) - | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₂⟩ - -theorem Theory.Derivable.disjE {T : Theory Atom} {A B C : Proposition Atom} : - T.Derivable (A.disj B) → T.Derivable (A.impl C) → T.Derivable (B.impl C) → T.Derivable C - | ⟨Γ, h, D⟩, ⟨Δ₁, h₁, E₁⟩, ⟨Δ₂, h₂, E₂⟩ => by - refine ⟨Γ ∪ Δ₁ ∪ Δ₂, by grind, ?_⟩ - apply Derivation.disjE (A := A) (B := B) - · exact D.weak' (by grind) - · apply Derivation.implE (A := A) - · exact E₁.weak' (by grind) - · exact Derivation.ax' (by grind) - · apply Derivation.implE (A := B) - · exact E₂.weak' (by grind) - · exact Derivation.ax' (by grind) - -theorem Theory.Derivable.implE {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable (A.impl B) → T.Derivable A → T.Derivable B - | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by - refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ - exact Derivation.implE (A := A) (D₁.weak' (by grind)) (D₂.weak' (by grind)) - -theorem Theory.Derivable.trans {T : Theory Atom} {A B C : Proposition Atom} : - T.Derivable (A.impl B) → T.Derivable (B.impl C) → T.Derivable (A.impl C) - | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by - refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ - apply implI - apply Derivation.implE (A := B) - · exact D₂.weak' (by grind) - · apply Derivation.implE (A := A) - · exact D₁.weak' (by grind) - · exact Derivation.ax' (by grind) - -/-! ### Properties of NJ-equivalence -/ - -theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition Atom) : - T.Derivable A ↔ T.Equiv A top := by - constructor <;> intro h - · constructor - · refine ⟨∅, by grind, ?_⟩ - exact implI (A := A) (B := Proposition.top) ∅ <| derivationTop.weak' (by grind) - · let ⟨Γ, hΓ, D⟩ := h - refine ⟨Γ, by grind, ?_⟩ - refine implI Γ <| D.weak' (by grind) - · let ⟨Γ, hΓ, D⟩ := h.2 - refine ⟨Γ, by grind, ?_⟩ - exact implE (A := Proposition.top) D <| derivationTop.weak' (by grind) - -/-- Change the conclusion along an equivalence. -/ -def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) : - Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ := e.1.subs' - -theorem Theory.equivalent_sDerivable_conclusion {T : Theory Atom} (Γ : Ctx Atom) - {A B : Proposition Atom} (h : T.Equiv A B) : T.SDerivable ⟨Γ, A⟩ ↔ T.SDerivable ⟨Γ, B⟩ := by - let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h - constructor <;> intro ⟨Γ', hΓ, D⟩ - · refine ⟨Γ₁ ∪ Γ', by grind, ?_⟩ - apply implE (A := A) - · exact D₁.weak' (by grind) - · exact D.weak' (by grind) - · refine ⟨Γ₂ ∪ Γ', by grind, ?_⟩ - apply implE (A := B) - · exact D₂.weak' (by grind) - · exact D.weak' (by grind) - -theorem equivalent_sDerivable_conclusion (Γ : Ctx Atom) {A B : Proposition Atom} (h : Equiv A B) : - SDerivable ⟨Γ, A⟩ ↔ SDerivable ⟨Γ, B⟩ := - (Theory.empty Atom).equivalent_sDerivable_conclusion Γ h - -/-- Replace a hypothesis along an equivalence. -/ -def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) - (C : Proposition Atom) (D : Derivation ⟨insert A Γ, C⟩) : Derivation ⟨insert B Γ, C⟩ := by - have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind - rw [this] - refine D.subs ?_ - exact e.2.weak' (by grind) - -theorem equivalent_hypotheses {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} - (h : T.Equiv A B) (C : Proposition Atom) : - T.SDerivable ⟨insert A Γ, C⟩ ↔ T.SDerivable ⟨insert B Γ, C⟩ := by - let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h - constructor <;> intro h' - · have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind - rw [this] - apply Theory.SDerivable.subs h' - refine ⟨insert B Γ₁ ∪ Γ₂, by grind, ?_⟩ - apply implE (A := B) - · exact D₂.weak' (by grind) - · exact ax' (by grind) - · have : insert A Γ = (insert B Γ \ {B}) ∪ (insert A Γ) := by grind - rw [this] - apply Theory.SDerivable.subs h' - refine ⟨insert A Γ₂ ∪ Γ₁, by grind, ?_⟩ - apply implE (A := A) - · exact D₁.weak' (by grind) - · exact ax' (by grind) - -def reflEquiv (A : Proposition Atom) : Proposition.equiv A A := - let D : Derivation ⟨{A},A⟩ := ax' <| by grind; - ⟨D,D⟩ - -def commEquiv {A B : Proposition Atom} (e : Proposition.equiv A B) : Proposition.equiv B A := - ⟨e.2, e.1⟩ - -def transEquiv {A B C : Proposition Atom} (eAB : Proposition.equiv A B) - (eBC : Proposition.equiv B C) : Proposition.equiv A C := - ⟨mapEquivConclusion _ eBC eAB.1, mapEquivConclusion _ (commEquiv eAB) eBC.2⟩ - -theorem equivalent_refl {T : Theory Atom} (A : Proposition Atom) : T.Equiv A A := by - have : T.Derivable (A.impl A) := by refine ⟨∅, by grind, ?_⟩; apply implI; exact ax' (by grind) - grind [Theory.Equiv] - -theorem equivalent_comm {T : Theory Atom} {A B : Proposition Atom} : - T.Equiv A B → T.Equiv B A := by grind [Theory.Equiv] - -theorem equivalent_trans {T : Theory Atom} {A B C : Proposition Atom} : - T.Equiv A B → T.Equiv B C → T.Equiv A C - | ⟨AB, BA⟩, ⟨BC, CB⟩ => ⟨AB.trans BC, CB.trans BA⟩ - -/-- Equivalence is indeed an equivalence relation. -/ -theorem Theory.equiv_equivalence (T : Theory Atom) : Equivalence (T.Equiv (Atom := Atom)) := - ⟨equivalent_refl, equivalent_comm, equivalent_trans⟩ - -protected def Theory.propositionSetoid (T : Theory Atom) : Setoid (Proposition Atom) := - ⟨T.Equiv, T.equiv_equivalence⟩ - -end NJ - -end IPL diff --git a/Cslib/Logics/IPL/NJ/Theorems.lean b/Cslib/Logics/IPL/NJ/Theorems.lean new file mode 100644 index 00000000..72db10d0 --- /dev/null +++ b/Cslib/Logics/IPL/NJ/Theorems.lean @@ -0,0 +1,331 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ +import Cslib.Logics.IPL.NJ.Basic + +/-! # Elementary derivations and equivalences in NJ -/ + +variable {Atom : Type u} [DecidableEq Atom] + +namespace IPL + +open Proposition + +namespace NJ + +open Derivation + +/-! +### Negation theorems + +The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. +-/ + +/-- Double negation introduction -/ +def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, impl (impl A B) B⟩ := + implI (A := A.impl B) _ <| + implE (A := A) (ax' (by grind)) (ax' (by grind)) + +theorem SDerivable.dni {A B : Proposition Atom} : SDerivable ⟨{A},impl (impl A B) B⟩ := + sDerivable_iff.mpr ⟨Derivation.dni⟩ + +/-- The double negation of excluded-middle, or in minimal-logic-style ⊢ (A ∨ (A → B)) → B → B. -/ +def Derivation.notNotLEM {A B : Proposition Atom} : + Derivation ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := + implI _ <| + implE (A := A.disj (A.impl B)) (ax' <| by grind) <| + disjI₂ <| + implI _ <| + implE (A := A.disj (A.impl B)) (ax' <| by grind) <| + disjI₁ <| + ax' <| by grind + +theorem Derivable.not_not_lem {A B : Proposition Atom} : + SDerivable ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := + sDerivable_iff.mpr ⟨Derivation.notNotLEM⟩ + +/-- Triple negation elimination -/ +def Derivation.tne {A B : Proposition Atom} : + Derivation ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := + implI _ <| + implE (A := (A.impl B).impl B) (ax' <| by grind) <| + Derivation.dni.weak' (Γ := {A}) (by grind) + +theorem Derivable.tne {A B : Proposition Atom} : + SDerivable ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := sDerivable_iff.mpr ⟨Derivation.tne⟩ + +def tneEquiv {A B : Proposition Atom} : + Proposition.equiv (A.impl B) (((A.impl B).impl B).impl B) := ⟨Derivation.dni, Derivation.tne⟩ + +theorem tne_equivalent {A B : Proposition Atom} : + Equiv (A.impl B) (((A.impl B).impl B).impl B) := equiv_iff.mpr ⟨tneEquiv⟩ + +/-- Modus tollens -/ +def Derivation.modusTollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) + (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B.impl C) Γ, A.impl C⟩ := + implI _ <| + implE (A := B) + (ax' (by grind)) + (D.weak' (h := by grind)) + +theorem Derivable.modus_tollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) + (h : SDerivable ⟨insert A Γ, B⟩) : SDerivable ⟨insert (B.impl C) Γ, A.impl C⟩ := + let ⟨D⟩ := sDerivable_iff.mp h; sDerivable_iff.mpr ⟨D.modusTollens C⟩ + +/-! +### De Morgan laws + +The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. +-/ + +/-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ +def disjImpOfConjImps {A B C : Proposition Atom} : + Derivation ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := + implI _ <| + disjE (A := A) (B := B) + (ax _ _) + (implE (A := A) + (conjE₁ (B := B.impl C) (ax' <| by grind)) + (ax _ _)) + (implE (A := B) + (conjE₂ (A := A.impl C) (ax' (by grind))) + (ax _ _)) + +/-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ +theorem disj_imp_of_conj_imps {A B C : Proposition Atom} : + SDerivable ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := + sDerivable_iff.mpr ⟨disjImpOfConjImps⟩ + +/-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ +def conjImpsOfDisjImp {A B C : Proposition Atom} : + Derivation ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := + conjI + (implI {impl (disj A B) C} <| + implE (A := A.disj B) (B := C) + (ax' (by grind)) + (disjI₁ (ax _ _))) + (implI {impl (disj A B) C} <| + implE (A := A.disj B) (B := C) + (ax' (by grind)) + (disjI₂ (ax _ _))) + +/-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ +theorem conj_imps_of_disj_imp {A B C : Proposition Atom} : + SDerivable ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := + sDerivable_iff.mpr ⟨conjImpsOfDisjImp⟩ + +def disjImpConjImpsEquiv {A B C : Proposition Atom} : + Proposition.equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := + ⟨conjImpsOfDisjImp, disjImpOfConjImps⟩ + +theorem disj_imp_conj_imps_equivalent {A B C : Proposition Atom} : + Equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := + equiv_iff.mpr ⟨disjImpConjImpsEquiv⟩ + +/-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ +def conjImpOfDisjImps {A B C : Proposition Atom} : + Derivation ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := by + apply implI + apply disjE (A := A.impl C) (B := B.impl C) + · exact ax' (by grind) + · apply implE (A := A) + · apply ax + · apply conjE₁ (B := B) + exact ax' (by grind) + · apply implE (A := B) + · apply ax + · apply conjE₂ (A := A) + exact ax' (by grind) + +/-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ +theorem conj_imp_of_disj_imps {A B C : Proposition Atom} : + SDerivable ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := + sDerivable_iff.mpr ⟨conjImpOfDisjImps⟩ + +/-! ### Further equivalences and implications -/ + +/-- Equivalence of A → (B → C) and (A ∧ B) → C -/ +def curryEquiv {A B C : Proposition Atom} : + Proposition.equiv (A.impl (B.impl C)) (impl (A.conj B) C) := by + constructor + · apply implI + apply implE (A := B) + · apply implE (A := A) + · exact ax' (by grind) + · apply conjE₁ (B := B) + exact ax' (by grind) + · apply conjE₂ (A := A) + exact ax' (by grind) + · apply implI + apply implI + apply implE (A := A.conj B) + · exact ax' (by grind) + · apply conjI <;> exact ax' (by grind) + +/-- Equivalence of A → (B → C) and (A ∧ B) → C -/ +theorem curry_equiv {A B C : Proposition Atom} : + Equiv (A.impl (B.impl C)) (impl (A.conj B) C) := equiv_iff.mpr ⟨curryEquiv⟩ + +/-- A ∧ B ⊢ B ∧ A -/ +def conjCommDer {A B : Proposition Atom} : Derivation ⟨{A.conj B}, B.conj A⟩ := by + apply conjI + · apply conjE₂ (A := A) + exact ax' (by grind) + · apply conjE₁ (B := B) + exact ax' (by grind) + +/-- Equivalence of A ∧ B and B ∧ A -/ +def conjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.conj B) (B.conj A) := + ⟨conjCommDer, conjCommDer⟩ + +/-- Equivalence of A ∧ B and B ∧ A -/ +theorem conj_comm_equiv {A B : Proposition Atom} : Equiv (A.conj B) (B.conj A) := + equiv_iff.mpr ⟨conjCommEquiv⟩ + +/-- Equivalence of A ∧ A and A -/ +def conjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.conj A) A := by + constructor + · apply conjE₁ (B := A) + exact ax' (by grind) + · apply conjI <;> exact ax' (by grind) + +/-- Equivalence of A ∧ A and A -/ +theorem conj_idem_equiv {A : Proposition Atom} : Equiv (A.conj A) A := + equiv_iff.mpr ⟨conjIdemEquiv⟩ + +/-- A ∨ B ⊢ B ∨ A -/ +def disjCommDer {A B : Proposition Atom} : Derivation ⟨{A.disj B}, B.disj A⟩ := by + apply disjE (A := A) (B := B) + · exact ax' (by grind) + · apply disjI₂ + exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∨ B and B ∨ A -/ +def disjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.disj B) (B.disj A) := + ⟨disjCommDer, disjCommDer⟩ + +/-- Equivalence of A ∨ B and B ∨ A -/ +theorem disj_comm_equiv {A B : Proposition Atom} : Equiv (A.disj B) (B.disj A) := + equiv_iff.mpr ⟨disjCommEquiv⟩ + +/-- Equivalence of A ∨ A and A -/ +def disjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.disj A) A := by + constructor + · apply disjE (A := A) (B := A) <;> exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∨ A and A -/ +theorem disj_idem_equiv {A : Proposition Atom} : Equiv (A.disj A) A := + equiv_iff.mpr ⟨disjIdemEquiv⟩ + +/-- Equivalence of A → (A → B) and A → B -/ +def implIdemEquiv {A B : Proposition Atom} : + Proposition.equiv (A.impl <| A.impl B) (A.impl B) := by + constructor + · apply implI + apply implE (A := A) + · apply implE (A := A) + · exact ax' (by grind) + · exact ax' (by grind) + · exact ax' (by grind) + · apply implI + exact ax' (by grind) + +/-- Equivalence of A → (A → B) and A → B -/ +theorem impl_idem_equiv {A B : Proposition Atom} : + Equiv (A.impl <| A.impl B) (A.impl B) := equiv_iff.mpr ⟨implIdemEquiv⟩ + +/-- A → (B → C) ⊢ B → (A → C) -/ +def implSwapDer {A B C : Proposition Atom} : + Derivation ⟨{A.impl <| B.impl C}, B.impl (A.impl C)⟩ := by + apply implI + apply implI + apply implE (A := B) + · apply implE (A := A) <;> exact ax' (by grind) + · exact ax' (by grind) + +/-- Equivalence of A → (B → C) and B → (A → C) -/ +def implSwapEquiv {A B C : Proposition Atom} : + Proposition.equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := ⟨implSwapDer, implSwapDer⟩ + +/-- Equivalence of A → (B → C) and B → (A → C) -/ +theorem impl_swap_equiv {A B C : Proposition Atom} : + Equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := equiv_iff.mpr ⟨implSwapEquiv⟩ + +/-- A → (B → C) ⊢ (A → B) → (A → C) -/ +def implImplDistrib {A B C : Proposition Atom} : + Derivation ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := by + apply implI + apply implI + apply implE (A := B) <;> apply implE (A := A) <;> exact ax' (by grind) + +theorem impl_impl_distrib {A B C : Proposition Atom} : + SDerivable ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := + sDerivable_iff.mpr ⟨implImplDistrib⟩ + +/-- Equivalence of A ∧ (A ∨ B) and A -/ +def absorbConjDisj {A B : Proposition Atom} : Proposition.equiv (A.conj <| (A.disj B)) A := by + constructor + · apply conjE₁ (B := (A.disj B)) + exact ax' (by grind) + · apply conjI + · exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∧ (A ∨ B) and A -/ +theorem absorb_conj_disj {A B : Proposition Atom} : Equiv (A.conj <| (A.disj B)) A := + equiv_iff.mpr ⟨absorbConjDisj⟩ + +/-- Equivalence of A ∨ (A ∧ B) and A -/ +def absorbDisjConj {A B : Proposition Atom} : Proposition.equiv (A.disj <| A.conj B) A := by + constructor + · apply disjE (A := A) (B := A.conj B) + · exact ax' (by grind) + · exact ax' (by grind) + · apply conjE₁ (B := B) + exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Equivalence of A ∨ (A ∧ B) and A -/ +theorem absorb_disj_conj {A B : Proposition Atom} : Equiv (A.disj <| A.conj B) A := + equiv_iff.mpr ⟨absorbDisjConj⟩ + +/-- Falsum is absorbing for conjunction -/ +def botConjAbsorb {A : Proposition Atom} : Proposition.equiv (A.conj bot) bot := by + constructor + · apply conjE₂ (A := A) + exact ax' (by grind) + · apply conjI + · apply botE + exact ax' (by grind) + · exact ax' (by grind) + +/-- Falsum is absorbing for conjunction -/ +theorem bot_conj_absorb {A : Proposition Atom} : Equiv (A.conj bot) bot := + equiv_iff.mpr ⟨botConjAbsorb⟩ + +/-- Falsum is neutral for disjunction -/ +def botDisjNeutral {A : Proposition Atom} : Proposition.equiv (A.disj bot) A := by + constructor + · apply disjE (A := A) (B := bot) + · exact ax' (by grind) + · exact ax' (by grind) + · apply botE + exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + +/-- Falsum is neutral for disjunction -/ +theorem bot_disj_neutral {A : Proposition Atom} : Equiv (A.disj bot) A := + equiv_iff.mpr ⟨botDisjNeutral⟩ + +end NJ + +end IPL From faf932c645b037c76c652d4401f8ee15fd97d5a5 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 4 Oct 2025 17:53:22 +0200 Subject: [PATCH 06/12] order theory laws --- Cslib/Logics/IPL/NJ/Basic.lean | 21 +++- Cslib/Logics/IPL/NJ/Theorems.lean | 174 ++++++++++++++++++++++++++++++ 2 files changed, 194 insertions(+), 1 deletion(-) diff --git a/Cslib/Logics/IPL/NJ/Basic.lean b/Cslib/Logics/IPL/NJ/Basic.lean index 13504e4d..59563749 100644 --- a/Cslib/Logics/IPL/NJ/Basic.lean +++ b/Cslib/Logics/IPL/NJ/Basic.lean @@ -130,6 +130,10 @@ def Proposition.equiv (A B : Proposition Atom) := Derivation ⟨{A},B⟩ × Deri def Theory.Equiv (T : Theory Atom) (A B : Proposition Atom) := T.Derivable (A.impl B) ∧ T.Derivable (B.impl A) +theorem Theory.Equiv.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (A B : Proposition Atom) : + T.Equiv A B → T'.Equiv A B + | ⟨hAB, hBA⟩ => ⟨hAB.theory_weak T T' hT, hBA.theory_weak T T' hT⟩ + /-- Two propositions A and B are equivalent if B can be derived from A and vice-versa. -/ abbrev Equiv : Proposition Atom → Proposition Atom → Prop := Theory.empty Atom |>.Equiv @@ -353,7 +357,6 @@ theorem equiv_iff {A B : Proposition Atom} : Equiv A B ↔ Nonempty (Proposition refine ⟨?_,?_⟩ all_goals apply derivable_iff.mpr; constructor; apply implI; assumption - theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition Atom) : T.Derivable A ↔ T.Equiv A top := by constructor <;> intro h @@ -371,6 +374,22 @@ theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition A def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ := e.1.subs' +theorem Theory.equivalent_derivable {T : Theory Atom} {A B : Proposition Atom} (h : T.Equiv A B) : + T.Derivable A ↔ T.Derivable B := by + let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h + constructor + · intro ⟨Γ, h, D⟩ + refine ⟨Γ ∪ Γ₁, by grind, ?_⟩ + apply implE (A := A) + · exact D₁.weak' (by grind) + · exact D.weak' (by grind) + · intro ⟨Γ, h, D⟩ + refine ⟨Γ ∪ Γ₂, by grind, ?_⟩ + apply implE (A := B) + · exact D₂.weak' (by grind) + · exact D.weak' (by grind) + + theorem Theory.equivalent_sDerivable_conclusion {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} (h : T.Equiv A B) : T.SDerivable ⟨Γ, A⟩ ↔ T.SDerivable ⟨Γ, B⟩ := by let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h diff --git a/Cslib/Logics/IPL/NJ/Theorems.lean b/Cslib/Logics/IPL/NJ/Theorems.lean index 72db10d0..2334e276 100644 --- a/Cslib/Logics/IPL/NJ/Theorems.lean +++ b/Cslib/Logics/IPL/NJ/Theorems.lean @@ -326,6 +326,180 @@ def botDisjNeutral {A : Proposition Atom} : Proposition.equiv (A.disj bot) A := theorem bot_disj_neutral {A : Proposition Atom} : Equiv (A.disj bot) A := equiv_iff.mpr ⟨botDisjNeutral⟩ +/-! ### Partial order, lattice, and Heyting algebra results + +The following amount to showing that "Propositions modulo equivalence" form a Heyting algebra: that +the operations are well-defined on equivalence classes, and the validity of the axioms. +-/ + +section OrderTheory + +variable (T : Theory Atom) + +theorem Theory.le_wd {A A' B B' : Proposition Atom} (hA : T.Equiv A A') (hB : T.Equiv B B') : + T.Derivable (A.impl B) ↔ T.Derivable (A'.impl B') := by + constructor <;> intro h + · exact hA.2.trans h |>.trans hB.1 + · exact hA.1.trans h |>.trans hB.2 + +theorem Theory.le_refl {A : Proposition Atom} : T.Derivable (A.impl A) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + exact ax _ _ + +theorem Theory.le_trans {A B C : Proposition Atom} (hAB : T.Derivable (A.impl B)) + (hBC : T.Derivable (B.impl C)) : T.Derivable (A.impl C) := hAB.trans hBC + +theorem Theory.le_antisymm {A B : Proposition Atom} (hAB : T.Derivable (A.impl B)) + (hBA : T.Derivable (B.impl A)) : T.Equiv A B := ⟨hAB, hBA⟩ + +theorem Theory.inf_wd {A A' B B' : Proposition Atom} : + T.Equiv A A' → T.Equiv B B' → T.Equiv (A.conj B) (A'.conj B') + | ⟨⟨ΓA, hA, DA⟩, ⟨ΓA', hA', DA'⟩⟩, ⟨⟨ΓB, hB, DB⟩, ⟨ΓB', hB', DB'⟩⟩ => by + constructor + · refine ⟨ΓA ∪ ΓB, by grind, ?_⟩ + apply implI + apply conjI + · apply implE (A := A) + · exact DA.weak' (by grind) + · apply conjE₁ (B := B) + apply ax' (by grind) + · apply implE (A := B) + · exact DB.weak' (by grind) + · apply conjE₂ (A := A) + apply ax' (by grind) + · refine ⟨ΓA' ∪ ΓB', by grind, ?_⟩ + apply implI + apply conjI + · apply implE (A := A') + · exact DA'.weak' (by grind) + · apply conjE₁ (B := B') + apply ax' (by grind) + · apply implE (A := B') + · exact DB'.weak' (by grind) + · apply conjE₂ (A := A') + apply ax' (by grind) + +theorem Theory.sup_wd {A A' B B' : Proposition Atom} : + T.Equiv A A' → T.Equiv B B' → T.Equiv (A.disj B) (A'.disj B') + | ⟨⟨ΓA, hA, DA⟩, ⟨ΓA', hA', DA'⟩⟩, ⟨⟨ΓB, hB, DB⟩, ⟨ΓB', hB', DB'⟩⟩ => by + constructor + · refine ⟨ΓA ∪ ΓB, by grind, ?_⟩ + apply implI + apply disjE (A := A) (B := B) (ax' <| by grind) + · apply disjI₁ + apply implE (A := A) + · exact DA.weak' (by grind) + · exact ax .. + · apply disjI₂ + apply implE (A := B) + · exact DB.weak' (by grind) + · exact ax .. + · refine ⟨ΓA' ∪ ΓB', by grind, ?_⟩ + apply implI + apply disjE (A := A') (B := B') (ax' <| by grind) + · apply disjI₁ + apply implE (A := A') + · exact DA'.weak' (by grind) + · exact ax .. + · apply disjI₂ + apply implE (A := B') + · exact DB'.weak' (by grind) + · exact ax .. + +theorem Theory.inf_le_left {A B : Proposition Atom} : T.Derivable ((A.conj B).impl A) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + apply conjE₁ (B := B) + exact ax .. + +theorem Theory.inf_le_right {A B : Proposition Atom} : T.Derivable ((A.conj B).impl B) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + apply conjE₂ (A := A) + exact ax .. + +theorem Theory.le_inf {A B C : Proposition Atom} : + T.Derivable (A.impl B) → T.Derivable (A.impl C) → T.Derivable (A.impl (B.conj C)) + | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => by + refine ⟨Γ ∪ Γ', by grind, ?_⟩ + apply implI + apply conjI + · apply implE (A := A) + · exact D.weak' (by grind) + · exact ax .. + · apply implE (A := A) + · exact D'.weak' (by grind) + · exact ax .. + +theorem Theory.le_sup_left {A B : Proposition Atom} : T.Derivable (A.impl (A.disj B)) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + apply disjI₁ + exact ax .. + +theorem Theory.le_sup_right {A B : Proposition Atom} : T.Derivable (B.impl (A.disj B)) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + apply disjI₂ + exact ax .. + +theorem Theory.sup_le {A B C : Proposition Atom} : + T.Derivable (A.impl C) → T.Derivable (B.impl C) → T.Derivable (A.disj B |>.impl C) + | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => by + refine ⟨Γ ∪ Γ', by grind, ?_⟩ + apply implI + apply disjE (A := A) (B := B) + · exact ax .. + · apply implE (A := A) + · exact D.weak' (by grind) + · exact ax .. + · apply implE (A := B) + · exact D'.weak' (by grind) + · exact ax .. + +theorem Theory.le_top {A : Proposition Atom} : T.Derivable (A.impl Proposition.top) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + exact derivationTop.weak' (by grind) + +theorem Theory.bot_le {A : Proposition Atom} : T.Derivable (bot.impl A) := by + refine ⟨∅, by grind, ?_⟩ + apply implI + apply botE + exact ax .. + +theorem Theory.himp_wd {A A' B B' : Proposition Atom} : + T.Equiv A A' → T.Equiv B B' → T.Equiv (A.impl B) (A'.impl B') + | ⟨⟨ΓA, hA, DA⟩, ⟨ΓA', hA', DA'⟩⟩, ⟨⟨ΓB, hB, DB⟩, ⟨ΓB', hB', DB'⟩⟩ => by + constructor + · refine ⟨ΓA' ∪ ΓB, by grind, ?_⟩ + apply implI; apply implI + apply implE (A := B) + · exact DB.weak' (by grind) + · apply implE (A := A) + · exact ax' (by grind) + · apply implE (A := A') + · exact DA'.weak' (by grind) + · exact ax .. + · refine ⟨ΓA ∪ ΓB', by grind, ?_⟩ + apply implI; apply implI + apply implE (A := B') + · exact DB'.weak' (by grind) + · apply implE (A := A') + · exact ax' (by grind) + · apply implE (A := A) + · exact DA.weak' (by grind) + · exact ax .. + +theorem Theory.le_himp_iff {A B C : Proposition Atom} : + T.Derivable (A.impl (B.impl C)) ↔ T.Derivable ((A.conj B).impl C) := by + apply T.equivalent_derivable + apply Theory.Equiv.theory_weak (Theory.empty Atom) T (by grind) + exact curry_equiv + +end OrderTheory + end NJ end IPL From 579495e399dd3ae7aa4ff576ac0b6cd7595f02db Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 4 Oct 2025 19:23:11 +0200 Subject: [PATCH 07/12] split off minimal logic --- .../NaturalDeduction}/Basic.lean | 54 +++++++++++++++--- .../NaturalDeduction}/Theorems.lean | 55 ++++++++++--------- 2 files changed, 74 insertions(+), 35 deletions(-) rename Cslib/Logics/{IPL/NJ => Propositional/NaturalDeduction}/Basic.lean (90%) rename Cslib/Logics/{IPL/NJ => Propositional/NaturalDeduction}/Theorems.lean (94%) diff --git a/Cslib/Logics/IPL/NJ/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean similarity index 90% rename from Cslib/Logics/IPL/NJ/Basic.lean rename to Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index 59563749..ab826295 100644 --- a/Cslib/Logics/IPL/NJ/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -40,7 +40,7 @@ universe u variable {Atom : Type u} [DecidableEq Atom] -namespace IPL +namespace PL /-- Propositions. We view negation as a defined connective ~A := A → ⊥ -/ inductive Proposition (Atom : Type u) : Type u where @@ -68,6 +68,32 @@ abbrev Theory (Atom) := Set (Proposition Atom) abbrev Theory.empty (Atom) : Theory (Atom) := ∅ +def IPL : Theory Atom := Set.range (impl bot) +def CPL : Theory Atom := + IPL ∪ Set.range (fun (A : Proposition Atom) ↦ (A.impl bot).impl bot |>.impl A) + +class IsIntuitionistic (T : Theory Atom) where + efq (A : Proposition Atom) : bot.impl A ∈ T + +class IsClassical (T : Theory Atom) where + efq (A : Proposition Atom) : bot.impl A ∈ T + dne (A : Proposition Atom) : ((A.impl bot).impl bot |>.impl A) ∈ T + +instance instIsIntuitionisticIPL : IsIntuitionistic (Atom := Atom) IPL where + efq A := Set.mem_range.mpr ⟨A, rfl⟩ + +instance instIsClassicalCPL : IsClassical (Atom := Atom) CPL where + efq A := Set.mem_union_left _ <| Set.mem_range.mpr ⟨A, rfl⟩ + dne A := Set.mem_union_right _ <| Set.mem_range.mpr ⟨A, rfl⟩ + +omit [DecidableEq Atom] in +theorem instIsIntuitionisticExtention {T T' : Theory Atom} [IsIntuitionistic T] (h : T ⊆ T') : + IsIntuitionistic T' := by grind [IsIntuitionistic] + +omit [DecidableEq Atom] in +theorem instIsClassicalExtention {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : + IsClassical T' := by grind [IsClassical] + /-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ abbrev Sequent (Atom) := Ctx Atom × Proposition Atom @@ -75,8 +101,8 @@ abbrev Sequent (Atom) := Ctx Atom × Proposition Atom inductive Derivation : Sequent Atom → Type _ where /-- Axiom (or assumption) -/ | ax (Γ : Ctx Atom) (A : Proposition Atom) : Derivation ⟨insert A Γ, A⟩ - /-- Falsum elimination (ex falso quodlibet) -/ - | botE {Γ : Ctx Atom} (A : Proposition Atom) : Derivation ⟨Γ, bot⟩ → Derivation ⟨Γ, A⟩ + -- /-- Falsum elimination (ex falso quodlibet) -/ + -- | botE {Γ : Ctx Atom} (A : Proposition Atom) : Derivation ⟨Γ, bot⟩ → Derivation ⟨Γ, A⟩ /-- Conjunction introduction -/ | conjI {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, conj A B⟩ @@ -163,7 +189,7 @@ def Derivation.ax' {Γ : Ctx Atom} {A : Proposition Atom} (h : A ∈ Γ) : Deriv def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) : (D : Derivation ⟨Γ, A⟩) → Derivation ⟨Γ ∪ Δ, A⟩ | ax Γ A => (Finset.insert_union A Γ Δ) ▸ ax (Γ ∪ Δ) A - | botE A D => botE A <| D.weak Δ + -- | botE A D => botE A <| D.weak Δ | conjI D D' => conjI (D.weak Δ) (D'.weak Δ) | conjE₁ D => conjE₁ <| D.weak Δ | conjE₂ D => conjE₂ <| D.weak Δ @@ -215,7 +241,7 @@ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} case neg h => rw [Finset.insert_sdiff_of_notMem (h := Finset.notMem_singleton.mpr h)] exact (ax _ B).weak _ - | botE _ D => exact botE B <| D.subs E + -- | botE _ D => exact botE B <| D.subs E | conjI D D' => exact conjI (D.subs E) (D'.subs E) | conjE₁ D => exact conjE₁ <| D.subs E | conjE₂ D => exact conjE₂ <| D.subs E @@ -288,9 +314,21 @@ theorem SDerivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} : theorem Theory.Derivable.ax' {T : Theory Atom} {A : Proposition Atom} (h : A ∈ T) : T.Derivable A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ -theorem Theory.Derivable.botE {T : Theory Atom} (A : Proposition Atom) : +theorem Theory.Derivable.botE {T : Theory Atom} [IsIntuitionistic T] (A : Proposition Atom) : T.Derivable Proposition.bot → T.Derivable A - | ⟨Γ, h, D⟩ => ⟨Γ, h, Derivation.botE A D⟩ + | ⟨Γ, h, D⟩ => by + refine ⟨insert (impl bot A) Γ, by grind [IsIntuitionistic], ?_⟩ + apply implE (A := bot) + · exact ax .. + · exact D.weak' (by grind) + +theorem Theory.Derivable.dne {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : + T.Derivable (impl (impl A bot) bot) → T.Derivable A + | ⟨Γ, h, D⟩ => by + refine ⟨insert ((impl (impl A bot) bot).impl A) Γ, by grind [IsClassical], ?_⟩ + apply implE (A := impl (impl A bot) bot) + · exact ax .. + · exact D.weak' (by grind) theorem Theory.Derivable.conjI {T : Theory Atom} {A B : Proposition Atom} : T.Derivable A → T.Derivable B → T.Derivable (A.conj B) @@ -466,4 +504,4 @@ protected def Theory.propositionSetoid (T : Theory Atom) : Setoid (Proposition A end NJ -end IPL +end PL diff --git a/Cslib/Logics/IPL/NJ/Theorems.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean similarity index 94% rename from Cslib/Logics/IPL/NJ/Theorems.lean rename to Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean index 2334e276..6a8df496 100644 --- a/Cslib/Logics/IPL/NJ/Theorems.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean @@ -3,13 +3,13 @@ Copyright (c) 2025 Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ -import Cslib.Logics.IPL.NJ.Basic +import Cslib.Logics.Propositional.NaturalDeduction.Basic /-! # Elementary derivations and equivalences in NJ -/ variable {Atom : Type u} [DecidableEq Atom] -namespace IPL +namespace PL open Proposition @@ -298,33 +298,37 @@ theorem absorb_disj_conj {A B : Proposition Atom} : Equiv (A.disj <| A.conj B) equiv_iff.mpr ⟨absorbDisjConj⟩ /-- Falsum is absorbing for conjunction -/ -def botConjAbsorb {A : Proposition Atom} : Proposition.equiv (A.conj bot) bot := by +theorem bot_conj_absorb (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : + T.Equiv (A.conj bot) bot := by constructor - · apply conjE₂ (A := A) + · refine ⟨∅, by grind, ?_⟩ + apply implI + apply conjE₂ (A := A) exact ax' (by grind) - · apply conjI - · apply botE - exact ax' (by grind) + · refine ⟨{bot.impl A}, by grind [IsIntuitionistic], ?_⟩ + apply implI + apply conjI + · apply implE (A := bot) + · exact ax' (by grind) + · exact ax .. · exact ax' (by grind) -/-- Falsum is absorbing for conjunction -/ -theorem bot_conj_absorb {A : Proposition Atom} : Equiv (A.conj bot) bot := - equiv_iff.mpr ⟨botConjAbsorb⟩ - /-- Falsum is neutral for disjunction -/ -def botDisjNeutral {A : Proposition Atom} : Proposition.equiv (A.disj bot) A := by +theorem bot_disj_neutral (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : + T.Equiv (A.disj bot) A := by constructor - · apply disjE (A := A) (B := bot) + · refine ⟨{impl bot A}, by grind [IsIntuitionistic], ?_⟩ + apply implI + apply disjE (A := A) (B := bot) · exact ax' (by grind) · exact ax' (by grind) - · apply botE - exact ax' (by grind) - · apply disjI₁ - exact ax' (by grind) - -/-- Falsum is neutral for disjunction -/ -theorem bot_disj_neutral {A : Proposition Atom} : Equiv (A.disj bot) A := - equiv_iff.mpr ⟨botDisjNeutral⟩ + · apply implE (A := bot) + · exact ax' (by grind) + · exact ax' (by grind) + · refine ⟨∅, by grind, ?_⟩ + apply implI + apply disjI₁ + exact ax .. /-! ### Partial order, lattice, and Heyting algebra results @@ -463,11 +467,8 @@ theorem Theory.le_top {A : Proposition Atom} : T.Derivable (A.impl Proposition.t apply implI exact derivationTop.weak' (by grind) -theorem Theory.bot_le {A : Proposition Atom} : T.Derivable (bot.impl A) := by - refine ⟨∅, by grind, ?_⟩ - apply implI - apply botE - exact ax .. +theorem Theory.bot_le {A : Proposition Atom} [IsIntuitionistic T] : T.Derivable (bot.impl A) := + Theory.Derivable.ax' (by grind [IsIntuitionistic]) theorem Theory.himp_wd {A A' B B' : Proposition Atom} : T.Equiv A A' → T.Equiv B B' → T.Equiv (A.impl B) (A'.impl B') @@ -502,4 +503,4 @@ end OrderTheory end NJ -end IPL +end PL From da39b76bbdd98ffb027fd704fbcd8f3829e8cae5 Mon Sep 17 00:00:00 2001 From: twwar Date: Sat, 4 Oct 2025 20:33:05 +0200 Subject: [PATCH 08/12] classical results --- .../NaturalDeduction/Theorems.lean | 94 ++++++++++++++++++- 1 file changed, 92 insertions(+), 2 deletions(-) diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean index 6a8df496..e771950a 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean @@ -43,8 +43,8 @@ def Derivation.notNotLEM {A B : Proposition Atom} : ax' <| by grind theorem Derivable.not_not_lem {A B : Proposition Atom} : - SDerivable ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := - sDerivable_iff.mpr ⟨Derivation.notNotLEM⟩ + Derivable <| ((A.disj <| impl A B).impl B).impl B := + derivable_iff.mpr ⟨Derivation.notNotLEM⟩ /-- Triple negation elimination -/ def Derivation.tne {A B : Proposition Atom} : @@ -144,6 +144,96 @@ theorem conj_imp_of_disj_imps {A B C : Proposition Atom} : SDerivable ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := sDerivable_iff.mpr ⟨conjImpOfDisjImps⟩ +/-! ### Classical theorems -/ + +theorem dn_equiv {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : + T.Equiv A ((A.impl bot).impl bot) := by + constructor + · refine ⟨∅, by grind, ?_⟩ + apply implI + exact Derivation.dni + · apply Theory.Derivable.ax' + grind [IsClassical] + +theorem lem {T : Theory Atom} [IsClassical T] {A : Proposition Atom} : + T.Derivable (A.disj (A.impl bot)) := by + apply Theory.Derivable.dne + apply Theory.Derivable.theory_weak (T := Theory.empty Atom) (hT := by grind) + exact Derivable.not_not_lem + +private def dneFor (A : Proposition Atom) := ((A.impl bot).impl bot).impl A + +theorem disj_not_of_not_conj {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : + T.SDerivable ⟨{(conj A B).impl bot}, disj (A.impl bot) (B.impl bot)⟩ := by + refine ⟨{(conj A B).impl bot, + dneFor A, + dneFor B, + dneFor (disj (A.impl bot) (B.impl bot))}, ?_, ?_⟩ + · grind [IsClassical, dneFor, Finset.coe_insert, Finset.coe_singleton] + · simp only [dneFor] + apply implE (A := ((disj (A.impl bot) (B.impl bot)).impl bot).impl bot) + · exact ax' (by grind) + · apply implI + apply implE (A := A.conj B) + · exact ax' (by grind) + · apply conjI + · apply implE (A := (A.impl bot).impl bot) + · exact ax' (by grind) + · apply implI + apply implE (A := (disj (A.impl bot) (B.impl bot))) + · exact ax' (by grind) + · apply disjI₁ + exact ax' (by grind) + · apply implE (A := (B.impl bot).impl bot) + · exact ax' (by grind) + · apply implI + apply implE (A := (disj (A.impl bot) (B.impl bot))) + · exact ax' (by grind) + · apply disjI₂ + exact ax' (by grind) + +theorem impl_equiv_disj {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : + T.Equiv (A.impl B) ((A.impl bot).disj B) := by + constructor + · let ⟨Γ, h, D⟩ := lem (T := T) (A := A) + refine ⟨Γ, h, ?_⟩ + apply implI + apply disjE (A := A) (B := A.impl bot) + · exact D.weak' (by grind) + · apply disjI₂ + apply implE (A := A) + all_goals exact ax' (by grind) + · apply disjI₁ + exact ax .. + · refine ⟨{bot.impl B}, by grind [IsClassical], ?_⟩ + apply implI + apply implI + apply disjE (A := A.impl bot) (B := B) + · exact ax' (by grind) + · apply implE (A := bot) + · exact ax' (by grind) + · apply implE (A := A) + all_goals exact ax' (by grind) + · exact ax' (by grind) + +theorem pierce {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : + T.Derivable (((A.impl B).impl A).impl A) := by + let ⟨Γ, h, D⟩ := lem (T := T) (A := A) + refine ⟨insert (bot.impl B) Γ, by grind [IsClassical], ?_⟩ + apply implI + apply disjE (A := A) (B := A.impl bot) + · exact D.weak' (by grind) + · exact ax .. + · apply implE (A := A.impl B) + · exact ax' (by grind) + · apply implI + apply implE (A := bot) + · apply ax' (by grind) + · apply implE (A := A) + · exact ax' (by grind) + · exact ax .. + + /-! ### Further equivalences and implications -/ /-- Equivalence of A → (B → C) and (A ∧ B) → C -/ From 854415e8d3e12cdd4b47a059b19ac6bd87897912 Mon Sep 17 00:00:00 2001 From: twwar Date: Sun, 5 Oct 2025 11:17:55 +0200 Subject: [PATCH 09/12] notation, docs --- .../Propositional/NaturalDeduction/Basic.lean | 224 ++++++++++++------ .../NaturalDeduction/Theorems.lean | 211 ++++++++--------- 2 files changed, 250 insertions(+), 185 deletions(-) diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index ab826295..d0141cd9 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -9,7 +9,10 @@ import Mathlib.Data.Finset.SDiff /-! # Gentzen's NJ -Natural deduction for intuitionistic propositional logic. +Natural deduction for propositional logic. We define deduction trees (a `Type`) for minimal logic, +and derivability (a `Prop`) is relative to a *theory* (set of propositions). Intuitionistic and +classical derivability are obtained by adding (respectively) the principles of explosion and +double negation elimination to minimal logic. ## Main definitions @@ -18,15 +21,29 @@ Natural deduction for intuitionistic propositional logic. hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit contraction and exchange, and the axiom rule derives `{A} ∪ Γ ⊢ A` for any context `Γ`, allowing weakening to be a derived rule. -- `Derivable` : defined as `Nonempty (Derivation S)`. -- `Proposition.equiv` and `Proposition.Equiv` : `Type`- and `Prop`-valued equivalence of -propositions. +- `Theory` : a theory is an arbitrary set of propositions. +- `Theory.Derivable` : a proposition `A` is derivable from a theory `T` if there is a derivation of +`Γ ⊢ A` for some context `Γ ⊆ T`. +- `Theory.SDerivable` : a sequent `Γ ⊢ A` is derivable from a theory `T` if there is a derivation +of `Γ' ⊢ A` for some context `Γ' ⊆ Γ ∪ T`. +- `Proposition.equiv` : `Type`-valued equivalence of propositions. +- `Theory.Equiv` : `Prop`-valued equivalence of propositions, conditional on a theory `T`. +- Unconditional versions of `Derivable`, `SDerivable` and `Equiv` are abbreviations for the relevant +concept relative to the empty theory. ## Main results - `Derivation.weak` : weakening as a derived rule. - `Derivation.subs` : substituting a derivation for a hypothesis. -- `equiv_equivalence` : equivalence of propositions is an equivalence. +- `Theory.equiv_equivalence` : equivalence of propositions is an equivalence. +- We also give deduction rules for derivability, and equivalent conditions for the unconditional +versions of `Derivable`, `SDerivable` and `Equiv`. + +## Notation + +We introduce notation for logical connectives `⊥ ⊤ ⋏ ⋎ ⟶ ~` for, respectively, falsum, verum, +conjunction, disjunction, implication and negation. For `T`-derivability, -sequent-derivability and +-equivalence we have `⊢[T] A`, `Γ ⊢[T] A` and `A ≡[T] B`, respectively. ## References @@ -42,7 +59,7 @@ variable {Atom : Type u} [DecidableEq Atom] namespace PL -/-- Propositions. We view negation as a defined connective ~A := A → ⊥ -/ +/-- Propositions. -/ inductive Proposition (Atom : Type u) : Type u where /-- Propositional atoms -/ | atom (x : Atom) @@ -56,6 +73,20 @@ inductive Proposition (Atom : Type u) : Type u where | impl (a b : Proposition Atom) deriving DecidableEq, BEq +/-- We view negation as a defined connective ~A := A → ⊥ -/ +abbrev Proposition.neg : Proposition Atom → Proposition Atom := (Proposition.impl · bot) + +/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ +def Proposition.top : Proposition Atom := impl bot bot + +instance : Bot (Proposition Atom) := ⟨.bot⟩ +instance : Top (Proposition Atom) := ⟨.top⟩ + +@[inherit_doc] scoped infix:35 " ⋏ " => Proposition.conj +@[inherit_doc] scoped infix:35 " ⋎ " => Proposition.disj +@[inherit_doc] scoped infix:30 " ⟶ " => Proposition.impl +@[inherit_doc] scoped prefix:40 " ~ " => Proposition.neg + namespace NJ open Proposition @@ -68,16 +99,16 @@ abbrev Theory (Atom) := Set (Proposition Atom) abbrev Theory.empty (Atom) : Theory (Atom) := ∅ -def IPL : Theory Atom := Set.range (impl bot) +def IPL : Theory Atom := Set.range (⊥ ⟶ ·) def CPL : Theory Atom := - IPL ∪ Set.range (fun (A : Proposition Atom) ↦ (A.impl bot).impl bot |>.impl A) + IPL ∪ Set.range (fun (A : Proposition Atom) ↦ ~~A ⟶ A) class IsIntuitionistic (T : Theory Atom) where - efq (A : Proposition Atom) : bot.impl A ∈ T + efq (A : Proposition Atom) : (⊥ ⟶ A) ∈ T class IsClassical (T : Theory Atom) where - efq (A : Proposition Atom) : bot.impl A ∈ T - dne (A : Proposition Atom) : ((A.impl bot).impl bot |>.impl A) ∈ T + efq (A : Proposition Atom) : (⊥ ⟶ A) ∈ T + dne (A : Proposition Atom) : (~~A ⟶ A) ∈ T instance instIsIntuitionisticIPL : IsIntuitionistic (Atom := Atom) IPL where efq A := Set.mem_range.mpr ⟨A, rfl⟩ @@ -101,49 +132,66 @@ abbrev Sequent (Atom) := Ctx Atom × Proposition Atom inductive Derivation : Sequent Atom → Type _ where /-- Axiom (or assumption) -/ | ax (Γ : Ctx Atom) (A : Proposition Atom) : Derivation ⟨insert A Γ, A⟩ - -- /-- Falsum elimination (ex falso quodlibet) -/ - -- | botE {Γ : Ctx Atom} (A : Proposition Atom) : Derivation ⟨Γ, bot⟩ → Derivation ⟨Γ, A⟩ /-- Conjunction introduction -/ | conjI {Γ : Ctx Atom} {A B : Proposition Atom} : - Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, conj A B⟩ + Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, A ⋏ B⟩ /-- Conjunction elimination left -/ - | conjE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, A⟩ + | conjE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A ⋏ B⟩ → Derivation ⟨Γ, A⟩ /-- Conjunction elimination right -/ - | conjE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, conj A B⟩ → Derivation ⟨Γ, B⟩ + | conjE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A ⋏ B⟩ → Derivation ⟨Γ, B⟩ /-- Disjunction introduction left -/ - | disjI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, disj A B⟩ + | disjI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, A ⋎ B⟩ /-- Disjunction introduction right -/ - | disjI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, disj A B⟩ + | disjI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation ⟨Γ, B⟩ → Derivation ⟨Γ, A ⋎ B⟩ /-- Disjunction elimination -/ - | disjE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation ⟨Γ, disj A B⟩ → + | disjE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation ⟨Γ, A ⋎ B⟩ → Derivation ⟨insert A Γ, C⟩ → Derivation ⟨insert B Γ, C⟩ → Derivation ⟨Γ, C⟩ /-- Implication introduction -/ | implI {A B : Proposition Atom} (Γ : Ctx Atom) : - Derivation ⟨insert A Γ, B⟩ → Derivation ⟨Γ, impl A B⟩ + Derivation ⟨insert A Γ, B⟩ → Derivation ⟨Γ, A ⟶ B⟩ /-- Implication elimination -/ | implE {Γ : Ctx Atom} {A B : Proposition Atom} : - Derivation ⟨Γ, impl A B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ + Derivation ⟨Γ, A ⟶ B⟩ → Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ +/-- +A proposition `A` is derivable from a theory `T` if `Γ ⊢ A` is derivable, for some context +`Γ ⊆ T`. +-/ inductive Theory.Derivable (T : Theory Atom) (A : Proposition Atom) : Prop | der (Γ : Ctx Atom) (hΓ : ↑Γ ⊆ T) (D : Derivation ⟨Γ, A⟩) : T.Derivable A +@[inherit_doc] +scoped notation "⊢[" T "]" => Theory.Derivable T + theorem Theory.Derivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (A : Proposition Atom) : - T.Derivable A → T'.Derivable A + ⊢[T] A → ⊢[T'] A | .der Γ hΓ D => ⟨Γ, fun ⦃_⦄ a_1 => hT (hΓ a_1), D⟩ -/-- A sequent is derivable if it has a derivation. -/ -abbrev Theory.SDerivable (T : Theory Atom) (S : Sequent Atom) := Theory.Derivable (T ∪ ↑S.1) S.2 +/-- A sequent `Γ ⊢ A` is derivable from a theory `T` if there is a derivation of `Γ' ⊢ A` for some +`Γ' ⊆ Γ ∪ T`. -/ +abbrev Theory.SDerivable (T : Theory Atom) (S : Sequent Atom) := ⊢[T ∪ ↑S.1] S.2 + +@[inherit_doc] +scoped notation Γ " ⊢[" T "] " A:90 => Theory.SDerivable T ⟨Γ, A⟩ theorem Theory.SDerivable.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (S : Sequent Atom) : T.SDerivable S → T'.SDerivable S | .der Γ hΓ D => ⟨Γ, by grind, D⟩ -/-- A proposition is derivable if it has a derivation from the empty context. -/ +/-- A proposition is derivable if it has a derivation from the empty theory. -/ abbrev Derivable : Proposition Atom → Prop := Theory.empty Atom |>.Derivable +@[inherit_doc] +scoped notation "⊢" A:90 => Derivable A + +/-- A sequent is derivable if it has a derivation from the empty theory. -/ abbrev SDerivable : Sequent Atom → Prop := Theory.empty Atom |>.SDerivable -theorem derivable_iff {A : Proposition Atom} : Derivable A ↔ Nonempty (Derivation ⟨∅, A⟩) := by +@[inherit_doc] +scoped notation Γ " ⊢ " A:90 => SDerivable ⟨Γ,A⟩ + +/-- A proposition is derivable iff it has a derivation from the empty context. -/ +theorem derivable_iff {A : Proposition Atom} : ⊢A ↔ Nonempty (Derivation ⟨∅, A⟩) := by constructor · intro ⟨Γ, hΓ, D⟩ exact Finset.eq_empty_of_forall_notMem hΓ ▸ ⟨D⟩ @@ -153,28 +201,31 @@ theorem derivable_iff {A : Proposition Atom} : Derivable A ↔ Nonempty (Derivat /-- An equivalence between A and B is a derivation of B from A and vice-versa. -/ def Proposition.equiv (A B : Proposition Atom) := Derivation ⟨{A},B⟩ × Derivation ⟨{B},A⟩ +/-- `A` and `B` are T-equivalent if `A.impl B` and `B.impl A` are T-derivable. -/ def Theory.Equiv (T : Theory Atom) (A B : Proposition Atom) := - T.Derivable (A.impl B) ∧ T.Derivable (B.impl A) + ⊢[T] (A ⟶ B) ∧ ⊢[T] (B ⟶ A) + +@[inherit_doc] scoped notation A " ≡[" T "] " B:29 => Theory.Equiv T A B theorem Theory.Equiv.theory_weak (T T' : Theory Atom) (hT : T ⊆ T') (A B : Proposition Atom) : - T.Equiv A B → T'.Equiv A B + A ≡[T] B → A ≡[T'] B | ⟨hAB, hBA⟩ => ⟨hAB.theory_weak T T' hT, hBA.theory_weak T T' hT⟩ /-- Two propositions A and B are equivalent if B can be derived from A and vice-versa. -/ abbrev Equiv : Proposition Atom → Proposition Atom → Prop := Theory.empty Atom |>.Equiv -open Derivation +@[inherit_doc] +scoped infix:29 " ≡ " => Equiv -/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ -def Proposition.top : Proposition Atom := impl bot bot +open Derivation -def derivationTop : Derivation (Atom := Atom) ⟨∅, Proposition.top⟩ := - implI ∅ <| ax (Atom := Atom) ∅ bot +def derivationTop : Derivation (Atom := Atom) ⟨∅, ⊤⟩ := + implI ∅ <| ax (Atom := Atom) ∅ ⊥ -theorem Theory.top_derivable (T : Theory Atom) : T.Derivable Proposition.top := by +theorem Theory.top_derivable (T : Theory Atom) : ⊢[T] ⊤ := by refine ⟨∅, by simp, derivationTop⟩ -theorem top_derivable : Derivable (Atom := Atom) Proposition.top := +theorem top_derivable : Derivable (Atom := Atom) ⊤ := Theory.top_derivable (Theory.empty Atom) /-! ### Common proof patterns -/ @@ -205,6 +256,7 @@ def Derivation.weak {Γ : Ctx Atom} {A : Proposition Atom} (Δ : Ctx Atom) : def Derivation.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h : Γ ⊆ Δ) (D : Derivation ⟨Γ, A⟩) : Derivation ⟨Δ, A⟩ := Finset.union_sdiff_of_subset h ▸ D.weak (Δ \ Γ) +/-- A sequent is derivable iff it has a derivation. -/ theorem sDerivable_iff {S : Sequent Atom} : SDerivable S ↔ Nonempty (Derivation S) := by constructor · intro ⟨Γ, hΓ, D⟩ @@ -214,20 +266,20 @@ theorem sDerivable_iff {S : Sequent Atom} : SDerivable S ↔ Nonempty (Derivatio refine ⟨S.1, by simp, D⟩ theorem Theory.SDerivable.sequent_weak (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} : - T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ ∪ Δ, A⟩ + Γ ⊢[T] A → (Γ ∪ Δ) ⊢[T] A | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind theorem Theory.SDerivable.sequent_weak' (T : Theory Atom) {Γ Δ : Ctx Atom} {A : Proposition Atom} - (h_ext : Γ ⊆ Δ) : T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Δ, A⟩ + (h_ext : Γ ⊆ Δ) : Γ ⊢[T] A → Δ ⊢[T] A | .der Γ' hΓ' D => by refine ⟨Γ' ∪ Δ, ?_, D.weak Δ⟩; trans T ∪ Γ ∪ Δ <;> grind -theorem SDerivable.weak {Γ Δ : Ctx Atom} {A : Proposition Atom} (_ : SDerivable ⟨Γ, A⟩) : - SDerivable ⟨Γ ∪ Δ, A⟩ := by - apply Theory.SDerivable.sequent_weak; assumption +theorem SDerivable.weak {Γ Δ : Ctx Atom} {A : Proposition Atom} : + Γ ⊢ A → (Γ ∪ Δ) ⊢ A := by + apply Theory.SDerivable.sequent_weak -theorem SDerivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) - (_ : SDerivable ⟨Γ, A⟩) : SDerivable ⟨Δ, A⟩ := by - apply Theory.SDerivable.sequent_weak' <;> assumption +theorem SDerivable.weak' {Γ Δ : Ctx Atom} {A : Proposition Atom} (h_ext : Γ ⊆ Δ) : + Γ ⊢ A → Δ ⊢ A := by + apply Theory.SDerivable.sequent_weak'; assumption /-- Substitution of a derivation `E` for one of the hypotheses in the context `Γ` of `D`. -/ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} @@ -284,7 +336,7 @@ def Derivation.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} | implE D D' => exact implE (D.subs E) (D'.subs E) theorem Theory.SDerivable.subs {T : Theory Atom} {Γ Δ : Ctx Atom} {A B : Proposition Atom} : - T.SDerivable ⟨Γ, B⟩ → T.SDerivable ⟨Δ, A⟩ → T.SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ + Γ ⊢[T] B → Δ ⊢[T] A → ((Γ \ {A}) ∪ Δ) ⊢[T] B | .der Γ' hΓ' D, .der Δ' hΔ' E => ⟨Γ' \ {A} ∪ Δ', by grind [Finset.coe_union, Finset.coe_sdiff], D.subs E⟩ @@ -295,7 +347,7 @@ def Derivation.subs' {Γ : Ctx Atom} {A B : Proposition Atom} exact D.subs E theorem Theory.SDerivable.subs' {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposition Atom} : - T.Derivable (A.impl B) → T.SDerivable ⟨Γ, A⟩ → T.SDerivable ⟨Γ, B⟩ + ⊢[T] (A ⟶ B) → Γ ⊢[T] A → Γ ⊢[T] B | ⟨Δ, hΔ, E⟩, ⟨Γ', hΓ', D⟩ => by refine ⟨Δ ∪ Γ', by grind, ?_⟩ apply implE (A := A) @@ -303,56 +355,71 @@ theorem Theory.SDerivable.subs' {T : Theory Atom} {Γ : Ctx Atom} {A B : Proposi · exact D.weak' (by grind) theorem SDerivable.subs {Γ Δ : Ctx Atom} {A B : Proposition Atom} : - SDerivable ⟨Γ, B⟩ → SDerivable ⟨Δ, A⟩ → SDerivable ⟨(Γ \ {A}) ∪ Δ, B⟩ := Theory.SDerivable.subs + Γ ⊢ B → Δ ⊢ A → ((Γ \ {A}) ∪ Δ) ⊢ B := Theory.SDerivable.subs theorem SDerivable.subs' {Γ : Ctx Atom} {A B : Proposition Atom} : - (h : Derivable (A.impl B)) → (h' : SDerivable ⟨Γ, A⟩) → SDerivable ⟨Γ, B⟩ := + ⊢ (A ⟶ B) → Γ ⊢ A → Γ ⊢ B := Theory.SDerivable.subs' /-! ### Inference rules for derivability -/ +/-- +The **Deduction theorem**, an implication `A ⟶ B` is derivable iff the sequent `A ⊢ B` is +derivable. +-/ +theorem Theory.impl_derivable_iff {T : Theory Atom} {A B : Proposition Atom} : + ⊢[T] (A ⟶ B) ↔ {A} ⊢[T] B := by + constructor <;> intro ⟨Γ, h, D⟩ + · refine ⟨insert A Γ, by grind, ?_⟩ + apply Derivation.implE (A := A) + · exact D.weak' (by grind) + · exact ax .. + · refine ⟨Γ \ {A}, by grind [Finset.coe_sdiff], ?_⟩ + apply Derivation.implI + exact D.weak' (by grind) + theorem Theory.Derivable.ax' {T : Theory Atom} {A : Proposition Atom} (h : A ∈ T) : - T.Derivable A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ + ⊢[T] A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ theorem Theory.Derivable.botE {T : Theory Atom} [IsIntuitionistic T] (A : Proposition Atom) : - T.Derivable Proposition.bot → T.Derivable A + ⊢[T] ⊥ → ⊢[T] A | ⟨Γ, h, D⟩ => by - refine ⟨insert (impl bot A) Γ, by grind [IsIntuitionistic], ?_⟩ + refine ⟨insert (⊥ ⟶ A) Γ, by grind [IsIntuitionistic], ?_⟩ apply implE (A := bot) · exact ax .. · exact D.weak' (by grind) theorem Theory.Derivable.dne {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : - T.Derivable (impl (impl A bot) bot) → T.Derivable A + ⊢[T] (~~A) → ⊢[T] A | ⟨Γ, h, D⟩ => by - refine ⟨insert ((impl (impl A bot) bot).impl A) Γ, by grind [IsClassical], ?_⟩ - apply implE (A := impl (impl A bot) bot) + refine ⟨insert (~~A ⟶ A) Γ, by grind [IsClassical], ?_⟩ + apply implE (A := ~~A) · exact ax .. · exact D.weak' (by grind) theorem Theory.Derivable.conjI {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable A → T.Derivable B → T.Derivable (A.conj B) + ⊢[T] A → ⊢[T] B → ⊢[T] (A ⋏ B) | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => ⟨Γ ∪ Γ', by grind, Derivation.conjI (D.weak' (by grind)) (D'.weak' (by grind))⟩ theorem Theory.Derivable.conjE₁ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable (A.conj B) → T.Derivable A + ⊢[T] (A ⋏ B) → ⊢[T] A | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₁⟩ theorem Theory.Derivable.conjE₂ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable (A.conj B) → T.Derivable B + ⊢[T] (A ⋏ B) → ⊢[T] B | ⟨Γ, h, D⟩ => ⟨Γ, h, D.conjE₂⟩ theorem Theory.Derivable.disjI₁ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable A → T.Derivable (A.disj B) + ⊢[T] A → ⊢[T] (A ⋎ B) | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₁⟩ theorem Theory.Derivable.disjI₂ {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable B → T.Derivable (A.disj B) + ⊢[T] B → ⊢[T] (A ⋎ B) | ⟨Γ, h, D⟩ => ⟨Γ, h, D.disjI₂⟩ theorem Theory.Derivable.disjE {T : Theory Atom} {A B C : Proposition Atom} : - T.Derivable (A.disj B) → T.Derivable (A.impl C) → T.Derivable (B.impl C) → T.Derivable C + ⊢[T] (A ⋎ B) → ⊢[T] (A ⟶ C) → ⊢[T] (B ⟶ C) → ⊢[T] C | ⟨Γ, h, D⟩, ⟨Δ₁, h₁, E₁⟩, ⟨Δ₂, h₂, E₂⟩ => by refine ⟨Γ ∪ Δ₁ ∪ Δ₂, by grind, ?_⟩ apply Derivation.disjE (A := A) (B := B) @@ -365,13 +432,13 @@ theorem Theory.Derivable.disjE {T : Theory Atom} {A B C : Proposition Atom} : · exact Derivation.ax' (by grind) theorem Theory.Derivable.implE {T : Theory Atom} {A B : Proposition Atom} : - T.Derivable (A.impl B) → T.Derivable A → T.Derivable B + ⊢[T] (A ⟶ B) → ⊢[T] A → ⊢[T] B | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ exact Derivation.implE (A := A) (D₁.weak' (by grind)) (D₂.weak' (by grind)) theorem Theory.Derivable.trans {T : Theory Atom} {A B C : Proposition Atom} : - T.Derivable (A.impl B) → T.Derivable (B.impl C) → T.Derivable (A.impl C) + ⊢[T] (A ⟶ B) → ⊢[T] (B ⟶ C) → ⊢[T] (A ⟶ C) | ⟨Γ₁, h₁, D₁⟩, ⟨Γ₂, h₂, D₂⟩ => by refine ⟨Γ₁ ∪ Γ₂, by grind, ?_⟩ apply implI @@ -383,7 +450,7 @@ theorem Theory.Derivable.trans {T : Theory Atom} {A B C : Proposition Atom} : /-! ### Properties of NJ-equivalence -/ -theorem equiv_iff {A B : Proposition Atom} : Equiv A B ↔ Nonempty (Proposition.equiv A B) := by +theorem equiv_iff {A B : Proposition Atom} : A ≡ B ↔ Nonempty (Proposition.equiv A B) := by constructor · intro ⟨hAB, hBA⟩ let ⟨DAB⟩ := derivable_iff.mp hAB @@ -396,24 +463,24 @@ theorem equiv_iff {A B : Proposition Atom} : Equiv A B ↔ Nonempty (Proposition all_goals apply derivable_iff.mpr; constructor; apply implI; assumption theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition Atom) : - T.Derivable A ↔ T.Equiv A top := by + ⊢[T] A ↔ A ≡[T] ⊤ := by constructor <;> intro h · constructor · refine ⟨∅, by grind, ?_⟩ - exact implI (A := A) (B := Proposition.top) ∅ <| derivationTop.weak' (by grind) + exact implI (A := A) (B := ⊤) ∅ <| derivationTop.weak' (by grind) · let ⟨Γ, hΓ, D⟩ := h refine ⟨Γ, by grind, ?_⟩ refine implI Γ <| D.weak' (by grind) · let ⟨Γ, hΓ, D⟩ := h.2 refine ⟨Γ, by grind, ?_⟩ - exact implE (A := Proposition.top) D <| derivationTop.weak' (by grind) + exact implE (A := ⊤) D <| derivationTop.weak' (by grind) /-- Change the conclusion along an equivalence. -/ def mapEquivConclusion (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition.equiv A B) : Derivation ⟨Γ, A⟩ → Derivation ⟨Γ, B⟩ := e.1.subs' -theorem Theory.equivalent_derivable {T : Theory Atom} {A B : Proposition Atom} (h : T.Equiv A B) : - T.Derivable A ↔ T.Derivable B := by +theorem Theory.equivalent_derivable {T : Theory Atom} {A B : Proposition Atom} (h : A ≡[T] B) : + ⊢[T] A ↔ ⊢[T] B := by let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h constructor · intro ⟨Γ, h, D⟩ @@ -427,9 +494,8 @@ theorem Theory.equivalent_derivable {T : Theory Atom} {A B : Proposition Atom} ( · exact D₂.weak' (by grind) · exact D.weak' (by grind) - theorem Theory.equivalent_sDerivable_conclusion {T : Theory Atom} (Γ : Ctx Atom) - {A B : Proposition Atom} (h : T.Equiv A B) : T.SDerivable ⟨Γ, A⟩ ↔ T.SDerivable ⟨Γ, B⟩ := by + {A B : Proposition Atom} (h : A ≡[T] B) : Γ ⊢[T] A ↔ Γ ⊢[T] B := by let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h constructor <;> intro ⟨Γ', hΓ, D⟩ · refine ⟨Γ₁ ∪ Γ', by grind, ?_⟩ @@ -441,8 +507,8 @@ theorem Theory.equivalent_sDerivable_conclusion {T : Theory Atom} (Γ : Ctx Atom · exact D₂.weak' (by grind) · exact D.weak' (by grind) -theorem equivalent_sDerivable_conclusion (Γ : Ctx Atom) {A B : Proposition Atom} (h : Equiv A B) : - SDerivable ⟨Γ, A⟩ ↔ SDerivable ⟨Γ, B⟩ := +theorem equivalent_sDerivable_conclusion (Γ : Ctx Atom) {A B : Proposition Atom} (h : A ≡ B) : + Γ ⊢ A ↔ Γ ⊢ B := (Theory.empty Atom).equivalent_sDerivable_conclusion Γ h /-- Replace a hypothesis along an equivalence. -/ @@ -454,20 +520,20 @@ def mapEquivHypothesis (Γ : Ctx Atom) {A B : Proposition Atom} (e : Proposition exact e.2.weak' (by grind) theorem equivalent_hypotheses {T : Theory Atom} (Γ : Ctx Atom) {A B : Proposition Atom} - (h : T.Equiv A B) (C : Proposition Atom) : - T.SDerivable ⟨insert A Γ, C⟩ ↔ T.SDerivable ⟨insert B Γ, C⟩ := by + (h : A ≡[T] B) (C : Proposition Atom) : + (insert A Γ) ⊢[T] C ↔ (insert B Γ) ⊢[T] C := by let ⟨⟨Γ₁, hΓ₁, D₁⟩, ⟨Γ₂, hΓ₂, D₂⟩⟩ := h constructor <;> intro h' · have : insert B Γ = (insert A Γ \ {A}) ∪ (insert B Γ) := by grind rw [this] - apply Theory.SDerivable.subs h' + apply h'.subs refine ⟨insert B Γ₁ ∪ Γ₂, by grind, ?_⟩ apply implE (A := B) · exact D₂.weak' (by grind) · exact ax' (by grind) · have : insert A Γ = (insert B Γ \ {B}) ∪ (insert A Γ) := by grind rw [this] - apply Theory.SDerivable.subs h' + apply h'.subs refine ⟨insert A Γ₂ ∪ Γ₁, by grind, ?_⟩ apply implE (A := A) · exact D₁.weak' (by grind) @@ -484,15 +550,15 @@ def transEquiv {A B C : Proposition Atom} (eAB : Proposition.equiv A B) (eBC : Proposition.equiv B C) : Proposition.equiv A C := ⟨mapEquivConclusion _ eBC eAB.1, mapEquivConclusion _ (commEquiv eAB) eBC.2⟩ -theorem equivalent_refl {T : Theory Atom} (A : Proposition Atom) : T.Equiv A A := by - have : T.Derivable (A.impl A) := by refine ⟨∅, by grind, ?_⟩; apply implI; exact ax' (by grind) +theorem equivalent_refl {T : Theory Atom} (A : Proposition Atom) : A ≡[T] A := by + have : T.Derivable (A ⟶ A) := by refine ⟨∅, by grind, ?_⟩; apply implI; exact ax' (by grind) grind [Theory.Equiv] theorem equivalent_comm {T : Theory Atom} {A B : Proposition Atom} : - T.Equiv A B → T.Equiv B A := by grind [Theory.Equiv] + A ≡[T] B → B ≡[T] A := by grind [Theory.Equiv] theorem equivalent_trans {T : Theory Atom} {A B C : Proposition Atom} : - T.Equiv A B → T.Equiv B C → T.Equiv A C + A ≡[T] B → B ≡[T] C → A ≡[T] C | ⟨AB, BA⟩, ⟨BC, CB⟩ => ⟨AB.trans BC, CB.trans BA⟩ /-- Equivalence is indeed an equivalence relation. -/ diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean index e771950a..9106af18 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean @@ -20,12 +20,12 @@ open Derivation /-! ### Negation theorems -The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := impl (-) bot`. +The following are valid in minimal logic, so we use `(-) ⟶ C` over `~(-)`. -/ /-- Double negation introduction -/ -def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, impl (impl A B) B⟩ := - implI (A := A.impl B) _ <| +def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A}, (A ⟶ B) ⟶ B⟩ := + implI (A := A ⟶ B) _ <| implE (A := A) (ax' (by grind)) (ax' (by grind)) theorem SDerivable.dni {A B : Proposition Atom} : SDerivable ⟨{A},impl (impl A B) B⟩ := @@ -33,45 +33,45 @@ theorem SDerivable.dni {A B : Proposition Atom} : SDerivable ⟨{A},impl (impl A /-- The double negation of excluded-middle, or in minimal-logic-style ⊢ (A ∨ (A → B)) → B → B. -/ def Derivation.notNotLEM {A B : Proposition Atom} : - Derivation ⟨∅, (A.disj <| impl A B).impl B |>.impl B⟩ := + Derivation ⟨∅, (A ⋎ (A ⟶ B) ⟶ B) ⟶ B⟩ := implI _ <| - implE (A := A.disj (A.impl B)) (ax' <| by grind) <| + implE (A := A ⋎ (A ⟶ B)) (ax' <| by grind) <| disjI₂ <| implI _ <| - implE (A := A.disj (A.impl B)) (ax' <| by grind) <| + implE (A := A ⋎ (A ⟶ B)) (ax' <| by grind) <| disjI₁ <| ax' <| by grind theorem Derivable.not_not_lem {A B : Proposition Atom} : - Derivable <| ((A.disj <| impl A B).impl B).impl B := + ⊢ ((A ⋎ (A ⟶ B) ⟶ B) ⟶ B) := derivable_iff.mpr ⟨Derivation.notNotLEM⟩ /-- Triple negation elimination -/ def Derivation.tne {A B : Proposition Atom} : - Derivation ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := + Derivation ⟨{((A ⟶ B) ⟶ B) ⟶ B}, A ⟶ B⟩ := implI _ <| - implE (A := (A.impl B).impl B) (ax' <| by grind) <| + implE (A := (A ⟶ B) ⟶ B) (ax' <| by grind) <| Derivation.dni.weak' (Γ := {A}) (by grind) theorem Derivable.tne {A B : Proposition Atom} : - SDerivable ⟨{((A.impl B).impl B).impl B}, A.impl B⟩ := sDerivable_iff.mpr ⟨Derivation.tne⟩ + SDerivable ⟨{((A ⟶ B) ⟶ B) ⟶ B}, A ⟶ B⟩ := sDerivable_iff.mpr ⟨Derivation.tne⟩ def tneEquiv {A B : Proposition Atom} : - Proposition.equiv (A.impl B) (((A.impl B).impl B).impl B) := ⟨Derivation.dni, Derivation.tne⟩ + Proposition.equiv (A ⟶ B) (((A ⟶ B) ⟶ B) ⟶ B) := ⟨Derivation.dni, Derivation.tne⟩ theorem tne_equivalent {A B : Proposition Atom} : - Equiv (A.impl B) (((A.impl B).impl B).impl B) := equiv_iff.mpr ⟨tneEquiv⟩ + (A ⟶ B) ≡ (((A ⟶ B) ⟶ B) ⟶ B) := equiv_iff.mpr ⟨tneEquiv⟩ /-- Modus tollens -/ def Derivation.modusTollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) - (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B.impl C) Γ, A.impl C⟩ := + (D : Derivation ⟨insert A Γ, B⟩) : Derivation ⟨insert (B ⟶ C) Γ, A ⟶ C⟩ := implI _ <| implE (A := B) (ax' (by grind)) (D.weak' (h := by grind)) theorem Derivable.modus_tollens {Γ : Ctx Atom} {A B : Proposition Atom} (C : Proposition Atom) - (h : SDerivable ⟨insert A Γ, B⟩) : SDerivable ⟨insert (B.impl C) Γ, A.impl C⟩ := + (h : (insert A Γ) ⊢ B) : (insert (B ⟶ C) Γ) ⊢ (A ⟶ C) := let ⟨D⟩ := sDerivable_iff.mp h; sDerivable_iff.mpr ⟨D.modusTollens C⟩ /-! @@ -82,53 +82,53 @@ The following are valid in minimal logic, so we use `impl (-) C` over `~(-) := i /-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ def disjImpOfConjImps {A B C : Proposition Atom} : - Derivation ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := + Derivation ⟨{(A ⟶ C) ⋏ (B ⟶ C)}, (A ⋎ B) ⟶ C⟩ := implI _ <| disjE (A := A) (B := B) (ax _ _) (implE (A := A) - (conjE₁ (B := B.impl C) (ax' <| by grind)) + (conjE₁ (B := B ⟶ C) (ax' <| by grind)) (ax _ _)) (implE (A := B) - (conjE₂ (A := A.impl C) (ax' (by grind))) + (conjE₂ (A := A ⟶ C) (ax' (by grind))) (ax _ _)) /-- (A → C) ∧ (B → C) ⊢ (A ∨ B) → C -/ theorem disj_imp_of_conj_imps {A B C : Proposition Atom} : - SDerivable ⟨{conj (impl A C) (impl B C)}, impl (disj A B) C⟩ := + {(A ⟶ C) ⋏ (B ⟶ C)} ⊢ ((A ⋎ B) ⟶ C) := sDerivable_iff.mpr ⟨disjImpOfConjImps⟩ /-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ def conjImpsOfDisjImp {A B C : Proposition Atom} : - Derivation ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := + Derivation ⟨{(A ⋎ B) ⟶ C}, (A ⟶ C) ⋏ (B ⟶ C)⟩ := conjI - (implI {impl (disj A B) C} <| - implE (A := A.disj B) (B := C) + (implI {(A ⋎ B) ⟶ C} <| + implE (A := A ⋎ B) (B := C) (ax' (by grind)) (disjI₁ (ax _ _))) - (implI {impl (disj A B) C} <| - implE (A := A.disj B) (B := C) + (implI {(A ⋎ B) ⟶ C} <| + implE (A := A ⋎ B) (B := C) (ax' (by grind)) (disjI₂ (ax _ _))) /-- (A ∨ B) → C ⊢ (A → C) ∧ (B → C) -/ theorem conj_imps_of_disj_imp {A B C : Proposition Atom} : - SDerivable ⟨{impl (disj A B) C}, conj (impl A C) (impl B C)⟩ := + SDerivable ⟨{(A ⋎ B) ⟶ C}, (A ⟶ C) ⋏ (B ⟶ C)⟩ := sDerivable_iff.mpr ⟨conjImpsOfDisjImp⟩ def disjImpConjImpsEquiv {A B C : Proposition Atom} : - Proposition.equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := + Proposition.equiv ((A ⋎ B) ⟶ C) ((A ⟶ C) ⋏ (B ⟶ C)) := ⟨conjImpsOfDisjImp, disjImpOfConjImps⟩ theorem disj_imp_conj_imps_equivalent {A B C : Proposition Atom} : - Equiv (impl (disj A B) C) (conj (impl A C) (impl B C)) := + Equiv ((A ⋎ B) ⟶ C) ((A ⟶ C) ⋏ (B ⟶ C)) := equiv_iff.mpr ⟨disjImpConjImpsEquiv⟩ /-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ def conjImpOfDisjImps {A B C : Proposition Atom} : - Derivation ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := by + Derivation ⟨{(A ⟶ C) ⋎ (B ⟶ C)}, (A ⋏ B) ⟶ C⟩ := by apply implI - apply disjE (A := A.impl C) (B := B.impl C) + apply disjE (A := A ⟶ C) (B := B ⟶ C) · exact ax' (by grind) · apply implE (A := A) · apply ax @@ -141,13 +141,13 @@ def conjImpOfDisjImps {A B C : Proposition Atom} : /-- (A → C) ∨ (B → C) ⊢ (A ∧ B) → C -/ theorem conj_imp_of_disj_imps {A B C : Proposition Atom} : - SDerivable ⟨{disj (impl A C) (impl B C)}, impl (conj A B) C⟩ := + SDerivable ⟨{(A ⟶ C) ⋎ (B ⟶ C)}, (A ⋏ B) ⟶ C⟩ := sDerivable_iff.mpr ⟨conjImpOfDisjImps⟩ /-! ### Classical theorems -/ theorem dn_equiv {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : - T.Equiv A ((A.impl bot).impl bot) := by + T.Equiv A (~~A) := by constructor · refine ⟨∅, by grind, ?_⟩ apply implI @@ -156,78 +156,77 @@ theorem dn_equiv {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : grind [IsClassical] theorem lem {T : Theory Atom} [IsClassical T] {A : Proposition Atom} : - T.Derivable (A.disj (A.impl bot)) := by + T.Derivable (A ⋎ ~A) := by apply Theory.Derivable.dne apply Theory.Derivable.theory_weak (T := Theory.empty Atom) (hT := by grind) exact Derivable.not_not_lem -private def dneFor (A : Proposition Atom) := ((A.impl bot).impl bot).impl A +private def dneFor (A : Proposition Atom) := ~~A ⟶ A theorem disj_not_of_not_conj {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : - T.SDerivable ⟨{(conj A B).impl bot}, disj (A.impl bot) (B.impl bot)⟩ := by - refine ⟨{(conj A B).impl bot, - dneFor A, - dneFor B, - dneFor (disj (A.impl bot) (B.impl bot))}, ?_, ?_⟩ + T.SDerivable ⟨{~(A ⋏ B)}, ~A ⋎ ~B⟩ := by + refine ⟨{~(A ⋏ B), dneFor A, dneFor B, dneFor (~A ⋎ ~B)}, ?_, ?_⟩ · grind [IsClassical, dneFor, Finset.coe_insert, Finset.coe_singleton] · simp only [dneFor] - apply implE (A := ((disj (A.impl bot) (B.impl bot)).impl bot).impl bot) + apply implE (A := ~~(~A ⋎ ~B)) · exact ax' (by grind) · apply implI - apply implE (A := A.conj B) + apply implE (A := A ⋏ B) · exact ax' (by grind) · apply conjI - · apply implE (A := (A.impl bot).impl bot) + · apply implE (A := ~~A) · exact ax' (by grind) · apply implI - apply implE (A := (disj (A.impl bot) (B.impl bot))) + apply implE (A := (~A ⋎ ~B)) · exact ax' (by grind) · apply disjI₁ exact ax' (by grind) - · apply implE (A := (B.impl bot).impl bot) + · apply implE (A := ~~B) · exact ax' (by grind) · apply implI - apply implE (A := (disj (A.impl bot) (B.impl bot))) + apply implE (A := (~A ⋎ ~B)) · exact ax' (by grind) · apply disjI₂ exact ax' (by grind) theorem impl_equiv_disj {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : - T.Equiv (A.impl B) ((A.impl bot).disj B) := by + (A ⟶ B) ≡[T] (~A ⋎ B) := by constructor · let ⟨Γ, h, D⟩ := lem (T := T) (A := A) refine ⟨Γ, h, ?_⟩ apply implI - apply disjE (A := A) (B := A.impl bot) + apply disjE (A := A) (B := ~A) · exact D.weak' (by grind) · apply disjI₂ apply implE (A := A) all_goals exact ax' (by grind) · apply disjI₁ exact ax .. - · refine ⟨{bot.impl B}, by grind [IsClassical], ?_⟩ + · refine ⟨{⊥ ⟶ B}, by grind [IsClassical], ?_⟩ apply implI apply implI - apply disjE (A := A.impl bot) (B := B) + apply disjE (A := ~A) (B := B) · exact ax' (by grind) - · apply implE (A := bot) + · apply implE (A := ⊥) · exact ax' (by grind) · apply implE (A := A) - all_goals exact ax' (by grind) + all_goals apply ax' + · simp [Bot.bot] + · grind · exact ax' (by grind) theorem pierce {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : - T.Derivable (((A.impl B).impl A).impl A) := by + T.Derivable (((A ⟶ B) ⟶ A) ⟶ A) := by let ⟨Γ, h, D⟩ := lem (T := T) (A := A) - refine ⟨insert (bot.impl B) Γ, by grind [IsClassical], ?_⟩ + refine ⟨insert (⊥ ⟶ B) Γ, by grind [IsClassical], ?_⟩ apply implI - apply disjE (A := A) (B := A.impl bot) + apply disjE (A := A) (B := A ⟶ ⊥) · exact D.weak' (by grind) · exact ax .. - · apply implE (A := A.impl B) + · apply implE (A := A ⟶ B) · exact ax' (by grind) · apply implI - apply implE (A := bot) + apply implE (A := ⊥) · apply ax' (by grind) · apply implE (A := A) · exact ax' (by grind) @@ -238,7 +237,7 @@ theorem pierce {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : /-- Equivalence of A → (B → C) and (A ∧ B) → C -/ def curryEquiv {A B C : Proposition Atom} : - Proposition.equiv (A.impl (B.impl C)) (impl (A.conj B) C) := by + Proposition.equiv (A ⟶ (B ⟶ C)) ((A ⋏ B) ⟶ C) := by constructor · apply implI apply implE (A := B) @@ -250,16 +249,16 @@ def curryEquiv {A B C : Proposition Atom} : exact ax' (by grind) · apply implI apply implI - apply implE (A := A.conj B) + apply implE (A := A ⋏ B) · exact ax' (by grind) · apply conjI <;> exact ax' (by grind) /-- Equivalence of A → (B → C) and (A ∧ B) → C -/ theorem curry_equiv {A B C : Proposition Atom} : - Equiv (A.impl (B.impl C)) (impl (A.conj B) C) := equiv_iff.mpr ⟨curryEquiv⟩ + Equiv (A ⟶ (B ⟶ C)) ((A ⋏ B) ⟶ C) := equiv_iff.mpr ⟨curryEquiv⟩ /-- A ∧ B ⊢ B ∧ A -/ -def conjCommDer {A B : Proposition Atom} : Derivation ⟨{A.conj B}, B.conj A⟩ := by +def conjCommDer {A B : Proposition Atom} : Derivation ⟨{A ⋏ B}, B ⋏ A⟩ := by apply conjI · apply conjE₂ (A := A) exact ax' (by grind) @@ -267,26 +266,26 @@ def conjCommDer {A B : Proposition Atom} : Derivation ⟨{A.conj B}, B.conj A⟩ exact ax' (by grind) /-- Equivalence of A ∧ B and B ∧ A -/ -def conjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.conj B) (B.conj A) := +def conjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A ⋏ B) (B ⋏ A) := ⟨conjCommDer, conjCommDer⟩ /-- Equivalence of A ∧ B and B ∧ A -/ -theorem conj_comm_equiv {A B : Proposition Atom} : Equiv (A.conj B) (B.conj A) := +theorem conj_comm_equiv {A B : Proposition Atom} : (A ⋏ B) ≡ (B ⋏ A) := equiv_iff.mpr ⟨conjCommEquiv⟩ /-- Equivalence of A ∧ A and A -/ -def conjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.conj A) A := by +def conjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A ⋏ A) A := by constructor · apply conjE₁ (B := A) exact ax' (by grind) · apply conjI <;> exact ax' (by grind) /-- Equivalence of A ∧ A and A -/ -theorem conj_idem_equiv {A : Proposition Atom} : Equiv (A.conj A) A := +theorem conj_idem_equiv {A : Proposition Atom} : (A ⋏ A) ≡ A := equiv_iff.mpr ⟨conjIdemEquiv⟩ /-- A ∨ B ⊢ B ∨ A -/ -def disjCommDer {A B : Proposition Atom} : Derivation ⟨{A.disj B}, B.disj A⟩ := by +def disjCommDer {A B : Proposition Atom} : Derivation ⟨{A ⋎ B}, B ⋎ A⟩ := by apply disjE (A := A) (B := B) · exact ax' (by grind) · apply disjI₂ @@ -295,27 +294,27 @@ def disjCommDer {A B : Proposition Atom} : Derivation ⟨{A.disj B}, B.disj A⟩ exact ax' (by grind) /-- Equivalence of A ∨ B and B ∨ A -/ -def disjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A.disj B) (B.disj A) := +def disjCommEquiv {A B : Proposition Atom} : Proposition.equiv (A ⋎ B) (B ⋎ A) := ⟨disjCommDer, disjCommDer⟩ /-- Equivalence of A ∨ B and B ∨ A -/ -theorem disj_comm_equiv {A B : Proposition Atom} : Equiv (A.disj B) (B.disj A) := +theorem disj_comm_equiv {A B : Proposition Atom} : (A ⋎ B) ≡ (B ⋎ A) := equiv_iff.mpr ⟨disjCommEquiv⟩ /-- Equivalence of A ∨ A and A -/ -def disjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A.disj A) A := by +def disjIdemEquiv {A : Proposition Atom} : Proposition.equiv (A ⋎ A) A := by constructor · apply disjE (A := A) (B := A) <;> exact ax' (by grind) · apply disjI₁ exact ax' (by grind) /-- Equivalence of A ∨ A and A -/ -theorem disj_idem_equiv {A : Proposition Atom} : Equiv (A.disj A) A := +theorem disj_idem_equiv {A : Proposition Atom} : (A ⋎ A) ≡ A := equiv_iff.mpr ⟨disjIdemEquiv⟩ /-- Equivalence of A → (A → B) and A → B -/ def implIdemEquiv {A B : Proposition Atom} : - Proposition.equiv (A.impl <| A.impl B) (A.impl B) := by + Proposition.equiv (A ⟶ (A ⟶ B)) (A ⟶ B) := by constructor · apply implI apply implE (A := A) @@ -328,11 +327,11 @@ def implIdemEquiv {A B : Proposition Atom} : /-- Equivalence of A → (A → B) and A → B -/ theorem impl_idem_equiv {A B : Proposition Atom} : - Equiv (A.impl <| A.impl B) (A.impl B) := equiv_iff.mpr ⟨implIdemEquiv⟩ + Equiv (A ⟶ (A ⟶ B)) (A ⟶ B) := equiv_iff.mpr ⟨implIdemEquiv⟩ /-- A → (B → C) ⊢ B → (A → C) -/ def implSwapDer {A B C : Proposition Atom} : - Derivation ⟨{A.impl <| B.impl C}, B.impl (A.impl C)⟩ := by + Derivation ⟨{A ⟶ (B ⟶ C)}, B ⟶ (A ⟶ C)⟩ := by apply implI apply implI apply implE (A := B) @@ -341,27 +340,27 @@ def implSwapDer {A B C : Proposition Atom} : /-- Equivalence of A → (B → C) and B → (A → C) -/ def implSwapEquiv {A B C : Proposition Atom} : - Proposition.equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := ⟨implSwapDer, implSwapDer⟩ + Proposition.equiv (A ⟶ (B ⟶ C)) (B ⟶ (A ⟶ C)) := ⟨implSwapDer, implSwapDer⟩ /-- Equivalence of A → (B → C) and B → (A → C) -/ theorem impl_swap_equiv {A B C : Proposition Atom} : - Equiv (A.impl <| B.impl C) (B.impl (A.impl C)) := equiv_iff.mpr ⟨implSwapEquiv⟩ + (A ⟶ (B ⟶ C)) ≡ (B ⟶ (A ⟶ C)) := equiv_iff.mpr ⟨implSwapEquiv⟩ /-- A → (B → C) ⊢ (A → B) → (A → C) -/ def implImplDistrib {A B C : Proposition Atom} : - Derivation ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := by + Derivation ⟨{A ⟶ (B ⟶ C)}, (A ⟶ B) ⟶ (A ⟶ C)⟩ := by apply implI apply implI apply implE (A := B) <;> apply implE (A := A) <;> exact ax' (by grind) theorem impl_impl_distrib {A B C : Proposition Atom} : - SDerivable ⟨{A.impl (B.impl C)}, impl (A.impl B) (A.impl C)⟩ := + {A ⟶ (B ⟶ C)} ⊢ ((A ⟶ B) ⟶ (A ⟶ C)) := sDerivable_iff.mpr ⟨implImplDistrib⟩ /-- Equivalence of A ∧ (A ∨ B) and A -/ -def absorbConjDisj {A B : Proposition Atom} : Proposition.equiv (A.conj <| (A.disj B)) A := by +def absorbConjDisj {A B : Proposition Atom} : Proposition.equiv (A ⋏ (A ⋎ B)) A := by constructor - · apply conjE₁ (B := (A.disj B)) + · apply conjE₁ (B := (A ⋎ B)) exact ax' (by grind) · apply conjI · exact ax' (by grind) @@ -369,13 +368,13 @@ def absorbConjDisj {A B : Proposition Atom} : Proposition.equiv (A.conj <| (A.di exact ax' (by grind) /-- Equivalence of A ∧ (A ∨ B) and A -/ -theorem absorb_conj_disj {A B : Proposition Atom} : Equiv (A.conj <| (A.disj B)) A := +theorem absorb_conj_disj {A B : Proposition Atom} : (A ⋏ (A ⋎ B)) ≡ A := equiv_iff.mpr ⟨absorbConjDisj⟩ /-- Equivalence of A ∨ (A ∧ B) and A -/ -def absorbDisjConj {A B : Proposition Atom} : Proposition.equiv (A.disj <| A.conj B) A := by +def absorbDisjConj {A B : Proposition Atom} : Proposition.equiv (A ⋎ (A ⋏ B)) A := by constructor - · apply disjE (A := A) (B := A.conj B) + · apply disjE (A := A) (B := A ⋏ B) · exact ax' (by grind) · exact ax' (by grind) · apply conjE₁ (B := B) @@ -384,35 +383,35 @@ def absorbDisjConj {A B : Proposition Atom} : Proposition.equiv (A.disj <| A.con exact ax' (by grind) /-- Equivalence of A ∨ (A ∧ B) and A -/ -theorem absorb_disj_conj {A B : Proposition Atom} : Equiv (A.disj <| A.conj B) A := +theorem absorb_disj_conj {A B : Proposition Atom} : (A ⋎ (A ⋏ B)) ≡ A := equiv_iff.mpr ⟨absorbDisjConj⟩ /-- Falsum is absorbing for conjunction -/ theorem bot_conj_absorb (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : - T.Equiv (A.conj bot) bot := by + (A ⋏ ⊥) ≡[T] ⊥ := by constructor · refine ⟨∅, by grind, ?_⟩ apply implI apply conjE₂ (A := A) exact ax' (by grind) - · refine ⟨{bot.impl A}, by grind [IsIntuitionistic], ?_⟩ + · refine ⟨{⊥ ⟶ A}, by grind [IsIntuitionistic], ?_⟩ apply implI apply conjI - · apply implE (A := bot) + · apply implE (A := ⊥) · exact ax' (by grind) · exact ax .. · exact ax' (by grind) /-- Falsum is neutral for disjunction -/ theorem bot_disj_neutral (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : - T.Equiv (A.disj bot) A := by + (A ⋎ ⊥) ≡[T] A := by constructor - · refine ⟨{impl bot A}, by grind [IsIntuitionistic], ?_⟩ + · refine ⟨{⊥ ⟶ A}, by grind [IsIntuitionistic], ?_⟩ apply implI - apply disjE (A := A) (B := bot) + apply disjE (A := A) (B := ⊥) · exact ax' (by grind) · exact ax' (by grind) - · apply implE (A := bot) + · apply implE (A := ⊥) · exact ax' (by grind) · exact ax' (by grind) · refine ⟨∅, by grind, ?_⟩ @@ -430,25 +429,25 @@ section OrderTheory variable (T : Theory Atom) -theorem Theory.le_wd {A A' B B' : Proposition Atom} (hA : T.Equiv A A') (hB : T.Equiv B B') : - T.Derivable (A.impl B) ↔ T.Derivable (A'.impl B') := by +theorem Theory.le_wd {A A' B B' : Proposition Atom} (hA : A ≡[T] A') (hB : B ≡[T] B') : + ⊢[T] (A ⟶ B) ↔ ⊢[T] (A'.impl B') := by constructor <;> intro h · exact hA.2.trans h |>.trans hB.1 · exact hA.1.trans h |>.trans hB.2 -theorem Theory.le_refl {A : Proposition Atom} : T.Derivable (A.impl A) := by +theorem Theory.le_refl {A : Proposition Atom} : ⊢[T] (A ⟶ A) := by refine ⟨∅, by grind, ?_⟩ apply implI exact ax _ _ -theorem Theory.le_trans {A B C : Proposition Atom} (hAB : T.Derivable (A.impl B)) - (hBC : T.Derivable (B.impl C)) : T.Derivable (A.impl C) := hAB.trans hBC +theorem Theory.le_trans {A B C : Proposition Atom} (hAB : ⊢[T] (A ⟶ B)) + (hBC : ⊢[T] (B ⟶ C)) : ⊢[T] (A ⟶ C) := hAB.trans hBC -theorem Theory.le_antisymm {A B : Proposition Atom} (hAB : T.Derivable (A.impl B)) - (hBA : T.Derivable (B.impl A)) : T.Equiv A B := ⟨hAB, hBA⟩ +theorem Theory.le_antisymm {A B : Proposition Atom} (hAB : ⊢[T] (A ⟶ B)) + (hBA : ⊢[T] (B ⟶ A)) : A ≡[T] B := ⟨hAB, hBA⟩ theorem Theory.inf_wd {A A' B B' : Proposition Atom} : - T.Equiv A A' → T.Equiv B B' → T.Equiv (A.conj B) (A'.conj B') + A ≡[T] A' → B ≡[T] B' → (A ⋏ B) ≡[T] (A' ⋏ B') | ⟨⟨ΓA, hA, DA⟩, ⟨ΓA', hA', DA'⟩⟩, ⟨⟨ΓB, hB, DB⟩, ⟨ΓB', hB', DB'⟩⟩ => by constructor · refine ⟨ΓA ∪ ΓB, by grind, ?_⟩ @@ -475,7 +474,7 @@ theorem Theory.inf_wd {A A' B B' : Proposition Atom} : apply ax' (by grind) theorem Theory.sup_wd {A A' B B' : Proposition Atom} : - T.Equiv A A' → T.Equiv B B' → T.Equiv (A.disj B) (A'.disj B') + A ≡[T] A' → B ≡[T] B' → (A ⋎ B) ≡[T] (A' ⋎ B') | ⟨⟨ΓA, hA, DA⟩, ⟨ΓA', hA', DA'⟩⟩, ⟨⟨ΓB, hB, DB⟩, ⟨ΓB', hB', DB'⟩⟩ => by constructor · refine ⟨ΓA ∪ ΓB, by grind, ?_⟩ @@ -501,20 +500,20 @@ theorem Theory.sup_wd {A A' B B' : Proposition Atom} : · exact DB'.weak' (by grind) · exact ax .. -theorem Theory.inf_le_left {A B : Proposition Atom} : T.Derivable ((A.conj B).impl A) := by +theorem Theory.inf_le_left {A B : Proposition Atom} : ⊢[T] ((A ⋏ B) ⟶ A) := by refine ⟨∅, by grind, ?_⟩ apply implI apply conjE₁ (B := B) exact ax .. -theorem Theory.inf_le_right {A B : Proposition Atom} : T.Derivable ((A.conj B).impl B) := by +theorem Theory.inf_le_right {A B : Proposition Atom} : ⊢[T] ((A ⋏ B) ⟶ B) := by refine ⟨∅, by grind, ?_⟩ apply implI apply conjE₂ (A := A) exact ax .. theorem Theory.le_inf {A B C : Proposition Atom} : - T.Derivable (A.impl B) → T.Derivable (A.impl C) → T.Derivable (A.impl (B.conj C)) + ⊢[T] (A ⟶ B) → ⊢[T] (A ⟶ C) → ⊢[T] (A ⟶ (B ⋏ C)) | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => by refine ⟨Γ ∪ Γ', by grind, ?_⟩ apply implI @@ -526,20 +525,20 @@ theorem Theory.le_inf {A B C : Proposition Atom} : · exact D'.weak' (by grind) · exact ax .. -theorem Theory.le_sup_left {A B : Proposition Atom} : T.Derivable (A.impl (A.disj B)) := by +theorem Theory.le_sup_left {A B : Proposition Atom} : ⊢[T] (A ⟶ (A ⋎ B)) := by refine ⟨∅, by grind, ?_⟩ apply implI apply disjI₁ exact ax .. -theorem Theory.le_sup_right {A B : Proposition Atom} : T.Derivable (B.impl (A.disj B)) := by +theorem Theory.le_sup_right {A B : Proposition Atom} : ⊢[T] (B ⟶ (A ⋎ B)) := by refine ⟨∅, by grind, ?_⟩ apply implI apply disjI₂ exact ax .. theorem Theory.sup_le {A B C : Proposition Atom} : - T.Derivable (A.impl C) → T.Derivable (B.impl C) → T.Derivable (A.disj B |>.impl C) + ⊢[T] (A ⟶ C) → ⊢[T] (B ⟶ C) → ⊢[T] (A ⋎ B ⟶ C) | ⟨Γ, h, D⟩, ⟨Γ', h', D'⟩ => by refine ⟨Γ ∪ Γ', by grind, ?_⟩ apply implI @@ -552,16 +551,16 @@ theorem Theory.sup_le {A B C : Proposition Atom} : · exact D'.weak' (by grind) · exact ax .. -theorem Theory.le_top {A : Proposition Atom} : T.Derivable (A.impl Proposition.top) := by +theorem Theory.le_top {A : Proposition Atom} : T.Derivable (A ⟶ ⊤) := by refine ⟨∅, by grind, ?_⟩ apply implI exact derivationTop.weak' (by grind) -theorem Theory.bot_le {A : Proposition Atom} [IsIntuitionistic T] : T.Derivable (bot.impl A) := +theorem Theory.bot_le {A : Proposition Atom} [IsIntuitionistic T] : T.Derivable (⊥ ⟶ A) := Theory.Derivable.ax' (by grind [IsIntuitionistic]) theorem Theory.himp_wd {A A' B B' : Proposition Atom} : - T.Equiv A A' → T.Equiv B B' → T.Equiv (A.impl B) (A'.impl B') + A ≡[T] A' → B ≡[T] B' → (A ⟶ B) ≡[T] (A' ⟶ B') | ⟨⟨ΓA, hA, DA⟩, ⟨ΓA', hA', DA'⟩⟩, ⟨⟨ΓB, hB, DB⟩, ⟨ΓB', hB', DB'⟩⟩ => by constructor · refine ⟨ΓA' ∪ ΓB, by grind, ?_⟩ @@ -584,7 +583,7 @@ theorem Theory.himp_wd {A A' B B' : Proposition Atom} : · exact ax .. theorem Theory.le_himp_iff {A B C : Proposition Atom} : - T.Derivable (A.impl (B.impl C)) ↔ T.Derivable ((A.conj B).impl C) := by + ⊢[T] (A ⟶ (B ⟶ C)) ↔ ⊢[T] (A ⋏ B ⟶ C) := by apply T.equivalent_derivable apply Theory.Equiv.theory_weak (Theory.empty Atom) T (by grind) exact curry_equiv From 7e7fe6499b10984e602fbcf7fcf440b3d97a6242 Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 6 Oct 2025 13:07:08 +0200 Subject: [PATCH 10/12] separate bot --- Cslib/Logics/Propositional/Defs.lean | 46 +++++++++++++ .../Propositional/NaturalDeduction/Basic.lean | 67 ++++++------------- .../NaturalDeduction/Theorems.lean | 21 +++--- 3 files changed, 77 insertions(+), 57 deletions(-) create mode 100644 Cslib/Logics/Propositional/Defs.lean diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean new file mode 100644 index 00000000..35152d78 --- /dev/null +++ b/Cslib/Logics/Propositional/Defs.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ +import Mathlib.Order.Notation + +/-! # Propositions -/ + +universe u + +variable {Atom : Type u} [DecidableEq Atom] + +namespace PL + +/-- Propositions. -/ +inductive Proposition (Atom : Type u) : Type u where + /-- Propositional atoms -/ + | atom (x : Atom) + /-- Conjunction -/ + | conj (a b : Proposition Atom) + /-- Disjunction -/ + | disj (a b : Proposition Atom) + /-- Implication -/ + | impl (a b : Proposition Atom) +deriving DecidableEq, BEq + +instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩ +instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩ + +/-- We view negation as a defined connective ~A := A → ⊥ -/ +abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥) + +/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ +def Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default) + +instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩ + +example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl + +@[inherit_doc] scoped infix:35 " ⋏ " => Proposition.conj +@[inherit_doc] scoped infix:35 " ⋎ " => Proposition.disj +@[inherit_doc] scoped infix:30 " ⟶ " => Proposition.impl +@[inherit_doc] scoped prefix:40 " ~ " => Proposition.neg + +end PL diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index d0141cd9..dca5aedf 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -3,6 +3,7 @@ Copyright (c) 2025 Thomas Waring. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Thomas Waring -/ +import Cslib.Logics.Propositional.Defs import Mathlib.Data.Finset.Insert import Mathlib.Data.Finset.SDiff @@ -59,34 +60,6 @@ variable {Atom : Type u} [DecidableEq Atom] namespace PL -/-- Propositions. -/ -inductive Proposition (Atom : Type u) : Type u where - /-- Propositional atoms -/ - | atom (x : Atom) - /-- Falsum -/ - | bot - /-- Conjunction -/ - | conj (a b : Proposition Atom) - /-- Disjunction -/ - | disj (a b : Proposition Atom) - /-- Implication -/ - | impl (a b : Proposition Atom) -deriving DecidableEq, BEq - -/-- We view negation as a defined connective ~A := A → ⊥ -/ -abbrev Proposition.neg : Proposition Atom → Proposition Atom := (Proposition.impl · bot) - -/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/ -def Proposition.top : Proposition Atom := impl bot bot - -instance : Bot (Proposition Atom) := ⟨.bot⟩ -instance : Top (Proposition Atom) := ⟨.top⟩ - -@[inherit_doc] scoped infix:35 " ⋏ " => Proposition.conj -@[inherit_doc] scoped infix:35 " ⋎ " => Proposition.disj -@[inherit_doc] scoped infix:30 " ⟶ " => Proposition.impl -@[inherit_doc] scoped prefix:40 " ~ " => Proposition.neg - namespace NJ open Proposition @@ -99,30 +72,30 @@ abbrev Theory (Atom) := Set (Proposition Atom) abbrev Theory.empty (Atom) : Theory (Atom) := ∅ -def IPL : Theory Atom := Set.range (⊥ ⟶ ·) -def CPL : Theory Atom := +def IPL [Bot Atom] : Theory Atom := Set.range (⊥ ⟶ ·) +def CPL [Bot Atom] : Theory Atom := IPL ∪ Set.range (fun (A : Proposition Atom) ↦ ~~A ⟶ A) -class IsIntuitionistic (T : Theory Atom) where +class IsIntuitionistic [Bot Atom] (T : Theory Atom) where efq (A : Proposition Atom) : (⊥ ⟶ A) ∈ T -class IsClassical (T : Theory Atom) where +class IsClassical [Bot Atom] (T : Theory Atom) where efq (A : Proposition Atom) : (⊥ ⟶ A) ∈ T dne (A : Proposition Atom) : (~~A ⟶ A) ∈ T -instance instIsIntuitionisticIPL : IsIntuitionistic (Atom := Atom) IPL where +instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where efq A := Set.mem_range.mpr ⟨A, rfl⟩ -instance instIsClassicalCPL : IsClassical (Atom := Atom) CPL where +instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where efq A := Set.mem_union_left _ <| Set.mem_range.mpr ⟨A, rfl⟩ dne A := Set.mem_union_right _ <| Set.mem_range.mpr ⟨A, rfl⟩ omit [DecidableEq Atom] in -theorem instIsIntuitionisticExtention {T T' : Theory Atom} [IsIntuitionistic T] (h : T ⊆ T') : - IsIntuitionistic T' := by grind [IsIntuitionistic] +theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T] + (h : T ⊆ T') : IsIntuitionistic T' := by grind [IsIntuitionistic] omit [DecidableEq Atom] in -theorem instIsClassicalExtention {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : +theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') : IsClassical T' := by grind [IsClassical] /-- Sequents {A₁, ..., Aₙ} ⊢ B. -/ @@ -219,13 +192,13 @@ scoped infix:29 " ≡ " => Equiv open Derivation -def derivationTop : Derivation (Atom := Atom) ⟨∅, ⊤⟩ := - implI ∅ <| ax (Atom := Atom) ∅ ⊥ +def derivationTop [Inhabited Atom] : Derivation (Atom := Atom) ⟨∅, ⊤⟩ := + implI ∅ <| ax (Atom := Atom) ∅ (atom default) -theorem Theory.top_derivable (T : Theory Atom) : ⊢[T] ⊤ := by +theorem Theory.top_derivable [Inhabited Atom] (T : Theory Atom) : ⊢[T] ⊤ := by refine ⟨∅, by simp, derivationTop⟩ -theorem top_derivable : Derivable (Atom := Atom) ⊤ := +theorem top_derivable [Inhabited Atom] : Derivable (Atom := Atom) ⊤ := Theory.top_derivable (Theory.empty Atom) /-! ### Common proof patterns -/ @@ -381,15 +354,15 @@ theorem Theory.impl_derivable_iff {T : Theory Atom} {A B : Proposition Atom} : theorem Theory.Derivable.ax' {T : Theory Atom} {A : Proposition Atom} (h : A ∈ T) : ⊢[T] A := ⟨{A}, by grind, Derivation.ax ∅ A⟩ -theorem Theory.Derivable.botE {T : Theory Atom} [IsIntuitionistic T] (A : Proposition Atom) : - ⊢[T] ⊥ → ⊢[T] A +theorem Theory.Derivable.botE [Bot Atom] {T : Theory Atom} [IsIntuitionistic T] + (A : Proposition Atom) : ⊢[T] ⊥ → ⊢[T] A | ⟨Γ, h, D⟩ => by refine ⟨insert (⊥ ⟶ A) Γ, by grind [IsIntuitionistic], ?_⟩ - apply implE (A := bot) + apply implE (A := ⊥) · exact ax .. · exact D.weak' (by grind) -theorem Theory.Derivable.dne {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : +theorem Theory.Derivable.dne [Bot Atom] {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : ⊢[T] (~~A) → ⊢[T] A | ⟨Γ, h, D⟩ => by refine ⟨insert (~~A ⟶ A) Γ, by grind [IsClassical], ?_⟩ @@ -462,8 +435,8 @@ theorem equiv_iff {A B : Proposition Atom} : A ≡ B ↔ Nonempty (Proposition.e refine ⟨?_,?_⟩ all_goals apply derivable_iff.mpr; constructor; apply implI; assumption -theorem Proposition.derivable_iff_equiv_top (T : Theory Atom) (A : Proposition Atom) : - ⊢[T] A ↔ A ≡[T] ⊤ := by +theorem Proposition.derivable_iff_equiv_top [Inhabited Atom] (T : Theory Atom) + (A : Proposition Atom) : ⊢[T] A ↔ A ≡[T] ⊤ := by constructor <;> intro h · constructor · refine ⟨∅, by grind, ?_⟩ diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean index 9106af18..be92ef0d 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Theorems.lean @@ -146,7 +146,7 @@ theorem conj_imp_of_disj_imps {A B C : Proposition Atom} : /-! ### Classical theorems -/ -theorem dn_equiv {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : +theorem dn_equiv [Bot Atom] {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : T.Equiv A (~~A) := by constructor · refine ⟨∅, by grind, ?_⟩ @@ -155,15 +155,15 @@ theorem dn_equiv {T : Theory Atom} [IsClassical T] (A : Proposition Atom) : · apply Theory.Derivable.ax' grind [IsClassical] -theorem lem {T : Theory Atom} [IsClassical T] {A : Proposition Atom} : +theorem lem [Bot Atom] {T : Theory Atom} [IsClassical T] {A : Proposition Atom} : T.Derivable (A ⋎ ~A) := by apply Theory.Derivable.dne apply Theory.Derivable.theory_weak (T := Theory.empty Atom) (hT := by grind) exact Derivable.not_not_lem -private def dneFor (A : Proposition Atom) := ~~A ⟶ A +private def dneFor [Bot Atom] (A : Proposition Atom) := ~~A ⟶ A -theorem disj_not_of_not_conj {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : +theorem disj_not_of_not_conj [Bot Atom] {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : T.SDerivable ⟨{~(A ⋏ B)}, ~A ⋎ ~B⟩ := by refine ⟨{~(A ⋏ B), dneFor A, dneFor B, dneFor (~A ⋎ ~B)}, ?_, ?_⟩ · grind [IsClassical, dneFor, Finset.coe_insert, Finset.coe_singleton] @@ -189,7 +189,7 @@ theorem disj_not_of_not_conj {T : Theory Atom} [IsClassical T] {A B : Propositio · apply disjI₂ exact ax' (by grind) -theorem impl_equiv_disj {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : +theorem impl_equiv_disj [Bot Atom] {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : (A ⟶ B) ≡[T] (~A ⋎ B) := by constructor · let ⟨Γ, h, D⟩ := lem (T := T) (A := A) @@ -215,7 +215,7 @@ theorem impl_equiv_disj {T : Theory Atom} [IsClassical T] {A B : Proposition Ato · grind · exact ax' (by grind) -theorem pierce {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : +theorem pierce [Bot Atom] {T : Theory Atom} [IsClassical T] {A B : Proposition Atom} : T.Derivable (((A ⟶ B) ⟶ A) ⟶ A) := by let ⟨Γ, h, D⟩ := lem (T := T) (A := A) refine ⟨insert (⊥ ⟶ B) Γ, by grind [IsClassical], ?_⟩ @@ -387,7 +387,7 @@ theorem absorb_disj_conj {A B : Proposition Atom} : (A ⋎ (A ⋏ B)) ≡ A := equiv_iff.mpr ⟨absorbDisjConj⟩ /-- Falsum is absorbing for conjunction -/ -theorem bot_conj_absorb (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : +theorem bot_conj_absorb [Bot Atom] (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : (A ⋏ ⊥) ≡[T] ⊥ := by constructor · refine ⟨∅, by grind, ?_⟩ @@ -403,7 +403,7 @@ theorem bot_conj_absorb (T : Theory Atom) {A : Proposition Atom} [IsIntuitionist · exact ax' (by grind) /-- Falsum is neutral for disjunction -/ -theorem bot_disj_neutral (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : +theorem bot_disj_neutral [Bot Atom] (T : Theory Atom) {A : Proposition Atom} [IsIntuitionistic T] : (A ⋎ ⊥) ≡[T] A := by constructor · refine ⟨{⊥ ⟶ A}, by grind [IsIntuitionistic], ?_⟩ @@ -551,12 +551,13 @@ theorem Theory.sup_le {A B C : Proposition Atom} : · exact D'.weak' (by grind) · exact ax .. -theorem Theory.le_top {A : Proposition Atom} : T.Derivable (A ⟶ ⊤) := by +theorem Theory.le_top [Inhabited Atom] {A : Proposition Atom} : T.Derivable (A ⟶ ⊤) := by refine ⟨∅, by grind, ?_⟩ apply implI exact derivationTop.weak' (by grind) -theorem Theory.bot_le {A : Proposition Atom} [IsIntuitionistic T] : T.Derivable (⊥ ⟶ A) := +theorem Theory.bot_le [Bot Atom] {A : Proposition Atom} [IsIntuitionistic T] : + T.Derivable (⊥ ⟶ A) := Theory.Derivable.ax' (by grind [IsIntuitionistic]) theorem Theory.himp_wd {A A' B B' : Proposition Atom} : From c4793c2cf9960a98aedc07afdae5b5c9c1b1b2d2 Mon Sep 17 00:00:00 2001 From: twwar Date: Mon, 6 Oct 2025 13:19:28 +0200 Subject: [PATCH 11/12] docs --- Cslib/Logics/Propositional/Defs.lean | 12 +++++++++++- .../Propositional/NaturalDeduction/Basic.lean | 13 +++++++++---- 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean index 35152d78..a73abe7f 100644 --- a/Cslib/Logics/Propositional/Defs.lean +++ b/Cslib/Logics/Propositional/Defs.lean @@ -5,7 +5,17 @@ Authors: Thomas Waring -/ import Mathlib.Order.Notation -/-! # Propositions -/ +/-! # Propositions + +We define `Proposition`, the type of propositions over a given type of atom. This type has a `Bot` +instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited. We introduce notation for +the logical connectives: `⊥ ⊤ ⋏ ⋎ ⟶ ~` for, respectively, falsum, verum, conjunction, disjunction, +implication and negation. + +NB: starting from a base type `Atom`, a canonical bottom element can be added using `WithBot Atom`, +from `Mathlib.Order.TypeTags` — this is defined as `Option Atom`, but conveniently adds all the +requisite coercions, instances, etc. +-/ universe u diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index dca5aedf..9a6f5bcb 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -17,7 +17,6 @@ double negation elimination to minimal logic. ## Main definitions -- `Proposition` : a type of propositions with atoms in a given type. - `Derivation` : natural deduction derivation, done in "sequent style", ie with explicit hypotheses at each step. Contexts are `Finset`'s of propositions, which avoids explicit contraction and exchange, and the axiom rule derives `{A} ∪ Γ ⊢ A` for any context `Γ`, allowing weakening to @@ -42,9 +41,15 @@ versions of `Derivable`, `SDerivable` and `Equiv`. ## Notation -We introduce notation for logical connectives `⊥ ⊤ ⋏ ⋎ ⟶ ~` for, respectively, falsum, verum, -conjunction, disjunction, implication and negation. For `T`-derivability, -sequent-derivability and --equivalence we have `⊢[T] A`, `Γ ⊢[T] A` and `A ≡[T] B`, respectively. +For `T`-derivability, -sequent-derivability and -equivalence we introduce the notations `⊢[T] A`, +`Γ ⊢[T] A` and `A ≡[T] B`, respectively. + +## TODO + +Add translations between minimal, intuitionistic and classical theories. For example: +- Complete `T : Theory Atom` to an intuitionistic `T' : Theory (WithBot Atom)`, ditto classical. +- Implement the Gödel-Gentzen and Kuroda negative translations, classical → intuitionistic and +classical → minimal, respectively. ## References From e698f1ed1cf4375d695f83919f2a242f576b5caf Mon Sep 17 00:00:00 2001 From: thomaskwaring <51426330+thomaskwaring@users.noreply.github.com> Date: Tue, 7 Oct 2025 18:29:15 +0200 Subject: [PATCH 12/12] typo --- Cslib/Logics/Propositional/NaturalDeduction/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean index 9a6f5bcb..8d23c031 100644 --- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean +++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean @@ -72,7 +72,7 @@ open Proposition /-- Contexts are finsets of propositions. -/ abbrev Ctx (Atom) := Finset (Proposition Atom) -/-- Theories are abitrary sets of propositions. -/ +/-- Theories are arbitrary sets of propositions. -/ abbrev Theory (Atom) := Set (Proposition Atom) abbrev Theory.empty (Atom) : Theory (Atom) := ∅