module peirce where
{-
In deduction.agda we presented minimal logic on => : the two axioms K and S,
and modus ponens. Everything we derived there was derivable.
How do we show that something is NOT derivable?
We build a MODEL: an interpretation of the formulae which
-validates the axioms K and S,
-is preserved by modus ponens,
and in which the formula we are interested in is FALSE. Soundness
(proved by induction on derivations) then turns a derivation into an
element of the empty type.
The formula we take is PEIRCE'S LAW
((A => B) => A) => A
It is a tautology for the classical truth tables -- we check this in
PART 2 -- so no interpretation in {false,true} can work. Instead we
interpret a formula, not by a truth value, but by a MONOTONE PREDICATE
on the poset with two elements
w0 <= w1
One should read w0 <= w1 as "w1 is a later stage of knowledge than w0",
and "X is forced at w" as "X is known at stage w". Monotone: what is
known at w0 is still known at w1.
The point is the interpretation of implication: X => Y is forced at w
when, at EVERY later stage u, X forced at u implies Y forced at u.
So X => Y being forced at w0 is a statement about the FUTURE, and this
is what makes Peirce's law fail.
-}
-- ------------------------------------------------------------
-- repeated from deduction.agda
-- ------------------------------------------------------------
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data list (A : Set) : Set where
nil : list A
cons : A -> list A -> list A
data ⊥ : Set where
efq : {A : Set} -> ⊥ -> A
efq ()
record ⊤ : Set where
constructor tt
-- we shall also need conjunction, to interpret a context
record _∧_ (A B : Set) : Set where
constructor pair
field
fst : A
snd : B
open _∧_
data Form : Set where
imply : Form -> Form -> Form
atom : Nat -> Form
context : Set
context = list Form
infixr 10 _=>_
_=>_ : Form -> Form -> Form
X => Y = imply X Y
infixr 10 _,_
_,_ : context -> Form -> context
G , X = cons X G
data isIn : context -> Form -> Set where
zero : {X : Form} -> {G : context} -> isIn (G , X) X
suc : {X Y : Form} -> {G : context} -> isIn G X -> isIn (G , Y) X
infixr 6 _⊢_
data _⊢_ : context -> Form -> Set where
var : {X : Form} -> {G : context} -> isIn G X -> G ⊢ X
axK : {X Y : Form} -> {G : context} -> G ⊢ X => (Y => X)
axS : {X Y Z : Form} -> {G : context} -> G ⊢ (X => (Y => Z)) => ((X => Y) => (X => Z))
mp : {Y X : Form} -> {G : context} ->
G ⊢ Y => X ->
G ⊢ Y ->
-------------
G ⊢ X
-- ------------------------------------------------------------
-- ABSOLUTE derivability
--
-- A formula is absolutely derivable when it can be deduced from NO
-- hypothesis at all. We can define this DIRECTLY, by an inductive
-- definition which is the one of _⊢_ with the rule var removed --
-- there is then no context left, and Deriv is indexed by a formula
-- only. This is the system of Hilbert.
-- ------------------------------------------------------------
data Deriv : Form -> Set where
K : {X Y : Form} -> Deriv (X => (Y => X))
S : {X Y Z : Form} -> Deriv ((X => (Y => Z)) => ((X => Y) => (X => Z)))
MP : {Y X : Form} ->
Deriv (Y => X) ->
Deriv Y ->
-------------
Deriv X
-- negation, at the level of Agda
not : Set -> Set
not A = A -> ⊥
-- for instance, the identity, as in dedlem1 of deduction.agda
derivId : (X : Form) -> Deriv (X => X)
derivId X = MP (MP S (K {Y = X => X})) (K {Y = X})
-- ------------------------------------------------------------
-- Deriv X <-> nil ⊢ X
--
-- Both directions are a plain induction on the derivation.
-- ------------------------------------------------------------
-- from left to right: a hypothesis-free derivation can be read in ANY
-- context (so this direction also gives weakening for free)
derivToHil : {G : context} -> {X : Form} -> Deriv X -> G ⊢ X
derivToHil K = axK
derivToHil S = axS
derivToHil (MP d d1) = mp (derivToHil d) (derivToHil d1)
-- from right to left: the case var cannot occur, since isIn nil X is
-- empty -- no position in the empty list. Agda checks this, and the
-- case is written ()
hilToDeriv : {X : Form} -> nil ⊢ X -> Deriv X
hilToDeriv (var ())
hilToDeriv axK = K
hilToDeriv axS = S
hilToDeriv (mp d d1) = MP (hilToDeriv d) (hilToDeriv d1)
-- the equivalence
derivIff : (X : Form) -> (Deriv X -> nil ⊢ X) ∧ (nil ⊢ X -> Deriv X)
derivIff X = pair derivToHil hilToDeriv
-- ------------------------------------------------------------
-- The two translations are in fact INVERSE to each other: they do
-- not merely preserve derivability, they are a bijection between
-- the derivation trees of Deriv X and those of nil ⊢ X.
-- ------------------------------------------------------------
data Id (A : Set) : A -> A -> Set where
refl : (a : A) -> Id A a a
cong2 : {A B C : Set} -> (f : A -> B -> C) ->
{a a' : A} -> {b b' : B} ->
Id A a a' -> Id B b b' -> Id C (f a b) (f a' b')
cong2 f (refl a) (refl b) = refl (f a b)
roundDeriv : {X : Form} -> (d : Deriv X) ->
Id (Deriv X) (hilToDeriv (derivToHil d)) d
roundDeriv K = refl K
roundDeriv S = refl S
roundDeriv (MP d d1) = cong2 MP (roundDeriv d) (roundDeriv d1)
roundHil : {X : Form} -> (d : nil ⊢ X) ->
Id (nil ⊢ X) (derivToHil (hilToDeriv d)) d
roundHil (var ())
roundHil axK = refl axK
roundHil axS = refl axS
roundHil (mp d d1) = cong2 mp (roundHil d) (roundHil d1)
-- ============================================================
-- PART 1. The formulae we want to refute
-- ============================================================
A B : Form
A = atom zero
B = atom (suc zero)
-- Peirce's law
peirce : Form
peirce = ((A => B) => A) => A
-- another classical law of the implicational fragment
peirce2 : Form
peirce2 = ((A => B) => B) => ((B => A) => A)
-- ============================================================
-- PART 2. The simplest model: the Boolean truth tables
--
-- A model is an interpretation of the formulae which validates K and
-- S and is preserved by MP. The simplest one interprets a formula by
-- a truth value, implication being given by its truth table.
--
-- It suffices to show that an ATOM is not derivable: interpret every
-- atom by false.
--
-- But it will NOT suffice for Peirce's law, and we prove this too:
-- peirce is true for EVERY Boolean interpretation (peirceTrue below).
-- This is why we shall need a second, finer model.
-- ============================================================
data Bool : Set where
false true : Bool
-- the truth table of implication
impB : Bool -> Bool -> Bool
impB false y = true
impB true y = y
-- a Boolean read as a proposition
True : Bool -> Set
True false = ⊥
True true = ⊤
-- the value of a formula, by recursion on the formula
evalB : (Nat -> Bool) -> Form -> Bool
evalB v (atom n) = v n
evalB v (imply X Y) = impB (evalB v X) (evalB v Y)
-- the two axioms are tautologies, and MP preserves truth:
-- all three are checked by trying the finitely many truth values
lemK : (a b : Bool) -> True (impB a (impB b a))
lemK false b = tt
lemK true false = tt
lemK true true = tt
lemS : (a b c : Bool) -> True (impB (impB a (impB b c)) (impB (impB a b) (impB a c)))
lemS false b c = tt
lemS true false c = tt
lemS true true false = tt
lemS true true true = tt
lemMP : (a b : Bool) -> True (impB a b) -> True a -> True b
lemMP false b p q = efq q
lemMP true b p q = p
-- soundness, by induction on the derivation: one case per constructor
soundB : (v : Nat -> Bool) -> {X : Form} -> Deriv X -> True (evalB v X)
soundB v (K {X} {Y}) = lemK (evalB v X) (evalB v Y)
soundB v (S {X} {Y} {Z}) = lemS (evalB v X) (evalB v Y) (evalB v Z)
soundB v (MP {Y} {X} d d1) =
lemMP (evalB v Y) (evalB v X) (soundB v d) (soundB v d1)
-- interpret every atom by false
vFalse : Nat -> Bool
vFalse n = false
-- hence no atom is derivable
-- (evalB vFalse (atom n) is false, and True false is the empty type)
notAtom : (n : Nat) -> not (Deriv (atom n))
notAtom n d = soundB vFalse d
-- Peirce's law, on the other hand, is a classical TAUTOLOGY: its
-- value is true whatever the values of the two atoms
lemPeirce : (a b : Bool) -> True (impB (impB (impB a b) a) a)
lemPeirce false b = tt
lemPeirce true false = tt
lemPeirce true true = tt
peirceTrue : (v : Nat -> Bool) -> True (evalB v peirce)
peirceTrue v = lemPeirce (v zero) (v (suc zero))
-- so NO Boolean interpretation refutes peirce, and we must look for
-- a model of another kind: this is PART 3 onwards
-- ============================================================
-- PART 3. The poset w0 <= w1
-- ============================================================
data World : Set where
w0 w1 : World
-- the order, defined by RECURSION, so that it computes
-- (as le did in deduction.agda: ⊤ and ⊥ instead of a data type)
infix 8 _≤_
_≤_ : World -> World -> Set
w0 ≤ v = ⊤
w1 ≤ w0 = ⊥
w1 ≤ w1 = ⊤
leRefl : (w : World) -> w ≤ w
leRefl w0 = tt
leRefl w1 = tt
leTrans : (u v z : World) -> u ≤ v -> v ≤ z -> u ≤ z
leTrans w0 v z p q = tt
leTrans w1 w0 z p q = efq p
leTrans w1 w1 w0 p q = efq q
leTrans w1 w1 w1 p q = tt
-- ============================================================
-- PART 4. The monotone predicates on this poset
--
-- A monotone predicate P satisfies P w0 -> P w1, so there are
-- exactly THREE of them, and we can list them:
--
-- never false at w0, false at w1
-- half false at w0, true at w1
-- always true at w0, true at w1
--
-- (the missing fourth combination, true at w0 and false at w1, is
-- the one which is not monotone)
--
-- Listing them keeps everything in Set: an interpretation of the
-- atoms is then simply a function Nat -> Val.
-- ============================================================
data Val : Set where
never half always : Val
holds : Val -> World -> Set
holds never w = ⊥
holds half w0 = ⊥
holds half w1 = ⊤
holds always w = ⊤
-- each of the three is indeed monotone
holdsMono : (a : Val) -> (u v : World) -> u ≤ v -> holds a u -> holds a v
holdsMono never u v p h = efq h
holdsMono half w0 v p h = efq h
holdsMono half w1 w0 p h = efq p
holdsMono half w1 w1 p h = tt
holdsMono always u v p h = tt
-- ============================================================
-- PART 5. Forcing
--
-- Given an interpretation V of the atoms we define, by recursion on
-- the formula X, the set force V w X of "proofs that X is known at
-- stage w". The clause for implication is the one of Kripke:
-- quantification over all LATER stages.
-- ============================================================
force : (Nat -> Val) -> World -> Form -> Set
force V w (atom n) = holds (V n) w
force V w (imply X Y) = (u : World) -> w ≤ u -> force V u X -> force V u Y
-- forcing is monotone for EVERY formula, by induction on the formula
-- (for an implication there is nothing to do but compose with leTrans:
-- a later stage of a later stage is a later stage)
mono : (V : Nat -> Val) -> (X : Form) -> (u v : World) ->
u ≤ v -> force V u X -> force V v X
mono V (atom n) u v p h = holdsMono (V n) u v p h
mono V (imply X Y) u v p h = \ z q hx -> h z (leTrans u v z p q) hx
-- a context is forced when all its formulae are
forceC : (Nat -> Val) -> World -> context -> Set
forceC V w nil = ⊤
forceC V w (cons X G) = force V w X ∧ forceC V w G
-- reading a hypothesis out of a forced context
lookupC : (V : Nat -> Val) -> {G : context} -> {X : Form} ->
isIn G X -> (w : World) -> forceC V w G -> force V w X
lookupC V zero w g = fst g
lookupC V (suc i) w g = lookupC V i w (snd g)
-- ============================================================
-- PART 6. Soundness
--
-- by induction on the derivation: exactly one case per constructor
-- of _⊢_ , as for dedthm in deduction.agda
-- ============================================================
sound : (V : Nat -> Val) -> {G : context} -> {X : Form} ->
G ⊢ X ->
(w : World) -> forceC V w G -> force V w X
sound V (var i) w g = lookupC V i w g
-- K: keep hx from stage u to the later stage v -- this is where
-- monotonicity of forcing is used
sound V (axK {X} {Y}) w g = \ u p hx v q hy -> mono V X u v q hx
-- S: at stage z we have f at u, g at v and hx at z, with u <= v <= z
sound V (axS {X} {Y} {Z}) w g =
\ u p f v q h z r hx -> f z (leTrans u v z q r) hx z (leRefl z) (h z r hx)
-- modus ponens: use the premise at the PRESENT stage, i.e. at w itself
sound V (mp d d1) w g = sound V d w g w (leRefl w) (sound V d1 w g)
-- ============================================================
-- PART 7. A warm-up: atom 0 => atom 1 is not derivable
--
-- Interpret atom 0 by always and every other atom by never. Then
-- atom 0 is forced at w0 and atom 1 is not, so atom 0 => atom 1 is
-- not forced at w0. (Here one world would already be enough: this
-- is just the classical truth table.)
-- ============================================================
V0 : Nat -> Val
V0 zero = always
V0 (suc n) = never
notImp : not (Deriv (atom zero => atom (suc zero)))
notImp d = sound V0 (derivToHil d) w0 tt w0 tt tt
-- ============================================================
-- PART 8. Peirce's law
--
-- Now we really use the two worlds. Take
--
-- A = atom 0 interpreted by half (unknown at w0, known at w1)
-- B = atom 1 interpreted by never
--
-- so that A => B is forced NOWHERE: at w0 it fails because of the
-- later stage w1, where A is known and B is not; at w1 it fails at w1.
--
-- Hence (A => B) => A is forced at w0 VACUOUSLY, at both stages.
-- But A itself is not forced at w0. So Peirce's law is not forced
-- at w0, and by soundness it has no derivation.
-- ============================================================
V1 : Nat -> Val
V1 zero = half
V1 (suc n) = never
-- the premise of Peirce's law IS forced at w0
-- at stage w0: from f we would get B known at w1, which is absurd
-- at stage w1: nothing to prove, A is known at w1
premise : force V1 w0 ((A => B) => A)
premise w0 p f = efq (f w1 tt tt)
premise w1 p f = tt
-- but the conclusion A is not forced at w0, so Peirce's law has
-- no derivation at all: this is the statement not (Deriv peirce)
notPeirce : not (Deriv peirce)
notPeirce d = sound V1 (derivToHil d) w0 tt w0 tt premise
{-
Remarks
The model also refutes the other classical laws of minimal logic, for
instance ((A => B) => B) => ((B => A) => A) -- see below -- and, once
negation is added, the law of excluded middle: at w0 neither A nor its
negation is known.
Note what soundness gives us: not merely that the axioms K and S do not
SUFFICE, but that no derivation whatsoever exists. A derivation would
be a finite tree, and induction on that tree produces an element of ⊥.
The Boolean model of PART 2 is the special case of this one where the
atoms are given values in never / always only: such a value is forced
at w0 exactly when it is forced at w1, the quantification over later
stages becomes vacuous, and forcing reduces to the truth tables. The
value half, which distinguishes the two stages, is the whole point.
Note also that the model is finite: forcing at a given world is decidable,
so this argument could be turned into an algorithm deciding derivability
for formulae built from two atoms in this fragment.
Conversely, Peirce's law added as an axiom scheme to K and S gives exactly
classical implicational logic; the derivation of dedthm in deduction.agda
goes through unchanged, since it only inspects var, axK, axS and mp.
-}
-- a second classical law, refuted by the same interpretation V1
-- A => B is forced nowhere, so (A => B) => B is forced at w0 vacuously
-- B is forced nowhere either, so B => A is forced at w0
-- and applying the conclusion to it would give A at w0, which is absurd
premise2 : force V1 w0 ((A => B) => B)
premise2 w0 p f = efq (f w1 tt tt)
premise2 w1 p f = efq (f w1 tt tt)
notPeirce2 : not (Deriv peirce2)
notPeirce2 d = sound V1 (derivToHil d) w0 tt w0 tt premise2 w0 tt (\ u q hb -> efq hb)