*L*, 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.

_{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.

*I*assigns the usual meanings to the non-logical vocabulary of

_{A}*L*.

_{A}
The language

*L*represents numerical properties using (open) wff's containing one free variable. For example, the following wff of_{A}*L*represents the property of being even:_{A}∃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*represents relations between two (or more) numbers using (open) wff's containing two (or more) free variables. For example, the following wff of_{A}*L*represents the relation between x and y stated as "y is a multiple of x:"_{A}
∃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

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.

*L*to represent a property, the set of numbers that have this property must make this wff true according to_{A}*I*. More precisely, we say that a_{A}**property P is**if and only if, for every n:*expressed*by the open wff φ(x)- 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**if and only if, for every m and n:*expressed*by the open wff φ(x,y)- 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**if and only if, for every n:*captures*the property P by the open wff φ(x)- 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**if and only if, for every m and n:*captures*the relation R by the open wff φ(x,y)- 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.

## No comments:

## Post a Comment