論理的妥当性

同義語：妥当式妥当性(論理学)論理的に妥当logical validityvalid formula

概要

前提知識: 一階述語論理, 命題論理, 論理式

「すべての元が性質 $P$ をもつならば、定数 $c$ の表す元も $P$ をもつ」という主張 $\forall x\,P(x)\to P(c)$ は、台集合が何であっても、$P$ と $c$ をどう解釈しても成り立つ。成り立つ理由は $P$ や $c$ の中身ではなく、$\forall$ と $\to$ の使い方だけにある。これに対し、$\forall x\,\exists y\,(x< y)$ は $(\mathbb N,<)$ では真だが、有限の全順序集合では偽になる。どの構造、どの割り当てで読んでも真になる論理式を 論理的に妥当 な論理式という。妥当な論理式は「論理だけで正しい」主張を数学的に定式化したものであり、証明体系で前提なしに導出できる論理式と一致する（Gödelの完全性定理）。
妥当性は命題論理の恒真式を一階論理に広げた概念である。恒真式に一階の論理式を代入したものは妥当だが、妥当な論理式は恒真式の代入例に限らない。また、恒真式かどうかは真理値表で機械的に判定できるのに対し、一階の論理式が妥当かどうかを判定する機械的な手順は存在しない。本記事では、妥当性の定義と基本性質を証明し、1 項の関係記号だけからなる文では妥当性が小さい有限構造だけで判定できることを証明して、一般の場合との違いを見る。

定義

一階言語 $L$、$L$ 構造 $\mathcal M$（台集合 $M$ は空でない）、割り当て $s$、充足関係 $\mathcal M\models\varphi[s]$、割り当ての書き換え $s_x^a$ は一階述語論理の記事の定義「構造」「充足関係」による。論理式、自由変数の集合 $\operatorname{FV}(\varphi)$、文、代入 $\varphi[t/x]$ は論理式の記事による。

論理的妥当性

$L$ の論理式 $\varphi$ が、すべての $L$ 構造 $\mathcal M$ とすべての割り当て $s$ について $\mathcal M\models\varphi[s]$ を満たすとき、$\varphi$ は 論理的に妥当（logically valid）、または単に妥当であるといい、$\models\varphi$ と書く。妥当な論理式を 妥当式 ともいう。

$\varphi$ が文なら、真偽は割り当てによらない（一階述語論理の記事の系「文の真偽は割り当てによらない」）。したがって、文が妥当であることは「すべての $L$ 構造で真」と同じであり、同記事の定義「モデル・妥当性・論理的帰結」の「妥当な文」と一致する。

充足可能・論理的帰結

論理式の集合 $\Gamma$ について、ある $L$ 構造 $\mathcal M$ と割り当て $s$ で $\Gamma$ のすべての元 $\gamma$ が $\mathcal M\models\gamma[s]$ を満たすとき、$\Gamma$ は 充足可能 であるという。充足可能でないことを 充足不能 という。論理式 $\varphi$ について、$\Gamma$ のすべての元を充足する $\mathcal M,s$ がつねに $\varphi$ も充足するとき、$\Gamma\models\varphi$ と書く。$\varphi$ が妥当であることは $\emptyset\models\varphi$ と同じである。

1 つの論理式 $\varphi$ について、「妥当」「充足可能だが妥当でない」「充足不能」のちょうど 1 つが成り立つ。$\models$ の記号は、左に構造と割り当てを書く $\mathcal M\models\varphi[s]$（充足）、左に集合を書く $\Gamma\models\varphi$（帰結）、左に何も書かない $\models\varphi$（妥当）の 3 通りに使い分ける。
妥当性は言語の選び方によらない。$L\subset L'$ で $\varphi$ が $L$ の論理式なら、$\varphi$ が $L$ 構造すべてで妥当であることと $L'$ 構造すべてで妥当であることは同値である。$\mathcal M\models\varphi[s]$ の定義の再帰は $\varphi$ に現れる記号の解釈しか参照しないので、$L'$ 構造 $\mathcal M'$ とそこから $L'\setminus L$ の記号の解釈を忘れた $L$ 構造 $\mathcal M$ とで $\varphi$ の充足は一致し（論理式に関する帰納法）、逆にどの $L$ 構造も、台集合が空でないので $L'\setminus L$ の記号に適当な解釈を与えて $L'$ 構造に広げられるからである。

直感

妥当な論理式は、構造を「読み方」とみたとき、どう読んでも崩れない記号列である。1 つの構造で真であることは、その構造についての数学的事実にすぎない。妥当性はそれより強く、記号 $P,R,c,f$ にどんな集合・関係・元・写像を当てはめても真であることを求める。逆に、妥当でないことを示すには、偽になる構造と割り当てを 1 つ作れば足りる。この非対称性が、「妥当なら（証明を探せば）いつかは分かるが、妥当でないことはいつまでも分からないことがある」という計算上の性質（rem-logical-validity-decidability）につながる。

例と反例

妥当な論理式

$P,Q$ を 1 項関係記号、$c$ を定数記号とする。

$\forall x\,P(x)\to P(c)$。$\forall x\,P(x)$ が真なら台集合のすべての元が $P^{\mathcal M}$ に属し、とくに $c^{\mathcal M}$ も属する。
$\forall x\,(P(x)\to Q(x))\to(\forall x\,P(x)\to\forall x\,Q(x))$。前件 2 つが真なら、各 $a\in M$ について $a\in P^{\mathcal M}$ かつ「$a\in P^{\mathcal M}$ ならば $a\in Q^{\mathcal M}$」なので $a\in Q^{\mathcal M}$ である。
$\lnot\exists x\,P(x)\leftrightarrow\forall x\,\lnot P(x)$。どちらも「$P^{\mathcal M}=\emptyset$」と同値である。
$\forall x\,P(x)\to\exists x\,P(x)$。台集合が空でないので元 $a$ がとれ、$\forall x\,P(x)$ が真なら $a\in P^{\mathcal M}$ となり $\exists x\,P(x)$ が真である（空の台集合を許すと崩れる。一階述語論理の記事の例「反例：空の台集合」）。
$\exists x\,(P(x)\to\forall y\,P(y))$。$P^{\mathcal M}=M$ なら任意の $a$ で後件が真、$P^{\mathcal M}\ne M$ なら $a\notin P^{\mathcal M}$ をとれば前件が偽になる（古典論理の記事の例「酒飲みの式」）。
どれも自由変数をもたないので、各 $\mathcal M$ で真であることを見ればよい。

反例：妥当でない論理式

$\forall x\,\exists y\,R(x,y)\to\exists y\,\forall x\,R(x,y)$ は妥当でない。$(\mathbb N,<)$ で $R$ を $<$ と読むと、前件「どの $x$ にもそれより大きい $y$ がある」は真だが、後件「すべての $x$ より大きい $y$ がある」は偽である。量化記号の順序を入れ替えると意味が変わる。逆向きの $\exists y\,\forall x\,R(x,y)\to\forall x\,\exists y\,R(x,y)$ は妥当である（前件の $y$ をどの $x$ にも使えばよい）。
$\exists x\,P(x)\to\forall x\,P(x)$ は妥当でない。台集合 $\{0,1\}$、$P$ の解釈 $\{0\}$ で前件は真、後件は偽である。ただし、1 元の構造ではこの式は真になるので、充足可能ではある。
$P(x)$ は充足可能だが妥当でない。$\emptyset\ne P^{\mathcal M}\ne M$ の構造で $s(x)\in P^{\mathcal M}$ とすれば充足され、$s(x)\notin P^{\mathcal M}$ とすれば充足されない。$P(x)\land\lnot P(x)$ は充足不能である。

妥当性の定義の条件を弱めたり、判定を簡単にしようとして調べる構造を減らしたりすると何が崩れるかを表にまとめる。

外す条件	反例	成り立たなくなること
すべての構造で真	$\forall x\,\exists y\,(x< y)$（$(\mathbb N,<)$ で真）	妥当
すべての割り当てで真	$P(x)$	妥当
台集合が空でない	空の台集合を許した構造	$\forall x\,(x=x)\to\exists x\,(x=x)$ の妥当性
無限構造も調べる	$\lnot(\text{非反射}\land\text{推移}\land\forall x\,\exists y\,R(x,y))$	「すべての有限構造で真なら妥当」
等号を使わない（1 項関係記号の文）	$\forall x\,\forall y\,(x=y)$	「$2^k$ 元以下の構造で真なら妥当」
1 項関係記号だけ	上の $R$ を使った文	「小さい有限構造で真なら妥当」

1 行目と 2 行目は ex-logical-validity-invalid の 1・3、3 行目は一階述語論理の記事の例「反例：空の台集合」による。4〜6 行目は「1 項関係記号だけの文」の節の ex-logical-validity-finite-not-valid と ex-logical-validity-equality で確かめる。

性質

全称閉包と充足不能性

全称化と妥当性

論理式 $\varphi$ と変数 $x$ について、$\models\varphi$ であることと $\models\forall x\,\varphi$ であることは同値である。したがって、$\operatorname{FV}(\varphi)=\{x_1,\dots,x_n\}$ のとき、$\varphi$ が妥当であることと、その 全称閉包 $\forall x_1\cdots\forall x_n\,\varphi$（文である）が妥当であることは同値である。

割り当てを書き換える

$\models\varphi$ とする。任意の $\mathcal M$、$s$、$a\in M$ について、割り当て $s_x^a$ でも $\varphi$ は充足されるので、充足関係の定義により $\mathcal M\models\forall x\,\varphi[s]$ である。よって $\models\forall x\,\varphi$ である。
逆に $\models\forall x\,\varphi$ とし、$\mathcal M$、$s$ を任意にとる。$\mathcal M\models\forall x\,\varphi[s]$ なので、すべての $a\in M$ で $\mathcal M\models\varphi[s_x^a]$ である。$a:=s(x)$ とすると $s_x^{s(x)}=s$ なので $\mathcal M\models\varphi[s]$ である。よって $\models\varphi$ である。
後半は前半を $x_n,x_{n-1},\dots,x_1$ の順に $n$ 回使えばよい。全称閉包の自由変数は $\operatorname{FV}(\varphi)\setminus\{x_1,\dots,x_n\}=\emptyset$ なので文である。$\square$

この命題は論理式の組についての主張である。1 つの構造の中で「$\varphi$ が $s$ のもとで真なら $\forall x\,\varphi$ も $s$ のもとで真」は成り立たない。ex-logical-validity-invalid の 3 の $P(x)$ が反例である。妥当性の問題は、この命題により文の妥当性の問題に帰着する。

充足不能性・有限個の前提との関係

$\varphi,\psi_1,\dots,\psi_n$ を論理式とする。

$\models\varphi$ であることと、$\lnot\varphi$ が充足不能であることは同値である。
$\{\psi_1,\dots,\psi_n\}\models\varphi$ であることと、$\models(\psi_1\land\cdots\land\psi_n)\to\varphi$ であることは同値である（$n=0$ なら左辺の前提は空、右辺は $\varphi$ とする）。

充足の定義を 1 段ずつ読む

1：充足関係の定義により、各 $\mathcal M$、$s$ で $\mathcal M\models\lnot\varphi[s]$ は $\mathcal M\models\varphi[s]$ でないことと同値である。したがって「すべての $\mathcal M,s$ で $\varphi$ が充足される」ことは「$\lnot\varphi$ を充足する $\mathcal M,s$ が存在しない」ことと同値である。
2：各 $\mathcal M$、$s$ で、$(\psi_1\land\cdots\land\psi_n)\to\varphi$ が充足されることは、「$\psi_1,\dots,\psi_n$ がすべて充足されるなら $\varphi$ も充足される」ことと同値である（$\land$ と $\to$ の充足条件）。これがすべての $\mathcal M,s$ で成り立つことが左辺の定義である。$\square$

1 により、妥当性の判定と充足可能性の判定は互いに移り合う。自動証明の多くの手法が「$\varphi$ を示す代わりに $\lnot\varphi$ が充足不能であることを示す」形をとるのはこのためである。2 とコンパクト性定理(一階論理) の記事の系「帰結の有限性」を合わせると、文の集合 $\Gamma$ からの帰結 $\Gamma\models\varphi$ も、ある有限個の $\psi_1,\dots,\psi_n\in\Gamma$ についての 1 つの文の妥当性に帰着する。

恒真式の代入例

命題論理の恒真式の命題変数に一階の論理式を代入すると、妥当な論理式が得られる。命題論理の論理式・付値・恒真式は命題論理の記事の定義「論理式」「付値と真理値」「恒真式・充足可能性・論理的帰結」による。

恒真式の代入例は妥当

$\theta$ を命題変数 $p_1,\dots,p_n$ だけを含む命題論理の論理式、$\psi_1,\dots,\psi_n$ を一階の論理式とし、$\theta$ の各 $p_i$ を $\psi_i$ に置き換えた一階の論理式を $\theta^{*}$ とする。$\theta$ が恒真式ならば、$\theta^{*}$ は妥当である。

構造と割り当てから付値を作る

$\mathcal M$、$s$ を任意にとり、付値 $v$ を「$v(p_i)=\mathrm T\iff\mathcal M\models\psi_i[s]$」（$1\le i\le n$。ほかの命題変数の値は任意）で定める。$\theta$ の部分論理式 $\eta$ と、それに対応する $\theta^{*}$ の部分論理式 $\eta^{*}$ について
$$ \mathcal M\models\eta^{*}[s]\iff v(\eta)=\mathrm T $$
を、$\eta$ の組み立てに沿った帰納法で示す。$\eta=p_i$ なら $v$ の定義そのものである。$\eta=\lnot\eta_1$ なら $\eta^{*}=\lnot\eta_1^{*}$ であり、左辺は $\mathcal M\models\eta_1^{*}[s]$ でないこと、右辺は $v(\eta_1)=\mathrm F$ であることなので、帰納法の仮定から同値である。$\eta=(\eta_1\ast\eta_2)$（$\ast$ は $\land,\lor,\to$）の場合も、一階の充足関係の $\ast$ の条件と付値の $\ast$ の規則が同じ形なので、帰納法の仮定から従う。
$\eta=\theta$ とすると、$\theta$ は恒真式なので $v(\theta)=\mathrm T$、よって $\mathcal M\models\theta^{*}[s]$ である。$\mathcal M,s$ は任意なので $\theta^{*}$ は妥当である。$\square$

たとえば $\theta=p_1\to p_1$ から $\forall x\,R(x,x)\to\forall x\,R(x,x)$ が、$\theta=p_1\lor\lnot p_1$（排中律）から $\exists x\,P(x)\lor\lnot\exists x\,P(x)$ が、それぞれ妥当と分かる。逆は成り立たない。

反例：恒真式の代入例でない妥当な論理式

ex-logical-validity-examples の 1 の $\forall x\,P(x)\to P(c)$ は妥当だが、どの恒真式の代入例でもない。$\theta^{*}=\forall x\,P(x)\to P(c)$ となる $\theta$ と $\psi_i$ があったとする。$\theta$ が命題変数 $p_i$ なら $\psi_i$ がこの式全体で、$p_i$ は恒真式でない。そうでなければ、命題論理の記事の定理「一意読み取り」と論理式の記事の定理「一意読み取り」により、$\theta$ は $\theta_1\to\theta_2$ の形で $\theta_1^{*}=\forall x\,P(x)$、$\theta_2^{*}=P(c)$ である。$\forall x\,P(x)$ と $P(c)$ は結合子で始まらないので、$\theta_1,\theta_2$ は命題変数 $p_i,p_j$ で $\psi_i=\forall x\,P(x)$、$\psi_j=P(c)$ である。$\psi_i\ne\psi_j$ なので $i\ne j$ であり、$p_i\to p_j$ は恒真式でない（$p_i$ を $\mathrm T$、$p_j$ を $\mathrm F$ にすればよい）。満たす性質は「妥当」、満たさない性質は「恒真式の代入例」であり、thm-logical-validity-tautology-instance の逆が成り立たないことを示す。量化記号の意味まで使って初めて妥当と分かる論理式がある。

「恒真」「トートロジー」という語を、命題論理の恒真式だけでなく一階の妥当な論理式にも使う文献がある。たとえば Bil03 は一階の論理式がすべての構造で真であることを tautology と呼んでいる（Definition 6.7、p. 38）。本記事では、命題論理の概念を恒真式（命題論理の記事の定義「恒真式・充足可能性・論理的帰結」）、一階の概念を妥当と呼び分ける。

1 項関係記号だけの文

妥当性の定義はすべての構造を相手にするので、一般には有限個の構造を調べて判定することはできない。ところが、言語の記号を 1 項の関係記号だけに制限すると、調べる構造を有限個にできる。

1 項関係記号の文は小さい構造で判定できる

$L$ を、1 項関係記号 $P_1,\dots,P_k$ だけからなる言語（定数記号・関数記号・2 項以上の関係記号をもたない）とし、等号 $=$ を含まない $L$ の文 $\varphi$ を考える。$\varphi$ が妥当であることと、元の個数が $2^k$ 以下のすべての $L$ 構造で $\varphi$ が真であることは同値である。

同じ性質をもつ元を 1 つにまとめる

妥当ならすべての構造で真なので、$\Rightarrow$ は明らかである。$\Leftarrow$ の対偶を示す。$\varphi$ が妥当でないとし、$\mathcal M\not\models\varphi$ となる $L$ 構造 $\mathcal M$ をとる。
段 1（まとめた構造）。$a,b\in M$ について、「すべての $i$ で $a\in P_i^{\mathcal M}\iff b\in P_i^{\mathcal M}$」のとき $a\sim b$ と定める。これは同値関係である。商集合 $N:=M/{\sim}$、商写像 $\pi\colon M\to N$ をとり、$P_i^{\mathcal N}:=\{\pi(a)\mid a\in P_i^{\mathcal M}\}$ とおいて $L$ 構造 $\mathcal N$ を作る。$\sim$ の定義から、すべての $a\in M$ と $i$ について
$$ a\in P_i^{\mathcal M}\iff\pi(a)\in P_i^{\mathcal N} $$
である（$\pi(a)=\pi(b)$、$b\in P_i^{\mathcal M}$ なら $a\sim b$ より $a\in P_i^{\mathcal M}$）。写像 $\pi(a)\mapsto(a\in P_1^{\mathcal M},\dots,a\in P_k^{\mathcal M})$ の真偽の組は代表元によらず、異なる同値類を異なる組に写すので、$N$ から $\{\mathrm T,\mathrm F\}^k$ への単射である。よって $\lvert N\rvert\le2^k$ であり、$M\ne\emptyset$ なので $N\ne\emptyset$ である。
段 2（充足が保たれる）。$L$ の等号を含まないすべての論理式 $\psi$ とすべての割り当て $s$ について
$$ \mathcal M\models\psi[s]\iff\mathcal N\models\psi[\pi\circ s] $$
を、$\psi$ に関する帰納法で示す。$L$ の項は変数だけなので、原子論理式は $P_i(x)$ の形であり、$\mathcal M\models P_i(x)[s]\iff s(x)\in P_i^{\mathcal M}\iff\pi(s(x))\in P_i^{\mathcal N}\iff\mathcal N\models P_i(x)[\pi\circ s]$ である。結合子の場合は帰納法の仮定と充足の定義から従う。$\psi=\forall x\,\chi$ の場合、各 $a\in M$ について $\pi\circ s_x^a=(\pi\circ s)_x^{\pi(a)}$ なので、帰納法の仮定により
$$ \mathcal M\models\forall x\,\chi[s]\iff\text{すべての }a\in M\text{ で }\mathcal N\models\chi[(\pi\circ s)_x^{\pi(a)}]. $$
$\pi$ は全射なので、$a$ が $M$ を動くとき $\pi(a)$ は $N$ 全体を動き、右辺は $\mathcal N\models\forall x\,\chi[\pi\circ s]$ と同値である。$\exists x\,\chi$ も同様である。
段 3。$\varphi$ は文で $\mathcal M\not\models\varphi$ なので、段 2 により $\mathcal N\not\models\varphi$ である。$\mathcal N$ は元の個数が $2^k$ 以下の構造なので、主張の対偶が示された。$\square$

段 2 は一階述語論理の記事の定理「同型補題」の証明と同じ形をしているが、$\pi$ は単射でない。同型補題の証明で単射性を使うのは等号の場合だけであり、ここでは等号を含まない論理式だけを扱うので単射性が要らない。等号を許すと、段 2 は成り立たなくなる。

反例：等号を含む文

$k=0$（関係記号なし）の言語で、等号を使った文 $\forall x\,\forall y\,(x=y)$ を考える。$2^0=1$ 元の構造ではこの文は真だが、2 元の構造では偽なので妥当でない。満たす性質は「$2^k$ 元以下のすべての構造で真」、満たさない性質は「妥当」であり、thm-logical-validity-monadic の「等号を含まない」という仮定は外せない。証明の段 2 では、2 元の構造を 1 元にまとめると $x=y$ の真偽が変わってしまう。

反例：2 項関係記号を含む文

2 項関係記号 $R$ の言語で、次の 3 つの文の連言を $\chi$ とし、$\tau:=\lnot\chi$ とおく。
$$ \forall x\,\lnot R(x,x),\qquad\forall x\,\forall y\,\forall z\,(R(x,y)\land R(y,z)\to R(x,z)),\qquad\forall x\,\exists y\,R(x,y). $$
$\tau$ はすべての有限構造で真である。有限構造 $\mathcal M$ で $\chi$ が真だとすると、3 つ目の文から $R^{\mathcal M}(a_0,a_1)$、$R^{\mathcal M}(a_1,a_2)$、… と続く列 $a_0,a_1,a_2,\dots$ がとれる（$M\ne\emptyset$ から $a_0$ をとる）。$M$ は有限なので $a_i=a_j$（$i< j$）となる番号があり、2 つ目の文（推移性）を繰り返し使うと $R^{\mathcal M}(a_i,a_j)$、すなわち $R^{\mathcal M}(a_i,a_i)$ となって 1 つ目の文に反する。一方、$(\mathbb N,<)$ では $\chi$ が真なので $\tau$ は偽であり、$\tau$ は妥当でない。
満たす性質は「すべての有限構造で真」、満たさない性質は「妥当」である。したがって、2 項関係記号を 1 つでも許すと、thm-logical-validity-monadic のような「決まった大きさ以下の構造を調べれば足りる」という判定は、大きさをいくら大きくしても成り立たない。

thm-logical-validity-monadic から、1 項関係記号だけの等号を含まない文については、妥当かどうかを判定する機械的な手順が得られる。一階述語論理の記事の定理「同型補題」により、台集合を $\{1,\dots,m\}$（$1\le m\le2^k$）とする構造だけを調べればよく、その個数は有限である（各 $P_i$ の解釈は $\{1,\dots,m\}$ の部分集合）。有限構造で文が真かどうかは、量化記号が有限集合を走るので、充足関係の定義に沿った有限回の計算で決まる。

判定可能性

妥当性の判定と列挙

一般の一階の文については、次の 3 つが知られている。この記事ではどれも証明しない。

妥当な文を 1 つずつ漏れなく書き出す機械的な手順がある。文が妥当なら有限時間で「妥当」と答え、妥当でなければ止まらない手順があると言い換えてもよい（Zac25 Theorem 15.18、p. 330）。これは、健全かつ完全な証明体系があり（一階論理の証明体系、Gödelの完全性定理）、導出を 1 つずつ並べて検査できることから従う。
任意の文が妥当かどうかを常に有限時間で正しく判定する手順は存在しない（Zac25 Theorem 15.16、p. 329）。prop-logical-validity-duality の 1 により、充足可能性も判定できない（同書 Corollary 15.17、p. 329）。
文が有限のモデルをもつかどうかも判定できない（Trakhtenbrot の定理、Zac25 Theorem 15.21、p. 334）。そのため、「すべての有限構造で真」を導出可能性と一致させる健全かつ完全な証明体系は存在しない（同書 Corollary 15.22、p. 334）。
2 は、命題論理の恒真式が真理値表で判定できること、1 項関係記号だけの文が thm-logical-validity-monadic で判定できることと対照的である。3 は、有限構造だけに制限しても判定が易しくならないことを示す。ex-logical-validity-finite-not-valid の $\tau$ は、「すべての有限構造で真」と「妥当」が異なることの具体例である。

証明可能性との一致

妥当性は意味の側の概念であり、証明体系で前提なしに導出できることは記号の側の概念である。健全な証明体系で導出できる論理式は妥当であり（一階論理の証明体系の記事の定理「健全性定理」）、完全な証明体系では妥当な文はすべて導出できる（Gödelの完全性定理）。prop-logical-validity-closure により、自由変数をもつ論理式の妥当性はその全称閉包の妥当性に帰着する。記号の側でも、一階論理の証明体系の記事の体系 $\mathbf H$ では、$\forall x\,\varphi\to\varphi$ が公理 (A4) の実例（$t:=x$）であることと同記事の定理「汎化定理」により、$\varphi$ が導出できることと $\forall x\,\varphi$ が導出できることは同値である。したがって、この一致は自由変数をもつ論理式にも広がる。こうして一階論理では、「論理だけで正しい」ことの意味による定式化（妥当性）と、記号の操作による定式化（証明可能性）が一致する。