|
|
It might just possibly help to contrast and compare (though this should
already be quite clear from e.g. Daryl's posts):
Take Baby Arithmetic, whose language is quantifier free, whose
non-logical vocab is "0", "S", "+" and ".", and which has as axioms all
the instances of the metalinguistic schemas
0 =/= Sx
Sx = Sy --> x = y
x + 0 = x
x + Sy = S(x + y)
x . 0 = 0
x . Sy = x.y + x
where x, y are treated as placeholders to be replaced by standard
numerals. Contrast BA with Q-, which is Robinson Arithmetic minus one
axiom: It's language is L_A, the standard first-order language of
arithmetic, with quantifier/variables, and its axioms are
(Ax)0 =/= Sx
(Ax)(Ay)(Sx = Sy --> x = y)
(Ax)x + 0 = x
(Ax)(Ay)x + Sy = S(x + y)
(Ax)x . 0 = 0
(Ax)(Ay)x . Sy = x.y + x
Here x, y are genuine object-language variables. Then it is familiar
that BA is a negation-complete theory (it can decide every wff of its
impoverished language), while Q- isn't -- it can't prove either (Ax)0 +
x = x or its negation.
Now contrast two other theories: first take the one you get by
extending BA's language with a function sign for each p.r. function,
and giving appropriate axiom schemata for each function. Call that
PRA--. Contrast what you get by adding to Q-'s logically richer
language a function sign for each p.r. function, and adding appropriate
quantified axioms; and also add in induction for quantifier-free
formulae. That is (one version of) PRA. Then, again, PRA-- is a
negation complete theory (it can decide every wff of its logically
impoverished language). But PRA is negation incomplete -- by Gödel's
theorem.
There's a wrinkle: it comes to much the same (since all the quantifiers
in the axioms are prenex universal) to recast PRA in a language which
has free variables, but no explicit quantifiers. And then its
non-induction axioms can look just like PRA--'s schemata (especially
here where we can't e.g. use sans-serif for a formal object language,
and greek letters for metalinguistic place-holders). But no matter. PRA
and PRA-- are two different theories: the first has induction, and is
negation-incomplete; the second can't express generalities at all, so
hasn't induction, and it is negation complete. OK?
|
|