━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
数理論理学 第10回「自然演繹 2」の要点
━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━

●述語論理の構文論

述語論理の構文
        項と論理式の集合は帰納的に定義でき，木構造としても表せる

項の帰納的定義
        変数は項
        f が k 変数の関数記号で t1, …, tk が項のとき，f(t1,…,tk) は項

論理式の帰納的定義
        P が k 変数の述語記号で t1, …, tk が項のとき，P(t1,…,tk) は論理式
        ⊥ は論理式
        A と B が論理式のとき，(A∧B) と (A∨B) と (A⇒B) は論理式
        x が変数で A が論理式のとき，(∀x A) と (∃x A) は論理式

●証明の形式化

自然演繹
        論理式，推論規則，導出

推論規則
        前提(0〜2個)から結論(1個)を導く推論の1段階を表す規則
        論理記号ごとに導入規則と除去規則がある

証明図
        推論規則を繰り返し使って図で表した証明

証明可能
        仮定をすべて解消した証明図が作れること

━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━
授業のホームページ

山田 俊行
https://www.cs.info.mie-u.ac.jp/~toshi/