[FOM] Arithmetic in ancestral logic

[Peter Smith]

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.

We know that the theory you get by augmenting first-order PA with such an 
operator and the axiom Ax(x = 0 v S*0x), where S is the successor relation, 
is categorical; so it semantically entails, in particular, every truth of 
the original language of PA. We also know that we can't give a sound and 
complete axiomatized deductive system for the logic of the * operator.

But we 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, 
ExEy(Rax & Rxy & Ryb) |- R*ab, and so on; 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?
-- 
Dr Peter Smith: Faculty of Philosophy, University of Cambridge

Gödel's Theorems: http://www.godelbook.net 
LaTeX for Logicians: http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/ 
Idle musings: http://logicmatters.blogspot.com