Unique Readability

Question

An essential ingredient of the workings of mathematical logic is the possibility of defining functions by recursion on the complexity of formulas. In order to ensure that such a function assigns exactly one value to each of its arguments one usually has to use a unique readability theorem, which says that every formula can be formed in only one way. More precisely, in the case of classical propositional logic the theorem says the following:

• For every formula $\phi$ exactly one of the following cases holds:

  • $\phi$ is a propositional variable.
  • there is unique formula $\psi$ such that $\phi = \neg \psi$.
  • there is a unique pair $\langle \psi, \chi \rangle$ of formulas and a unique binary connective $\circ$ such that $\phi = (\psi \circ \chi)$.

The complexity of the proof of this theorem crucially depends on how formulas are defined. If we follow orthodoxy and define formulas as some finite sequences the proof gets quite involved.

However, there is a different way of defining formulas, which immediately implies the result. According to that approach formulas are ordered tuples whose members belong to the usual propositional alphabet. Such a definition might run as follows:

• The set of formulas, $\mathcal{F}$, is the smallest set such that:
  • $\langle p \rangle \in \mathcal{F}$ for every propositional variable $p$.
  • $\langle \neg, \phi \rangle \in \mathcal{F}$, if $\phi \in \mathcal{F}$
  • $\langle \phi, \circ, \psi \rangle \in \mathcal{F}$, if $\phi, \psi \in \mathcal{F}$ and $\circ$ is binary.

On may retain familiar notation by letting $\neg \phi := \langle \neg, \phi \rangle$ etc. It's obvious that under such a treatment we can dispense with brackets. If we want to stick to them one has to introduce them as part of the meta language.

Question: Why is this definition of formulas, which is equivalent to the orthodox one, so rarely seen in the literature? Are there any problems technical or conceptual that arise in connection with this definition but not in connection with the orthodox one?

Answer 1

Short, rough answer: the first style of definition is [naturally read as] a definition for a class of well-formed formulae as expression-types, and the second style of definitions is a definition for a class of set-theoretic proxies for formulae in the sense of expression-types.

Suppose we say '$P$' and '$Q$' are propositional variables, and that '$\to$' is a connective. What are we talking about here? Surely not particular ink markings, or particular arrays of pixels. The obvious thing to say is that we are talking of expression types, types or patterns of which particular inscriptions are physical tokens or instances. Likewise, when we say '$(P \to Q)$' is a wff: what we are talking about is surely another expression type (which has many instances on bits of paper and laptop screens etc). Defining the class of wffs is naturally done, then, by telling us the rules for forming more complex expression types out of simpler ones. And that's what the first-style of definition for the class of wffs does -- it deals directly in expression types. This is the obvious line to take.

How are we to read the second kind of definition? It too talks of propositional variables, so on the face of it, the construction is done in a set theory with expressions types as urelemente (which might seem to be more heavy-duty apparatus than we need: if we already countenance expression types, why not do the whole story simply in terms of them??). But perhaps the so-called propositional variables here are really more sets, being used as proxies (or models or implementations) for expression-types, so the whole construction is done in pure set theory.

If you look at the fine print of many logic books, you find authors take different lines about what's going on in their formal languages, and it takes patience to sort things out. For example, while many introduce the symbol '$\to$' as a conditional, for some the symbol serves as proxy or representation for whatever symbol is the conditional connective of your favourite ground-level language $L$ (as Bell and Machover put it, "what the latter symbol actually looks like is of no importance; and the reader may give free rein to his imagination"). If you take this more abstract line, you aren't directly specifying expression-types but providing abstract representations of them. In this case, you might as well use set-theoretic representations of them with nice properties (like trivial "unique readability"). But note the nice properties come at a price -- you've stopped talking about expression types directly, and started talking about set-theoretic proxies for them.

Answer 2

There are, as the question says and Peter Smith describes, two main options:

• Define formulas to be a particular kind of expression - a concrete object like a sequence of written symbols.

• Define formulas to be a particular kind of abstract object - for example, when formalizing logic in ZFC, we may define a formula to be a particular kind of set such as an ordered tuple or a tree.

The main reason for being interested in the former is that, apart from the mathematical goals of logic, there are also foundational and computational goals. These are closely related.

Foundationally, we may want to rely on as few abstract concepts as possible when setting up our logic. Some results (e.g. completeness) will rely on abstract concepts, but the basic concepts of syntax and provability don't have to. We can define an expression to be a particular kind of physical structure - a sequence of physical objects of a certain type. There is a small amount of idealization, because no physical object can make a perfect "$\land$", but this is a much smaller amount of idealization than if we define an expression to be some kind of abstract object with no physical token. This goal of having foundational systems with the minimum number of abstract assumptions was particularly of interest during the period in time when the details of modern formal logic were first developed.

Computationally, we may want to be able to verify a formal deduction, or to create a formal deduction automatically with a theorem prover. For example, there are completely formalized and verified proofs of the prime number theorem and a few other "big" theorems. We need to pass the input to the theorem prover in some concrete form (probably inside a computer file). Until we have a computer program to which we can directly pass a set, it won't help us to define a formula to be a set if we want to pass that formula to the computer.

In elementary settings, the authors will want to keep the students' options open. So the author is likely to choose a presentation that can be used by students whose primary goals are mathematical, foundational, or computational. Of course each book will have its own mix of the three.

In more advanced settings, it is more common to define a formula to be a set (e.g. a tuple or a tree). This is because readers in those settings will be familiar with the possibility of representing everything in a more concrete way. Making the definition abstract avoids the need to prove the unique readability theorem. But even these authors probably still think of formulas as expressions; they are likely to look at the abstract definitions as a slick way of doing things from an advanced point of view.

Answer 3

Because both options are exactly isomorphic to ASTs (abstract syntax trees).