Problemas para entender as declarações usando consequência semântica, apesar de conhecer a definição
Eu sei que consequência semântica significa que todas as declarações à esquerda podem ser todas verdadeiras (são satisfatórias) se o lado direito for verdadeiro. Se o lado direito for falso, então as afirmações à esquerda não podem ser todas verdadeiras.
Algumas afirmações estão me causando problemas.
O primeiro: $$ [\{\Gamma, \phi \} \vDash \psi] \ \ iff \ \ [\{\Gamma\} \vDash (\phi \rightarrow \psi)] $$ Se eu começar com a esquerda do iff, todas as declarações fazem sentido.
O problema é quando eu começo com o lado direito do iff e $\Gamma$ é verdade, $\phi$ é falso, e $\psi$é verdade. Essa é uma declaração legítima, mas prova que toda a declaração está errada.
O segundo: $$ [\{\bot\} \vDash \psi] $$
$\psi$pode ser verdadeiro apesar do lado esquerdo ser falso. Achei que isso fosse impossível.
O terceiro:
$$ If \ [\{\Delta, \lnot \phi\} \vDash \bot]\ then \ [\{\Delta\} \vDash \phi] $$
E se $\Delta$ é insaciável e $\phi$ for verdade, a parte if é verdadeira e a parte then está errada.
Certamente, estou entendendo mal alguma coisa se continuar enfrentando esse problema.
Respostas
Eu sei que consequência semântica significa que todas as afirmações à esquerda podem ser todas verdadeiras (são satisfatórias) se o lado direito for verdadeiro.
Não, não é isso que significa. É exatamente o contrário: o lado direito é verdadeiro se todas as afirmações do lado esquerdo forem verdadeiras. Iow, a definição de consequência semântica é que sob qualquer interpretação dada, ou o RHS é verdadeiro ou pelo menos uma afirmação no LHS é falsa. Não é necessário que o LHS seja verdadeiro se o RHS for!
Talvez seja mais fácil ver pelo negativo: a única coisa que não deve acontecer é que todas as afirmações no LHS sejam verdadeiras, mas o RHS falso simultaneamente. Se, sob alguma interpretação, o RHS for verdadeiro, mas o LHS não, tudo bem. Isso significa, em particular, que se o LHS nunca pode ser simultaneamente verdadeiro (= é insatisfatório), então não pode haver tal contra-interpretação, e a consequência se mantém vagamente.
(Consulte também a nota sobre (insatisfação) no último parágrafo; seu uso aqui sugere um mal-entendido sobre o que isso significa.)
$$ [\{\Gamma, \phi \} \vDash \psi] \ \ iff \ \ [\{\Gamma\} \vDash (\phi \rightarrow \psi)] $$ Se eu começar com a esquerda do iff, todas as declarações fazem sentido.
O problema é quando eu começo com o lado direito do iff e $\Gamma$ é verdade, $\phi$ é falso, e $\psi$é verdade. Essa é uma declaração legítima, mas prova que toda a declaração está errada.
Você está interpretando mal a estrutura da declaração. Você está olhando para uma atribuição concreta de valores de verdade e tenta descobrir, a partir dessa única interpretação, se as consequências semânticas à esquerda e à direita se mantêm. Mas não é isso que diz: a declaração se traduz em
[Sob todas as interpretações, qualquer uma das declarações em $\Gamma, \phi$ é falso ou $\psi$é verdadeiro]
iff
[Em todas as interpretações, qualquer uma das declarações em$\Gamma$ é falso ou $\phi \to \psi$ é verdade].
Ou seja, primeiro precisamos examinar todas as interpretações para determinar se as consequências semânticas são válidas e, em seguida, avaliar o "se e somente se". Olhando para apenas um caso onde$\Gamma$ é verdade, $\phi$ falso e $\psi$ true não nos permite tirar uma conclusão sobre se algum dos lados do "iff" é válido.
O segundo: $$ [\{\bot\} \vDash \psi] $$
$\psi$pode ser verdadeiro apesar do lado esquerdo ser falso. Achei que isso fosse impossível.
Veja acima: é o contrário; só é necessário que não seja possível que o RHS seja falso, apesar de o LHS ser verdadeiro. E isso nunca pode ser o caso se o LHS não puder se tornar verdadeiro sob qualquer interpretação em primeiro lugar, que é o caso para$\bot$, então a consequência permanece vazia.
$$ If \ [\{\Delta, \lnot \phi\} \vDash \bot]\ then \ [\{\Delta\} \vDash \phi] $$
E se $\Delta$ é insaciável e $\phi$ for verdade, a parte if é verdadeira e a parte then está errada.
Você pode parar de ler depois de "Se $\Delta$ é insatisfatório ": Então, nenhum dos LHSs pode se tornar verdadeiro, então ambas as consequências permanecem vazias, e o" se então "é satisfeito.
E só para esclarecer a terminologia: "$\Delta$ satisfazível / insatisfatório "significa que é possível / impossível que todas as suas declarações se tornem simultaneamente verdadeiras sob qualquer interpretação, ou seja, $\Delta$não é contraditório / contraditório. Se for apenas o caso em uma interpretação particular que todas / não todas as declarações em$\Delta$ são verdade, então não dizemos isso $\Delta$é satisfatório / insatisfatório, mas apenas verdadeiro / falso. O mesmo vale para fórmulas simples:$\phi$ é verdadeiro / falso em uma interpretação particular e satisfatório / insatisfatório se houver pelo menos uma / nenhuma interpretação sob a qual seja verdadeiro.
Um modelo de $\Gamma$ no qual $\phi$ é falso não diz nada sobre a declaração $\{\Gamma,\phi\}\vDash\psi$: essa declaração apenas diz que$\psi$ é verdade em todos os modelos de $\Gamma$ e $\phi$, que é realmente o caso se $\phi\to\psi$ é verdade em todos os modelos de $\Gamma$.