「一階述語論理」の版間の差分

命題論理においては、論理式の解釈とは各命題記号に対する真理値 0 , 1 の割り当てであったる。これに対して、一階述語論理の論理式の解釈は'''議論領域'''あるいは'''領域''' (universe, domain) と呼ばれる空でない集合と、それぞれの'''非論理記号'''（述語記号・関数記号・定数記号）の "意味" の割り当てからなる。議論領域とは「すべての ''x'' について」といったときの ''x'' が動きうる値の範囲である。一階述語論理の論理式はこのような解釈を一つ与えることによって真偽が決定される。一階述語論理を改良することによって、議論領域を種 (sort) ごとに分割し、それぞれの領域上を動く種別の変数を導入することもできる（詳細は「[[多種論理]]」を参照）。

* 括弧の使い方の流儀は様々である。ある人は ∀''x'' を '''('''∀''x''''')''' と書く。括弧の代わりにコロンや終止符を使う場合もある。もちろんその場合には、言語にコロンや終止符を含めておく必要がある。括弧を全く使わない表記法に[[ポーランド記法]]と呼ばれるものがある。これは、∧ や ∨ を先頭に書いて '''('''φ ∧ ψ''')''' をの代わりに ∧ φ ψ のように書く方法である。ポーランド記法はコンパクトで数学的に取り扱いやすいという利点があるがり、可読性が低いという欠点がある。

項が何らかの対象を表す記号列であったのに対して、論理式は何らかの文命題を表すものである。論理式は原子論理式と呼ばれる最も基本的な論理式から結合記号と量化記号を繰り返し用いることによって形成される。まず、原子論理式は次のように定義される：

自然数論の言語における論理式 '''S0 + S0 = SS0''' の各記号を通常の意味で解釈すれば「1 + 1 = 2」となり、これは正しい命題である。'''('''¬ '''S0 + S0 ≠= SS0)''' は「1 + 1 ≠ 2」となるので正しい命題でない。また、変数の動く範囲（議論領域）は[[自然数]]全体の集合だとすれば、論理式 ∀''x''₁ '''0 < S'''''x''₁ は「すべての自然数 ''n'' について 0 < ''n'' + 1」という意味になり、これは正しい命題であることが分かる。一方、論理式 '''0 +'''''x''₅''' = S0''' の意味を考えてみると、「0 + x₅ = 1」となるがこれは正しいか正しくないかを判断することができない。なぜなら、''x''₅ という変数が何を表しているかが決まっていないからである。このようなとき、''x''₅ は論理式 '''0 +'''''x''₅''' = S0''' における'''自由変数''' (free variable) であると言われる。正式には、各論理式 φ に対して、"φ における自由変数全体の集合" fr(φ) を次のように再帰的に定義する：

: 一階の言語に対する'''解釈''' (interpretation) あるいは'''構造''' (structure) とは、空でない集合 ''D'' と、非論理記号全体の集合を[[写像|定義域]]とする関数 ''F'' の組 ''M'' = (''D'', ''F'') で次をみたすものをいう：

=== 代入に関して ===

'''代入： ''' ''t'' を項、 φ(''x'') を（''x''を自由変項として含む）論理式とする。このとき φ(''t'') は、φ(''x'') 中の ''x'' の自由な出現すべてを ''t'' で置き換えたものと定義される。'''ただしここで、''t'' に含まれるいかなる自由変項も、この置き換えによって束縛されてしまうことがないようにしなければならない'''。もし ''t'' の自由変項が束縛されるなら、''x'' を ''t'' で置換する前に φ 内の[[束縛変項]]名を ''t'' 内の自由変項名以外のものに変更しなければならない。この条件が必要となる理由を説明するために、以下のような場合を考えてみよう。論理式 φ(''x'') の中身が ∀''y'' ''y'' ≤ ''x''（これは「''x'' は最大値」を意味する）だとする。''t'' が ''y'' を自由変項として持たない項であれば、φ(''t'') はまさに ''t'' が最大値であると主張していることになる。しかし、もし ''t'' が ''y'' である場合、φ(''t'') は ∀''y'' ''y'' ≤ ''y'' となり、主張することが変わってしまう。この問題は、自由変項 ''x'' に ''y'' を代入したときに、φ(''x'') の中で ''t'' の自由変項 ''y'' が束縛されてしまうために発生する。そこで、事前に束縛変項 ''y'' を他の名前、例えば ''z'' に変えて、∀''z'' ''z'' ≤ ''y'' とすることで問題を回避する。これを忘れるとひどい間違いを犯すことになる。

=== 同一性 ===

=== 量化子の公理 ===

# 命題計算とは異なり、一階述語恒真論理式全体の集合は（言語に高々[[アリティ]]2の述語が一つでも含まれていると）[[決定不可能]]であるない。つまり、任意のに論理式 ''P'' についてが与えられたとき、''P'' それが恒真であるか否かを決判定する一般的な[[アルゴリズム]]は存在しない（「[[チューリングマシンの停止問題]]」を参照せよ）。正確には、恒真論理式の[[ゲーデル数]]全体の集合は[[帰納的関数|帰納的]]でない。この結果は[[アロンゾ・チャーチ]]と[[アラン・チューリング]]がそれぞれ独立に導き出した。

# ただしそれでも、与えられた文（論理式）が恒真であるとき、かつそのときにのみ 1 (yes) を出力して停止するチューアルゴリングマシンズムは存在する。逆にただし、恒真でない論理式の場合は判定がこのアルゴリズムは停止しないかもしれない。これを「恒真論理式全体の集合は部分決定性が可能である」という。

# 単項1 変数述語記号だけを非論理（単項記号に持つ言語の述語だけからなる述語恒真論理）式全体の集合は[[決定可能]]である。

こうした論理の多くは、一階述語論理の何らかの拡張と言える。これらは、一階述語論理の論理演算子と量化子を全て含んでいて、それらの意味も同じである。リンドストレムは、一階述語論理の拡張には、レーヴェンハイム＝・スコーレムの下降定理とコンパクト性定理の両方を満足するものが存在しないことを示した。この定理の内容を精確に述べるには、論理が満たしていなければならない条件を数ページにわたって列挙する必要がある。例えば、言語の記号を変更しても各文の真偽が基本的に変わらないようになっていなければならない。