Re: What is the 1st order formal system known as PA?

Nam Nguyen wrote:

> I apologize that I'm too lazy to type all the axioms of PA; it should
> be listed in a typical logic book.

I only mention this since I do see different formulations, especially
in the difference of whether 'x is a number' is expressed as a 1-place
predicate or whether it is expressed as 'x is a member of the set of
numbers' while also exploting 'member of' by using a bit of set theory.
So I am never sure what people mean when they refer to 'first order
PA'. Also, I am unclear of the ramifications of dropping 'is a number'
as a primitive predicate and reducing the axioms to just:

~En 0 = Sn

If Sn = Sk -> n = k

(phi(0) & An(phi(n) -> phi(n+)) -> An phi(n)

So I guess I took the title of this thread too literally.

Anyway, I take it that you're referring to a theory in which the
primitives are:

0 - 0-place function symbol
S - 1-place function symbol
N - 1-place predicate symbol

With axioms:

N0

An(Nn -> NSn)

~En(Nn & 0 = Sn)

Ank((Nn & Nk & Sn = Sk) -> n = k)

(phi[0] & An(Nn -> (phi[n] -> phi[Sn]))) -> An(Nn -> phi[n])

Is this correct?

> But what I think is relevant in my
> post is the unary function symbol S (designating the successor function)
> in "PA". Note that given any successor (1-1) function f in a domain of
> PA, one could always infer another successor (1-1) function f'. Which of
> f and f', should S designate then? The answer, imho, is that it depends
> on who is the beholder of PA.

You'd like some expert opinion about this. Though I'm not an expert,
I'd like to understand what you mean. (I got lost with your explanation
in your first post.) I could be wrong here, but if we assign a
structure for the language, then

N is a subset of the domain.
S is a function on the domain.
0 is a member of N.

But the axioms only provide that S restricted to N is 1-1 in the
structure. No? We don't know that S is 1-1 on the domain~N, right?

But what do you mean by 'we can infer another 1-1 function f''?

MoeBlee

.

Relevant Pages

  • Re: What is the 1st order formal system known as PA?
    ... common to see Peano arithmetic as having axioms not including those for the operations of addition and multiplication. ... These axioms can be expressed straightforwardly in the second order language with a symbol S for the successor function. ... the Paris-Harrington independence result mentioned is about first order Peano arithmetic. ... The function symbol S is only applicable to a natural number and produces a natural number; the function symbols + and * are only applicable to natural numbers and produce a natural number; the relation symbol "in" holds between a natural numner and a set. ...
    (sci.logic)
  • Re: What is the 1st order formal system known as PA?
    ... > Then there's a fair amount of terminological slippage among writers. ... > When I look up 'Peano arithmetic' or 'Peano axioms', ... I usually get a list of five axioms that are ... > 0 0-place function symbol ...
    (sci.logic)
  • Re: What is the 1st order formal system known as PA?
    ... all of which would share the same unary [successor] function symbol "S". ... There is a standard definition of PA and there's only one theory that ... having the same language L, satisfying Peano axioms [which means all have the same successor function symbol "S", among ...
    (sci.logic)
  • Re: What is the 1st order formal system known as PA?
    ... When I look up 'Peano arithmetic' or 'Peano axioms', ... S 1-place function symbol ... >> axioms for a complete ordered field, ...
    (sci.logic)
  • Re: The basic idea behind M theories
    ... A trial would be to define the predicate "universe" in the following ... Axioms assuring that the class of all universes is well ordered by ... contain x as a member and at the same time be a member of y, ...
    (sci.logic)
Quantcast