日々の流転

λ. パースの論理式

パースの論理式(Peirce's formula)*1「((P→Q)→P)→P」というのを直観主義論理に加えると古典論理になるそうだ。 なので、二重否定の除去と同値になることを、簡単な haskell プログラムを書いて確かめてみた*2。

type Absurd = forall a. a
type Not a = a -> Absurd

prop1 :: forall a b. (forall a. Not (Not a) -> a) -> (((a->b)->a)->a)
prop1 callCC f = callCC (\(k :: Not a)-> k (f (k :: a->b)))

prop2 :: forall a. (forall a b. ((a->b)->a)->a) -> (Not (Not a) -> a)
prop2 p k1 = p (k1 :: Not a -> a)

λ. オーシャンズ13

を観てきた。