proof that the truth value that is recursively defined is a function

Question

In first order logic: https://www.cs.ox.ac.uk/people/james.worrell/lecture9-2015.pdf, there is a recursive definition of the truth value of the formulaes:

This seems to be a recursive definition, so how can we prove that a function exists from the set of closed formulaes to $\{0,1\}$? I have seen the recursion theorem in Halmos book naive set theory, but that is not suited for this case. Are there other recursion theorems that can help, or can this be proven directly? One aspect that complicates the situation is the formulaes are either closed or not closed so we must also handle the case where they are not closed.

Answer 1

In the referenced PDF, the very concepts of "term" and "formula" are defined inductively on page 1. Note that the text also has an error on that same page when it states

We assume that the quantifiers bind more tightly than any of the Boolean operators, e.g., $∀x F ∧ G$ denotes the formula $(∀x F ) ∧ G$.

In fact, neither $∀x F ∧ G$ nor $(∀x F ) ∧ G$ are formulas (at least not when $F,G$ are formulas) because by the very definition a few lines above that statement, a formula containing "$\land$" must always have an extra "$($" to the left and an extra "$)$" to the right of the "$\land$".

What is presented on page 2 as "Example 1" is even worse: If we follow the inductive definition, this "example" can only be a formula if it was produced by prepending $\forall x$ to the formula $\forall y\forall z(R(x,y)\land R(y,z)\to R(x,z))$ as in the fourth bullet point because it does not match any of the patterns produced by the other bullet points. This formula(?) again can only be produced by prepending $\forall y$ to the formula $\forall z(R(x,y)\land R(y,z)\to R(x,z))$, and this only by prepending $\forall z$ to the formula $(R(x,y)\land R(y,z)\to R(x,z))$. This matches only what is produced by the third bullet point as $(F\land G)$ with $F\equiv R(x,y)$ and $G\equiv R(y,z)\to R(x,z)$. Not only is this certainly not what the author intended (assuming they wanted to express that $R$ is a transitive relation), but the required $G$ is not even a formula because the symbol "$\to$" cannot be introduced via any of the bullet points!

I insist on this because being lazy with the notation in a formal context may introduce ambiguity. If we ignore the parentheses used in the formal inductive definition, then we may end up using formulae such as $F\land G\lor H$, and while we may agree on some convention about operator precedence, the inductive rules in the definition of "formula" do not allow this. Or, if we were to allow this, then $F\land G\lor H$ could be viewed as produced by joining $F$ and $G\lor H$ with "$\land$" as well as by joining $F\land G$ and $H$ with "$\lor$". In that case, the claimed recursive definition of a truth value may fail as we may arrive at different truth values for $F\land G\lor H$ depending on which of the teo valid productions we pick!

Thus an important observation regarding the inductive definition of formulae is:

Every formula is either of the form $P(t_1,\ldots, t_k)$ (and in this case, $P$ and $k$ and all $t_i$ are uniquely determined), or of the form $\neg F$ with a uniquely determined $F$, or of the form $(F\lor G)$ with uniquely determined $F,G$, or of the form $(F\land G)$ with uniquely determined $F,G$, or of the form $\exists x F$ with uniquely determined variable $x$ and formula $F$, or of the form $\forall x F$ with uniquely determined variable $x$ and formula $F$.

Apparently, the PDF did not spell it out, but the production rules on page 1 are indeed carefully designed in a way that makes this uniqueness property hold. To be strict, one has of course to prove this carefully.

And guess what, we do so by induction.

To do so, we formalize the inductive definitions on page 1. That is, we let $\mathcal V$ be the (countably) infinite set of variables, $\mathcal C$ the set of constant symbols, and for each $k\in\Bbb N$ the set $\mathcal F_k$ of $k$-ary function symbols and $\mathcal P_k$ the set of $k$-ary predicate symbols. In addition, we let $\mathcal L$ be the set containing the following eight logical symbols: $$ \tt(\qquad)\qquad,\qquad\land\qquad \lor\qquad\neg\qquad \forall\qquad \exists$$ (and remark that the PDF forgot to specify that most of these sets better be pairwise disjoint!!). Then we let $\mathcal A$ be the (disjoint!!) union of all these sets and will define terms and formulae as finite strings over this alphabet $\mathcal A$.

Given $\mathcal X\subset \mathcal A^*$, we define comma separated lists of elements of $\mathcal X$ recursively via $$ \mathcal S_1(\mathcal X)=\mathcal X,\qquad \mathcal S_{n+1}(\mathcal X)=\{\,x{\tt ,}y\mid x\in \mathcal S_{n}(\mathcal X), y\in\mathcal X\,\}$$

More precisely (but following the bullet points in page 1), we let $$\mathcal T_0=\mathcal V\cup \mathcal C $$ and recursively $$ \mathcal T_{n+1}=\mathcal T_n\cup\bigcup_{k=1}^\infty \{\, f {\tt(}s{\tt)}\mid f\in \mathcal f_k, s\in \mathcal S_k(\mathcal T_n)\,\}$$

and ultimately $$\mathcal T=\bigcup_{n=0}^\infty \mathcal T_n.$$ as set of terms.

As a first exercise, try to formally show:

Proposition. Given $t\in \mathcal T$, exactly one of the following is true:

• $t\in \mathcal V$
• $t\in \mathcal C$
• there exists a unique(!) $k\in\Bbb N$ and unique(!) $f\in\mathcal F_k$ and for $1\le i\le k$ unique(!) $t_i\in\mathcal T$ and $s_i\in\mathcal S_i(\mathcal T)$ auch that $s_1=t_1$, $s_{i+1}=s_i{\tt ,}t_{i+1}$ for $1\le i<k$, and $t=f{\tt (}s_k{\tt)}$.

This does get very technical and we haven't even started with formulae! Nevertheless, it is the uniqueness expressed in this lemma (together with the fact that we only produce $t$ from strictly shorter terms in the third bullet point) that allows us (without me going into the nitty-gritty details) to prove theorems about $\mathcal T$ by structural induction (which is essentially just strong induction by the length of strings) and likewise to define functions on the set $\mathcal T$ by structural recursion.

The same goes for formulae: As an exercise, try to repeat the formal definition of the set of formulae as a subset of $\mathcal A^*$ in the same fashion as done above for terms. Then try to formulate and prove a similar lemma about uniqueness of production for formulae. Then agree that structural induction/recursion works for formulae.