[FOM] Arithmetic in ancestral logic

[Andreas Blass]

Peter Smith wrote:

> Suppose we add to the logical apparatus of a first-order language an
> operator *, such that for a relational expression R, R* is  
> interpreted as
> the ancestral of R. . . . .  [W] e can give a partial  
> axiomatization. For a start, there will be a
> series of introduction rules like Rab |- R*ab, Ex(Rax & Rxb) |-  
> R*ab, ...  and a schematic elimination rule that says, in effect,  
> that R*ab implies that if a property is had by a and
> if x has it, and Rxy, then y has it, then b has it.
>
> Question: is PA augmented with the *-operator and the new axiom and  
> this
> sort of partial deductive system for the operator deductively  
> conservative
> over PA for the *-less wffs of PA's original language?

The answer is affirmative because the proposed deductive system can  
be interpreted in PA without changing anything in PA itself.   
Specifically, since PA provides a definable coding of finite  
sequences, we can interpret R*ab as the formula in the language of PA  
that says "there is a finite sequence that starts with a, ends with  
b, and has every pair of consecutive terms related by R".   
Admittedly, when this formula is interpreted in a nonstandard model  
of PA, it won't mean what R*ab is intended to mean, since the "finite  
sequence" mentioned in the formula might be finite only in the sense  
of the model, not really finite.  Nevertheless, this interpretation  
of R* satisfies the axioms proposed by Smith.  In particular, the  
schematic elimination rule will be satisfied precisely because it is  
schematic; the properties that it refers to will be only those  
properties that are definable in the language of PA, and for these my  
nonstandard interpretation of R* works just as well as the standard one.

Andreas Blass