1 基本概念
述語論理は、対象（個体）に関する性質や、対象同士の関係を記号化し、それらをもとに推論を行う論理体系である。命題論理が「真／偽」といった命題の真理値に着目するのに対し、述語論理は「どの対象について」「どのような性質が成り立つか」を形式的に扱う点に特徴がある。これにより、「すべての」「ある」といった量化を用いた一般化が可能になる。
本体系では、構文（記号の並べ方）と意味（記号の解釈）が区別される。構文論は式がどのように構成されるか、意味論は同じ式がどの対象構成のもとで真になるかを扱う。推論論は、構文的な操作によって妥当な結論が導かれる条件を定式化し、体系の力を数学的に評価する。
1.1 命題論理との関係
述語論理は命題論理を拡張する。命題論理では、原子的な命題変数に真理値を割り当て、その組合せに基づき論理式の評価を行う。一方、述語論理では、原子部分に相当する要素が命題変数ではなく述語記号と項からなる原子式となる。ここで述語記号は対象集合上の性質や関係を表し、量化子を通じて対象全体にわたる主張が表現される。
この関係は「述語を次数0のものとして扱う」などの観点で形式化でき、命題論理の各命題は述語論理の式として回収される。したがって、述語論理の枠組みは命題論理を含みつつ、対象に関する一般的推論を可能にする。
1.2 対象と性質
述語論理では、議論の対象となる集合（対象領域）をまず想定する。そのうえで、性質は述語記号により表される。ある対象について述語が成り立つかどうかは、述語記号の解釈に従って決まる。多くの場合、性質だけでなく複数対象を結びつける関係も同じ仕組みで記述する。
1.2.1 個体と述語
個体は個体変数や定数記号によって表現される。変数は値の未確定な対象を指し、代入によって具体的な対象に対応づけられる。定数記号は、意味論上では対象領域の要素を指す記号であり、一定の対象を固定した表現となる。
述語は、個体が持つ性質（単項述語）や、複数の個体の間に成り立つ関係（多項述語）を表す。たとえば単項述語は「xが性質Pを満たす」という形に対応し、多項述語は「xとyが関係Rにある」という形に対応する。これにより、対象に関する主張が式として書き下される。
1.2.2 関係と多項述語
関係の概念は、n項述語として表現される。n項述語記号は、対象領域のn個の要素の組に対して真になる／ならないを定める解釈を持つ。したがって、対象の組に依存する条件は、適切な数の項を述語の引数として並べることで記述できる。
多項述語の導入は、単なる性質表示を超えて、関係の推論を可能にする。例えば「集合の包含」は二項関係として扱えるし、「親である」「隣接する」のような関係も同様に記号化できる。述語論理では、関係の多様さを一つの枠で扱うため、述語の項数が体系的に管理される。
1.3 量化の考え方
量化は、変数を通じて「範囲全体にわたる主張」や「少なくとも一つ存在する場合の主張」を形式化する装置である。量化子は、変数の意味に直接作用し、式がどのように真になるかを決定するための基準を与える。
1.3.1 全称量化
全称量化は「すべての対象について成り立つ」という性質を表す。形式的には、全称量化の束縛変数を用いた式は、対象領域の各要素に対して中身の条件が真になることを要求する。したがって、対象領域が広がるほど要求は強くなり、成否の判断も変化する。
全称量化は、一般法則や普遍的制約の表現に対応する。たとえば「任意のxについて性質Pが成り立つ」という主張は、全称量化としてそのまま書き下せる。推論では、全称量化の内部にある条件を任意の具体項に適用する規則などが体系化される。
1.3.2 存在量化
存在量化は「ある対象が存在して条件を満たす」という主張を表す。形式的には、対象領域の少なくとも一つの要素が、束縛変数に代入されたときに中身の条件を真にすることを要求する。全称量化が「全てに対して」だったのに対し、存在量化は「少なくとも一つ」に焦点を当てる。
存在量化は、具体例の存在や、満たす証人（witness）の要求といった意味合いを持つ。推論では、存在量化された式からその証人に相当する項を導く、あるいは存在量化の内部の性質を満たす状況を組み立てるといった考え方が、証明体系の規則に反映される。
2 構文
構文は、述語論理の式がどのように文字列として組み立てられるかを規定する部分である。意味論が「それが何を指すか」を扱うのに対し、構文論は「それがどう書けているか」を扱う。構文的に正しい式（ well-formed formula ）のみが、意味論や推論の対象として扱われる。
2.1 記号体系
述語論理の構文は、変数・定数・関数記号・述語記号といった語彙、および論理記号（量化子、論理結合子、記号）からなる記号体系に基づく。これらの記号が、項や原子式、複合式へと組み立てられる。
2.1.1 変数
変数は、項や述語の引数として用いられる記号である。変数は束縛される場合と、自由なまま残る場合がある。自由変数がある式は、解釈のもとで変数の値に依存して真偽が決まる。
構文上の変数の役割は、代入によって変更可能な位置を表す点にある。束縛変数は量化子によって範囲が決まるため、意味論ではその量化の意図に従って扱われる。
2.1.2 定数記号
定数記号は、項として現れうる記号であり、意味論において対象領域の特定の要素を指す。変数と異なり、定数記号の指す対象は解釈に依存するが、項の段階で任意性を持たない。
定数記号は、例えば「ゼロ」「特定の人物」のような議論の固定点を表現するために用いられる。構文上は項の一種であり、他の記号から合成されることなく基本として扱える。
2.1.3 関数記号
関数記号は、複数の項を引数として受け取り、別の項を作るための記号である。n項関数記号は、n個の項を与えると新しい項が構成される。関数記号は、構文上は項形成のための操作として働き、意味論では対象領域上の関数に対応する。
これにより「xの後者」「xからyを作る操作」などの構造を、述語論理の枠内で表現できる。関数記号があることで、述語の引数に複雑な項を渡すことが可能になり、式の表現力が増す。
2.1.4 述語記号
述語記号は、n個の項を引数として受け取り、原子式を形成する記号である。単項述語なら1個の項を、二項述語なら2個の項を受け取る。構文上、述語記号と適切な数の項を組み合わせることにより、最小単位の原子式が得られる。
意味論では、述語記号は対象領域のn要素組に対して真偽を決める関数に相当する。これにより「ある対象が性質を持つ」「ある対象の組が関係を満たす」といった主張が、統一的な形で扱える。
2.2 項と式
項と式の区別は、構文論の基礎である。項は対象（または対象から得る構造）を表すための記号列であり、式は真偽を持つ主張として扱われる。述語論理では、項は関数記号を通じて合成され、式は原子式と論理結合子、量化子によって拡張される。
2.2.1 項の定義
項は、変数、定数記号、そして関数記号の適用によって再帰的に定義される。具体的には、与えられた関数記号に対して、引数として与えられた項の列が適切なら、その関数適用が新たな項になる。
この定義により、項は有限回の合成手続きで構成される。結果として、項の複雑さは関数記号の入れ子構造として明確になる。
2.2.2 原子式
原子式は、述語記号と所定数の項を並べることで構成される最小単位の式である。ここには論理結合子は含まれないため、原子式は一般に「直接に評価できる」形になっている。
原子式の真偽は、意味論では述語記号の解釈により決まる。したがって原子式は、論理の構造における基底として位置付く。
2.2.3 複合式
複合式は、原子式に対して論理結合子（否定、連言、選言、含意など）や量化子を適用して作られる。さらに、複合式の内部にも複合式を入れ子にできるため、式全体の構造は木構造として捉えられる。
この構文的拡張によって、複雑な条件や分岐的な主張を表現できる。構文の正しさは、量化子の形式、結合子の適用範囲などの規則に従って判定される。
2.3 自由変数と束縛変数
量化子は変数を束縛するため、同じ変数記号であっても式の中での役割は変わりうる。束縛されていない変数は自由変数として残る。自由変数の有無は、意味論で真偽を評価するときに重要になる。
2.3.1 変数の出現
変数の出現は、式の中でその記号がどの位置に現れているかを指す。出現には、量化子によってその変数が管理される範囲内にあるかどうかが関わる。量化子が変数を束縛する範囲では、出現は束縛変数として扱われる。
一方、量化子の範囲外に現れた場合、その出現は自由なまま残る。これにより同一の記号でも、式の部分構造ごとに性格が異なる。
2.3.2 代入
代入は、項を変数に割り当てる操作である。意味論では、束縛変数がある箇所では量化の構造が優先され、自由変数については与えられた値が真偽評価に影響する。構文上の代入では、置き換えが衝突を起こさないように注意が必要である。
とりわけ、置換される変数が量化子によって束縛されているかどうか、また同名の束縛変数が生じないように整合性を取る必要がある。適切な形式化では、変数の衝突を避けるための変換（変数の取り換え）も扱われる。
3 意味論
意味論は、構文で定義された式が、どの解釈の下で真となるかを定める。構文が記号の形だけを規定するのに対し、意味論は対象領域や解釈関数を通じて「意味」を与える。これにより、妥当性、充足可能性、論理的帰結といった概念が明確になる。
3.1 解釈
解釈は、述語記号や関数記号、定数記号を対象領域上の適切な数学的対象へ対応させる写像の集まりとして与えられる。これにより、項や原子式の真偽が計算可能な形で規定される。
3.1.1 対象領域
対象領域は、量化の対象となる要素の集合である。量化子はこの集合上を走査するため、対象領域の選択は式の評価に直接影響する。通常、対象領域は空集合でないと仮定して議論される。
この仮定は、全称量化や存在量化の意味を安定させる。対象領域が変わると、同じ構文の式でも真になるかどうかが変化しうる。
3.1.2 記号の解釈
解釈では、定数記号は対象領域の特定要素に、関数記号は対象領域のn要素組から一要素への関数に、述語記号は対象領域のn要素組から真偽への関数に対応づけられる。これにより、項は対象領域の要素として評価され、原子式は真偽として評価される。
さらに、自由変数が含まれる場合には、変数割当（割り当て関数）を用いて自由変数の値を指定する。こうして式全体の真理が決まる。
3.2 真理条件
真理条件は、ある解釈および変数割当において、式が真になるための条件を再帰的に定義する枠組みである。原子式から論理結合子、量化子へと拡張して定義されるため、計算可能な意味が与えられる。
3.2.1 充足
充足は、対象領域と記号解釈からなる構成のもとで、ある式が真になることを指す。特に、集合の式が同時に真となる場合には、その集合は充足可能であるという言い方をする。個々の式に対する真偽だけでなく、複数条件の同時成立にも意味論の概念が適用される。
充足の有無は、モデルの存在として言い換えられることが多い。したがって、充足は妥当性や論理的帰結の議論へ橋渡しをする役目を持つ。
3.2.2 モデル
モデルは、式群を同時に満たす解釈（あるいはその解釈を含む構成）を指す。具体的には、対象領域と記号解釈が与えられたときに、対象となる文（閉形式の式）や式集合が真になるなら、その解釈はモデルと呼ばれる。
モデルの概念により、単なる式評価を超えて、理論全体（集合としての公理系）を「実現する」構成を議論できる。モデル理論では、モデルの構造や数、同型性などが体系的に研究される。
3.3 妥当性と充足可能性
妥当性と充足可能性は、意味論に基づいて論理関係を測る中心的な概念である。妥当性は「どの解釈でも成り立つ」ことを意味し、充足可能性は「少なくとも一つの解釈で成り立つ」ことを意味する。
3.3.1 論理的真理
論理的真理は、任意の解釈のもとで真となる閉形式の式である。量化や論理結合子が導入されても、意味論上の真理が普遍的に保たれる場合に、この性質が成立する。
この概念は証明可能性と深い関係を持つ。どの構成でも真であるなら、妥当な推論体系ではそれが証明として導かれるべきだ、という期待が生まれるためである。
3.3.2 論理的帰結
論理的帰結は、ある式集合が別の式を含意する関係を意味論的に捉えたものである。つまり、前件の式群が真となる任意の解釈で、後件の式も必ず真になるとき、その帰結が成り立つ。
論理的帰結は、推論体系の正しさ（健全性）や、真に関する完全性と関連づけられる。充足可能性を用いた別表現とも結びつき、証明と意味論の対応を確かめるための鍵となる。
4 推論理論
推論理論は、構文上の操作により妥当な結論が導けることを規定する分野である。ここでの対象は、式の真偽そのものではなく、どのような手順で式から式が導かれるかに置かれる。体系の設計によって、扱える問題の種類や証明の性質が変わる。
4.1 証明体系
証明体系は、与えられた前提から結論を導くための枠組みを与える。一般に証明は、有限回の推論規則の適用として定義され、最終的に導出された式が「証明可能」と呼ばれる。
4.1.1 自然演繹
自然演繹は、推論を演算のように積み上げる形式化である。仮定を導入し、必要に応じて解消しながら結論へ至る構造が、証明の見通しのよさに結びつく。含意の導入、否定の除去といった基本的な考え方が、規則として表現される。
述語論理では、量化に関する導入・除去規則が組み込まれることが多い。さらに、変数の扱い（束縛の干渉回避）を保証する条件が規則の前提に含まれる。
4.1.2 シーケント計算
シーケント計算は、前提と結論の関係を「シーケント」という形で扱う証明体系である。一般に、形式は「ある式群からある式が導かれる」といった関係を、左側に仮定の集合、右側に結論を置く形で表す。
シーケント計算は、カット除去などの理論的性質を得やすい体系として知られる。量化子の扱いも、シーケント上で体系的に整理されるため、構造の制御がしやすい。
4.1.3 公理系
公理系は、特定の式を公理として与え、それらから推論規則で新しい式を導く形式である。公理は、体系が正しい推論を行うための基礎となる原則を表す。
述語論理の公理化は多様であり、量化や等号を含む場合の取り扱い方針も体系ごとに異なる。公理系の利点は、規則を最小限に抑えつつ機械的に推論を生成できる点にある。
4.2 推論規則
推論規則は、証明の各段階でどのように式を変形できるかを定める。自然演繹やシーケント計算などの証明体系ごとに、規則の形は異なるが、量化と等号の扱いは特に重要である。
4.2.1 量化子に関する規則
量化に関する規則では、束縛変数の新規性や、証明中で用いる変数が仮定との関係で安全であることを保証する条件が設けられることが多い。全称量化の導入では、任意性に関する条件が必要になり、存在量化の導入では証人に相当する項の選び方が関係する。
これらの規則は、意味論における量化の真理条件と整合するように設計される。結果として、証明で用いた変形が意味論的な含意と対応づくことが期待される。
4.2.2 等号に関する規則
等号は、対象の同一性を表す論理記号であり、単なる述語と同等に扱うには注意が必要である。等号の反射律、置換（等しいものは同じ性質を持つ）に相当する推論規則が体系に含まれる。
等号に関する規則が適切に入ることで、関数適用や述語適用の場面での置換が一貫して扱える。特に、証明の段階で項の同一視が意味論に反映されるよう、規則の前提条件が整えられる。
4.3 健全性と完全性
健全性と完全性は、推論体系で導けることと、意味論で真であることの対応を述べる定理である。健全性は「証明できるなら意味論的に正しい」ことを保証し、完全性は「意味論的に正しければ証明できる」ことを保証する。
4.3.1 健全性定理
健全性定理は、証明体系において前提から結論が導出可能なら、意味論でも同じ含意関係が成り立つことを言う。つまり、推論規則の適用が意味論の真理条件を壊さない。
健全性があることで、証明によって得た主張を信頼できる。機械的手続きで導かれた結論が、解釈のいかなる選択に対しても破綻しないことが保証される。
4.3.2 完全性定理
完全性定理は、意味論で成立する含意が、推論体系でも証明可能であることを述べる。これにより、意味論的な真理を形式的証明へ橋渡しできる。
完全性は、理論が十分に表現力を持つことと結びつく。結局のところ、推論が意味に対して不足していないことを確かめる性質として位置づく。
4.4 主要な定理
述語論理の理論的性質を示す主要定理として、コンパクト性、レーヴェンハイム・スコーレム、決定不能性に関する結果が挙げられる。これらは、モデルの存在や推論の限界を特徴づける。
4.4.1 コンパクト性定理
コンパクト性定理は、任意の無限個の前提を扱うとき、有限部分での充足可能性が全体の充足可能性に結びつくことを述べる。具体的には、式集合の任意の有限部分が充足可能なら、その全体も充足可能である。
この性質は、有限の検査で無限の整合性が担保されるという意味で強力である。さらに、理論の性質を論理的に推し量る際の基本道具として利用される。
4.4.2 レーヴェンハイム・スコーレムの定理
レーヴェンハイム・スコーレムの定理は、ある濃さ（可算性など）を持つモデルが存在するなら、異なる濃さのモデルも存在するという現象を扱う。対象領域の大きさに関する制約が、論理式の性質によってどの程度制御されるかを示す。
この定理は、量化論理が「どのサイズのモデルまで記述できるか」という限界と関係する。特定のサイズを厳密に固定した理論が、一般には表現できない場合があることを示唆する。
4.4.3 決定不能性に関する結果
決定不能性に関する結果は、述語論理に基づく問題の中に、一般の場合に機械的に正否を判定できないものがあることを示す。典型的には、充足可能性や論理的妥当性を、任意の入力に対して必ず停止する手続きで判定することが不可能であるという形で現れる。
これにより、論理の形式化が大きな表現力を持つ一方で、計算可能な推論の限界も生じることが明確になる。結果は計算機科学とも結びつき、論理と計算の境界を示す指標として扱われる。