正式に証明または反証する: $(\forall x F) \lor G \vDash \forall x (F \lor G)$
このステートメントが偽または真であることを正式に証明したいと思います。私はそれが間違っていると思います。$G$ 変数を含めることができます $x$ 束縛されておらず、いくつかの解釈のために $\mathcal A$、 $G$ 一部の人に当てはまる可能性があります $x$ 一方 $(\forall x G)$ 偽であり、 $(\forall x F)$は誤りです。そう$(\forall x F) \lor G$ trueと評価されますが、 $\forall x (F \lor G)$ falseと評価されるため、 $(\forall x F) \lor G \nvDash \forall x (F \lor G)$ 同じ解釈のために $\mathcal A$。
しかし、私の推論が正しいかどうかは疑問であり、これを正式に証明する方法がわかりません。
回答
システムで、自由変数を含む数式に代入関数に関連する真理値を割り当てることができると仮定すると、次のような疑いがあります。 $G$ あるオブジェクトには当てはまりますが、別のオブジェクトには当てはまりません。
仮定します $F$ 自由変数があり、 $F(x)$、および $G$ 自由変数があり、 $G(x)$。カウンターモデルを検討してください$\mathcal{M} = \langle D, \mathcal{I} \rangle$ と $D = \{a, b\}, \mathcal{I}(F) = \emptyset, \mathcal{I}(G) = \{a\}$ と代入機能 $v : x \mapsto a$。
その後、 $v(x) = a \in \mathcal{I}(G)$、私たちはそれを持っています $\mathcal{M}, v \vDash G(x)$、 そう $\mathcal{M}, v \vDash (\forall x F(x)) \lor G(x)$。
しかしそれ以来$b \not \in \mathcal{I}(F)$ そして $b \not \in \mathcal{I}(G)$、割り当てバリアントにも当てはまります $v'$ の $v$ と $v': x \mapsto b$ それ $\mathcal{M}, v' \not \vDash F(x) \lor G(x)$、したがって $\mathcal{M}, v \not \vDash \forall x (F(x) \lor G(x))$。
前提式は真であるが結論は真ではないような式のインスタンス、構造、および代入関数があるため、推論スキームは成り立たない。
声明の中で $(\forall x F) \vee G$、 $G$ の数量詞の範囲内ではありません $x$。つまり、これが「真」または「偽」と評価できる文である場合、$G$ 含めることはできません $x$。つまり、数量詞を置くと$x$ その前に $(\forall x)G$、結果は直感に反します-数量詞は効果がありません!
簡単な例として、 $G$ 「空は青い」かもしれません。 $(\forall x)G$ そうすれば「何があっても $x$ つまり、空は青い」ですが、空が青いかどうかは、どのオブジェクトに「$x$"、 そう $(\forall x)G$ 正確に真である $G$ です。
これについては、特定の人に何が起こるかを考えることをお勧めします $x$、 いう $a$。仮定$(\forall x F) \vee G$本当です。あなたはそれを示すことができますか$F(a) \vee G$本当ですか?もしそうなら、$a$ 任意に選ばれた、それはそれでなければなりません $(\forall x)(F \vee G)$ 本当です。