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?
Best Answer
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:
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]\!]$.