循環証明体系 - Internet Explorer 2.0

循環証明体系

$ \text{Nat},\text{Even},\text{Odd}を帰納的述語とし，次のプロダクション(Production)を考える

定数$ \mathbf{0}は自然数

$ \dfrac{}{\text{Nat}(\mathbf{0})}

項$ xが自然数なら項$ s.xも自然数

$ \dfrac{\text{Nat}(x)}{\text{Nat}(s.x)}

定数0は偶数

$ \dfrac{}{\text{Even}(\mathbf{0})}

$ xが奇数なら$ s.xは偶数

$ \dfrac{\text{Even}(x)}{\text{Odd}(s.x)}

$ xが偶数なら$ s.xは奇数

$ \dfrac{\text{Odd}(x)}{\text{Even}(s.x)}

ここから次の導出規則が定義される

$ \text{Nat} Right1

$ \dfrac{}{\Gamma \vdash \Delta, \text{Nat}(0)}

$ \text{Nat} Right2

$ \dfrac{\Gamma \vdash \Delta, \text{Nat}(t)}{\Gamma \vdash \Delta, \text{Nat}(s.t)}

$ \text{Even}Right1

$ \dfrac{}{\Gamma \vdash \Delta, \text{Even}(0)}

$ \text{Even} Right2

$ \dfrac{\Gamma \vdash \Delta, \text{Odd}(t)}{\Gamma \vdash \Delta, \text{Even}(s.t)}

$ \text{Odd} Right1

$ \dfrac{\Gamma \vdash \Delta, \text{Even}(t)}{\Gamma \vdash \Delta, \text{Odd}(s.t)}

$ \text{Nat} Left

$ \dfrac{\Gamma, t=0 \vdash \Delta \quad \Gamma, t=s.x, \text{Nat}(t) \vdash \Delta}{\Gamma,\text{Nat}(t) \vdash \Delta}

$ \text{Even} Left

$ \dfrac{\Gamma, t=0 \vdash \Delta \quad \Gamma, t=s.x, \text{Odd}(t) \vdash \Delta}{\Gamma,\text{Even}(t) \vdash \Delta}

$ \text{Odd} Left

$ \dfrac{\Gamma, t=s.x, \text{Even}(t) \vdash \Delta}{\Gamma,\text{Odd}(t) \vdash \Delta}

なお普通は左導入規則はCaseと言うらしい？

諸々を定義すると，次が循環証明体系で証明可能

$ \text{Nat}(x) \vdash \text{Even}(x),\text{Odd}(x)

シーケントだと$ \text{Even}(x) \lor \text{Odd}(x)と読み替えても良い

以下$ \text{Nat},\text{Even},\text{Odd}はN,E,Oに略記

code:Nat_Is_Even_Or_Odd

------------------

N(y) |- O(y), E(y) : *1

--------------------

N(y) |- O(y), O(s.y)

------------------- --------------------

|- E(0), O(0) N(y) |- E(s.y), O(s.y)

-------------------=I --------------------=I

x = 0 |- E(x), O(x) x = s.y, N(y) |- E(x), O(x)

----------------------------------------------------N,L

N(x) |- E(x), O(x) : *1

*1で循環している