[FOM] Arithmetic in ancestral logic
Andreas Blass
ablass at umich.edu
Thu May 4 12:58:27 EDT 2006
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
More information about the FOM
mailing list