Lo fa $\phi\vDash\bot$ implica quello $\vDash\phi\to\bot$ Se $\phi$ è una formula che ha variabili libere?
Questa domanda è un sequel di questa in cui ho chiesto la stessa cosa$\vDash$ sostituito da $\vdash$.
Ispirato dai commenti ricevuti su quella domanda, sono passato dalla sintassi alla semantica.
Permettere $\mathcal{L}$ essere una lingua del primo ordine.
Permettere $\phi$ denotano a $\mathcal L$-formula che ha almeno una variabile libera.
Per comodità, esaminiamo solo il caso in cui ha esattamente una variabile libera $x$.
Se la mia comprensione va bene allora:
$\phi\vDash\bot$iff ogni $\mathcal L$-struttura $\mathfrak{A}$ ha qualche elemento$a$ nel suo dominio tale che $\phi\left[a\right]$ è falso in $\mathfrak{A}$. Questo perché solo in quella situazione no$\mathcal L$-struttura $\mathfrak A$ esiste che soddisfa $\mathfrak A\vDash\phi$.
$\vDash\phi\to\bot$iff per ogni $\mathcal L$-struttura $\mathfrak{A}$ e ogni elemento$a$ nella sua dichiarazione di dominio $\phi\left[a\right]$ è falso in $\mathfrak{A}$. Questo perché solo in quella situazione$\mathfrak A\vDash\phi\to\bot$ per ogni $\mathcal L$-struttura $\mathfrak A$.
Purtroppo non è chiaro questo $\phi\vDash\bot$ implica che $\vDash\phi\to\bot$ e mi chiedo persino se sia vero.
Potresti mettere in chiaro intese sbagliate o togliere un punto cieco (se c'è) per favore?
Grazie in anticipo.
Addendum per chiarire dove la mia comprensione $\phi\vDash\bot$ viene da.
- $\mathfrak A\vDash\phi\iff\forall a\in\mathsf{dom}\mathfrak A[\mathfrak A\vDash\phi[a]]$ (1.7.9 Leary)
- $\phi\vDash\psi\iff\forall\mathfrak A[\mathfrak A\vDash\phi\implies\mathfrak A\vDash\psi]$ (1.9.1 Leary)
Prendendo $\bot$ per $\psi$ nell'ultimo punto otteniamo:
$\phi\vDash\bot\iff\forall\mathfrak A[\mathfrak A\nvDash\phi]$
Quindi applicando il primo punto si arriva a:
$\phi\vDash\bot\iff\forall\mathfrak A[\exists a\in\mathsf{dom}\mathfrak A[\mathfrak A\nvDash\phi[a]]]$
Risposte
Lo abbiamo davvero $$\phi\models\perp\quad\iff\quad\models\phi\rightarrow\perp.$$
La tua comprensione di $\phi\models\perp$ non è corretto: abbiamo $\phi\models\perp$ iff per ogni struttura $\mathcal{M}$, ogni assegnazione di variabile che fa$\phi$ vere marche $\perp$vero. Dal momento che nessun incarico può fare$\perp$vero, questo significa che non c'è struttura$\mathcal{M}$ e creazione di assegnazioni variabili $\phi$ true - o in altre parole, nessuna struttura ha una tupla soddisfacente $\phi$.
E questo chiaramente coincide con $\models\phi\rightarrow\perp$ (la tua analisi di questo è corretta).
EDIT: In particolare, il problema è che la tua definizione di $\phi\models\psi$nel contesto delle variabili consentite non è corretto: la "quantificazione sulle valutazioni" deve avvenire al di fuori del$\models$-parte sul lato destro.
La definizione giusta è $$\forall \mathfrak{A}, a\in\mathfrak{A}(\mathfrak{A}\models\phi[a]\implies\mathfrak{A}\models\psi[a]).$$ D'altra parte, la relazione che hai definito, che chiamerò "$\models_?$"per chiarezza - è equivalente a quanto segue: $$\forall\mathfrak{A}[\forall a\in\mathfrak{A}(\mathfrak{A}\models\phi[a])\implies \forall a\in\mathfrak{A}(\mathfrak{A}\models\psi[a])].$$ Per vedere la differenza tra questi, si consideri la seguente formula nel linguaggio costituito da un unico simbolo di relazione unario $U$:
$\phi(x):\quad$ Se $U$ descrive un sottoinsieme proprio non vuoto del dominio, quindi $U(x)$.
Puoi controllare che abbiamo $\phi(x)\models_?\phi(y)$, che chiaramente non dovrebbe reggere.
E questo spiega l'apparente discrepanza nel PO. Usando la giusta definizione, abbiamo$\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])$$ come desiderato.