一階述語論理の形式的体系(統語論) (Syntax)

一階述語論理の言語 L の構成


• すべての言語に共通
  1. (個体)変数 (logical variable) : 可算無限個供給される

  2. 論理演算子(論理記号, logical operator)，¬，∧，∨，→，≡，∀，∃

  3. 補助記号: 括弧やコンマ

• 言語によって異なるもの
  1. 個体定数 (constant)

  2. 関数記号 (function symbol)

  3. 述語記号 (predicate symbol)

項(term)


定義 [項] 項は次のようにして再帰的に定義される．

個体定項は項である．

個体変数は項である．

f が n-引数 (n-ary) の関数記号，t₁, t₂, ..., t_n, が項であるとき f(t₁, t₂, ..., t_n) も項である．

上の規則を適用して生成されたものだけが項．

素論理式 (atomic formula)


定義 [素論理式] P が n-項述語記号， t₁, t₂, ..., t_n が項であるとき， P(t₁, t₂, ...,t_n)を素論理式(基本論理 式)，もしくはアトムという．さらに，この論理式の 引数の数 (arity) は n であるという．

論理式 (formula)


定義 [論理式] 次のように定義される表 現を L の論理式という．

1. 素論理式は L の論理式である．

2. α，β を L の論理式とすると，¬α，α → β はそれぞれ L の論理式 である．

3. x を論理変数，α を L の論理式とすると，(∀x)α，(∃x)αは L の論 理式である．( (∃x)α = ¬((∀x)¬α) であることに注意)

限量子 (quantifier)


定義 [全称限量子 (universal quantifier, 全称 記号)]
論理式 (∀x)α において，個体変数xの出現は全称限量されているという． α を (∀x) の作用域 (scope)という．α中の 個体変数 x の全ては (∀x)により束縛 (bound) されているという．

定義 [存在限量子 (existential quantifier，存 在記号)]
論理式 (∃x)α において，個体変数xの出現は存在限量されているという．α を (∃x) の作用域 (scope)という．α中の 個体変数 x の全ては (∃x)により束縛 (bound) されているという．

定義 [自由変数 (free variable)]
論理式の中で束縛されていない変数は自由である (free) といい，その変数を自由変数 (free variable) とよぶ．自由 変数を含まない論理式を閉論理式 (closed formula)という．

具体例
(∀x) (P(y) (∀y) (P(x) ∧ Q(y)))

(∀x)(∃y) (Q(f(x), y) → (∃z) R(y, z, w))

上記の論理式に自由変数はあるか? これらは閉論理式か?

...Return

• 講義の詳細