open import 1Lab.Prelude hiding (_β_)

open import Data.Bool
open import Data.List hiding (_++_ ; drop)
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)

infixr 12 _βββ_
infixr 11 _ββ§β_
infixr 10 _ββ¨β_
infixl 10 _β¨Ύ_
infix 9 _β’_ _β¨_


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 Ξ Ξ

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 (βββ Ο) Ο  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$, we will add $x$ to $\hat{\rho}$. Conversely, if $\rho$ assigns false to $x$, we add $\neg x$ to $\hat{\rho}$. We will then show that for any assignment $\rho$, if $\llbracket P \rrbracket \rho$ is true, then $\hat{\rho} \vdash P$; likewise, if $\llbracket P \rrbracket \rho$ is false, then $\hat{\rho} \vdash \neg P$. From this fact, we can deduce that $\vDash P$ entails $\vdash P$ by repeatedly applying excluded middle to every single atom in $P$, and applying our previous lemmas when we are done. Finally, we can transform any sequent $\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 $\rho(x)$ assigns a truth value to $x$, 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 $P$, we can note that if $\llbracket P \rrbracket \rho$ is true, then $\hat{\rho} \vdash P$ and, conversely, that $\hat{\rho} \vdash \neg P$ if $\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 $P$ be a proposition and let $\rho$ be an assignment for the first $n$ atoms in $P$. If $P$ is a tautology, then $\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 $P$, then by our previous lemma we have $\hat{\rho} \vdash P$. For the inductive step, let $x$ be a atom not covered by $\rho$. Excluded middle lets us case on the truth value of $x$; if it is true, then we extend $\rho$ with $x := \top$, and use the induction hypothesis. Likewise, if $x$ is false, then we extend $\rho$ with $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 $P$ is a tautology in $k+n$ atoms, and we have an assignment $\rho$ of truth values for the first $k$ atoms in $P$, then $\hat{\rho} \vdash P$, by induction on $n$, 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$, and once on it extended with $x := \bot$. We now have proofs that $x \vdash P$ and $\neg x \vdash P$; but by the excluded middle (and disjunction elimination), this suffices to prove $P$! 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 $P$, 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 \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)   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 \vDash P$! complete : Ο β¨ P β Ο β’ P complete {Ο = Ο} {P = P} valid = β-closed$ taut-complete (Ο βββ P) (β-valid Ο P valid)