open import 1Lab.Prelude

open import Data.Bool
open import Data.List hiding (_++_ ; drop ; tabulate)
open import Data.Fin using (Fin; fzero; fsuc; weaken; inject; _[_≔_])
open import Data.Nat
open import Data.Sum

open import Meta.Brackets

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)

instance
  Membership-Ctx : ∀ {Γ} → Membership (Proposition Γ) (Ctx Γ) lzero
  Membership-Ctx = record { _∈_ = _∈ᶜ_ }

infixr  _“⇒”_
infixr  _“∧”_
infixr  _“∨”_
infixl  _⨾_
infix  _⊢_ _⊨_

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

private variable
  Γ Δ Θ : Nat
  ψ θ ζ : Ctx Γ
  P Q R : Proposition Γ

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 Γ Δ

¬weaken-suc-zero : Weakening (suc Γ)  → ⊥
¬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  Γ
!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 \text{.}$ 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 (“⋀” ψ) ρ

instance
  ⟦⟧-Proposition : ∀ {Γ} → ⟦⟧-notation (Proposition Γ)
  ⟦⟧-Proposition {Γ = Γ} = brackets ((Fin Γ → Bool) → Bool) sem-prop

  ⟦⟧-Ctx : ∀ {Γ} → ⟦⟧-notation (Ctx Γ)
  ⟦⟧-Ctx {Γ = Γ} = brackets ((Fin Γ → Bool) → Bool) sem-ctx

  Number-Proposition : ∀ {Γ} → Number (Proposition Γ)
  Number-Proposition {Γ} .Number.Constraint k = k Data.Nat.< Γ
  Number-Proposition .Number.fromNat n        = atom (fromNat n)

opaque
  unfolding _“⇒”_
  ⇒-sem
    : ∀ {Γ} {P Q : Proposition Γ}
    → ∀ (ρ : Fin Γ → Bool) → ⟦ P “⇒” Q ⟧ ρ ≡ imp (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)
  ⇒-sem {P = P} {Q = Q} ρ =
    imp-not-or (⟦ P ⟧ ρ) (⟦ Q ⟧ ρ)

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 $x\text{,}$ we will add $x$ to $\hat{\rho }\text{.}$ Conversely, if $\rho$ assigns false to $x\text{,}$ we add $\neg x$ to $\hat{\rho }\text{.}$

We will then show that for any assignment $\rho \text{,}$ if $[[P]]\rho$ is true, then $\hat{\rho }⊢P\text{;}$ likewise, if $[[P]]\rho$ is false, then $\hat{\rho }⊢\neg P\text{.}$

From this fact, we can deduce that $\models P$ entails $⊢P$ by repeatedly applying excluded middle to every single atom in $P\text{,}$ and applying our previous lemmas when we are done. Finally, we can transform any sequent $\psi ⊢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 ρ  then  else “¬” )

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

tabulate-atom-true
  : (x : Fin Γ)
  → (ρ : Fin Γ → Bool)
  → ρ x ≡ true
  → tabulate ρ ⊢ atom x
tabulate-atom-true {Γ = suc Γ} fzero ρ x-true with ρ 
... | 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 ρ 
... | 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 $P\text{,}$ we can note that if $[[P]]\rho$ is true, then $\hat{\rho }⊢P$ and, conversely, that $\hat{\rho }⊢\neg P$ if $[[P]]\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 $P$ be a proposition and let $\rho$ be an assignment for the first $n$ atoms in $P\text{.}$ If $P$ is a tautology, then $\hat{\rho }⊢P\text{.}$ This follows from induction on the number of atoms not assigned by $\rho \text{.}$ If $\rho$ assigns all of the atoms of $P\text{,}$ then by our previous lemma we have $\hat{\rho }⊢P\text{.}$ For the inductive step, let $x$ be a atom not covered by $\rho \text{.}$ Excluded middle lets us case on the truth value of $x\text{;}$ if it is true, then we extend $\rho$ with $x:=\top \text{,}$ and use the induction hypothesis. Likewise, if $x$ is false, then we extend $\rho$ with $x:=\perp \text{.}$

We’ll then show an appropriate generalisation of the completeness theorem, which will allow us to apply induction. Specifically, we’ll show that, if $P$ is a tautology in $k+n$ atoms, and we have an assignment $\rho$ of truth values for the first $k$ atoms in $P\text{,}$ then $\hat{\rho }⊢P\text{,}$ by induction on $n\text{,}$ 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+n$ new atoms, and we’re free to assume that any tautology in $k+n$ atoms is a theorem. We use this induction hypothesis twice, once on $\rho$ extended with $x:=\top \text{,}$ and once on it extended with $x:=\perp \text{.}$ We now have proofs that $x⊢P$ and $\neg x⊢P\text{;}$ but by the excluded middle (and disjunction elimination), this suffices to prove $P\text{!}$

tabulate-complete {Γ = Γ} P (weak σ) ρ P-taut = ∨-elim
  (lem (shift-prop σ (atom )))
  (subst (_⊢ P)
    (shift-ctx-⨾ σ _ _)
    (tabulate-complete P σ (ρ [  ≔ true ]) P-taut))
  (subst (_⊢ P)
    (shift-ctx-⨾ σ _ _ ∙ ap₂ _⨾_ refl (shift-prop-“¬” σ (atom )))
    (tabulate-complete P σ (ρ [  ≔ 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 $P\text{,}$ 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 $P_1\to \cdots \to P_n\to Q$ yield proofs of $P_1,\cdots ,P_n⊢Q\text{,}$ 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)

  where
  it : ∀ ρ' (ψ-true : ⟦ ψ ⟧ ρ' ≡ true) (b : Bool)
     → ⟦ Q ⟧ ρ' ≡ b
     → ⟦ Q “⇒” P ⟧ ρ' ≡ true
  it ρ' ψ-true true Q-true =
    ⇒-sem ρ'
    ∙ ap₂ imp refl (valid ρ' (ap₂ and ψ-true Q-true))
    ∙ imp-truer _
  it ρ' ψ-true false Q-false =
    ⇒-sem ρ' ∙ ap₂ imp Q-false refl

This lets us generalize our result for tautologies to any proposition-in-context $\psi \models P\text{!}$

complete : ψ ⊨ P → ψ ⊢ P
complete {ψ = ψ} {P = P} valid =
  ⇛-closed $ taut-complete (ψ “⇛” P) (⇛-valid ψ P valid)