\(\def\tauequ{\mathbin{\vDash\style{display:
inline-block; transform: scaleX(-1)}{\vDash}}}\) \(\def\Dashv{\mathbin{\style{display: inline-block;
transform: scaleX(-1)}{\vDash}}}\) \(\def\DEF{\sf{D\scriptsize EF}.\quad}\)
\(\def\DEFi{\sf{D\scriptsize
EF}^*.\quad}\) \(\def\DEFn{\sf{D\scriptsize EF}_*.\quad}\)
\(\def\DEFin{\sf{D\scriptsize
EF}^*_*.\quad}\) \(\def\llbracket{\unicode{x27E6}}\) \(\def\rrbracket{\unicode{x27E7}}\) \(\def\PROOF{\sf{P\scriptsize
ROOF}.\quad}\)
点击这里进入AMIL目录
Problem 1
Show that (a) \(\Gamma;\alpha\vDash\varphi\) iff \(\Gamma\vDash(\alpha\rightarrow\varphi)\);
and (b) \(\varphi\tauequ\psi\) iff
\(\vDash(\varphi\leftrightarrow\psi)\).
\(\PROOF\)
(a) \[
\begin{array}{lcll}
\Gamma;\alpha\vDash\varphi & \Leftrightarrow &
\forall\psi\forall{\frak
A}\forall{s}(\psi\in\Gamma;\alpha\land\vDash_{\frak
A}\psi[s]\rightarrow\vDash_{\frak A}\varphi[s]) &
(\text{ definition of }\href{/a55d499#LogicallyImply}{\text{logical
imply}}) \\
& \Leftrightarrow & \left\{\begin{array}{l}
\forall\psi\forall{\frak
A}\forall{s}(\psi\in\Gamma\land\vDash_{\frak
A}\psi[s]\land\nvDash_{\frak A}\alpha[s]\rightarrow\vDash_{\frak
A}\varphi[s]) \\
\forall{\frak A}\forall{s}(\vDash_{\frak
A}\alpha[s]\rightarrow\vDash_{\frak A}\varphi[s])
\end{array}
\right. \\
& \Leftrightarrow & \forall\psi\forall{\frak
A}\forall{s}(\psi\in\Gamma\land\vDash_{\frak
A}\psi[s]\rightarrow(\nvDash_{\frak A}\alpha[s]\lor\vDash_{\frak
A}\varphi[s]\lor(\vDash_{\frak A}\alpha[s]\land\vDash_{\frak
A}\varphi[s]))) \\
& \Leftrightarrow & \forall\psi\forall{\frak
A}\forall{s}(\psi\in\Gamma\land\vDash_{\frak
A}\psi[s]\rightarrow\vDash_{\frak A}(\alpha\rightarrow\varphi)[s])
& (\text{ definition of }
\href{/a55d499#SatisfyConditionalSymbol}{\vDash_{\frak
A}(\alpha\rightarrow\varphi)[s]}) \\
& \Leftrightarrow & \Gamma\vDash(\alpha\rightarrow\varphi) &
(\text{ definition of logical imply})
\end{array}
\]
(b) \[
\begin{array}{lcll}
\varphi\tauequ\psi & \Leftrightarrow &
\varphi\vDash\psi\land\psi\vDash\varphi \\
& \Leftrightarrow &
\vDash(\varphi\rightarrow\psi)\land\vDash(\psi\rightarrow\varphi) &
(\text{according to (a)}) \\
& \Leftrightarrow & \forall{\frak A}\forall{s}(\vDash_{\frak
A}(\varphi\rightarrow\psi)[s]\land\vDash_{\frak
A}(\psi\rightarrow\varphi)[s]) \\
& \Leftrightarrow & \forall{\frak A}\forall{s}(\vDash_{\frak
A}(\varphi\rightarrow\psi\land\psi\rightarrow\varphi)[s]) \\
& \Leftrightarrow & \vDash(\varphi\leftrightarrow\psi)
\end{array}
\]
点击这里进入AMIL目录