module Logic.Propositional.Classical where

Classical propositional logic๐Ÿ”—

Classical propositional logic is a simple classical logic that only contains โ€œatomicโ€ propositions and connectives like โ€œandโ€, โ€œorโ€ and โ€œnotโ€. Notably, it does not contain any quantifiers like โ€œforallโ€ and โ€œexistsโ€.

We can define the syntax of classical propositional logic in Agda as the following indexed inductive type.

data Proposition (ฮ“ : Nat) : Type where
  atom        : Fin ฮ“ โ†’ Proposition ฮ“
  โ€œโŠคโ€ โ€œโŠฅโ€     : Proposition ฮ“
  _โ€œโˆงโ€_ _โ€œโˆจโ€_ : Proposition ฮ“ โ†’ Proposition ฮ“ โ†’ Proposition ฮ“
  โ€œยฌโ€_        : Proposition ฮ“ โ†’ Proposition ฮ“

We represent atomic propositions as elements of Fin, and our indexing scheme gives an upper bound on the number of atomic propositions.

Next, we introduce contexts; these are simply lists of propositions.

data Ctx (ฮ“ : Nat) : Type where
  []  : Ctx ฮ“
  _โจพ_ : Ctx ฮ“ โ†’ Proposition ฮ“ โ†’ Ctx ฮ“

_++_ : โˆ€ {ฮ“} โ†’ Ctx ฮ“ โ†’ Ctx ฮ“ โ†’ Ctx ฮ“
ฯˆ ++ [] = ฯˆ
ฯˆ ++ (ฮธ โจพ P) = (ฯˆ ++ ฮธ) โจพ P

We also define a membership relation for contexts.

data _โˆˆ_ {ฮ“ : Nat} (P : Proposition ฮ“) : Ctx ฮ“ โ†’ Type where
  here  : โˆ€ {ฯˆ} โ†’ P โˆˆ (ฯˆ โจพ P)
  there : โˆ€ {ฯˆ Q} โ†’ P โˆˆ ฯˆ โ†’ P โˆˆ (ฯˆ โจพ Q)

Finally, we define a natural deduction proof calculus for classical propositional logic. Our proof systems is encoded as an indexed inductive _โŠข_; elements of ฯˆ โŠข P are proof trees that show P from some set of hypotheses ฯˆ.

data _โŠข_ {ฮ“ : Nat} (ฯˆ : Ctx ฮ“) : Proposition ฮ“ โ†’ Type where

Our first rule is pretty intuitive: If P is in our hypotheses ฯˆ, then we can deduce P from ฯˆ.

  hyp : โˆ€ {P} โ†’ P โˆˆ ฯˆ โ†’ ฯˆ โŠข P

Next, we give an introduction rule for โ€œtrueโ€ and an elimination rule for โ€œfalseโ€.

  โŠค-intro : ฯˆ โŠข โ€œโŠคโ€
  โŠฅ-elim  : โˆ€ {P} โ†’ ฯˆ โŠข โ€œโŠฅโ€ โ†’ ฯˆ โŠข P

The rules for โ€œandโ€ are more or less what one would expect.

  โˆง-intro  : โˆ€ {P Q} โ†’ ฯˆ โŠข P โ†’ ฯˆ โŠข Q โ†’ ฯˆ โŠข P โ€œโˆงโ€ Q
  โˆง-elim-l : โˆ€ {P Q} โ†’ ฯˆ โŠข P โ€œโˆงโ€ Q โ†’ ฯˆ โŠข P
  โˆง-elim-r : โˆ€ {P Q} โ†’ ฯˆ โŠข P โ€œโˆงโ€ Q โ†’ ฯˆ โŠข Q

However, โ€œorโ€ is a bit trickier, as we need to add things to our hypotheses in the elimination rule.

  โˆจ-intro-l : โˆ€ {P Q}   โ†’ ฯˆ โŠข P โ†’ ฯˆ โŠข P โ€œโˆจโ€ Q
  โˆจ-intro-r : โˆ€ {P Q}   โ†’ ฯˆ โŠข Q โ†’ ฯˆ โŠข P โ€œโˆจโ€ Q
  โˆจ-elim    : โˆ€ {P Q R} โ†’ ฯˆ โŠข P โ€œโˆจโ€ Q โ†’ ฯˆ โจพ P โŠข R โ†’ ฯˆ โจพ Q โŠข R โ†’ ฯˆ โŠข R

Finally, we add the rules for negation. To ensure that we are working with classical logic, we add a rule for double-negation elimination.

  ยฌ-intro   : โˆ€ {P} โ†’ ฯˆ โจพ P โŠข โ€œโŠฅโ€ โ†’ ฯˆ โŠข โ€œยฌโ€ P
  ยฌ-elim    : โˆ€ {P} โ†’ ฯˆ โŠข โ€œยฌโ€ P โ†’ ฯˆ โŠข P โ†’ ฯˆ โŠข โ€œโŠฅโ€
  dneg-elim : โˆ€ {P} โ†’ ฯˆ โŠข โ€œยฌโ€ (โ€œยฌโ€ P) โ†’ ฯˆ โŠข P

Weakening๐Ÿ”—

Indexing the type of propositions by the number of atomic propositions makes our life easier later. However, it does mean that we need to define weakening, which lets us increase the upper bound on the number of atoms in a proposition.

data Weakening (ฮ“ : Nat) : Nat โ†’ Type where
  done : Weakening ฮ“ ฮ“
  weak : โˆ€ {ฮ”} โ†’ Weakening (suc ฮ“) ฮ” โ†’ Weakening ฮ“ ฮ”
We omit the implementation of applying weakenings to the syntactic types, since itโ€™s pretty much mechanical.
ยฌweaken-suc-zero : Weakening (suc ฮ“) 0 โ†’ โŠฅ
ยฌweaken-suc-zero (weak ฯƒ) = ยฌweaken-suc-zero ฯƒ

wk-suc : Weakening ฮ“ ฮ” โ†’ Weakening ฮ“ (suc ฮ”)
wk-suc done     = weak done
wk-suc (weak ฯƒ) = weak (wk-suc ฯƒ)

!wk : Weakening 0 ฮ“
!wk {ฮ“ = zero}  = done
!wk {ฮ“ = suc ฮ“} = wk-suc !wk

inc-prop : Proposition ฮ“ โ†’ Proposition (suc ฮ“)
inc-prop (atom x)  = atom (weaken x)
inc-prop โ€œโŠคโ€       = โ€œโŠคโ€
inc-prop โ€œโŠฅโ€       = โ€œโŠฅโ€
inc-prop (p โ€œโˆงโ€ q) = inc-prop p โ€œโˆงโ€ inc-prop q
inc-prop (p โ€œโˆจโ€ q) = inc-prop p โ€œโˆจโ€ inc-prop q
inc-prop (โ€œยฌโ€ p)   = โ€œยฌโ€ (inc-prop p)

inc-ctx : Ctx ฮ“ โ†’ Ctx (suc ฮ“)
inc-ctx []      = []
inc-ctx (ฯˆ โจพ P) = inc-ctx ฯˆ โจพ inc-prop P

inc-atom : P โˆˆ ฯˆ โ†’ inc-prop P โˆˆ inc-ctx ฯˆ
inc-atom here      = here
inc-atom (there x) = there (inc-atom x)

inc-proof : ฯˆ โŠข P โ†’ inc-ctx ฯˆ โŠข inc-prop P
inc-proof (hyp x)        = hyp (inc-atom  x)
inc-proof โŠค-intro        = โŠค-intro
inc-proof (โŠฅ-elim p)     = โŠฅ-elim (inc-proof p)
inc-proof (โˆง-intro p q)  = โˆง-intro (inc-proof p) (inc-proof q)
inc-proof (โˆง-elim-l p)   = โˆง-elim-l (inc-proof p)
inc-proof (โˆง-elim-r p)   = โˆง-elim-r (inc-proof p)
inc-proof (โˆจ-intro-l p)  = โˆจ-intro-l (inc-proof p)
inc-proof (โˆจ-intro-r p)  = โˆจ-intro-r (inc-proof p)
inc-proof (โˆจ-elim p q r) = โˆจ-elim (inc-proof p) (inc-proof q) (inc-proof r)
inc-proof (ยฌ-intro p)    = ยฌ-intro (inc-proof p)
inc-proof (ยฌ-elim p q)   = ยฌ-elim (inc-proof p) (inc-proof q)
inc-proof (dneg-elim p)  = dneg-elim (inc-proof p)

bump-prop : Proposition ฮ“ โ†’ Proposition (suc ฮ“)
bump-prop (atom x)  = atom (fsuc x)
bump-prop โ€œโŠคโ€       = โ€œโŠคโ€
bump-prop โ€œโŠฅโ€       = โ€œโŠฅโ€
bump-prop (p โ€œโˆงโ€ q) = bump-prop p โ€œโˆงโ€ bump-prop q
bump-prop (p โ€œโˆจโ€ q) = bump-prop p โ€œโˆจโ€ bump-prop q
bump-prop (โ€œยฌโ€ p)   = โ€œยฌโ€ bump-prop p

bump-ctx : Ctx ฮ“ โ†’ Ctx (suc ฮ“)
bump-ctx []      = []
bump-ctx (ฯˆ โจพ P) = bump-ctx ฯˆ โจพ bump-prop P

bump-atom : P โˆˆ ฯˆ โ†’ bump-prop P โˆˆ bump-ctx ฯˆ
bump-atom here      = here
bump-atom (there p) = there (bump-atom p)

bump-proof : ฯˆ โŠข P โ†’ bump-ctx ฯˆ โŠข bump-prop P
bump-proof (hyp x)        = hyp (bump-atom x)
bump-proof โŠค-intro        = โŠค-intro
bump-proof (โŠฅ-elim p)     = โŠฅ-elim (bump-proof p)
bump-proof (โˆง-intro p q)  = โˆง-intro (bump-proof p) (bump-proof q)
bump-proof (โˆง-elim-l p)   = โˆง-elim-l (bump-proof p)
bump-proof (โˆง-elim-r p)   = โˆง-elim-r (bump-proof p)
bump-proof (โˆจ-intro-l p)  = โˆจ-intro-l (bump-proof p)
bump-proof (โˆจ-intro-r p)  = โˆจ-intro-r (bump-proof p)
bump-proof (โˆจ-elim p q r) = โˆจ-elim (bump-proof p) (bump-proof q) (bump-proof r)
bump-proof (ยฌ-intro p)    = ยฌ-intro (bump-proof p)
bump-proof (ยฌ-elim p q)   = ยฌ-elim (bump-proof p) (bump-proof q)
bump-proof (dneg-elim p)  = dneg-elim (bump-proof p)

wk-atom : Weakening ฮ“ ฮ” โ†’ Fin ฮ“ โ†’ Fin ฮ”
wk-atom done     x = x
wk-atom (weak ฯƒ) x = wk-atom ฯƒ (weaken x)

wk-prop : Weakening ฮ“ ฮ” โ†’ Proposition ฮ“ โ†’ Proposition ฮ”
wk-prop done     P = P
wk-prop (weak ฯƒ) P = wk-prop ฯƒ (inc-prop P)

wk-ctx : Weakening ฮ“ ฮ” โ†’ Ctx ฮ“ โ†’ Ctx ฮ”
wk-ctx done     ฯˆ = ฯˆ
wk-ctx (weak ฯƒ) ฯˆ = wk-ctx ฯƒ (inc-ctx ฯˆ)

wk-proof : (ฯƒ : Weakening ฮ“ ฮ”) โ†’ ฯˆ โŠข P โ†’ wk-ctx ฯƒ ฯˆ โŠข wk-prop ฯƒ P
wk-proof done     pf = pf
wk-proof (weak ฯƒ) pf = wk-proof ฯƒ (inc-proof pf)

shift-atom : Weakening ฮ“ ฮ” โ†’ Fin ฮ“ โ†’ Fin ฮ”
shift-atom done     i = i
shift-atom (weak ฯƒ) i = shift-atom ฯƒ (fsuc i)

shift-prop : Weakening ฮ“ ฮ” โ†’ Proposition ฮ“ โ†’ Proposition ฮ”
shift-prop done     p = p
shift-prop (weak ฯƒ) p = shift-prop ฯƒ (bump-prop p)

shift-ctx : Weakening ฮ“ ฮ” โ†’ Ctx ฮ“ โ†’ Ctx ฮ”
shift-ctx done     ฯˆ = ฯˆ
shift-ctx (weak ฯƒ) ฯˆ = shift-ctx ฯƒ (bump-ctx ฯˆ)

shift-ctx-[]
  : (ฯƒ : Weakening ฮ“ ฮ”)
  โ†’ shift-ctx ฯƒ [] โ‰ก []
shift-ctx-[] done = refl
shift-ctx-[] (weak ฯƒ) = shift-ctx-[] ฯƒ

shift-ctx-โจพ
  : (ฯƒ : Weakening ฮ“ ฮ”)
  โ†’ (ฯˆ : Ctx ฮ“) (P : Proposition ฮ“)
  โ†’ shift-ctx ฯƒ (ฯˆ โจพ P) โ‰ก shift-ctx ฯƒ ฯˆ โจพ shift-prop ฯƒ P
shift-ctx-โจพ done     ฯˆ P = refl
shift-ctx-โจพ (weak ฯƒ) ฯˆ P = shift-ctx-โจพ ฯƒ (bump-ctx ฯˆ) (bump-prop P)

shift-prop-โ€œยฌโ€
  : (ฯƒ : Weakening ฮ“ ฮ”)
  โ†’ (P : Proposition ฮ“)
  โ†’ shift-prop ฯƒ (โ€œยฌโ€ P) โ‰ก โ€œยฌโ€ (shift-prop ฯƒ P)
shift-prop-โ€œยฌโ€ done     P = refl
shift-prop-โ€œยฌโ€ (weak ฯƒ) P = shift-prop-โ€œยฌโ€ ฯƒ (bump-prop P)

Context inclusions๐Ÿ”—

We also want to be able to modify our collection of hypotheses. We do this by defining a notion of context inclusion, where an inclusion ฮ“โ†’ฮ”\Gamma \to \Delta denotes that we can obtain every hypothesis in ฮ”\Delta by dropping hypotheses from ฮ“\Gamma. We call such context inclusions renamings.

data Rename {ฮ“} : Ctx ฮ“ โ†’ Ctx ฮ“ โ†’ Type where
  done : Rename [] []
  drop : โˆ€ {ฯˆ ฮธ P} โ†’ Rename ฯˆ ฮธ โ†’ Rename (ฯˆ โจพ P) ฮธ
  keep : โˆ€ {ฯˆ ฮธ P} โ†’ Rename ฯˆ ฮธ โ†’ Rename (ฯˆ โจพ P) (ฮธ โจพ P)

Identity renamings exist, and renamings are closed under composition. With a bit of elbow grease, we could show that contexts and renamings form a precategory, thought we do not do so here.

idrn : Rename ฯˆ ฯˆ
idrn {ฯˆ = []} = done
idrn {ฯˆ = ฯˆ โจพ P} = keep (idrn {ฯˆ = ฯˆ})

_โˆ˜rn_ : Rename ฮธ ฮถ โ†’ Rename ฯˆ ฮธ โ†’ Rename ฯˆ ฮถ
p      โˆ˜rn done   = p
p      โˆ˜rn drop q = drop (p โˆ˜rn q)
drop p โˆ˜rn keep q = drop (p โˆ˜rn q)
keep p โˆ˜rn keep q = keep (p โˆ˜rn q)

We also have a renaming that drops every hypothesis, and renamings that project out half of a context. Categorically, these correspond to the maps into the terminal object and maps out of the product, resp.

!rn : Rename ฯˆ []
!rn {ฯˆ = []}    = done
!rn {ฯˆ = ฯˆ โจพ x} = drop !rn

ฯ€โ‚-rn : Rename (ฯˆ ++ ฮธ) ฯˆ
ฯ€โ‚-rn {ฮธ = []}    = idrn
ฯ€โ‚-rn {ฮธ = ฮธ โจพ P} = drop ฯ€โ‚-rn

ฯ€โ‚‚-rn : Rename (ฯˆ ++ ฮธ) ฮธ
ฯ€โ‚‚-rn {ฮธ = []}    = !rn
ฯ€โ‚‚-rn {ฮธ = ฮธ โจพ P} = keep ฯ€โ‚‚-rn

Renamings act contravariantly on variables and derivations. In categorical terms, this induces a presheaf on the category of contexts.

rename-hyp : Rename ฯˆ ฮธ โ†’ P โˆˆ ฮธ โ†’ P โˆˆ ฯˆ
rename-hyp (drop rn) mem         = there (rename-hyp rn mem)
rename-hyp (keep rn) here        = here
rename-hyp (keep rn) (there mem) = there (rename-hyp rn mem)

rename : Rename ฯˆ ฮธ โ†’ ฮธ โŠข P โ†’ ฯˆ โŠข P
rename rn (hyp x)        = hyp (rename-hyp rn x)
rename rn โŠค-intro        = โŠค-intro
rename rn (โŠฅ-elim p)     = โŠฅ-elim (rename rn p)
rename rn (โˆง-intro p q)  = โˆง-intro (rename rn p) (rename rn q)
rename rn (โˆง-elim-l p)   = โˆง-elim-l (rename rn p)
rename rn (โˆง-elim-r p)   = โˆง-elim-r (rename rn p)
rename rn (โˆจ-intro-l p)  = โˆจ-intro-l (rename rn p)
rename rn (โˆจ-intro-r p)  = โˆจ-intro-r (rename rn p)
rename rn (โˆจ-elim p q r) = โˆจ-elim
  (rename rn p) (rename (keep rn) q) (rename (keep rn) r)
rename rn (ยฌ-intro p)    = ยฌ-intro (rename (keep rn) p)
rename rn (ยฌ-elim p q)   = ยฌ-elim (rename rn p) (rename rn q)
rename rn (dneg-elim p)  = dneg-elim (rename rn p)

Some elementary theorems๐Ÿ”—

With those bits of structural work completed, we can focus our attention to some theorems. First, note that we can prove the law of excluded middle.

lem : โˆ€ {ฮ“} {ฯˆ : Ctx ฮ“} (P : Proposition ฮ“) โ†’ ฯˆ โŠข P โ€œโˆจโ€ (โ€œยฌโ€ P)
lem P =
  dneg-elim                 $
  ยฌ-intro                   $
  ยฌ-elim (hyp here)         $
  โˆจ-intro-r                 $
  ยฌ-intro                   $
  ยฌ-elim (hyp (there here)) $
  โˆจ-intro-l (hyp here)

We also have all four De Morgan laws.

dneg-intro : ฯˆ โŠข P โ†’ ฯˆ โŠข โ€œยฌโ€ (โ€œยฌโ€ P)
dneg-intro p = ยฌ-intro (ยฌ-elim (hyp here) (rename (drop idrn) p))

ยฌโˆง-intro-l : ฯˆ โŠข โ€œยฌโ€ P โ†’ ฯˆ โŠข โ€œยฌโ€ (P โ€œโˆงโ€ Q)
ยฌโˆง-intro-l p = ยฌ-intro (ยฌ-elim (rename (drop idrn) p) (โˆง-elim-l (hyp here)))

ยฌโˆง-intro-r : ฯˆ โŠข โ€œยฌโ€ Q โ†’ ฯˆ โŠข โ€œยฌโ€ (P โ€œโˆงโ€ Q)
ยฌโˆง-intro-r p = ยฌ-intro (ยฌ-elim (rename (drop idrn) p) (โˆง-elim-r (hyp here)))

ยฌโˆง-elim : ฯˆ โŠข โ€œยฌโ€ (P โ€œโˆงโ€ Q) โ†’ ฯˆ โŠข (โ€œยฌโ€ P) โ€œโˆจโ€ (โ€œยฌโ€ Q)
ยฌโˆง-elim {P = P} {Q = Q} p =
  โˆจ-elim (lem P)
    (โˆจ-elim (lem Q)
      (โŠฅ-elim
        (ยฌ-elim (rename (drop (drop idrn)) p)
        (โˆง-intro (hyp (there here)) (hyp here))))
      (โˆจ-intro-r (hyp here)))
    (โˆจ-intro-l (hyp here))

ยฌโˆจ-intro : ฯˆ โŠข โ€œยฌโ€ P โ†’ ฯˆ โŠข โ€œยฌโ€ Q โ†’ ฯˆ โŠข โ€œยฌโ€ (P โ€œโˆจโ€ Q)
ยฌโˆจ-intro p q =
  ยฌ-intro $
  โˆจ-elim (hyp here)
    (ยฌ-elim (rename (drop (drop idrn)) p) (hyp here))
    (ยฌ-elim (rename (drop (drop idrn)) q) (hyp here))

As we are working in a classical setting, we can define implication P โ‡’ Q as ยฌ P โˆจ Q. Note that the normal introduction and elimination rules for implications are theorems.

opaque
  _โ€œโ‡’โ€_ : โˆ€ {ฮ“} โ†’ Proposition ฮ“ โ†’ Proposition ฮ“ โ†’ Proposition ฮ“
  P โ€œโ‡’โ€ Q = (โ€œยฌโ€ P) โ€œโˆจโ€ Q

  โ‡’-intro : ฯˆ โจพ P โŠข Q โ†’ ฯˆ โŠข P โ€œโ‡’โ€ Q
  โ‡’-intro {P = P} pf = โˆจ-elim (lem P) (โˆจ-intro-r pf) (โˆจ-intro-l (hyp here))

  โ‡’-elim : ฯˆ โŠข P โ€œโ‡’โ€ Q โ†’ ฯˆ โŠข P โ†’ ฯˆ โŠข Q
  โ‡’-elim {Q = Q} imp p = โˆจ-elim imp
    (โŠฅ-elim (ยฌ-elim (hyp here) (rename (drop idrn) p)))
    (hyp here)

We also prove some helpful extra lemmas regarding implications.

โ‡’-uncurry : ฯˆ โŠข P โ€œโ‡’โ€ Q โ†’ ฯˆ โจพ P โŠข Q
โ‡’-uncurry p = โ‡’-elim (rename (drop idrn) p) (hyp here)

โ‡’-flip : ฯˆ โŠข P โ€œโ‡’โ€ Q โ€œโ‡’โ€ R โ†’ ฯˆ โŠข Q โ€œโ‡’โ€ P โ€œโ‡’โ€ R
โ‡’-flip p =
  โ‡’-intro $ โ‡’-intro $
  โ‡’-elim
    (โ‡’-elim (rename (drop (drop idrn)) p) (hyp here))
    (hyp (there here))

Next, we define a conjunction operator that works on lists of propositions.

โ€œโ‹€โ€ : Ctx ฮ“ โ†’ Proposition ฮ“
โ€œโ‹€โ€ []      = โ€œโŠคโ€
โ€œโ‹€โ€ (ฯˆ โจพ P) = โ€œโ‹€โ€ ฯˆ โ€œโˆงโ€ P

โ‹€-intro : (โˆ€ {P} โ†’ P โˆˆ ฯˆ โ†’ ฮธ โŠข P) โ†’ ฮธ โŠข โ€œโ‹€โ€ ฯˆ
โ‹€-intro {ฯˆ = []}    pfs = โŠค-intro
โ‹€-intro {ฯˆ = ฯˆ โจพ P} pfs = โˆง-intro (โ‹€-intro (pfs โˆ˜ there)) (pfs here)

โ‹€-elim : P โˆˆ ฯˆ โ†’ ฮธ โŠข โ€œโ‹€โ€ ฯˆ โ†’ ฮธ โŠข P
โ‹€-elim here      p = โˆง-elim-r p
โ‹€-elim (there x) p = โ‹€-elim x (โˆง-elim-l p)

We can also define an n-ary implication connective.

_โ€œโ‡›โ€_ : Ctx ฮ“ โ†’ Proposition ฮ“ โ†’ Proposition ฮ“
[]      โ€œโ‡›โ€ P = P
(ฯˆ โจพ Q) โ€œโ‡›โ€ P = ฯˆ โ€œโ‡›โ€ (Q โ€œโ‡’โ€ P)

โ‡›-intro : ฮธ ++ ฯˆ โŠข P โ†’ ฮธ โŠข ฯˆ โ€œโ‡›โ€ P
โ‡›-intro {ฯˆ = []}    p = p
โ‡›-intro {ฯˆ = ฯˆ โจพ Q} p = โ‡›-intro (โ‡’-intro p)

โ‡›-uncurry : ฮธ โŠข ฯˆ โ€œโ‡›โ€ P โ†’ ฮธ ++ ฯˆ โŠข P
โ‡›-uncurry {ฯˆ = []}    p = p
โ‡›-uncurry {ฯˆ = ฯˆ โจพ Q} p = โ‡’-uncurry (โ‡›-uncurry p)

โ‡›-elim : ฮธ โŠข (ฯˆ โจพ P) โ€œโ‡›โ€ Q โ†’ ฮธ โŠข P โ†’ ฮธ โŠข ฯˆ โ€œโ‡›โ€ Q
โ‡›-elim {ฯˆ = ฯˆ} p q = โ‡›-intro (โ‡’-elim (โ‡›-uncurry {ฯˆ = ฯˆ} p) (rename ฯ€โ‚-rn q))

Semantics๐Ÿ”—

The most obvious way to interpret classical logic is as operations on booleans.

sem-prop : โˆ€ {ฮ“} โ†’ Proposition ฮ“ โ†’ (Fin ฮ“ โ†’ Bool) โ†’ Bool
sem-prop (atom x)  ฯ = ฯ x
sem-prop โ€œโŠคโ€       ฯ = true
sem-prop โ€œโŠฅโ€       ฯ = false
sem-prop (P โ€œโˆงโ€ Q) ฯ = and (sem-prop P ฯ) (sem-prop Q ฯ)
sem-prop (P โ€œโˆจโ€ Q) ฯ = or (sem-prop P ฯ) (sem-prop Q ฯ)
sem-prop (โ€œยฌโ€ P)   ฯ = not (sem-prop P ฯ)

sem-ctx : โˆ€ {ฮ“} โ†’ Ctx ฮ“ โ†’ (Fin ฮ“ โ†’ Bool) โ†’ Bool
sem-ctx ฯˆ ฯ = sem-prop (โ€œโ‹€โ€ ฯˆ) ฯ

We also define a notion of semantic entailment, wherein ฯˆ semantically entails P when for every assigment of variables ฯ, if โŸฆ ฯˆ โŸง ฯ โ‰ก true, then โŸฆ P โŸง ฯ โ‰ก true.

_โŠจ_ : โˆ€ {ฮ“} โ†’ Ctx ฮ“ โ†’ Proposition ฮ“ โ†’ Type
_โŠจ_ {ฮ“} ฯˆ P = โˆ€ (ฯ : Fin ฮ“ โ†’ Bool) โ†’ โŸฆ ฯˆ โŸง ฯ โ‰ก true โ†’ โŸฆ P โŸง ฯ โ‰ก true

Soundness๐Ÿ”—

Soundness is something that is often poorly explained in classical logic.

The traditional definition goes something like this: a logic is sound if every provable theorem ฯˆ โŠข P is true. This definition obscures what is really going on: what we care about is that a provable theorem ฯˆ โŠข P is true in some semantics.

For classical propositional logic, it happens to be the case that we can focus our attention on one semantics (the booleans) โ€” weโ€™ll see ahead why this is the case โ€” so authors often conflate โ€œtrueโ€ with โ€œtrue in this particular semanticsโ€.

The actual statement of soundness that we will be using is the following: if ฯˆ โŠข P is provable, then we have the semantic entailment ฯˆ โŠจ P. This follows by induction on the proof trees, and itโ€™s mostly mechanical.

hyp-sound : โˆ€ {ฮ“} {ฯˆ : Ctx ฮ“} {P : Proposition ฮ“} โ†’ P โˆˆ ฯˆ โ†’ ฯˆ โŠจ P
hyp-sound here      ฯ hyps-true = and-reflect-true-r hyps-true
hyp-sound (there m) ฯ hyps-true = hyp-sound m ฯ (and-reflect-true-l hyps-true)

sound : ฯˆ โŠข P โ†’ ฯˆ โŠจ P
sound (hyp x)    ฯ hyps-true = hyp-sound x ฯ hyps-true
sound โŠค-intro    ฯ hyps-true = refl
sound (โŠฅ-elim p) ฯ hyps-true =
  absurd (trueโ‰false (sym (sound p ฯ hyps-true)))

sound (โˆง-intro p q) ฯ hyps-true =
  apโ‚‚ and (sound p ฯ hyps-true) (sound q ฯ hyps-true)
sound (โˆง-elim-l p) ฯ hyps-true =
  and-reflect-true-l (sound p ฯ hyps-true)
sound (โˆง-elim-r p) ฯ hyps-true =
  and-reflect-true-r (sound p ฯ hyps-true)

sound (โˆจ-intro-l p) ฯ hyps-true =
  apโ‚‚ or (sound p ฯ hyps-true) refl
sound (โˆจ-intro-r p) ฯ hyps-true =
  apโ‚‚ or refl (sound p ฯ hyps-true) โˆ™ or-truer _
sound (โˆจ-elim p q r) ฯ hyps-true with or-reflect-true (sound p ฯ hyps-true)
... | inl P-true = sound q ฯ (apโ‚‚ and hyps-true P-true)
... | inr Q-true = sound r ฯ (apโ‚‚ and hyps-true Q-true)

sound (ยฌ-intro {P = P} p) ฯ hyps-true =
  Bool-elim (ฮป b โ†’ โŸฆ P โŸง ฯ โ‰ก b โ†’ not b โ‰ก true)
    (ฮป P-true โ†’ sound p ฯ (apโ‚‚ and hyps-true P-true))
    (ฮป _ โ†’ refl)
    (โŸฆ P โŸง ฯ) refl
sound (ยฌ-elim {P = P} p q) ฯ hyps-true =
  absurd (not-no-fixed (sound q ฯ hyps-true โˆ™ sym (sound p ฯ hyps-true)))
sound (dneg-elim {P = P} p) ฯ hyps-true =
  sym (not-involutive (โŸฆ P โŸง ฯ)) โˆ™ sound p ฯ hyps-true

Completeness๐Ÿ”—

As mentioned earlier, we often think of classical propositional logic as having a single semantics. This is largely justified by the fact that if ฯˆ semantically entails P in the booleans, then we can prove that ฯˆ โŠข P! In other words, the Boolean semantics for classical propositional logic is complete.

This somewhat miraculous theorem is often taken for granted. Completeness is why truth-tables are a valid form of reasoning, but this is hardly ever mentioned when teaching logic. As we shall soon see, this theorem isnโ€™t exactly trivial, either.

First, let us lay out our general proof strategy. We shall start by building a context ฯ^\hat{\rho} from an assignment ฯ\rho that contains only (potentially negated) atoms. If ฯ\rho assigns true to an atom xx, we will add xx to ฯ^\hat{\rho}. Conversely, if ฯ\rho assigns false to xx, we add ยฌx\neg x to ฯ^\hat{\rho}.

We will then show that for any assignment ฯ\rho, if โŸฆPโŸงฯ\llbracket P \rrbracket \rho is true, then ฯ^โŠขP\hat{\rho} \vdash P; likewise, if โŸฆPโŸงฯ\llbracket P \rrbracket \rho is false, then ฯ^โŠขยฌP\hat{\rho} \vdash \neg P.

From this fact, we can deduce that โŠจP\vDash P entails โŠขP\vdash P by repeatedly applying excluded middle to every single atom in PP, and applying our previous lemmas when we are done. Finally, we can transform any sequent ฯˆโŠขP\psi \vdash P into an equivalent sequent in a closed context by repeatedly introducing implications, which lets us apply the argument involving excluded middle.

With that sketch out of the way, letโ€™s dive into the details! First, we define a function tabulate that forms a context from an assignment; this is the ฯ^\hat{\rho} from the proof sketch. Some variable munging is required to make Agda happy, but it is more or less what one would expect.

tabulate : (Fin ฮ“ โ†’ Bool) โ†’ Ctx ฮ“
tabulate {ฮ“ = zero}  ฯ = []
tabulate {ฮ“ = suc ฮ“} ฯ =
  bump-ctx (tabulate (ฯ โˆ˜ fsuc)) โจพ (if ฯ 0 then 0 else โ€œยฌโ€ 0)

Next, some small helper lemmas that let us link assignments of atoms and proofs of those atoms. Essentially, these state that if ฯ(x)\rho(x) assigns a truth value to xx, then we should be able to prove this under the assumptions ฯ^\hat{\rho}.

tabulate-atom-true
  : (x : Fin ฮ“)
  โ†’ (ฯ : Fin ฮ“ โ†’ Bool)
  โ†’ ฯ x โ‰ก true
  โ†’ tabulate ฯ โŠข atom x
tabulate-atom-true {ฮ“ = suc ฮ“} fzero ฯ x-true with ฯ 0
... | true  = hyp here
... | false = absurd (trueโ‰false $ sym x-true)
tabulate-atom-true {ฮ“ = suc ฮ“} (fsuc x) ฯ x-true =
  rename (drop idrn) (bump-proof (tabulate-atom-true x (ฯ โˆ˜ fsuc) x-true))

tabulate-atom-false
  : (x : Fin ฮ“)
  โ†’ (ฯ : Fin ฮ“ โ†’ Bool)
  โ†’ ฯ x โ‰ก false
  โ†’ tabulate ฯ โŠข โ€œยฌโ€ atom x
tabulate-atom-false {ฮ“ = suc ฮ“} fzero ฯ x-false with ฯ 0
... | false = hyp here
... | true  = absurd (trueโ‰false x-false)
tabulate-atom-false {ฮ“ = suc ฮ“} (fsuc x) ฯ x-false =
  rename (drop idrn) (bump-proof (tabulate-atom-false x (ฯ โˆ˜ fsuc) x-false))

Now onto the key lemmas. By performing mutual induction on PP, we can note that if โŸฆPโŸงฯ\llbracket P \rrbracket \rho is true, then ฯ^โŠขP\hat{\rho} \vdash P and, conversely, that ฯ^โŠขยฌP\hat{\rho} \vdash \neg P if โŸฆPโŸงฯ\llbracket P \rrbracket \rho is false.

tabulate-true
  : โˆ€ (P : Proposition ฮ“) (ฯ : Fin ฮ“ โ†’ Bool)
  โ†’ โŸฆ P โŸง ฯ โ‰ก true
  โ†’ tabulate ฯ โŠข P

tabulate-false
  : โˆ€ (P : Proposition ฮ“) (ฯ : Fin ฮ“ โ†’ Bool)
  โ†’ โŸฆ P โŸง ฯ โ‰ก false
  โ†’ tabulate ฯ โŠข โ€œยฌโ€ P

tabulate-true (atom x)  ฯ P-true = tabulate-atom-true x ฯ P-true
tabulate-true โ€œโŠคโ€       ฯ P-true = โŠค-intro
tabulate-true โ€œโŠฅโ€       ฯ P-true = absurd (trueโ‰false $ sym P-true)
tabulate-true (P โ€œโˆงโ€ Q) ฯ PโˆงQ-true = โˆง-intro
  (tabulate-true P ฯ (and-reflect-true-l PโˆงQ-true))
  (tabulate-true Q ฯ (and-reflect-true-r PโˆงQ-true))
tabulate-true (P โ€œโˆจโ€ Q) ฯ PโˆจQ-true with or-reflect-true PโˆจQ-true
... | inl P-true = โˆจ-intro-l (tabulate-true P ฯ P-true)
... | inr Q-true = โˆจ-intro-r (tabulate-true Q ฯ Q-true)
tabulate-true (โ€œยฌโ€ P) ฯ P-true = tabulate-false P ฯ (not-inj P-true)

tabulate-false (atom x)  ฯ P-false = tabulate-atom-false x ฯ P-false
tabulate-false โ€œโŠคโ€       ฯ P-false = absurd (trueโ‰false P-false)
tabulate-false โ€œโŠฅโ€       ฯ P-false = ยฌ-intro (hyp here)
tabulate-false (P โ€œโˆงโ€ Q) ฯ PโˆงQ-false with and-reflect-false PโˆงQ-false
... | inl P-false = ยฌโˆง-intro-l (tabulate-false P ฯ P-false)
... | inr Q-false = ยฌโˆง-intro-r (tabulate-false Q ฯ Q-false)
tabulate-false (P โ€œโˆจโ€ Q) ฯ PโˆจQ-false = ยฌโˆจ-intro
  (tabulate-false P ฯ (or-reflect-false-l PโˆจQ-false))
  (tabulate-false Q ฯ (or-reflect-false-r PโˆจQ-false))
tabulate-false (โ€œยฌโ€ P) ฯ P-false =
  dneg-intro (tabulate-true P ฯ (not-inj P-false))

Next, let PP be a proposition and let ฯ\rho be an assignment for the first nn atoms in PP. If PP is a tautology, then ฯ^โŠขP\hat{\rho} \vdash P. This follows from induction on the number of atoms not assigned by ฯ\rho. If ฯ\rho assigns all of the atoms of PP, then by our previous lemma we have ฯ^โŠขP\hat{\rho} \vdash P. For the inductive step, let xx be a atom not covered by ฯ\rho. Excluded middle lets us case on the truth value of xx; if it is true, then we extend ฯ\rho with x:=โŠคx := \top, and use the induction hypothesis. Likewise, if xx is false, then we extend ฯ\rho with x:=โŠฅx := \bot.

Weโ€™ll then show an appropriate generalisation of the completeness theorem, which will allow us to apply induction. Specifically, weโ€™ll show that, if PP is a tautology in k+nk+n atoms, and we have an assignment ฯ\rho of truth values for the first kk atoms in PP, then ฯ^โŠขP\hat{\rho} \vdash P, by induction on nn, i.e.ยthe number of atoms which ฯ\rho does not assign.

tabulate-complete
  : โˆ€ {ฮ” ฮ“} (P : Proposition ฮ“)
  โ†’ (ฯƒ : Weakening ฮ” ฮ“) (ฯ : Fin ฮ” โ†’ Bool)
  โ†’ [] โŠจ P โ†’ shift-ctx ฯƒ (tabulate ฯ) โŠข P

The base case is when we have no new atoms: we can then appeal to our previous theorem tabulate-true.

tabulate-complete P done ฯ P-taut =
  tabulate-true P ฯ (P-taut ฯ refl)

For the inductive step, we have some 1+n1+n new atoms, and weโ€™re free to assume that any tautology in k+nk+n atoms is a theorem. We use this induction hypothesis twice, once on ฯ\rho extended with x:=โŠคx := \top, and once on it extended with x:=โŠฅx := \bot. We now have proofs that xโŠขPx \vdash P and ยฌxโŠขP\neg x \vdash P; but by the excluded middle (and disjunction elimination), this suffices to prove PP!

tabulate-complete {ฮ“ = ฮ“} P (weak ฯƒ) ฯ P-taut = โˆจ-elim
  (lem (shift-prop ฯƒ (atom 0)))
  (subst (_โŠข P)
    (shift-ctx-โจพ ฯƒ _ _)
    (tabulate-complete P ฯƒ (ฯ [ 0 โ‰” true ]) P-taut))
  (subst (_โŠข P)
    (shift-ctx-โจพ ฯƒ _ _ โˆ™ apโ‚‚ _โจพ_ refl (shift-prop-โ€œยฌโ€ ฯƒ (atom 0)))
    (tabulate-complete P ฯƒ (ฯ [ 0 โ‰” false ]) P-taut))

If we start this with an empty assignment, we will construct a gigantic proof, which applies excluded middle to every single atom in PP, and then applies the relevant introduction rules at the leaves. Despite the obvious inefficiency of this procedure, it allows us to deduce that we have completeness for tautologies.

taut-complete : (P : Proposition ฮ“) โ†’ [] โŠจ P โ†’ [] โŠข P
taut-complete P taut =
  subst (_โŠข P) (shift-ctx-[] !wk) (tabulate-complete P !wk (ฮป ()) taut)

Finally, we note that proofs of P1โ†’โ‹ฏโ†’Pnโ†’QP_1 \to \cdots \to P_n \to Q yield proofs of P1,โ‹ฏโ€‰,PnโŠขQP_1, \cdots, P_n \vdash Q, and likewise for semantic entailments.

โ‡›-closed : [] โŠข ฯˆ โ€œโ‡›โ€ P โ†’ ฯˆ โŠข P
โ‡›-closed {ฯˆ = []}    p = p
โ‡›-closed {ฯˆ = ฯˆ โจพ Q} p = โ‡’-uncurry (โ‡›-closed p)

โ‡›-valid : โˆ€ (ฯˆ : Ctx ฮ“) (P : Proposition ฮ“) โ†’ ฯˆ โŠจ P โ†’ [] โŠจ (ฯˆ โ€œโ‡›โ€ P)
โ‡›-valid []      P valid = valid
โ‡›-valid (ฯˆ โจพ Q) P valid ฯ taut = apโ‚‚ and refl
  (โ‡›-valid ฯˆ (Q โ€œโ‡’โ€ P) (ฮป ฯ' ฯˆ-true โ†’ it ฯ' ฯˆ-true (โŸฆ Q โŸง ฯ') refl) ฯ taut)

This lets us generalize our result for tautologies to any proposition-in-context ฯˆโŠจP\psi \vDash P!

complete : ฯˆ โŠจ P โ†’ ฯˆ โŠข P
complete {ฯˆ = ฯˆ} {P = P} valid =
  โ‡›-closed $ taut-complete (ฯˆ โ€œโ‡›โ€ P) (โ‡›-valid ฯˆ P valid)