直観主義論理: 可能世界意味論(1階述語論理)

公開日: 2022/09/14

最終更新: 2023/05/07

この記事では、直観主義論理の 可能世界意味論(possible world semantics) の1階述語論理バージョンを紹介する。

なお以下では、1階述語論理の言語$\L$と変数記号の加算無限集合$\Var$があらかじめ与えられているものとする。ただし、定数記号は0変数の関数記号、命題変数は0変数の述語記号であると見なす。

項と原子論理式は通常通り定める。また、論理式の集合$\Fml$を以下のように帰納的に定める。

  • $\vphi$が原子論理式ならば、$\vphi\in\Fml$
  • $\top,\bot\in\Fml$
  • $\vphi,\psi\in\Fml$ならば、$\vphi\land\psi, \vphi\lor\psi, \vphi\to\psi\in\Fml$
  • $x\in\Var, \vphi\in\Fml$ならば、$\forall x.\vphi,\exists x.\vphi\in\Fml$

自由変数を含まない項を閉項という。また、自由変数を含まない論理式のことを文(sentence)といい、文の集合を$\Snt$とする。

命題論理と同様に、$\lnot \vphi \defeq \vphi\to\bot$とする。

非形式的な説明

直観主義命題論理の可能世界意味論では、論理式の真偽はそれぞれの状態で定まり、状態と状態の間の遷移関係を時間の経過としてモデル化した。そして、時間の経過とともに真と判明した論理式が増加するように制約を設けた(遺伝性)。

述語論理の場合は量化の範囲(領域)を考慮に入れることになるが、考え方は同じである。各状態に領域を付随させ、時間の経過とともに「発見された(存在が保証された)」対象が増えていくように制約を与えればよい。

また、量化子の解釈を与えるために、BHK解釈を以下のように拡張しよう。全称量化$\forall$は含意$\to$に、存在量化$\exists$は連言$\land$に似ていることが観察できる。1

定義. BHK解釈(量化子)
  • $\forall x.\vphi$の証明は、任意の対象$d$を$\vphi[x:=d]$の証明へと変換する手続きである
  • $\exists x.\vphi$の証明は、ある対象$d$と$\vphi[x:=d]$の証明の組である

定義

まずは、古典述語論理の場合と同様に、言語に対する解釈を与えるための構造を与える。

定義. 構造

(言語$\L$に対する) 構造(structure) $\A$を、以下から成る組とする。

  • $|\A|$: 非空な集合
  • $n$変数関数記号$f$に対して、$f^\A:|\A|^n\to |\A|$
  • $n$変数述語記号$P$に対して、$P^\A\sube |\A|^n$

$|\A|$を 領域(domain) といい、記号$s$に対して$s^\A$を$\A$上の$s$の 解釈(interpretation) という。

定義. 構造の包含関係

(言語$\L$に対する)構造$\A,\A'$に対して、$\A\sube\A'\defiff$以下の条件が成り立つ

  • $|\A|\sube|\A'|$
  • $\L$の任意の関数記号$f$に対して、$f^\A\sube f^{\A'}$2
  • $\L$の任意の述語記号$P$に対して、$P^\A\sube P^{\A'}$

モデルの定義は、命題論理バージョンのモデルの付値$v$を構造に置き換えたものになる。

定義. モデル

直観主義述語論理の モデル(model) を、以下から成る組$\tuple{W, \leq, (\A_w)_{w\in W}}$のこととする。

  • $W$: 非空な集合
  • $\leq$: $W$上の擬順序
  • 各$\A_w$は構造であり、以下を満たす
$$ \Forall w,w'\in W.w\leq w'\implies \A_w\sube \A_{w'} $$
命題変数(0変数述語記号)に対する遺伝性の条件を書き下すと、以下のようになる(ただし単元集合$X^0$を$T$と書く)。
$$ w\leq w'\And P^{\A_w} \in T \implies P^{\A_{w'}} \in T $$
$P^{\A_w} \in T$を$v_w(P)=1$と読み替えれば、これは命題論理の付値に対する遺伝性の条件と対応していることが分かる。

以下では、モデルの各状態における論理式の真偽を定義する。そのために、自由変数に対して領域上の対象を割り当てる関数を定義する。

定義. 割り当て・値

構造$\A$に対して、$\A$上の 割り当て(assignment) を関数$g:\Var\to |\A|$とする。また、$d\in|\A|$に対して、関数$g[x\mapsto d]:\Var\to |\A|$を以下のように定義する。

$$ g[x\mapsto d] (v) \defeq \begin{cases} d&(\If v=x)\\ g(v)&(\Otherwise) \end{cases} $$

$\A$上の割り当て$g$による項$t$の 値(value) $\intpr{t}_{\A,g}$を、項の構成に関する帰納法で以下のように定める。

  • $x\in\Var$: $\intpr{x}_{\A,g}\defeq g(x)$
  • $\intpr{ft_1\ldots t_n}_{\A,g}\defeq f^{\A}(\intpr{t_1}_{\A,g},\ldots,\intpr{t_n}_{\A,g})$

ここで、充足関係の定義のために以下の点に注意する必要がある。

補題.

$\A\sube\A'$のとき、$\A$上の割り当て$g$に対して、

  • $g$は$\A'$上の割り当てである
  • 任意の$d\in|\A'|$に対して、$g[x\mapsto d]$は$\A'$上の割り当てである
$\A\sube\A'$ならば$|\A|\sube|\A'|$なので明らか。

この補題により、以下の定義が可能になる。

定義. 充足関係

モデル$\M=\tuple{W, \leq, (\A_w)_{w\in W}}$と$w\in W$、および$\A_w$上の変数割り当て$g$に対して、論理式$\vphi$の充足関係$\M,w\vDash_g\vphi$を以下のように帰納的に定める3。

  • 原子論理式:$\M,w\vDash_g Rt_1\ldots t_n\defiff \tuple{\intpr{t_1}_{\A_w,g},\ldots,\intpr{t_n}_{\A_w,g}}\in R^{\A_w}$
  • $\M,w\vDash_g\top$
  • $\M,w\nvDash_g\bot$
  • $\M,w\vDash_g\vphi\land\psi \defiff \M,w\vDash_g\vphi\And \M,w\vDash_g\psi$
  • $\M,w\vDash_g\vphi\lor\psi \defiff \M,w\vDash_g\vphi \Or \M,w\vDash_g\psi$
  • $\M,w\vDash_g\vphi\to\psi \defiff \Forall w'\geq w.~\M,w'\vDash_g\vphi\implies\M,w'\vDash_g\psi$
  • $\M,w\vDash_g\exists x.\vphi\defiff \Exists d\in |\A_w|.~\M,w\vDash_{g[x\mapsto d]}\vphi$
  • $\M,w\vDash_g\forall x.\vphi\defiff \Forall w'\geq w.\Forall d\in |\A_{w'}|.~\M,w'\vDash_{g[x\mapsto d]}\vphi$

このとき($\M$において)状態$w$と割り当て$g$のもとで$\vphi$が真であるという。モデルが明らかな場合は$\M$を省略して$w\vDash_g\vphi$と書く。

また、論理式の集合$\Gamma\sube\Fml$に対して、

$$ w\vDash_g\Gamma\defiff\Forall \vphi\in\Gamma.w\vDash_g\vphi $$

推論の妥当性の定義は、命題論理の場合と同様である。

定義. 妥当性

$\Gamma\cup\qty{\vphi}\sube\Snt$とする。$\Gamma$から$\vphi$への推論が 妥当である(valid) ことを、任意のモデル$\M=\tuple{W,\leq,(\A_w)_{w\in W}}$、および$w\in W$と$\A_w$上の割り当て$g$に対して$w\vDash_g\Gamma$ならば$w\vDash_g\vphi$であることと定義する。これを$\Gamma\vDash\vphi$と書く。

前提を真・結論を偽とするような状態が存在するモデルのことを 反例モデル(counter model) という。すなわち、$\Gamma$から$\vphi$への推論に対する反例モデル$\M=\tuple{W,\leq,(\A_w)_{w\in W}}$は以下を満たす。

$$ \Exists w\in W.\Exists g:\text{$\A_w$上の割り当て}.~ w\vDash_g\Gamma \And w\nvDash_g\vphi $$

性質

基本的な性質

遺伝性の拡張

モデルの定義から、原子論理式に対する遺伝性は保証されている。命題論理の場合と同様に、この性質は一般の論理式に拡張できる。

命題. 遺伝性の拡張

任意のモデル$\M=\tuple{W,\leq,(\A_w)_{w\in W}}$, $w\leq w'$となる状態$w,w'\in W$, $\A_x$上の割り当て$g$について、

$$ \Forall\vphi\in\Fml.~w\vDash_g\vphi \implies w'\vDash_g\vphi $$

論理式の構成に関する帰納法で示す。$\forall$についてのみ示す。

$w\vDash_g\forall x.\vphi$を仮定する。$w'\vDash_g\forall x.\vphi$を示すために、$w''\geq w'$となる$w''\in W$, および$d\in |\A_{w''}|$を任意にとる。このとき、推移性より$w''\geq w$でもあるから、仮定より$w'''\vDash_{g[x\mapsto d]}\vphi$となる。これと充足関係の定義より$w'\vDash_g\forall x.\vphi$となる。

※$\forall$の場合には帰納法の仮定を使う必要がない。

存在特性

命題論理の場合と同様に選言特性が成り立つ。さらに、存在量化を連言が無限に連なったものと見なすことにより、以下の 存在特性(existence propery) が得られる。

命題.
$$ \Forall(\exists x.\vphi)\in\Snt.~\vDash\exists x.\vphi \implies \Exists t:閉項. {}\vDash\vphi[x:=t] $$

なお、これが古典論理では成り立たないことは、例えば適当な命題記号$P$と定数記号$c,c'$に対して$\vphi = (P \land x=c)\lor(\lnot P\land x=c')$が反例になることから分かる。

証明の大枠は選言特性と同じだが、構造・割り当ての扱いに注意する必要がある。

概略のみ示す。任意の閉項$t$に対して$\nvDash\vphi[x:=t]$となることを仮定し、対偶を示す。仮定より、それぞれの閉項$t$に対してモデル$\M_t=\tuple{W_t,\leq_t,(\A_{w})_{w\in W_t}}$, 状態$w_t\in W_t$が存在して、$\M_t,w_t\nvDash_g\vphi[x:=t]$となる ($\vphi[x:=t]$は文なので、割り当て$g$は任意)。

反例モデルのフレームとして、各$W_t$のそれぞれ$w_t$より後の部分だけ取り出し、それらに新たな最小元$w_0$を付け加えたようなものを考える(下図参照)。$w_0$での構造は、各構造$\A_{w_t}$で共通部分をとって定義する。これにより構成されたモデルを$\overline{\M}$とする。

$$ \begin{xy} (0,0) *+{w_0}*\frm{o}="w0", (0,-9) *+{\small \Forall t: 閉項.~-\vphi[x:=t]}="pto", (-30,20) *+{w_t}*\frm{o}="w1", (-43,10) *+{\small -\vphi[x:=t]}="pfrom1", (-30,30) *++++++++++{}*\frm{o}, (-30,31) *+{\vdots}, (-25,30) *+{\small\leq}, (-30,40) *+{W_t}, (10,20) *+{~~~}*\frm{o}="w2", (10,30) *++++++++++{}*\frm{o}, (10,31) *+{\vdots}, (15,30) *+{\small\leq}, (10,40) *+{}, (50,20) *+{~~~}*\frm{}="w3", (45, 30) *{\large\cdots}, \ar^{\leq} "w0";"w1", \ar_{\leq} "w0";"w2", \ar_{\leq} "w0";"w3", \ar@{-->}@/_1.35pc/_{遺伝性} "pfrom1";"pto", \ar@{-->}@/^2pc/ "w2";"pto", \ar@{-->}@/^2pc/ "w3";"pto" \end{xy} $$

$\A_{w_0}$上の割り当て$g$を1つとる(任意でよい)。このとき、任意の閉項$t$に対して$\overline{\M},w_t\nvDash_g\vphi[x:=t]$になることが示せる。これと遺伝性(の対偶)より$\overline{\M},w_0\nvDash_g\vphi[x:=t]$がいえる。ここから$\overline{\M},w_0\nvDash_g\exists x.\vphi$を示すためには、以下の性質を利用する必要がある(証明は論理式の構成に関する帰納法による)。

補題. 代入の可換性
$$ \M, w\vDash_g \vphi[x:=t] \iff \M, w\vDash_{g\left[x \mapsto \intpr{t}_{\A_w, g}\right]} \vphi $$

これにより$\overline{\M},w_0\nvDash_{g\left[x\mapsto\intpr{t}_{\A_{w_0},g}\right]}\vphi$が言えるので、確かに$\overline{\M},w_0\nvDash_g\exists x.\vphi$となり、$\overline{\M}$が反例モデルになることが分かる。

推論に関する性質

命題論理の場合と同様に、古典(述語)論理で妥当な推論は直観主義論理でも妥当になる。

また、古典論理では妥当な推論の一部が実際に非妥当になることが確認できる。ここでは量化子が関係するものを挙げる。

命題. 非妥当な推論
  • $\lnot\forall x.\vphi\nvDash \exists x.\lnot\vphi$
  • $\nvDash\lnot\lnot\forall x.(\vphi\lor\lnot\vphi)$
  • $\forall x.\lnot\lnot\vphi \nvDash \lnot\lnot\forall x.\vphi$
  • Markov's Principle: $\forall x.(\vphi\lor\lnot\vphi)\land \lnot\lnot\exists x.\vphi \nvDash \exists x.\vphi$
  • Grzegorczyk's Scheme: $\forall x.(\vphi\lor\psi)\nvDash \vphi\lor\forall x.\psi$ (ただし$x\notin\FV(\vphi)$)

1つ目についてのみ示す。1変数述語記号$P$を1つとって固定し、以下のようにモデル$\M$を定義する。

  • $W=\qty{w_1,w_2}$
  • $\leq{}=\qty{\tuple{w_1,w_1},\tuple{w_2,w_2},\tuple{w_1,w_2}}$ (確かに擬順序)
  • 構造は以下のように定義する(可読性のため$\A_{w_i}$ではなく$\A_i$と書く)
    • $|\A_1|=\qty{d},~P^{\A_1}=\varnothing$
    • $|\A_2|=\qty{d,d'},~P^{\A_2}=\qty{d}$

$\A_1$上の割り当て$g$を1つとる(任意でよい)。このとき、

  • $d'\notin P^{\A_2}$なので$w_2\nvDash_g\forall x.Px$であり、これと遺伝性(の対偶)から$w_1\nvDash_g\forall x.Px$でもある。よって$w_1\vDash_g\lnot\forall x.Px$がいえる。
  • $P^{\A_1}=\varnothing$より$w_1\vDash_{g[x\mapsto e]} Px$となる$e\in|\A_1|$は存在しないので、$w_1\nvDash_g\exists x.Px$がいえる。

よって、状態$w_1$において前提が真・結論が偽となるから、$\M$は反例モデルになっていることが分かる。

参考文献

  • Sørensen, M. H., & Urzyczyn, P. (2006). Lectures on the Curry-Howard isomorphism. Elsevier.
  • van Dalen, D. (2004). Logic and structure. Berlin: Springer.

Footnotes

  1. 実際、型理論において全称・存在量化子に対応する型は、それぞれ関数型・直積型の一般化として定義される(依存関数型$\Pi x{:}A.B$・依存直積型$\Sigma x{:}A.B$)。 ↩
  2. ここでは関数を関係の特殊な場合と見なした場合の包含関係のことを言っている。 ↩
  3. 言語に等号を含める場合は、以下の定義を加える: $\M,w\vDash_g t_1 = t_2\defiff \intpr{t_1}_{\A_w,g} = \intpr{t_2}_{\A_w,g}$ ↩