表示中 $\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle \implies \langle \exists y: P.y : Q.y \rangle $ 定理です。
フィッチのような自然演繹システムを使用した可能な証明は難しくありません。しかし、私はそれを方程式論理を使って証明したいと思います。このシステムは、DeMorganなどの命題論理の一般的な規則と、次のような本で使用される述語論理規則を使用します。
- 離散数学への論理的アプローチ(David Gries)。
- 完全な本はここで見つけることができます: https://link.springer.com/book/10.1007/978-1-4757-3837-7
- 503ページのルールのリスト。
- 1990年代のプログラミング(エドワードコーエン)。
私の証明は次のように始まります:
先行詞が成り立つと思います $$\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle$$ 到達しようとします $$\langle \exists x:: P.x \land Q.x \rangle$$
試みられた証拠:
$$ \begin{align*} & \langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle\\ \implies & \{\text{Instantiation } (\forall)\}\\ & P.a \land \langle \exists x:: Q.x \rangle \\ \equiv & \{\text{Distributivity of} \land \text{over} \exists \} \\ & \langle \exists x:: P.a \land Q.x \rangle \end{align*} $$
もちろん、証明は完全ではありません。この文脈でこの証明が可能かどうか誰かが知っていますか?
回答
論理的帰結の正式な証明を作成するときは、最初に直感的に推論するのに役立ちます。これは、作業中の部分的な証明が行き止まりにつながるかどうかを明らかにするのにも役立ちます。たとえば、部分的な証明は直感的に次のように読み取られます。
私は落ちる $x$ プロパティを持っている $P.x$ そしていくつかあります $x$ プロパティ付き $Q.x$、それからいくつかある必要があります $x$ プロパティ付き $P.x\land Q.x$:確かに、 $a$ 任意のオブジェクトである場合、プロパティがあることがわかります $P.a$。いくつかあるので$x$ プロパティ付き $Q.x$、いくつかあると結論付けることができます $x$ と $P.a\land Q.x$...しかし今何?
これは、最初に全称記号をインスタンス化するのがおそらく最善のアイデアではなく、存在記号をインスタンス化するのが最善のアイデアであったことを示しています。
私は落ちる $x$ プロパティを持っている $P.x$ そしていくつかあります $x$ プロパティ付き $Q.x$、それからいくつかある必要があります $x$ プロパティで $P.x\land Q.x$:確かに、プロパティを持つオブジェクトを言う $Q$ と呼ばれる $a$ (そのため $Q.a$)、それからすべて以来 $x$ プロパティを持っている $P.x$、そして特に $a$ プロパティが必要です $P.a$。これを次の事実と組み合わせる$a$ プロパティがあります $Q.a$、私たちはそれを結論付けることができます $a$ プロパティがあります $P.a\land Q.a$。特に、いくつかあります $x$ と $P.x\land Q.x$。
自然演繹を使用してこれを正式に書き出すと、次のようになります。
- $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle$ (含意イントロの仮定)
- $\langle \exists x :: Q.x\rangle$(接続詞エリム、1)
2.1$Q.a$(実存的エリムの仮定)
2.2$\langle \forall x :: P.x\rangle$(接続詞エリム、1)
2.3$P.a$(ユニバーサルエリム、2.2)
2.4$P.a\land Q.a$(論理積の導入、2.1、2.3)
2.5$\langle \exists x :: P.x\land Q.x\rangle$ (実存的イントロ、2.4) - $\langle \exists x :: P.x\land Q.x\rangle$ (実存的エリム、2、2.1-2.5)
そこから結論 $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle \implies \langle \exists x :: P.x\land Q.x\rangle$ 1-3の含意イントロによって。
この引数は、公理的引数を生成する方法をガイドします。この場合の主なトリックは、存在記号で引数全体をラップする方向に推論することによって、存在イントロが回避されることです。次に、存在記号の範囲内で、存在記号が存在しないかのように推論できます。
(先行) $\langle \forall x :: P.x\rangle\land\langle\exists x :: Q.x\rangle$
$\equiv$ $\langle \forall y :: P.y\rangle\land\langle\exists x :: Q.x\rangle$ (変数変換)
$\equiv$ $\langle \exists x :: \langle \forall y :: P.y\rangle \land Q.x\rangle$ (の分配性 $\land$ 以上 $\exists$; これはステートメント全体をでラップします$\exists$)
$\implies$ $\langle \exists x :: P.x \land Q.x \rangle$ (のインスタンス化 $\forall$ で $x$)
秘訣は、実在する証人に具体的にインスタンス化することです。
$${\langle\forall x::P.x\rangle\land\langle\exists x::Q.x\rangle\\\Downarrow~\\\langle\exists x:Q.x:P.x\rangle\land\langle\exists x::Q.x\rangle}$$