**1. Formal systems **

Before introducing first order logic, I want to present a “toy example” of the issues we will face, and the results we are after.

In a *formal system* we present a set of rules about manipulation of finite strings of symbols, and attempt to study which strings can be obtained through these manipulations.

Informally, this corresponds to the *syntactic* part of logic, and the beginning of proof theory.

I will follow an example from Richard Kaye’s book *The Mathematics of Logic*.

Denote the empty string by The reason for choosing this symbol will be explained later.

The example I want to study is a *tree system*. The name will be explained later.

We begin with a given subset Consider the following “game” where one can apply the following rules:

- (Axioms) One can write down any string
- (Extension) If can be written down, one can also write down (one or both of) and
- (Compression) If and can be written down, one can also write down

Given such and a the goal of the game is to see whether can be written down using the rules just described. In that case, we write

which can be read as “ can be derived from ” or “ is provable from ” or a variant of these expressions. (This is why we call *axioms* the strings in as they are the “basic assumptions” in our proofs.) We can think of as a (formal) theorem derivable from the set of *axioms*

A *(formal) proof* of from is then a sequence where:

- and
- Each is in , or comes from for some by applying the extension rule (i.e., or ), or comes from and for some by applying the compression rule (i.e., and ).

We can think of the proof as a certificate that, indeed, If does not prove we write

Some immediate observations are useful.

- Note first that if is a proof of some string from then each is also provable from as witnessed by the proof
- proves something iff
- iff for all

In logic, it is customary to write to denote falsehood. It is also standard that if one can prove something false, then one can prove anything. This explains why we are denoting by the empty string. One calls a system that proves anything *inconsistent*, and it is a desirable feature that is consistent. On the other hand, we want to be somewhat useful, so we can derive at least some statements from it.

Here is a simple example: iff begins with

One direction of this assertion is clear: The proof shows that can be derived from the given and repeated applications of the extension rule show now that any that begins with is indeed derivable.

On the other hand, an argument is needed to check that these are the only provable statements. Typically in these arguments, one proceeds by induction in either the length of proofs, or the length of the strings involved. Here we use induction on the length of proofs, to show that, for any any proof from of length is a proof of a string that begins with

Once the right induction hypothesis has been identified, the argument is in many cases straightforward, and that is indeed the case here: If is a proof of length then or and in both cases the result holds. Assume now the result for all proofs of length at most and suppose is a proof of length

Say If we are done. If comes from a previous by extension, then having a proof of length starts with by the induction hypothesis, and then so does since Finally, if comes from previous by compression, then and begin with by hypothesis. In particular, considering it follows that must begin with This completes the inductive argument, and therefore the proof.

(It is customary to refer to these statements about proofs as *metatheorems*, to help us distinguish between formal proofs (the strings such as above) and proofs (such as the argument of the last four paragraphs). One also talks about reasoning in the metatheory and similar expressions. For a while at least these distinctions should be obvious and hopefully do not lead to confusion.)

Now we proceed to establish some metatheorems explaining some of the properties of the formal system.

If then there is a finite such that

Of course, as above depends in general on

If then there is a proof of from where first rule (1) is used (perhaps several times), then rule (3) (perhaps none, perhaps several times), and finally rule (2) (perhaps none, perhaps several times).

*Proof:* Let be a proof of from We describe a procedure that transforms such a proof into another such proof We will argue that if we start with and iteratively apply the procedure, thus producing a sequence of proofs of

eventually (after finitely many steps) we reach a proof to which the procedure does not apply. We then argue that this means that is as in the statement of the fact.

First, say that has *property * iff is a proof of from where some application of rule (1) comes after applying either rule (2) or (3).

Suppose has property say

where is the first place where this occurs, i.e., but some with comes from extension or compression, and is least with this property. In this case, we say that is a *witness* to property in

For such an if replace with Otherwise, replace with

Note that, in either case, is a proof of from and Moreover, either does not have property or else property is witnessed in by some with

Second, say that has *property * iff is a proof of from that does not have property but there is in some application of rule (3) after some application of rule (2).

Suppose has property say

where is the first place where this occurs, i.e., is the result of applying compression to previous strings but some with is the result of applying extension to some with moreover, is least with this property. In this case, we say that witnesses property in

For such an consider and so and There are several cases:

**Case 1: **If both are in let be largest such that If replace with

Otherwise, replace with

**Case 2: **Either or comes from extension. Say it is so there is such that Then (Similarly if it is that comes from extension.) If replace with

Otherwise, replace with

**Case 3: **Neither nor comes from extension, but at least one of them comes from compression. Without loss, Note that in there are no applications of rule (2), by minimality of If replace with

Otherwise, replace with

Note that these cases are exhaustive, and that in all three cases, is a proof of from without property and Moreover, either does not have property or else property is witnessed in by some with

Finally, we describe the procedure: If has property apply the transformation explained in that case. If has property apply the transformation described in that case. Note that if has neither property, then it is a proof as wanted.

Now we explain that iterative application of this procedure, starting with should stop after finitely many steps. This is because each application of the procedure either shortens the length of the proof, or increases the size of the witnesses (which are bounded by the length of the proof). We are done.

*Typeset using LaTeX2WP. Here is a printable version of this post.*