Capturing numerical properties in a formal language of arithmetic

Peter Smith starts Chapter 4 by describing L_A, a formal language that is at the core of several AFTs (axiomatized formal theories) of arithmetic. Then Smith explains what it means for a formal language of arithmetic to "express" a numerical property and the stronger notion of "capturing" a numerical property.

Here is the definition of L_A:

• Logical vocabulary: the symbols for variables, the usual logical connectives and quantifiers, the identity (or equality) symbol, and parentheses.
• Non-logical vocabulary: the symbol for the constant 0, the unary successor function symbol S, and the binary function symbols + and ×.
• The numerals are 0, S0, SS0, SSS0, etc., which we will sometimes abbreviate 0, 1, 2, 3, etc., respectively. n represents the numeral for the integer value that n stands for. So, if n stands for 5, then n represents SSSSS0.
• Terms are numerical expressions. The set of terms includes 0 and any variable, as well as any expression built up from those using the functions S, + and ×. So, SS0 × y and S(x + Sn) are examples of terms. Closed terms are variable free.
• An atomic well-formed formula (or atomic wff) has the form σ = τ, where σ and τ are terms. Note that = is the only predicate in L_A.
• The wff's are formed from atomic wff's using the connectives and quantifiers, as usual.

The interpretation I_A assigns the usual meanings to the non-logical vocabulary of L_A.

The language L_A represents numerical properties using (open) wff's containing one free variable. For example, the following wff of L_A represents the property of being even:

∃v (SS0 × v = x)

where x is a free variable standing in for an even number. More precisely, the statement "n is even" would be represented by the wff: ∃v (SS0 × v = n) in which the numeral for n is substituted for all of the occurrences of x.

Similarly, the language L_A represents relations between two (or more) numbers using (open) wff's containing two (or more) free variables. For example, the following wff of L_A represents the relation between x and y stated as "y is a multiple of x:"

∃v (x × v = y)

where x and y are free variables. More precisely, the statement "m is a multiple of n" would be represented by the wff: ∃v (n × v = m).

For a wff of L_A to represent a property, the set of numbers that have this property must make this wff true according to I_A. More precisely, we say that a property P is expressed by the open wff φ(x) if and only if, for every n:

• If n has property P, then φ(n) is true according to I_A.
• If n does not have property P, then ¬ φ(n) is true according to I_A.

Similarly, we say that a relation R is expressed by the open wff φ(x,y) if and only if, for every m and n:

• If m has the relation R to n, then φ(m,n) is true according to I_A.
• If m does not have the relation R to n, then ¬ φ(m,n) is true according to I_A.

The fact that an AFT of arithmetic can express a numerical property or relation only depends on the expressive power of its interpreted formal language. It is independent of its proof system. Since we care very much about proofs, we do not only need for wff's to express numerical properties, we would also like for the AFT to prove these wff's. This is what the "capture" concept is about.

We say that an AFT T captures the property P by the open wff φ(x) if and only if, for every n:

• If n has property P, then T ⊢ φ(n).
• If n does not have property P, then T ⊢ ¬ φ(n).

Similarly, we say that an AFT T captures the relation R by the open wff φ(x,y) if and only if, for every m and n:

• If m has the relation R to n, then T ⊢ φ(m,n).
• If m does not have the relation R to n, then T ⊢ ¬ φ(m,n).

Smith emphasizes that the way he uses the words "express" and "capture" is his own, but that there is no standard terminology in this area anyway. He likes the word 'capture' for the stronger property because 'CAPture' is a good mnemonic for 'CAse-by-case Proof.' I think what he means here is that, in the definition for 'capturing P' above, each φ(n) is proved separately for each value of n, which is very different from proving a single, universally quantified wff that would represent the entire set of numbers with property P.

In conclusion:

• Capturing a property (or relation) is stronger than expressing it: A language may be expressive enough to express a property (or relation) but its axioms and inference rules may not be strong enough to capture it, that is, to prove it (even case by case).
• However, if T is a sound AFT and T captures P with the wff φ(x), then φ(x) does express P, since, in a sound theory, every theorem is true in its own interpretation.