代入について

ウィキペディア小見出し辞書

代入について

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/03/25 04:10 UTC 版)

「一階述語論理」の記事における「代入について」の解説

φx [ t ] は、論理式 φ において "束縛されていない" 変数 x をすべて項 t で置き換えて得られる論理式を表すと述べた。正確には、φx [ t ] は再帰によって次に述べるような仕方で定義される。 まず、それぞれの項 u に対して ux [ t ] を次のように再帰的に定義する：xx [ t ] = t 。 y が x と異なる変数ならば、yx [ t ] = y 。 c 定数記号ならば、cx [ t ] = c 。 t1 , ..., tn が項で、f がアリティ n の関数記号ならば、(f t1 … tn)x [ t ] = f (t1)x [ t ] … (tn)x [ t ] 。 そして、φx [ t ] を次のように再帰的に定義する：原子論理式 P t1 … tn に対しては、(P t1 … tn)x [ t ] = P (t1)x [ t ] … (tn)x [ t ] 。 (¬ φ)x [ t ] = (¬ φx [ t ]) (φ ∧ ψ)x [ t ] = (φx [ t ] ∧ ψx [ t ]) (φ ∨ ψ)x [ t ] = (φx [ t ] ∨ ψx [ t ]) (φ → ψ)x [ t ] = (φx [ t ] → ψx [ t ]) (φ ↔ ψ)x [ t ] = (φx [ t ] ↔ ψx [ t ]) (∀x φ)x [ t ] = ∀x φ 、(∃x φ)x [ t ] = ∃x φ 。 y が x と異なる変数ならば、(∀y φ)x [ t ] = ∀y φx [ t ] 、(∃y φ)x [ t ] = ∃y φx [ t ] 。 次に、論理式 φ において項 t が変数 x に代入可能であるということを定義する。このことの直観的な意味は、φ が x について述べていることと同じことを φx [ t ] が t について述べているということである。例えば、。これに対して、。代入可能性の正式な定義は次の通りである。 論理式 φ において項 t が変数 x に代入可能 (substitutable) であるということを次のように再帰的に定義する：原子論理式においては、常に t は x に代入可能である。 (¬ φ) において t が x に代入可能 ⇔ φ において t が x に代入可能 。 (φ ∧ ψ) において t が x に代入可能 ⇔ φ と ψ において t が x に代入可能 。 (φ ∨ ψ) において t が x に代入可能 ⇔ φ と ψ において t が x に代入可能 。 (φ → ψ) において t が x に代入可能 ⇔ φ と ψ において t が x に代入可能 。 (φ ↔ ψ) において t が x に代入可能 ⇔ φ と ψ において t が x に代入可能 。 ∀y φ において t が x に代入可能 ⇔ x ≠ y または x ∉ fr(φ) または（φ において t が x に代入可能かつ t の中に y が現れない）。 ∃y φ において t が x に代入可能 ⇔ x ≠ y または x ∉ fr(φ) または（φ において t が x に代入可能かつ t の中に y が現れない）。