20260527_1

20260520_1

---

証明論に入る

伝統的な論理学では論理的思考の技術(妥当な推論の分類)

ライプニッツ: 知識を記号体系でまとめる(有限的、計算的)

フレーゲ: 論理主義(数学基礎論)

その他にも直観主義や形式主義を経て不完全性定理に

1930s以降に数理論理学が

1. 証明論(有限的な記号の列としての証明、無矛盾性証明など)
2. 意味論(モデル論)
3. 計算論(チューリングマシンとか)
4. 集合論(連続体問題など)

キーパーソンはヒルベルトらしい

---

自然言語の証明ははっきりと定義されていない(書き方に個人差がある)
→これを何とかしたい

Bと仮定する。よってAが示された

↑これはさすがにヤバイ
中間ステップの必要性(意味論ではこれが存在していなかった)

中間ステップでは推論規則をつかっている

$A\wedge B\to C$、$B$。よって$A\wedge B$。したがって、$C$

↑こんな感じになる

ゲンツェン(ヒルベルトの学生)の自然演繹

証明を木みたいな形式に

$B$から$A\wedge B$を導いてよい

\dfrac{B}{A\land B}

$A$と$A\to B$から$B$を導いてよい

\dfrac{A \quad A\to B}{B}

どちらかというと言語的な活動が先になるらしい

証明を木みたいにするけど使いやすく分かりやすい、その一方自動証明は難しい

• 導入規則
  • ある論理的な語彙($\wedge$)などを主張するにはどのような文を主張したら十分か？
  • 語彙を知っていくようなプロセスと似ている
• 除去規則
  • ある論理的な語彙($\wedge$)などを含む分が主張できるときにそこ仮名何が帰結できるのかを定める

$\to$の除去規則(Elminination rule for implication)

$\frac{PP\to Q}{Q}\to E$

$\mathbb{P},\mathbb{Q}$には任意の論理式が入る

---

$\wedge$の除去規則

$$\frac{P\wedge Q}{P}\wedge E\frac{P\wedge Q}{Q}\wedge E$$

$\mathbb{P},\mathbb{Q}$には任意の論理式が入る

これが当てはまる例はたくさんある

---

証明(図): 推論規則が正しく組み合わされたもの

$A_1,\dots ,A_n⊢B$:$A_1,\dots ,A_n$を家庭として$B$を結論とする証明が存在する

• 仮定: 証明の一番上に現れる論理式
• 結論: 証明の一番下に現れる論理式

$Ft\wedge Fh\to (Gt\to Ht),Ft\wedge Fh,Gt⊢Ht$の証明図

$$\frac{Gt\frac{Ft\wedge FhFt\wedge Fh\to (Gt\to hT)}{Gt\to Ht}\to E}{Ht}\to E$$

木構造になっている
仮定が木の先端(葉)、結論が一番下(根)

---

$Fa,Fa\to Fb,Fb\to Fc⊢Fc$を例に

$$\frac{\frac{FaFa\to Fb}{Fb}\to EFb\to Fc}{Fc}\to E$$

$Fa\to (Ga\to Gb),Fa\wedge Ga⊢Gb$を証明する

$$\frac{\frac{Fa\wedge Ga}{Ga}\wedge E\frac{\frac{Fa\wedge Ga}{Fa}\wedge EFa\to (Ga\to Gb)}{Ga\to Gb}\to E}{Gb}\to E$$

前提にある論理式は複数回使ってもいい

$\forall$の除去規則

$$\frac{\forall \mathbb{P}(x)}{\mathbb{P}(t)}\forall E$$

$t$は任意の個体定項ないし個体変項

→すべてのものについて$P$が成り立つなら任意の個体$x$にも$P$が成り立つ

$$\frac{\frac{\forall y\forall xRxy}{\forall xRxa}\forall E}{Rba}\forall E$$

記号は一つずつしか消せない

$\forall x(Fx\wedge Gx)⊢Fa$

$$\frac{\frac{\forall x(Fx\wedge Gx)}{\forall x(Fa\wedge gx)}\forall E}{Fa}\wedge E$$

↑違う

$$\frac{\frac{\forall x(Fx\wedge Gx)}{Fa\wedge Ga}\forall E}{Fa}\wedge E$$

$\forall x(\exists yFy\to Gx),\exists yFy⊢Ga$

$$\frac{\exists yFy\frac{\forall x(\exists yFy\to Gx)}{\exists yFy\to Ga}\forall E}{Ga}\to E$$

$\forall x\forall y(Rxy\to Fy),\forall xRax⊢Fb$

$$\frac{\frac{\forall xRax}{Rab}\forall E\frac{\frac{\forall x\forall y(Rxy\to Fy)}{\forall x(Ray\to Fy)}\forall E}{Rab\to Fb}\forall E}{Fb}\to E$$