しますか $\phi\vDash\bot$ それを意味する $\vDash\phi\to\bot$ もし $\phi$ 自由変数を持つ式は何ですか？
この質問はの続編です https://math.stackexchange.com/q/3797528/75923 私が同じことを尋ねたところ $\vDash$ と取り換える $\vdash$。
その質問に対して受け取ったコメントに触発されて、構文からセマンティクスに切り替えました。
しましょう $\mathcal{L}$ 一階述語である。
しましょう $\phi$ を示す $\mathcal L$-少なくとも1つの自由変数を持つ式。
純粋に便宜上、自由変数が1つだけある場合のみを見てみましょう。 $x$。
私の理解が大丈夫なら：
$\phi\vDash\bot$すべての場合 $\mathcal L$-構造 $\mathfrak{A}$いくつかの要素があります$a$ そのドメインで $\phi\left[a\right]$ で偽です $\mathfrak{A}$。これは、その状況でのみ$\mathcal L$-構造 $\mathfrak A$ を満たすものが存在する $\mathfrak A\vDash\phi$。
$\vDash\phi\to\bot$すべてのiff $\mathcal L$-構造 $\mathfrak{A}$そしてすべての要素$a$ そのドメインステートメントで $\phi\left[a\right]$ で偽です $\mathfrak{A}$。これはその状況でのみ$\mathfrak A\vDash\phi\to\bot$ すべてのための $\mathcal L$-構造 $\mathfrak A$。
残念ながら、それは明らかではありません $\phi\vDash\bot$ ことを意味します $\vDash\phi\to\bot$ それが本当かどうかさえ疑問に思います。
あなたはまっすぐに間違った理解を設定したり、死角（もしあれば）を取り除いてくれませんか？
前もって感謝します。
私の理解がどこにあるかを明確にするための補遺 $\phi\vDash\bot$ から来た。
- $\mathfrak A\vDash\phi\iff\forall a\in\mathsf{dom}\mathfrak A[\mathfrak A\vDash\phi[a]]$ （1.7.9リアリー）
- $\phi\vDash\psi\iff\forall\mathfrak A[\mathfrak A\vDash\phi\implies\mathfrak A\vDash\psi]$ （1.9.1リアリー）
取る $\bot$ ために $\psi$ 最後の箇条書きでは、次のようになります。
$\phi\vDash\bot\iff\forall\mathfrak A[\mathfrak A\nvDash\phi]$
次に、到着した最初の弾丸を適用します。
$\phi\vDash\bot\iff\forall\mathfrak A[\exists a\in\mathsf{dom}\mathfrak A[\mathfrak A\nvDash\phi[a]]]$
回答
私たちは確かに持っています $$\phi\models\perp\quad\iff\quad\models\phi\rightarrow\perp.$$
あなたの理解 $\phi\models\perp$ 正しくありません： $\phi\models\perp$ すべての構造のiff $\mathcal{M}$、を作るすべての変数の割り当て$\phi$ 真になります $\perp$本当。割り当てができないので$\perp$本当、これは構造がないことを意味します$\mathcal{M}$ および変数代入の作成 $\phi$ true-つまり、満足のいくタプルを持つ構造はありません $\phi$。
そしてこれは明らかに $\models\phi\rightarrow\perp$ （これのあなたの分析は正しいです）。
編集：具体的には、問題はあなたの定義が $\phi\models\psi$変数-許可コンテキストで間違っています：「評価額を超える定量化は、」起こることがある外$\models$-右側の部分。
正しい定義は $$\forall \mathfrak{A}, a\in\mathfrak{A}(\mathfrak{A}\models\phi[a]\implies\mathfrak{A}\models\psi[a]).$$ 一方、あなたが定義した関係-私はこれを「$\models_?$「わかりやすくするために、次のようになります。 $$\forall\mathfrak{A}[\forall a\in\mathfrak{A}(\mathfrak{A}\models\phi[a])\implies \forall a\in\mathfrak{A}(\mathfrak{A}\models\psi[a])].$$ これらの違いを確認するには、単一の単項関係記号で構成される言語で次の式を検討してください。 $U$：
$\phi(x):\quad$ 場合 $U$ ドメインの空でない適切なサブセットを記述し、次に $U(x)$。
あなたは私たちが持っていることを確認することができます $\phi(x)\models_?\phi(y)$、明らかに保持すべきではありません。
そして、これはOPの明らかな不一致を説明しています。正しい定義を使用すると、$\phi\models\perp$ iff $$\forall \mathfrak{A},a\in\mathfrak{A}(\mathfrak{A}\models\phi[a]\implies \mathfrak{A}\models\perp)$$ iff $$\forall \mathfrak{A}\color{red}{\forall} a\in\mathfrak{A}(\neg\mathfrak{A}\models\phi[a])$$ 望んだ通りに。