形式的証明
形式的証明
定義.
φ の T における形式的証明とは，次の条件を満たす有限列 φ0, · · · , φn のことをいう．
(1) 各番号 i = 0, · · · , n に対して φi は論理式である．
(2) φn ≡ φ である．
(3) 各番号 i = 0, · · · , n に対して，次のいずれかが成り立つ．
φi は T の元である．
ある番号 j < i が存在して，φi は φj から直ちに導かれる． ある番号 j, k < i が存在して，φi は φj と φk から直ちに導かれる． φ の T における形式的証明が存在することを $ T \vdash φ で表し，
T で φ が証明可能という言い方をする．
また T が {ψ1, · · · , ψn} というメタ集合のときは $ T \vdash \varphi のことを
$ \psi_1, ... \psi_n \vdash \varphiと書く
またTが空集合のときは$ T \vdash \varphiのことを$ \vdash \varphiと書く．
注意
$ T \vdash \varphiは、メタ数学における記号
論理式ではない
つまり、
「直ちに導かれる」ことは自明として認めたうえで、
公理から直ちに導かれるｋとをだけをつなげてφが得られたら、これは形式的証明