数理論理１：言語
ちょっとした経緯があり，数理論理（古典一階論理）の基本事項を少し書きます．
今回は
・言語に対して，その言語の項，論理式の全体が定まること
を述べます．
（定義１－１）言語は，次のような互いに区別できる記号の集合です．
ｎ項関数記号 （各ｎは非負整数）
ｎ項述語記号 （１個以上，各ｎは非負整数）
変数記号 ｘ１ ｘ２ … （可算個）
論理記号 ￢ ∨ ∧ → （結合子とも呼びます） ∀ ∃ （量化子とも呼びます）
補助記号 （ ， ）
ここで，関数記号，述語記号は言語を特徴付けるもので
・それぞれの全体（と各記号に上記のｎを対応させる関数）の組をその言語のシグネチャーと呼びます．
なお
・関数記号，述語記号を非論理記号，その他（つまり，全ての言語に共通するもの）を論理記号と呼ぶ流儀，また，等号＝を論理記号に含める流儀もあります．
言語を固定すると，その言語の項，論理式が以下のように定まります．
（定義１－２）項は
０項関数記号 （定数記号とも呼びます）
変数記号
適当なｎ（＞０）項関数記号ｆ，ｎ個の適当な項ｔ１，...，ｔｎ，補助記号によってｆ（ｔ１，...，ｔｎ）と表せるもの
のいずれかです．
（例１－１）ｘが変数記号，ｃが定数記号，ｆが２項関数記号ならば，ｆ（ｘ，ｃ）は項です．
なお，（定義１－２）では「逆にこれらはいずれも項です．」を略しており，正確には，現れる定数記号でない関数記号の個数に関する帰納法により
Ｔ（０）＝変数記号の全体と定数記号の全体との和集合
任意の非負の整数ｊに対して
Ｔ（ｊ＋１）＝∪＿｛ｎ≧１｝｛ｆ（ｔ１，...，ｔｎ）：ｆはｎ項関数記号，ｔ１，...，ｔｎはそれぞれＴ（ｍ＿１），...，Ｔ（ｍ＿ｎ）の元．ただし，ｍ＿１，...，ｍ＿ｎは和がｊである非負の整数．｝
と定め，項全体を
∪＿｛ｊ≧０｝Ｔ（ｊ）
と定めます．
そして，ｆ（ｔ１，...，ｔｎ）は，項の個数に関する帰納法により
ｆ（ｔ１，...，ｔ１）＝ｆ（ｔ１）
任意の正の整数ｊに対して
ｆ（ｔ１，...，ｔ(ｊ＋１)）＝ｆ（ｔ１，...，ｔｊ）の最後の "）" を "，ｔ(ｊ＋１)）" に置き換えたもの
と定めます．
同様に（定義１－３），（定義２－３）は関数，述語，論理記号の出現の個数，（定義３－１）は推論規則を適用した回数に関する帰納法による定義です．
（定義１－３）論理式は
０項述語記号 （命題記号とも呼びます）
適当なｎ（＞０）項述語記号ｆ，ｎ個の適当な項ｔ１，...，ｔｎ，補助記号によってｐ（ｔ１，...，ｔｎ）と表せるもの
のどちらか（これらを原子論理式と呼びます），或いは，適当な変数記号ｘ，論理式Ａ，Ｂおよび論理記号，補助記号によって
￢（Ａ）
（Ａ）∧（Ｂ）
（Ａ）∨（Ｂ）
（Ａ）→（Ｂ）
（∀ｘ）（Ａ） （この∀ｘのｘ，および，Ａ内の各ｘをｘの（全称）束縛出現といいます）
（∃ｘ）（Ａ） （この∃ｘのｘ，および，Ａ内の各ｘをｘの（特称）束縛出現といいます）
のいずれかと表せるものです．
ここで
・論理式に現れる個々の変数記号をその変数記号の出現
・束縛出現でない変数記号の出現を自由出現
・各変数記号の出現がすべて束縛出現である論理式を閉（じた）論理式，そうでない論理式を開（いた）論理式
そして
・閉論理式以外の元をもたない集合を理論
と呼びます．
なお，Ａ，Ｂが論理式ならな
（Ａ）（Ｂ）は（（Ａ）→（Ｂ））∧（（Ｂ）→（Ａ））
の略記とします．
また，言語の定義において，論理記号は，例えば ￢ ∧ ∃ のみとして
（Ａ）∨（Ｂ）は ￢（（￢（Ａ））∧（￢（Ｂ）））
（Ａ）→（Ｂ）は ￢（Ａ∧（￢（Ｂ）））
（∀ｘ）（Ａ）は ￢（（∃ｘ）（￢（Ａ）））
それぞれの略記と定義する流儀もあります．
（例１－２）ｘ，ｙが変数記号，ｆが１項関数記号，ｐが１項述語記号，ｒが２項述語記号ならば
ｒ（ｆ（ｘ），ｙ）
（（∀ｘ）（ｐ（ｘ）））→（ｐ（ｘ））
はどちらも論理式，そして
（∃ｘ）（（ｐ（ｘ））→（（∀ｘ）（ｐ（ｘ））））
は閉論理式です．
（例１－２）の論理式をそれぞれ
ｒｆｘｙ
（∀ｘｐｘ）→ｐｘ 或いは （∀ｘ（ｐ（ｘ）））→ｐ（ｘ）
∃ｘ（ｐｘ→∀ｘｐｘ） 或いは ∃ｘ（ｐ（ｘ）→∀ｘ（ｐ（ｘ）））
などのように記すこともあり，本稿もその作法に従います．
（定義１－４）Ａが論理式，ｘ，ｙ，..がＡに現れる束縛されていない全ての変数記号ならば，Ａの全称閉包は閉論理式∀ｘ∀ｙ...（Ａ）です．
論理式を"閉じる"方法としては，各変数の自由出現を各変数ごとに新たな定数記号に置き換えるというものもあり，本稿のメタ論理でも暗にそれを採用しています．
（参考）
https://www.encyclopediaofmath.org/index.php/Formalized_language
