Conseguenza semantica (doppio tornello) in LaTeX (\models)

Dove si usa

Doppio tornello: conseguenza semantica o soddisfacibilità, cioè verità in ogni modello.

\mathcal{M} \models \varphi dice che la struttura M soddisfa la formula \varphi, e \Gamma \models \varphi dice che ogni modello di \Gamma soddisfa \varphi. Si contrappone a \vdash, che è la derivabilità sintattica. La sua negazione è \not\models oppure il glifo dedicato \nvDash. Il simile \vDash ha proporzioni leggermente diverse ed è usato in alcune logiche insieme a \Vdash per il forcing in teoria degli insiemi. In quanto relazione, riceve spazio su entrambi i lati. Nel model checking si scrive s \models \phi per uno stato che soddisfa una formula temporale.

Esempio minimo compilabile

Incollalo in un file .tex vuoto e compilalo con pdfLaTeX, XeLaTeX o LuaLaTeX.

\documentclass{article}
\begin{document}
Models: $\models$

\[ \Gamma \models \varphi \iff \Gamma \vdash \varphi \]
\end{document}

Simboli correlati

• Simbolo “quindi”\therefore
• Simbolo di deduzione (tornello)\vdash
• Simbolo “poiché”\because
• Equivalenza (se e solo se)\iff
• Contraddizione (falsum, bottom)\bot
• Implicazione\implies

Domande frequenti

Come si scrive Conseguenza semantica (doppio tornello) in LaTeX?

Scrivi \models in modalità matematica, per esempio $\Gamma \models \varphi \iff \Gamma \vdash \varphi$. Funziona in LaTeX standard senza caricare alcun pacchetto.

Quale pacchetto serve per \models?

Nessuno. \models fa parte di LaTeX standard, quindi compila con la sola classe del documento nel preambolo.

Posso usare \models in modalità testo o solo in modalità matematica?

Solo in modalità matematica. Fuori da $...$ LaTeX si ferma con "Missing $ inserted", quindi nel testo scrivi $\models$. Se ti serve solo il glifo nel testo, incolla invece il carattere Unicode ⊨ (con XeLaTeX o LuaLaTeX e un font che lo contenga).