The Iverson bracket, denoted $[P]$, is a “function” that evaluates to $1$ if the given proposition $P$ is true and $0$ if it’s false. That is to say:
\[[P]={\begin{cases}1,&{P}\\0,&{\neg P}\end{cases}}\]The bracket notation can also be used with predicates:
\[[P(x)]={\begin{cases}1,&{P(x)}\\0,&{\neg P(x)}\end{cases}}\]Below I give two set-theoretic definitions of the Iverson bracket. One for the propositional case and one for the predicate case.
Propositional Definition
The Iverson bracket is not a true function as there is no such set of all propositions to be its domain. We can instead think of the notation $[P]$ as being shorthand for the following set:
\[[P]\equiv\bigcup\{x\in \{0,1\}\mid(x=1\wedge P) \vee (x=0\wedge\neg P)\}\]The set builder notation above will end up being $\{0\}$ or $\{1\}$, depending on whether $P$ is true, and the arbitrary union $\bigcup$ outside of the set ‘unwraps’ the resulting singleton, leaving us with just $0$ or $1$.
This definition allows us to truly equate $[P]$ with the values $0$ and $1$ in the set-theoretic sense.
Predicate Definition
For the predicate version of the Iverson bracket, we’d like $[P(x)]$ to be some function of $x$ and always return either $0$ or $1$. To this end, we must limit our $x$ to some domain $S$.
Also, to aid in defining $[P(x)]$ we’ll call it $Q(x)$ for the time being and define $Q$ as:
\[\begin{gather*} Q\equiv(S\times\{0,1\}, G_Q)\\ G_Q=\{(x,y)\in S\times\{0,1\}\mid(P(x)\wedge y=1)\vee(\neg P(x)\wedge y=0)\} \end{gather*}\]Where $S$ is the domain, ${0,1}$ the codomain, and $G_Q$ the graph of the function $Q$.
Proof of Function
Clearly $Q$ is a relation as $G_Q\subseteq S\times\{0,1\}$. But to show that $Q$ is a function, we must show that it is right-unique. This should be clear as for any $x\in S$, $P(x)\oplus\neg P(x)$ due to the law of the excluded middle, meaning there is only a single pair $(x,y)\in G_Q$.And so $Q:S\to \{0,1\}$ is a function. We can now define $Q(x)\equiv [P(x)]$, to return to our original notation. Note that due to the simultaneity of arity, this definition works just as well for $n$-ary predicates, netting $n$-ary functions.
Also note that while we do limit ourselves to some domain $S$ rather than the whole universe, this is unavoidable if we are to identify the notation $[P(x)]$ with (not just a function) but any set, where $x$ is a free variable. At least in ZFC, that is.
Arithmetic Properties
Below are some of the immediate properties of the Iverson bracket. We can think of these equalities as bridges between the first order logic notions of truth (true vs. false) and the arithmetic/computational notion of booleans ($0$ vs. $1$).
- $[\neg P]=1-[P]$
- $[P\wedge Q]=[P][Q]$
- $[P\vee Q]=[P]+[Q]-[P][Q]$
- $[P\oplus Q]=([P]-[Q])^2$
- $[P\rightarrow Q]=1-[P]+[P][Q]$
- $[P\equiv Q]=1-([P]-[Q])^2$
Examples
Iverson brackets are, in many cases, a more natural way to express certain conditional functions or properties.