3
$\begingroup$

This question is merely about notation.

Let $\varphi(x)$ be a predicate, i.e. a formula of first order logic, written in a given language, and having exactly one free variable denoted by $x$. Let also $M$ be a model of a theory $T$ in the same language. I will write $\varphi$ for $\varphi^M$ etc, leaving the interpretation as understood.

Now, the set of elements of $M$ satisfying $\varphi(x)$ can of course be written as $$\{ x\in M \mid \varphi(x)\}.$$

But I kind of remember that there is some other notation, something like $[[\varphi]]$ (or, rather, \llbracket\varphi\rrbracket in LaTeX, which I can't seem to be able to visualize in my browser).

I had a look in the internet, and it seems that the double bracket notation is used for Boolean-valued models (of which I know nothing!), so that if $\mathbb B$ is a given Boolean algebra, under a certain interpretation we have $[[\varphi]]\in\mathbb{B}$, so that for example $$[[\varphi\wedge\psi]]=[[\varphi]]\wedge_{\mathbb{B}}[[\psi]]$$ $$[[\varphi\vee\psi]]=[[\varphi]]\vee_{\mathbb{B}}[[\psi]]$$ $$[[\lnot\varphi]]=\lnot_{\mathbb{B}}[[\varphi]]$$

and so on.

Since $2^M$ is indeed a Boolean algebra, it wouldn't seem strange to me. We would have $[[\varphi\wedge\psi]]=[[\varphi]]\cap[[\psi]]$, $[[\varphi\vee\psi]]=[[\varphi]]\cup[[\psi]]$, $[[\lnot\varphi]]=M\setminus[[\varphi]]$, and so forth.

Is the notation $[[\varphi]]$ for $\{ x\in M \mid \varphi(x)\}$ common? Is it indeed a special case of Boolean-valued models?

$\endgroup$
4
  • 1
    $\begingroup$ In computer science, e.g. denotational semantics, double brackets like that (often called "semantic brackets") are very common. With the connections between logic and computer science, it is natural for a computer scientist, to use similar notation for logic which is what I do personally. I would use $[\![\varphi]\!]$ to mean an $n$-ary relation (or more likely subobject...) where $n$ is at least the number of free variables of $\varphi$. Incidentally, one way to get these brackets in MathJax is [\![\varphi]\!]. $\endgroup$ Commented Oct 7, 2018 at 19:23
  • $\begingroup$ @Mauro ALLEGRANZA: I think the case of sentences would be the case in which the Boolean algebra is the set of truth values $2^{M^0}=\{0,1\}$. Does it make sense to you? - Derek Elkins: thank you. $\endgroup$
    – Qfwfq
    Commented Oct 7, 2018 at 19:50
  • $\begingroup$ I have also met this notation often. $\endgroup$
    – Berci
    Commented Oct 7, 2018 at 22:44
  • 1
    $\begingroup$ In model theory, the most common notation for $\{a\in M\mid M\models \varphi(a)\}$ is $\varphi(M)$. I typically write $[\varphi(x)]$ for the basic clopen set in the Stone space $S_x(T)$ defined by $\varphi(x)$. That is, $[\varphi(x)] = \{p\mid \varphi(x)\in p\}$, where $p$ ranges over complete types in the variable context $x$. $\endgroup$ Commented Oct 8, 2018 at 4:29

1 Answer 1

4
$\begingroup$

The use of semantic brackets is largely community-dependent. The places where I know that this notation appears most frequently are denotational semantics of programs in computer science, semantics of modal logic, categorical semantics and type theory. As notation, the semantic brackets originate from the paper "A Proof of the Independence of the Continuum Hypothesis" of Dana Scott in 1967, see The history of the use of $[\![\,.]\!]$-notation in natural language semantics by Brian Rabern. In the semantics of logic one typically finds two styles: the denotational style and the satisfaction style. The former is thereby closely related to Algebraic Semantics, while the latter more commonly found in Model Theory as mentioned by Alex Kruckman.

In algebraic semantics, one establishes a function from (well-formed) formulas into some algebraic structure that allows the evaluation of formulas. You gave an example yourself, where $[\![\,.]\!]$ is essentially a function from Boolean formulas into a Boolean algebra. Other notations that can be found are just regular letters (often bold-face) like $\mathbf{v}$ (for valuation). In this sense, the Boolean semantics are a special case.

Let me provide a few further examples where the denotational style together with the semantic brackets is used:

  • Semantics of the modal $\mu$-calulus
  • Topos semantics (although the forcing notation $\Vdash$ can be found frequently in this field in a result referred to as Kripke-Joyal semantics, see the presentation and this introduction by Thomas Streicher)
  • More generally: Categorical logic. John Bell uses, for example, in his introductory text the semantic brackets, but the type-setting in the online version does not work well and the brackets are frequently replaced by empty boxes in the linked pdf.
  • Similar: semantics of type theory. See: Hofmann, Martin, Syntax and semantics of dependent types, Cambridge University Press (ISBN 0-521-58057-9/hbk), 1997.

You will note that in all these example the denotational style is used because having to invent notations like $. \vDash \varphi$ for the set of elements that satisfy $\varphi$ renders a text fairly unreadable. An example where this is necessary are the semantics of fixed points in the above mentioned modal $\mu$-calulus. The notation $[\![\varphi]\!]$, or variations like $|\!| \,.|\!|$ thereof, are typically preferred for their brevity.

Incidentally, people resort also in these areas to different names like $\mathbf{v}$ for reasons of convenience. In particular, to use the semantics brackets as a function requires one to always write $[\![\,.]\!]$, $[\![-]\!]$ or something similar. This quickly becomes cumbersome and one write then $\mathbf{v}(\varphi)$ instead of $[\![\varphi]\!]$.

$\endgroup$

You must log in to answer this question.

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