直ちに導かれる

直ちに導かれる

定義. φ, ψ, χ を論理式とする．

(1) φ が、 ψ から直ちに導かれる

⇐⇒ ある変数記号 x が存在して φ ≡ ∀x ψ となる．

(2) φ が 、ψ と χ から直ちに導かれる

⇐⇒ χ ≡ ψ → φ となる．

ただし、

論理式 φ と ψ が文字列として等しいことを φ ≡ ψ で表すことにする

(= は論理記号と紛らわしいため代わりに ≡ を使う)．

これの意味するところ

ψから∀x ψは導いて良い

ψ と ψ → φ から、φ を導いて良い

これは結局形式的証明の中で使われている言葉に対して、

ある番号 j < i が存在して，φi は φj から直ちに導かれる．

ある番号 j, k < i が存在して，φi は φj と φk から直ちに導かれる．

ある番号 j < i が存在して，φi は ある変数記号 x が存在して φi ≡ ∀x φj となる

ある番号 j, k < i が存在して， φk ≡ φj → φi を満たす

「直ちに導かれる」は、記号が同一であるという主張しかしてない