IdrisとDecとFixと不完全性定理

Idrisでゲーデルの不完全性定理を証明しました。

Decは、引数が真ならYesと証明を、偽ならNoと反証を返します。
（実際に判定、証明してくれる訳ではありません）
そして、Not . Decな命題とは、証明も反証もできない命題という事になります。

Fixは不動点コンビネータです。ここでは説明しません。

そして、notDec (Fix notDec)を証明しました。
これは、(Fix notDec)は証明できない事を表しています。

何気にすごいと自分では思っているのですが、どうでしょうか。

と思ったら、fixValueが停止しない気がしてきた。ダメっぽい。

18/09/30　修正しました。
いとうかつとしさんのuniversesを参考にしました。

ついでに第二不完全性定理も証明しました。

module Godel04

%default total
-- %language ElabReflection
%hide Dec

-- Decは、引数が真ならYesと証明を、偽ならNoと反証を返す
-- そして、Not . Decな命題とは、証明も反証もできない命題という事になる
data Dec : Type -> Type where
  Yes : (prf    : prop)         -> Dec prop
  No  : (contra : prop -> Void) -> Dec prop

notDec : Type -> Type
notDec = Not . Dec

-- 不動点コンビネータ
data Fix : (Type -> Type) -> Type where
  In : f (Fix f) -> Fix f
partial
Out : Fix f -> f (Fix f)
Out (In x) = x


partial
fixValue : Fix notDec
fixValue = In (Out fixValue)

-- (Fix notDec)は証明できない
partial
Godel'sIncompletenessTheorem : notDec (Fix notDec)
Godel'sIncompletenessTheorem = Out {f=notDec} fixValue

修正後

module Godel06

%default total
-- %language ElabReflection
%hide Dec
%hide Functor


-- Decは、引数が真ならYesと証明を、偽ならNoと反証を返す
-- そして、Not . Decな命題とは、証明も反証もできない命題という事になる
data Dec : Type -> Type where
  Yes : (prf    : prop)         -> Dec prop
  No  : (contra : prop -> Void) -> Dec prop

notDec : Type -> Type
notDec = Not . Dec

-- Functor
data Functor : Type where
  I : Functor
  K : Type -> Functor
  H : (Type -> Type) -> Functor

-- decoding function
decode : Functor -> Type -> Type
decode I x = x
decode (K c) _ = c
decode (H f) x = f x
syntax "[" [F] "]" [x] = decode F x

-- 不動点コンビネータ
data Fix : Functor -> Type where
  In : {F : Functor} -> decode F (Fix F) -> Fix F
Out : {F : Functor} -> Fix F -> [ F ] (Fix F)
Out (In x) = x


-- 第一不完全性定理
-- Fix (H notDec)が真ならば、Fix (H notDec)は証明できない
godel'sIncompletenessTheorem : Fix (H notDec) -> notDec (Fix (H notDec))
godel'sIncompletenessTheorem p = Out p



-- 二重否定除去
postulate dne : ((a -> Void) -> Void) -> a 

-- 第二不完全性定理
-- (0=1)が証明されない事が、体系の無矛盾性を表しているらしい
-- 体系が無矛盾ならば、それを証明できない
godel'sIncompletenessTheorem2nd : notDec (Z = (S Z)) -> notDec (notDec (Z = (S Z)))
godel'sIncompletenessTheorem2nd p _ = let p2 = dne (p . No) in absurd p2

18/12/08　さらに追記