12/01/08 23:25:07.20
>>177
|- は本当は |-_X などの添え字が付く。
このXは推論規則と公理型の集まり。
A |-_X B と書いたとき、
AからXの推論規則と公理型を使ってBを証明できる、を意味する。
このとき、Aは論理式の集合、Bは論理式。
だから別にAの中身が公理でなければならないのではない。
通常の古典論理では、XにHKやLKが入る。
そしてペアノ算術などではXにPAが入る。
だから右側がPAの公理なら、 |-_PA ∀x￢(sx=0) と書いてよい。
しかし |-_PA ￢(0x=0) などは無条件に書けない。
（エルブランの定理が関与する。言語内に定数がない場合がある。）
だから PA |-_PA φ とする必要がある。
ここで左側のPAはPAが定義されている言語上のすべての論理式になる。
もちろんモデルを持たせるには閉論理式である必要がある。
数学書では大抵 PA |- ∀x￢(sx=0) と書かれる。
これは |-_PA を略しているのだが、次のような事例の識別ができなくなる。
PA |-_HK φ ⇔ PA |=_HK φ は成り立つ。
PA |-_PA φ ⇔ PA |=_PA φ は成り立たない。
これは計算機や非古典論理や証明論では致命傷になり得る。