1
$\begingroup$

If a finite set of well-formed formulas appears as the right argument to $\models$, how is it usually interpreted? Is it usually interpreted with an implicit disjunction like a sequent, or an implicit conjunction?

This question references this book, which the following definition

Suppose that $\Delta$ and $\Gamma$ are $\mathcal{L}$-formulas. We will say that $\Delta$ logically implies $\Gamma$ and write $\Delta \models \Gamma$ if for every $\mathcal{L}$-structure $\mathfrak{A}$, if $\mathfrak{A} \models \Delta$, then $\mathfrak{A} \models \Gamma$.

I'll use the equivalent statement below for this question, which changes the notation and language slightly.

$$ \textbf{(I)}\;\;\; \Delta \models \Gamma \iff \text{for every $L$-structure $M$ where $M \models \Delta$, $M \models \Gamma$ holds} $$

So, $\Delta \vdash \Gamma$ as a sequent, is equivalent to $\bigwedge \Delta \vdash \bigvee \Gamma$. By analogy, I'll assume for a second that $\Delta \models \Gamma$ is equivalent to $\bigwedge \Delta \models \bigvee \Gamma $.

$$ \textbf{(II)} \;\small\textbf{BAD} \;\; \bigwedge \Delta \models \bigvee \Gamma \iff \text{for every $L$-structure $M$ where $M \models \bigvee \Delta$, $M \models \bigvee \Gamma$ holds } $$

(II) clearly isn't true. We're quantifying over all structures that satisfy any statement in $\Delta$ instead of all of them.

This makes me think that $\Delta \models \Gamma$ is meant to be equivalent to $\bigwedge \Delta \models \bigwedge \Gamma$. Is this how $\models$ is normally used?

$\endgroup$
5
  • 2
    $\begingroup$ yes, that is correct :) $\endgroup$
    – Atticus Stonestrom
    Mar 13, 2021 at 3:47
  • $\begingroup$ @AtticusStonestrom, is $\models$ always/nearly-always used this way or is the right argument ever implicitly treated as a disjunction? Granted, treating the right argument as a disjunction is less useful outside of a sequent-calculus-like setting. $\endgroup$
    – Greg Nisbet
    Mar 13, 2021 at 4:33
  • 1
    $\begingroup$ I have never seen the argument on the right of the $\models$ symbol treated as a disjunction, but of course that doesn't mean it's impossible! however it would certainly be highly non-standard notation (trivia: the $\models$ symbol is also called a "double turnstile") $\endgroup$
    – Atticus Stonestrom
    Mar 13, 2021 at 5:55
  • 1
    $\begingroup$ one way of thinking about the notation $\Delta\models\Gamma$ is as shorthand for "$\Delta\models\gamma$ for every $\gamma\in\Gamma$". for instance, in model theory one often sees this kind of notation used when dealing with types, if you have learned about those. eg if $p(\overline{v})$ and $q(\overline{v})$ are partial types, one might use the notation $p\models q$, modulo some theory $T$, to mean "for every $\varphi\in q$, there are some $\psi_1,\dots,\psi_n\in p$ such that $$T\models\forall\overline{v}\left[\bigwedge_{i\in[n]}\psi_i(\overline{v})\right]\to\varphi(\overline{v})$$ $\endgroup$
    – Atticus Stonestrom
    Mar 13, 2021 at 6:21
  • 1
    $\begingroup$ If you go back a couple of pages in the book, you will find it does give a definition of the notation which agrees with the suggestion made by @AtticusStonestrom. For sequents, with multiple succedents, it is usual to read the set of succedents as a disjunction, but that is not the convention here. $\endgroup$
    – Rob Arthan
    Mar 13, 2021 at 15:48

1 Answer 1

Reset to default
3
$\begingroup$

I have literally never seen the expression "$\Gamma\models\Delta$" interpreted as "Every structure satisfying each sentence in $\Gamma$ satisfies some sentence in $\Delta$." Now granted, logicians (of which I am one!) are truly terrible about notation and terminology so it is totally possible that somebody somewhere did do that, but in all the logic texts I've read and presentations I've attended I've only ever seen the "conjunct-conjunct" use.

(An ill-informed historical gloss: remember that the "conjunct-disjunct" style of sequents was introduced for its technical value: it provides a very convenient framework for analyzing deductions. But this is very specific to the details of the proof apparatus; there isn't really a similar semantic counterpart. So nothing motivated a "conjunct-disjunct" version of satisfaction.)

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .