Syntax of First-Order Logic

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

How to use Read

This page follows Syntax of First-Order Logic in source order. Equations are native, unflattened MathML, and every source coordinate is available offline.

Thirteen disclosed reader corrections

The frozen source remains unchanged. These reviewed interventions are visible wherever affected material is presented.

occurrence-correction-projected-formula-0006646: The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed conjunction. Open the affected occurrence.
occurrence-correction-projected-formula-0006648: The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed disjunction. Open the affected occurrence.
occurrence-correction-projected-formula-0006650: The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed conditional. Open the affected occurrence.
occurrence-correction-projected-formula-0006725: The source uses k both as the declared arity and as the final zero-based argument index, which displays k plus one arguments. The reader preserves and explicitly flags this mismatch. Open the affected occurrence.
occurrence-correction-projected-formula-0006727: The displayed index range contains k plus one argument positions, although the preceding source calls the function k-ary. The reader preserves and explicitly flags this mismatch. Open the affected occurrence.
occurrence-correction-projected-formula-0006728: The source calls f k-ary but displays arguments indexed from m sub zero through m sub k, which is k plus one displayed arguments. The reader preserves that source mismatch and does not silently choose a correction. Open the affected occurrence.
occurrence-correction-projected-formula-0006791: The reader interprets n as the final sequence index. The source calls the following m a length, but a sequence indexed zero through n has length n plus one. Open the affected occurrence.
occurrence-correction-projected-formula-0006792: The source calls m a sequence length while inducting on the final index n. Since a sequence indexed from zero through n has n plus one entries, the literal length statement is off by one. The reader treats m and n as final indices; equivalently, the proof may induct on length n plus one and use all shorter lengths. Open the affected occurrence.
occurrence-correction-projected-formula-0006794: The printed sentence has a garden-path construction: 'either A is syntactically identical to A sub n is atomic.' The reader supplies appositive wording so the intended claim is that A, identical to the final entry A sub n, is atomic. Open the affected occurrence.
occurrence-correction-projected-formula-0006803: The source prints the undefined language L sub zero here, although this theorem fixes the first-order language L. The reader uses L and preserves the printed source in the source view. Open the affected occurrence.
occurrence-correction-projected-formula-0006804: The source prints material-equivalence notation in this proof case, while the formation clauses and the argument require syntactic identity. The reader uses syntactic identity and preserves the printed source in the source view. Open the affected occurrence.
occurrence-correction-projected-formula-0006810: The source says the proper initial sequences have length less than n. The correct final-index statement is that they end at indices less than n; equivalently their lengths are less than n plus one. Open the affected occurrence.
occurrence-correction-projected-formula-0006813: The source again prints the undefined language L sub zero here. The theorem concerns the fixed first-order language L, which the reader uses while preserving the printed source in the source view. Open the affected occurrence.

Introduction

In order to develop the theory and metatheory of first-order logic, we must first define the syntax and semantics of its expressions. The expressions of first-order logic are terms and formulas. Terms are formed from variables, constants, and functions. Formulas, in turn, are formed from predicates together with terms (these form the smallest, “atomic” formulas), and then from atomic formulas we can form more complex ones using logical connectives and quantifiers. There are many different ways to set down the formation rules; we give just one possible one. Other systems will chose different symbols, will select different sets of connectives as primitive, will use parentheses differently (or even not at all, as in the case of so-called Polish notation). What all approaches have in common, though, is that the formation rules define the set of terms and formulas inductively. If done properly, every expression can result essentially in only one way according to the formation rules. The inductive definition resulting in expressions that are uniquely readable means we can give meanings to these expressions using the same method—inductive definition.

First-Order Languages

Expressions of first-order logic are built up from a basic vocabulary containing variables, constants, predicates and sometimes functions. From them, together with logical connectives, quantifiers, and punctuation symbols such as parentheses and commas, terms and formulas are formed.

In the general case, we make use of the following symbols in first-order logic:

Logical symbols
1. Logical connectives: $\neg$ source 39 (negation), $\land$ source 40 (conjunction), $\lor$ source 41 (disjunction), $\to$ source 42 (conditional)
  $\forall$ source 44 (universal quantifier), $\exists$ source 45 (existential quantifier). The propositional constant for falsity $⊥$ source 46.
2. The two-place identity $=$ source 48.
3. A denumerables set of variables: $v_{0}$ source 49, $v_{1}$ source 49, $v_{2}$ source 49, …
Non-logical symbols, making up the standard language of first-order logic
1. A denumerables set of $n$ source 55-place predicates for each $n > 0$ source 55: ${A^{n}}_{0}$ source 55, ${A^{n}}_{1}$ source 56, ${A^{n}}_{2}$ source 56, …
2. A denumerables set of constants: $c_{0}$ source 57, $c_{1}$ source 57, $c_{2}$ source 57, ….
3. A denumerables set of $n$ source 59-place functions for each $n > 0$ source 59: ${f^{n}}_{0}$ source 60, ${f^{n}}_{1}$ source 60, ${f^{n}}_{2}$ source 60, …
Punctuation marks: (, ), and the comma.

Most of our definitions and results will be formulated for the full standard language of first-order logic. However, depending on the application, we may also restrict the language to only a few predicates, constants, and functions.

Arithmetic language example

The language $L_{A}$ source 71 of arithmetic contains a single two-place predicate $<$ source 72, a single constant $0$ source 72, one one-place function $'$ source 73, and two two-place functions $+$ source 73 and $\times$ source 73.

source 70

Set-theory language example

The language of set theory $L_{Z}$ source 77 contains only the single two-place predicate $\in$ source 78.

source 76

Order language example

The language of orders $L_{\leq}$ source 82 contains only the two-place predicate $\leq$ source 83.

source 81

Again, these are conventions: officially, these are just aliases, e.g., $<$ source 87, $\in$ source 87, and $\leq$ source 87 are aliases for ${A^{2}}_{0}$ source 87, $0$ source 87 for $c_{0}$ source 88, $'$ source 88 for ${f^{1}}_{0}$ source 88, $+$ source 88 for ${f^{2}}_{0}$ source 88, $\times$ source 88 for ${f^{2}}_{1}$ source 89.

In addition to the primitive connectives and quantifiers introduced above, we also use the following defined symbols:

$\leftrightarrow$ source 100 (biconditional)

Truth $⊤$ source 104.

Introduction

You may be familiar with different terminology and symbols than the ones we use above. Logic texts (and teachers) commonly use $\sim$ source 123, $\neg$ source 123, or ! for “negation”, $\land$ source 123, $\cdot$ source 123, or $&$ source 123 for “conjunction”. Commonly used symbols for the “conditional” or “implication” are $\to$ source 125, $\Rightarrow$ source 125, and $\supset$ source 125. Symbols for “biconditional,” “bi-implication,” or “(material) equivalence” are $\leftrightarrow$ source 127, $\Leftrightarrow$ source 128, and $\equiv$ source 128. The $⊥$ source 129 symbol is variously called “falsity,” “falsum,”, “absurdity,” or “bottom.” The $⊤$ source 131 symbol is variously called “truth,” “verum,” or “top.”

It is conventional to use lower case letters (e.g., $a$ source 134, $b$ source 134, $c$ source 134) from the beginning of the Latin alphabet for constants (sometimes called names), and lower case letters from the end (e.g., $x$ source 136, $y$ source 136, $z$ source 136) for variables. Quantifiers combine with variables, e.g., $x$ source 137; notational variations include $\forall x$ source 138, $(\forall x)$ source 138, $(x)$ source 138, $Π x$ source 138, $⋀_{x}$ source 139 for the universal quantifier and $\exists x$ source 139, $(\exists x)$ source 139, $(E x)$ source 140, $Σ x$ source 140, $⋁_{x}$ source 140 for the existential quantifier.

Terms and formula

Once a first-order language $L$ source 13 is given, we can define expressions built up from the basic vocabulary of $L$ source 14. These include in particular terms and formulas.

Inductive definition of first-order terms

The set of terms $Trm (L)$ source 19 of $L$ source 19 is defined inductively by:

Every variable is a term.
Every constant of $L$ source 23 is a term.
If $f$ source 24 is an $n$ source 24-place function and $t_{1}$ source 24, …, $t_{n}$ source 24 are terms, then $f (t_{1}, \dots, t_{n})$ source 25 is a term.
Nothing else is a term.

A term containing no variables is a closed term.

source 17

Inductive definition of first-order formulas

The set of formulas $Frm (L)$ source 43 of the language $L$ source 43 is defined inductively as follows:

$⊥$ source 46 is an atomic formula.

If $R$ source 50 is an $n$ source 50-place predicate of $L$ source 50 and $t_{1}$ source 50, …, $t_{n}$ source 51 are terms of $L$ source 51, then $R (t_{1}, \dots, t_{n})$ source 51 is an atomic formula.
If $t_{1}$ source 54 and $t_{2}$ source 54 are terms of $L$ source 54, then $= (t_{1}, t_{2})$ source 54 is an atomic formula.
If $A$ source 57 is a formula, then $\neg A$ source 57 is a formula.
If $A$ source 60 and $B$ source 60 are formulas, then $(A \land B)$ source 60 is a formula.
If $A$ source 63 and $B$ source 63 are formulas, then $(A \lor B)$ source 63 is a formula.
If $A$ source 66 and $B$ source 66 are formulas, then $(A \to B)$ source 66 is a formula.
If $A$ source 72 is a formula and $x$ source 72 is a variable, then $\forall x A$ source 73 is a formula.
If $A$ source 75 is a formula and $x$ source 75 is a variable, then $\exists x A$ source 76 is a formula.
Nothing else is a formula.

source 41

Explanation

The definitions of the set of terms and that of formulas are inductive definitions. Essentially, we construct the set of formulas in infinitely many stages. In the initial stage, we pronounce all atomic formulas to be formulas; this corresponds to the first few cases of the definition, i.e., the cases for

$⊥$ source 89, $R (t_{1}, \dots, t_{n})$ source 90 and $= (t_{1}, t_{2})$ source 90. “Atomic formula” thus means any formula of this form.

The other cases of the definition give rules for constructing new formulas out of formulas already constructed. At the second stage, we can use them to construct formulas out of atomic formulas. At the third stage, we construct new formulas from the atomic formulas and those obtained in the second stage, and so on. A formula is anything that is eventually constructed at such a stage, and nothing else.

By convention, we write $=$ source 102 between its arguments and leave out the parentheses: $t_{1} = t_{2}$ source 103 is an abbreviation for $= (t_{1}, t_{2})$ source 104. Moreover, $\neg = (t_{1}, t_{2})$ source 104 is abbreviated as $t_{1} \neq t_{2}$ source 105. When writing a formula $(B * C)$ source 105 constructed from $B$ source 106, $C$ source 106 using a two-place connective $*$ source 106, we will often leave out the outermost pair of parentheses and write simply $B * C$ source 108.

Definitions of derived logical operators

Formulas constructed using the defined operators are to be understood as follows:

$⊤$ source 129 abbreviates $\neg ⊥$ source 130.

$A \leftrightarrow B$ source 150 abbreviates $(A \to B) \land (B \to A)$ source 150.

source 123

If we work in a language for a specific application, we will often write two-place predicates and functions between the respective terms, e.g., $t_{1} < t_{2}$ source 162 and $(t_{1} + t_{2})$ source 162 in the language of arithmetic and $t_{1} \in t_{2}$ source 163 in the language of set theory. The successor function in the language of arithmetic is even written conventionally after its argument: $t'$ source 165. Officially, however, these are just conventional abbreviations for ${A^{2}}_{0} (t_{1}, t_{2})$ source 166, ${f^{2}}_{0} (t_{1}, t_{2})$ source 167, ${A^{2}}_{0} (t_{1}, t_{2})$ source 167 and ${f^{1}}_{0} (t)$ source 167, respectively.

Definition of syntactic identity

The symbol $\equiv$ source 171 expresses syntactic identity between strings of symbols, i.e., $A \equiv B$ source 172 iff $A$ source 172 and $B$ source 172 are strings of symbols of the same length and which contain the same symbol in each place.

source 170

The $\equiv$ source 176 symbol may be flanked by strings obtained by concatenation, e.g., $A \equiv (B \lor C)$ source 177 means: the string of symbols $A$ source 178 is the same string as the one obtained by concatenating an opening parenthesis, the string $B$ source 179, the $\lor$ source 179 symbol, the string $C$ source 180, and a closing parenthesis, in this order. If this is the case, then we know that the first symbol of $A$ source 181 is an opening parenthesis, $A$ source 182 contains $B$ source 182 as a substring (starting at the second symbol), that substring is followed by $\lor$ source 183, etc.

As terms and formulas are built up from basic elements via inductive definitions, we can use the following induction principles to prove things about them.

Principle of induction on terms

Let $L$ source 191 be a first-order language. If some property $P$ source 192 is such that

it holds for every variable $v$ source 195,
it holds for every constant $a$ source 197 of $L$ source 197, and
it holds for $f (t_{1}, \dots, t_{n})$ source 199 whenever it holds for $t_{1}$ source 200, …, $t_{n}$ source 200 and $f$ source 200 is an $n$ source 200-place function of $L$ source 201

(assuming $t_{1}$ source 203, …, $t_{n}$ source 203 are terms of $L$ source 203), then $P$ source 204 holds for every term in $Trm (L)$ source 204.

source 189

Exercise on induction for terms

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Principle of induction on terms.

source 207

Principle of induction on formulas

Let $L$ source 213 be a first-order language. If some property $P$ source 214 holds for all the atomic formulas and is such that

it holds for $\neg A$ source 218 whenever it holds for $A$ source 219; it holds for $(A \land B)$ source 220 whenever it holds for $A$ source 221 and $B$ source 221; it holds for $(A \lor B)$ source 222 whenever it holds for $A$ source 223 and $B$ source 223; it holds for $(A \to B)$ source 224 whenever it holds for $A$ source 225 and $B$ source 225;

it holds for $\exists x A$ source 228 whenever it holds for $A$ source 229; it holds for $\forall x A$ source 230 whenever it holds for $A$ source 231;

(assuming $A$ source 233 and $B$ source 233 are formulas of $L$ source 233), then $P$ source 234 holds for all formulas in $Frm (L)$ source 234.

source 211

Unique Readability

Explanation

The way we defined formulas guarantees that every formula has a unique reading, i.e., there is essentially only one way of constructing it according to our formation rules for formulas and only one way of “interpreting” it. If this were not so, we would have ambiguous formulas, i.e., formulas that have more than one reading or intepretation—and that is clearly something we want to avoid. But more importantly, without this property, most of the definitions and proofs we are going to give will not go through.

Perhaps the best way to make this clear is to see what would happen if we had given bad rules for forming formulas that would not guarantee unique readability. For instance, we could have forgotten the parentheses in the formation rules for connectives, e.g., we might have allowed this:

If $A$ source 29 and $B$ source 29 are formulas, then so is $A \to B$ source 29.

Starting from an atomic formula $D$ source 31, this would allow us to form $D \to D$ source 31. From this, together with $D$ source 32, we would get $D \to D \to D$ source 32. But there are two ways to do this:

We take $D$ source 35 to be $A$ source 35 and $D \to D$ source 35 to be $B$ source 35.
We take $A$ source 36 to be $D \to D$ source 36 and $B$ source 36 is $D$ source 36.

Correspondingly, there are two ways to “read” the formula $D \to D \to D$ source 39. It is of the form $B \to C$ source 39 where $B$ source 40 is $D$ source 40 and $C$ source 40 is $D \to D$ source 40, but it is also of the form $B \to C$ source 41 with $B$ source 41 being $D \to D$ source 41 and $C$ source 41 being $D$ source 42.

If this happens, our definitions will not always work. For instance, when we define the main operator of a formula, we say: in a formula of the form $B \to C$ source 46, the main operator is the indicated occurrence of $\to$ source 47. But if we can match the formula $D \to D \to D$ source 47 with $B \to C$ source 48 in the two different ways mentioned above, then in one case we get the first occurrence of $\to$ source 49 as the main operator, and in the second case the second occurrence. But we intend the main operator to be a function of the formula, i.e., every formula must have exactly one main operator occurrence.

Balanced-parentheses lemma for formulas

The number of left and right parentheses in a formula $A$ source 57 are equal.

source 56

Proof

We prove this by induction on the way $A$ source 62 is constructed. This requires two things: (a) We have to prove first that all atomic formulas have the property in question (the induction basis). (b) Then we have to prove that when we construct new formulas out of given formulas, the new formulas have the property provided the old ones do.

Let $l (A)$ source 68 be the number of left parentheses, and $r (A)$ source 68 the number of right parentheses in $A$ source 69, and $l (t)$ source 69 and $r (t)$ source 69 similarly the number of left and right parentheses in a term $t$ source 70.

Exercise on parentheses in terms

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove that for any term $t$ source 73, $l (t) = r (t)$ source 73.

source 72

Case: $A$ source 77 has $0$ source 77 left and $0$ source 77 right parentheses.

Case: $l (A) = 1 + l (t_{1}) + \dots + l (t_{n}) = 1 + r (t_{1}) + \dots + r (t_{n}) = r (A)$ source 83. Here we make use of the fact, left as an exercise, that $l (t) = r (t)$ source 85 for any term $t$ source 86.
Case: $l (A) = l (t_{1}) + l (t_{2}) = r (t_{1}) + r (t_{2}) = r (A)$ source 88.
Case: By induction hypothesis, $l (B) = r (B)$ source 92. Thus $l (A) = l (B) = r (B) = r (A)$ source 92.
Case: By induction hypothesis, $l (B) = r (B)$ source 95 and $l (C) = r (C)$ source 96. Thus $l (A) = 1 + l (B) + l (C) = 1 + r (B) + r (C) = r (A)$ source 96.
Case: By induction hypothesis, $l (B) = r (B)$ source 100. Thus, $l (A) = l (B) = r (B) = r (A)$ source 100.
Case: Similarly.

End of proof.

Definition of proper prefix

A string of symbols $B$ source 114 is a proper prefix of a string of symbols $A$ source 114 if concatenating $B$ source 115 and a non-empty string of symbols yields $A$ source 115.

source 113

No-formula-prefix lemma

If $A$ source 119 is a formula, and $B$ source 119 is a proper prefix of $A$ source 119, then $B$ source 120 is not a formula.

source 118

Proof

Exercise.

End of proof.

Exercise on the no-formula-prefix lemma

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove No-formula-prefix lemma.

source 127

Unique form of atomic formulas

If $A$ source 133 is an atomic formula, then it satisfies one, and only one of the following conditions.

$A \equiv ⊥$ source 136.

$A \equiv R (t_{1}, \dots, t_{n})$ source 138 where $R$ source 138 is an $n$ source 138-place predicate, $t_{1}$ source 139, …, $t_{n}$ source 139 are terms, and each of $R$ source 139, $t_{1}$ source 140, …, $t_{n}$ source 140 is uniquely determined.
$A \equiv t_{1} = t_{2}$ source 141 where $t_{1}$ source 141 and $t_{2}$ source 141 are uniquely determined terms.

source 131

Proof

Exercise.

End of proof.

Exercise on unique atomic form

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Unique form of atomic formulas (Hint: Formulate and prove a version of No-formula-prefix lemma for terms.)

source 150

Unique readability proposition

Every formula satisfies one, and only one of the following conditions.

$A$ source 158 is atomic.
$A$ source 160 is of the form $\neg B$ source 160.
$A$ source 162 is of the form $(B \land C)$ source 162.
$A$ source 164 is of the form $(B \lor C)$ source 164.
$A$ source 166 is of the form $(B \to C)$ source 166.
$A$ source 170 is of the form $\forall x B$ source 170.
$A$ source 172 is of the form $\exists x B$ source 172.

Moreover, in each case $B$ source 174, or $B$ source 174 and $C$ source 174, are uniquely determined. This means that, e.g., there are no different pairs $B$ source 175, $C$ source 176 and $B'$ source 176, $C'$ source 176 so that $A$ source 176 is both of the form $(B \to C)$ source 177 and $(B' \to C')$ source 177.

source 155

Proof

The formation rules require that if a formula is not atomic, it must start with an opening parenthesis (, $\neg$ source 184, or a quantifier. On the other hand, every formula that starts with one of the following symbols must be atomic: a predicate, a function, a constant, $⊥$ source 186.

So we really only have to show that if $A$ source 188 is of the form $(B * C)$ source 188 and also of the form $(B' *' C')$ source 189, then $B \equiv B'$ source 189, $C \equiv C'$ source 190, and $* = *'$ source 190.

So suppose both $A \equiv (B * C)$ source 192 and $A \equiv (B' *' C')$ source 192. Then either $B \equiv B'$ source 193 or not. If it is, clearly $* = *'$ source 194 and $C \equiv C'$ source 194, since they then are substrings of $A$ source 195 that begin in the same place and are of the same length. The other case is $B ≢ B'$ source 196. Since $B$ source 196 and $B'$ source 197 are both substrings of $A$ source 197 that begin at the same place, one must be a proper prefix of the other. But this is impossible by No-formula-prefix lemma.

End of proof.

main operator of a Formula

Definition of a formula's main operator

The main operator of a formula $A$ source 24 is defined as follows:

Case: $A$ source 27 has no main operator.
Case: the main operator of $A$ source 29 is $\neg$ source 30.
Case: the main operator of $A$ source 33 is $\land$ source 33.
Case: the main operator of $A$ source 36 is $\lor$ source 36.
Case: the main operator of $A$ source 39 is $\to$ source 39.
Case: the main operator of $A$ source 45 is $\forall$ source 45.
Case: the main operator of $A$ source 48 is $\exists$ source 48.

source 22

In each case, we intend the specific indicated occurrence of the main operator in the formula. For instance, since the formula $((D \to E) \to (E \to D))$ source 54 is of the form $(B \to C)$ source 54 where $B$ source 55 is $(D \to E)$ source 55 and $C$ source 55 is $(E \to D)$ source 55, the second occurrence of $\to$ source 56 is the main operator.

We call formulas by the names in Table of main operators and formula types depending on which symbol their main operator is. Recall, however, that defined operators do not officially appear in formulas. They are just abbreviations, so officially they cannot be the main operator of a formula. In proofs about all formulas they therefore do not have to be treated separately.

Table of main operators and formula types

The table pairs each outer operator with its formula type and an example.

Main operators, formula types, and examples
Main operator	Type of formula	Example
None	Atomic formula	$⊥$ source 85; $R (t_{1}, \dots, t_{n})$ source 87; $t_{1} = t_{2}$ source 88
$\neg$ source 89	Negation	$\neg A$ source 89
$\land$ source 90	Conjunction	$(A \land B)$ source 90 (Reader correction: The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed conjunction)
$\lor$ source 91	Disjunction	$(A \lor B)$ source 91 (Reader correction: The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed disjunction)
$\to$ source 92	Conditional	$(A \to B)$ source 92 (Reader correction: The source table places the closing parenthesis outside the math delimiter. The reader rendering includes it in the displayed conditional)
$\leftrightarrow$ source 93	Biconditional	$(A \leftrightarrow B)$ source 93
$\forall$ source 94	Universal formula	$\forall x A$ source 94
$\exists$ source 95	Existential formula	$\exists x A$ source 95

Source: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 81.

subformula

Definition of immediate subformulas

If $A$ source 21 is a formula, the immediate subformulas of $A$ source 22 are defined inductively as follows:

Atomic formulas have no immediate subformulas.
Case: The only immediate subformula of $A$ source 27 is $B$ source 27.
Case: The immediate subformulas of $A$ source 30 are $B$ source 30 and $C$ source 30 ( $*$ source 30 is any one of the two-place connectives).
Case: The only immediate subformula of $A$ source 34 is $B$ source 34.
Case: The only immediate subformula of $A$ source 37 is $B$ source 37.

source 20

Definition of proper subformulas

If $A$ source 42 is a formula, the proper subformulas of $A$ source 43 are defined recursively as follows:

Atomic formulas have no proper subformulas.
Case: The proper subformulas of $A$ source 48 are $B$ source 48 together with all proper subformulas of $B$ source 49.
Case: The proper subformulas of $A$ source 52 are $B$ source 52, $C$ source 52, together with all proper subformulas of $B$ source 53 and those of $C$ source 53.
Case: The proper subformulas of $A$ source 56 are $B$ source 56 together with all proper subformulas of $B$ source 57.
Case: The proper subformulas of $A$ source 60 are $B$ source 60 together with all proper subformulas of $B$ source 61.

source 41

Definition of subformula

The subformulas of $A$ source 66 are $A$ source 66 itself together with all its proper subformulas.

source 65

Explanation

Note the subtle difference in how we have defined immediate subformulas and proper subformulas. In the first case, we have directly defined the immediate subformulas of a formula $A$ source 73 for each possible form of $A$ source 74. It is an explicit definition by cases, and the cases mirror the inductive definition of the set of formulas. In the second case, we have also mirrored the way the set of all formulas is defined, but in each case we have also included the proper subformulas of the smaller formulas $B$ source 78, $C$ source 79 in addition to these formulas themselves. This makes the definition recursive. In general, a definition of a function on an inductively defined set (in our case, formulas) is recursive if the cases in the definition of the function make use of the function itself. To be well defined, we must make sure, however, that we only ever use the values of the function for arguments that come “before” the one we are defining—in our case, when defining “proper subformula” for $(B * C)$ source 86 we only use the proper subformulas of the “earlier” formulas $B$ source 87 and $C$ source 87.

Transitivity of the subformula relation

Suppose $B$ source 92 is a subformula of $A$ source 92 and $C$ source 92 is a subformula of $B$ source 92. Then $C$ source 93 is a subformula of $A$ source 93. In other words, the subformula relation is transitive.

source 90

Exercise on subformula transitivity

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Transitivity of the subformula relation.

source 97

Upper bound on the number of subformulas

Suppose $A$ source 103 is a formula with $n$ source 103 connectives and quantifiers. Then $A$ source 104 has at most $2 n + 1$ source 104 subformulas.

source 101

Exercise on counting subformulas

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Upper bound on the number of subformulas.

source 107

Formation Sequences

Defining formulas via an inductive definition, and the complementary technique of proving properties of formulas via induction, is an elegant and efficient approach. However, it can also be useful to consider a more bottom-up, step-by-step approach to the construction of formulas, which we do here using the notion of a formation sequence.

To show how terms and formulas can be introduced in this way without needing to refer to their inductive definitions, we first introduce the notion of an arbitrary string of symbols drawn from some language $L$ source 23.

Definition of language strings

Suppose $L$ source 27 is a first-order language. An $L$ source 27-string is a finite sequence of symbols of $L$ source 28. Where the language $L$ source 29 is clearly fixed by the context, we will often refer to a $L$ source 30-string simply as a string.

source 25

Example of a string that is not a formula

For any first-order language $L$ source 34, all $L$ source 35-formulas are $L$ source 35-strings, but not conversely. For example, $) (v_{0} \to \exists$ source 36 is an $L$ source 37-string but not an $L$ source 37-formula.

source 33

Definition of term formation sequence

A finite sequence of $L$ source 42-strings $⟨ t_{0}, \dots, t_{n} ⟩$ source 42 is a formation sequence for a term $t$ source 43 if $t \equiv t_{n}$ source 43 and for all $i \leq n$ source 44, either $t_{i}$ source 44 is a variable or a constant, or $L$ source 44 contains a $k$ source 45-ary function $f$ source 45 (Reader correction: The source uses k both as the declared arity and as the final zero-based argument index, which displays k plus one arguments. The reader preserves and explicitly flags this mismatch) and there exist $m_{0}, \dots, m_{k} < i$ source 46 (Reader correction: The displayed index range contains k plus one argument positions, although the preceding source calls the function k-ary. The reader preserves and explicitly flags this mismatch) such that $t_{i} \equiv f (t_{m_{0}}, \dots, t_{m_{k}})$ source 46 (Reader correction: The source calls f k-ary but displays arguments indexed from m sub zero through m sub k, which is k plus one displayed arguments. The reader preserves that source mismatch and does not silently choose a correction). When it is necessary to distinguish, we will refer to formation sequences for terms as term formation sequences.

source 40

Examples of term formation sequences

The sequence $⟨ c_{0}, v_{0}, {f^{2}}_{0} (c_{0}, v_{0}), {f^{1}}_{0} ({f^{2}}_{0} (c_{0}, v_{0})) ⟩$ source 53 is a formation sequence for the term ${f^{1}}_{0} ({f^{2}}_{0} (c_{0}, v_{0}))$ source 56, as is $⟨ v_{0}, c_{0}, {f^{2}}_{0} (c_{0}, v_{0}), {f^{1}}_{0} ({f^{2}}_{0} (c_{0}, v_{0})) ⟩ .$ source 58

source 51

Definition of formula formation sequence

A finite sequence of $L$ source 65-strings $⟨ A_{0}, \dots, A_{n} ⟩$ source 65 is a formation sequence for $A$ source 66 if $A \equiv A_{n}$ source 66 and for all $i \leq n$ source 67, either $A_{i}$ source 67 is an atomic formula or there exist $j, k < i$ source 68 and a variable $x$ source 68 such that one of the following holds:

$A_{i} \equiv \neg A_{j}$ source 71. $A_{i} \equiv (A_{j} \land A_{k})$ source 72. $A_{i} \equiv (A_{j} \lor A_{k})$ source 73. $A_{i} \equiv (A_{j} \to A_{k})$ source 74.

$A_{i} \equiv \forall x A_{j}$ source 76. $A_{i} \equiv \exists x A_{j}$ source 77.

When it is necessary to distinguish, we will refer to formation sequences for formulas as formula formation sequences.

source 63

Examples of formula formation sequences

$⟨ {A^{1}}_{0} (v_{0}), {A^{1}}_{1} (c_{1}), ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})), \exists v_{0} ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})) ⟩$ source 84 is a formation sequence of $\exists v_{0} ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0}))$ source 92, as is Displayed redundant formula formation sequence $⟨ {A^{1}}_{0} (v_{0}), {A^{1}}_{1} (c_{1}), ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})), {A^{1}}_{1} (c_{1}), \forall v_{1} {A^{1}}_{0} (v_{0}), \exists v_{0} ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})) ⟩ .$ source 94

As can be seen from the second example, formation sequences may contain “junk”: formulas which are redundant or do not contribute to the construction.

source 83

Existence of formula formation sequences

Every formula $A$ source 111 in $Frm (L)$ source 111 has a formation sequence.

source 110

Proof

Suppose $A$ source 115 is atomic. Then the sequence $⟨ A ⟩$ source 115 is a formation sequence for $A$ source 116.

Now suppose that $B$ source 118 and $C$ source 118 have formation sequences $⟨ B_{0}, \dots, B_{n} ⟩$ source 119 and $⟨ C_{0}, \dots, C_{m} ⟩$ source 119 respectively.

If $A \equiv \neg B$ source 123, then $⟨ B_{0}, \dots, B_{n}, \neg B_{n} ⟩$ source 124 is a formation sequence for $A$ source 125. If $A \equiv (B \land C)$ source 126, then $⟨ B_{0}, \dots, B_{n}, C_{0}, \dots, C_{m}, (B_{n} \land C_{m}) ⟩$ source 127 is a formation sequence for $A$ source 128. If $A \equiv (B \lor C)$ source 129, then $⟨ B_{0}, \dots, B_{n}, C_{0}, \dots, C_{m}, (B_{n} \lor C_{m}) ⟩$ source 130 is a formation sequence for $A$ source 131. If $A \equiv (B \to C)$ source 132, then $⟨ B_{0}, \dots, B_{n}, C_{0}, \dots, C_{m}, (B_{n} \to C_{m}) ⟩$ source 133 is a formation sequence for $A$ source 134.

If $A \equiv \forall x B$ source 138, then $⟨ B_{0}, \dots, B_{n}, \forall x B_{n} ⟩$ source 139 is a formation sequence for $A$ source 140. If $A \equiv \exists x B$ source 141, then $⟨ B_{0}, \dots, B_{n}, \exists x B_{n} ⟩$ source 142 is a formation sequence for $A$ source 143.

By the principle of induction on formulas, every formula has a formation sequence.

End of proof.

We can also prove the converse. This is important because it shows that our two ways of defining formulas are equivalent: they give the same results. It also means that we can prove theorems about formulas by using ordinary induction on the length of formation sequences.

Initial-subsequence lemma

Suppose that $⟨ A_{0}, \dots, A_{n} ⟩$ source 157 is a formation sequence for $A_{n}$ source 158, and that $k \leq n$ source 158. Then $⟨ A_{0}, \dots, A_{k} ⟩$ source 158 is a formation sequence for $A_{k}$ source 159.

source 155

Proof

Exercise.

End of proof.

Exercise on initial formation subsequences

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Initial-subsequence lemma.

source 166

Equivalence of formula definitions

$Frm (L)$ source 172 is the set of all $L$ source 172-strings $A$ source 172 such that there exists a formula formation sequence for $A$ source 173.

source 170

Proof

Let $F$ source 177 be the set of all strings of symbols in the language $L$ source 177 that have a formation sequence. We have seen in Existence of formula formation sequences that $Frm (L) \subseteq F$ source 179, so now we prove the converse.

Suppose $A$ source 182 has a formation sequence $⟨ A_{0}, \dots, A_{n} ⟩$ source 182. We prove that $A \in Frm (L)$ source 183 by strong induction on $n$ source 183 (Reader correction: The reader interprets n as the final sequence index. The source calls the following m a length, but a sequence indexed zero through n has length n plus one). Our induction hypothesis is that every string of symbols with a formation sequence of length $m < n$ source 185 (Reader correction: The source calls m a sequence length while inducting on the final index n. Since a sequence indexed from zero through n has n plus one entries, the literal length statement is off by one. The reader treats m and n as final indices; equivalently, the proof may induct on length n plus one and use all shorter lengths) is in $Frm (L)$ source 185. By the definition of a formation sequence, either $A \equiv A_{n}$ source 186 (Reader correction: The printed sentence has a garden-path construction: 'either A is syntactically identical to A sub n is atomic.' The reader supplies appositive wording so the intended claim is that A, identical to the final entry A sub n, is atomic) is atomic or there must exist $j, k < n$ source 187 such that one of the following is the case:

$A \equiv \neg A_{j}$ source 190. $A \equiv (A_{j} \land A_{k})$ source 191. $A \equiv (A_{j} \lor A_{k})$ source 192. $A \equiv (A_{j} \to A_{k})$ source 193.

$A \equiv \forall x A_{j}$ source 195. $A \equiv \exists x A_{j}$ source 196.

Now we reason by cases. If $A$ source 198 is atomic then $A_{n} \in Frm (L)$ source 199 (Reader correction: The source prints the undefined language L sub zero here, although this theorem fixes the first-order language L. The reader uses L and preserves the printed source in the source view). Suppose instead that $A \equiv (A_{j} \land A_{k})$ source 200 (Reader correction: The source prints material-equivalence notation in this proof case, while the formation clauses and the argument require syntactic identity. The reader uses syntactic identity and preserves the printed source in the source view). By Initial-subsequence lemma, $⟨ A_{0}, \dots, A_{j} ⟩$ source 202 and $⟨ A_{0}, \dots, A_{k} ⟩$ source 202 are formation sequences for $A_{j}$ source 203 and $A_{k}$ source 203, respectively. Since these are proper initial subsequences of the formation sequence for $A$ source 205, they both have length less than $n$ source 205 (Reader correction: The source says the proper initial sequences have length less than n. The correct final-index statement is that they end at indices less than n; equivalently their lengths are less than n plus one). Therefore by the induction hypothesis, $A_{j}$ source 206 and $A_{k}$ source 206 are in $Frm (L)$ source 206 (Reader correction: The source again prints the undefined language L sub zero here. The theorem concerns the fixed first-order language L, which the reader uses while preserving the printed source in the source view), and by the definition of a formula, so is $(A_{j} \land A_{k})$ source 208. The other cases follow by parallel reasoning.

End of proof.

Formation sequences for terms have similar properties to those for formulas.

Equivalence for term formation sequences

$Trm (L)$ source 217 is the set of all $L$ source 217-strings $t$ source 217 such that there exists a term formation sequence for $t$ source 218.

source 215

Proof

Exercise.

End of proof.

Exercise on term formation sequences

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Equivalence for term formation sequences. Hint: use a similar strategy to that used in the proof of Equivalence of formula definitions.

source 225

There are two types of “junk” that can appear in formation sequences: repeated elements, and elements that are irrelevant to the construction of the formation or term. We can eliminate both by looking at minimal formation sequences.

Definition of minimal formation sequence

A formation sequence $⟨ A_{0}, \dots, A_{n} ⟩$ source 238 for a formula $A$ source 239 is a minimal formation sequence for $A$ source 239 if for every other formation sequence $s$ source 240 for $A$ source 240, the length of $s$ source 241 is greater than or equal to $n + 1$ source 241.

Similarly, a formation sequence $⟨ t_{0}, \dots, t_{n} ⟩$ source 243 for a term $t$ source 244 is a minimal formation sequence for $t$ source 245 if for every other formation sequence $s$ source 245 for $t$ source 245, the length of $s$ source 246 is greater than or equal to $n + 1$ source 246.

source 236

Note that a formula or term can have more than one minimal formation sequence, but they will contain exactly the same strings.

Formation-sequence characterization of subformulas

The following are equivalent:

$B$ source 257 is a sub-formula of $A$ source 257.
$B$ source 258 occurs in every formation sequence of $A$ source 258.
$B$ source 259 occurs in a minimal formation sequence of $A$ source 259.

source 253

Proof

Exercise.

End of proof.

Exercise on subformulas and formation sequences

Unsolved exercise. The source supplies the prompt only; no solution is added.

Prove Formation-sequence characterization of subformulas.

source 267

Free variable and sentence

Definition of free variable occurrences

The free occurrences of a variable in a formula are defined inductively as follows:

Case: $A$ source 18 is atomic: all variable occurrences in $A$ source 19 are free.
Case: the free variable occurrences of $A$ source 22 are exactly those of $B$ source 22.
Case: the free variable occurrences of $A$ source 25 are those in $B$ source 25 together with those in $C$ source 26.
Case: the free variable occurrences in $A$ source 29 are all of those in $B$ source 29 except for occurrences of $x$ source 30.
Case: the free variable occurrences in $A$ source 33 are all of those in $B$ source 33 except for occurrences of $x$ source 34.

source 13

Definition of bound variable occurrence

An occurrence of a variable in a formula $A$ source 39 is bound if it is not free.

source 38

Exercise on bound variable occurrences

Unsolved exercise. The source supplies the prompt only; no solution is added.

Give an inductive definition of the bound variable occurrences along the lines of Definition of free variable occurrences.

source 43

Definition of quantifier scope and binding

If $\forall x B$ source 49 is an occurrence of a subformula in a formula $A$ source 50, then the corresponding occurrence of $B$ source 50 in $A$ source 50 is called the scope of the corresponding occurrence of $\forall x$ source 52. Similarly for $\exists x$ source 52.

If $B$ source 58 is the scope of a quantifier occurrence $\forall x$ source 59 or $\exists x$ source 60 in $A$ source 60, then the free occurrences of $x$ source 61 in $B$ source 61 are bound in $\forall x B$ source 61 and $\exists x B$ source 62. We say that these occurrences are bound by the mentioned quantifier occurrence.

source 48

Examples of scope, binding, and free variables

Consider the following formula: $\exists v_{0} \underset{B}{{A^{2}}_{0} (v_{0}, v_{1})}$ source 69. $B$ source 72 represents the scope of $\exists v_{0}$ source 72. The quantifier binds the occurrence of $v_{0}$ source 73 in $B$ source 73, but does not bind the occurrence of $v_{1}$ source 74. So $v_{1}$ source 74 is a free variable in this case.

We can now see how this might work in a more complicated formula $A$ source 79: $\forall v_{0} \underset{B}{({A^{1}}_{0} (v_{0}) \to {A^{2}}_{0} (v_{0}, v_{1}))} \to \exists v_{1} \underset{C}{({A^{2}}_{1} (v_{0}, v_{1}) \lor \forall v_{0} \overset{D}{\neg {A^{1}}_{1} (v_{0})})}$ source 80. $B$ source 85 is the scope of the first $\forall v_{0}$ source 85, $C$ source 85 is the scope of $\exists v_{1}$ source 86, and $D$ source 86 is the scope of the second $\forall v_{0}$ source 87. The first $\forall v_{0}$ source 87 binds the occurrences of $v_{0}$ source 88 in $B$ source 88, $\exists v_{1}$ source 88 binds the occurrence of $v_{1}$ source 89 in $C$ source 89, and the second $\forall v_{0}$ source 89 binds the occurrence of $v_{0}$ source 90 in $D$ source 90. The first occurrence of $v_{1}$ source 90 and the fourth occurrence of $v_{0}$ source 91 are free in $A$ source 91. The last occurrence of $v_{0}$ source 92 is free in $D$ source 92, but bound in $C$ source 92 and $A$ source 92.

source 67

Definition of sentence

A formula $A$ source 96 is a sentence iff it contains no free occurrences of variables.

source 95

Substitution

Recursive definition of substitution in a term

We define $s [t / x]$ source 14, the result of substituting $t$ source 14 for every occurrence of $x$ source 15 in $s$ source 15, recursively:

Case: $s [t / x]$ source 17 is just $s$ source 17.
Case: $s [t / x]$ source 19 is also just $s$ source 19, provided $y$ source 20 is a variable and $y ≢ x$ source 20.
Case: $s [t / x]$ source 22 is $t$ source 22.
Case: $s [t / x]$ source 24 is $f (t_{1} [t / x], \dots, t_{n} [t / x])$ source 25.

source 13

Definition of a term being free for a variable

A term $t$ source 30 is free for $x$ source 30 in $A$ source 30 if none of the free occurrences of $x$ source 31 in $A$ source 31 occur in the scope of a quantifier that binds a variable in $t$ source 32.

source 29

Examples of terms free and not free for substitution

$v_{8}$ source 37 is free for $v_{1}$ source 37 in $\exists v_{3} {A^{2}}_{4} (v_{3}, v_{1})$ source 37
${f^{2}}_{1} (v_{1}, v_{2})$ source 40 is not free for $v_{0}$ source 40 in $\forall v_{2} {A^{2}}_{4} (v_{0}, v_{2})$ source 41

source 35

Recursive definition of substitution in a formula

If $A$ source 46 is a formula, $x$ source 46 is a variable, and $t$ source 46 is a term free for $x$ source 47 in $A$ source 47, then $A [t / x]$ source 47 is the result of substituting $t$ source 48 for all free occurrences of $x$ source 48 in $A$ source 48.

Case: $A [t / x]$ source 50 is $⊥$ source 51.

Case: $A [t / x]$ source 57 is $P (t_{1} [t / x], \dots, t_{n} [t / x])$ source 57.
Case: $A [t / x]$ source 60 is $t_{1} [t / x] = t_{2} [t / x]$ source 61.
Case: $A [t / x]$ source 63 is $\neg B [t / x]$ source 64.
Case: $A [t / x]$ source 67 is $(B [t / x] \land C [t / x])$ source 67.
Case: $A [t / x]$ source 71 is $(B [t / x] \lor C [t / x])$ source 71.
Case: $A [t / x]$ source 75 is $(B [t / x] \to C [t / x])$ source 75.
Case: $A [t / x]$ source 83 is $\forall y B [t / x]$ source 84, provided $y$ source 84 is a variable other than $x$ source 85; otherwise $A [t / x]$ source 85 is just $A$ source 86.
Case: $A [t / x]$ source 89 is $\exists y B [t / x]$ source 90, provided $y$ source 90 is a variable other than $x$ source 91; otherwise $A [t / x]$ source 91 is just $A$ source 92.

source 45

Explanation

Note that substitution may be vacuous: If $x$ source 97 does not occur in $A$ source 97 at all, then $A [t / x]$ source 98 is just $A$ source 98.

The restriction that $t$ source 100 must be free for $x$ source 100 in $A$ source 100 is necessary to exclude cases like the following. If $A \equiv \exists y x < y$ source 101 and $t \equiv y$ source 102, then $A [t / x]$ source 102 would be $\exists y y < y$ source 102. In this case the free variable $y$ source 103 is “captured” by the quantifier $\exists y$ source 104 upon substitution, and that is undesirable. For instance, we would like it to be the case that whenever $\forall x B$ source 106 holds, so does $B [t / x]$ source 106. But consider $\forall x \exists y x < y$ source 107 (here $B$ source 107 is $\exists y x < y$ source 107). It is a sentence that is true about, e.g., the natural numbers: for every number $x$ source 109 there is a number $y$ source 109 greater than it. If we allowed $y$ source 110 as a possible substitution for $x$ source 110, we would end up with $B [y / x] \equiv \exists y y < y$ source 111, which is false. We prevent this by requiring that none of the free variables in $t$ source 112 would end up being bound by a quantifier in $A$ source 113.

We often use the following convention to avoid cumbersome notation: If $A$ source 117 is a formula which may contain the variable $x$ source 117 free, we also write $A (x)$ source 118 to indicate this. When it is clear which $A$ source 118 and $x$ source 119 we have in mind, and $t$ source 119 is a term (assumed to be free for $x$ source 119 in $A (x)$ source 120), then we write $A (t)$ source 120 as short for $A [t / x]$ source 120. So for instance, we might say, “we call $A (t)$ source 121 an instance of $\forall x A (x)$ source 122.” By this we mean that if $A$ source 122 is any formula, $x$ source 123 a variable, and $t$ source 123 a term that's free for $x$ source 123 in $A$ source 124, then $A [t / x]$ source 124 is an instance of $\forall x A$ source 124.