Past exam of the logic and set theory course of the University of Oxford / 2008 / A / 1 / e

A propositional variable $p_i$ is a single symbol of the alphabet. Its only nonempty substring is that symbol itself. Every propositional formula is nonempty, so the only substring that is a logical formula is $p_i$. ThereforeThe subscript is part of the name of an atomic token; it does not introduce additional symbol positions inside the logical variable.

A useful consequence of the formation rules is that logical formulas form a prefix-free set of strings. To see this, describe a deterministic parser that reads one logical formula from its starting position. On a logical variable it consumes that one symbol. On a negation symbol it recursively reads one following logical formula. On an opening parenthesis it recursively reads a left logical formula, requires a logical implication symbol, recursively reads a right logical formula, and requires the closing parenthesis. Induction on formation proves that, if a valid logical formula begins at the current position, this procedure consumes exactly that logical formula and stops at its end.

Suppose now that both $\alpha$ and $\varphi$ are logical formulas and $\varphi =\alpha ϵ$. The same parser, started at their common first symbol, must stop both at the end of $\alpha$ and at the end of $\varphi$. Its deterministic stopping position cannot differ, so $ϵ$ is empty. HenceThis argument applies to symbol strings; it does not use truth values or logical equivalence.

First note that a substring which is itself a logical formula must coincide with a subtree of the formula syntax tree of the surrounding logical formula. Indeed, a logical formula can begin only at a logical variable, a negation symbol or an opening parenthesis. Every such position in a valid logical formula is the start of one of its parsed subtrees. If $\beta$ is the logical formula at that subtree and $\alpha$ is another logical formula starting at the same position, one is an initial segment of the other; prefix-freeness of fully parenthesized formulas from the preceding part forces $\alpha =\beta$.

Now consider a final subformula. For a logical variable, it can only be the whole logical formula. For a binary logical implication $(\psi \to \chi )$, every proper subtree is contained in $\psi$ or $\chi$ and finishes before the final closing parenthesis of the whole expression. It therefore cannot be a final substring of the whole. The only remaining possible outer formation is negation. ThusThe second alternative is a necessary possibility, not a claim that every negated logical formula has every one of its subformulas as a suffix.

The whole logical formula $\neg \psi$ is a subformula of itself, and any subformula of $\psi$ remains a contiguous substring after placing a negation symbol in front of $\psi$.

Conversely, a subformula occurrence starting at the first symbol of $\neg \psi$ is an initial subformula, so equals the whole logical formula by prefix-freeness of fully parenthesized formulas. An occurrence starting later lies wholly inside the following string $\psi$, and is therefore a subformula of $\psi$. ConsequentlyHere $\mathrm{Sub}$ records distinct logical formulas; multiple occurrences of the same logical formula do not create different elements of this set.

A subformula beginning at the first opening parenthesis equals the whole logical formula by prefix-freeness of fully parenthesized formulas. Every other subformula is the logical formula of a proper syntax subtree, by the parsing argument in part (iii). The two children of the root are precisely $\psi$ and $\chi$, so such a subtree lies entirely inside one of those children. In particular no logical formula substring can begin in $\psi$ and cross the principal logical implication symbol into $\chi$.

Conversely, each subformula of either child is visibly a substring of the whole expression, as is the whole expression itself. ThusTogether these cases identify the substring definition of a subformula with its usual syntax-tree definition.