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


MoeBlee wrote:
> Rupert wrote:
> > Usually there is no predicate "is a number".
>
> Then there's a fair amount of terminological slippage among writers.
> When I look up 'Peano arithmetic' or 'Peano axioms', even among
> contemporary sources, I usually get a list of five axioms that are
> pretty close to five of the nine axioms in Peano's paper (the other
> four are axioms about identity), as I cast this in first order logic
> with identity (I omit leading univesal quantifiers):
>
> 0 0-place function symbol
> S 1-place function symbol
> N 1-place predicate symbol
>
> Axioms:
>
> N0
>
> Nn -> NSn
>
> ~(Nn & 0=Sn)
>
> (Nn & Nk & Sn=Sk) -> n=k)
>
> (phi[0] & An(Nn -> (phi[n] -> phi[Sn]))) -> An(Nn -> phi[n])
>

The answer to this, I suppose, is that when writers present the axioms
informally they might throw around phrases like "is a number" which
don't actually show up in the formalization. This is about all I can
say unless you can point me to a specific writer.

> [I'm confused about Peano's own formulation as it is given on page 94
> of van Heijenoort's 'From Frege To Godel'. There, axiom 7 does not seem
> to state that S is 1-1. Is this the result of typos? Should the second
> '=' be the symbol for material implication instead, and the antecedent
> and consequent reversed?]
>

I'm afraid I can't comment on this until I've had a chance to look at
the source you cite.

> But Shoenfield on page 204 of 'Mathematical Logic' specifies Peano
> arithmetic as axiomatized in first order logic with identity and
> omitting leading universal quantifiers (cf. page 22 also):
>
> 0 0-place function symbol
> S 1-place function symbol
> + 2-place function symbol
> * 2-place function symbol
> < 2-place predicate symbol
>
> Sn not= 0
>
> Sn=Sk -> n=k
>
> n+0=n
>
> n+Sk=S(n+k)
>
> n*0=0
>
> n*Sk=(n*k)+n
>
> n not< 0
>
> n<Sk -> (n<k v n=k)
>
> (phi[0] & An(phi(n) -> phi[Sn])) -> An phi[n]
>
> So am I correct to take it that in current discussions, by 'Peano
> arithmetic', people mean the theory axiomatized by the above axioms?

Yes, except for the fact that < is usually taken as a defined symbol;
see below.

> (It could be a different set of axioms as long as it axiomatizes the
> same theory.) Also, that each of those axioms is independent of the set
> of the others? But, as to independence of primitive symbols, couldn't
> we take '<' as defined by:
>
> Df. n < k <-> Ej(j not= 0 & n+j=k)
>

Yes.

> > > Also, in set theory we prove that any two Peano systems are isomorphic.
> > > And, if I'm not mistaken, we prove that any two completely ordered
> > > fields are isomorphic. Yet, Lowenheim-Skolem tells us that for the
> > > axioms of Peano arithmetic there are non-isomorphic models, and for the
> > > axioms for a complete ordered field, there are non-isomorphic models.
> >
> > The axioms for a complete ordered field are second-order.
> > Loewenheim-Skolem applies to first-order theories.
>
> Yes, I overlooked that. To speak of bounds on subsets of the domain, we
> have to speak of sets, so that we're in set theory or we can cast the
> matter in second-order. But, to express subsets of the domain couldn't
> we use an axiom schema with phi, for formulas, instead of using sets or
> quantifying over second-order predicate symbols; thus we could express
> the axioms of a complete ordered field as a first order theory with
> axioms and one axiom schema?
>

You could do that; then it would have nonisomorphic models by
Loewenheim-Skolem. This is because the first-order axiom schema doesn't
capture the full power of the second-order axiom.

In fact we consider nonstandard models for the theory you're talking
about in nonstandard analysis.

> And, by noting for myself that indeed 'Peano arithmetic' denotes
> different things depending on the writer or context, I understood the
> rest of your comments.
>
> Thanks for you remarks. They have been helpful.
>
> 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?
    ... 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: What is the 1st order formal system known as PA?
    ... > I apologize that I'm too lazy to type all the axioms of PA; ... numbers' while also exploting 'member of' by using a bit of set theory. ... as a primitive predicate and reducing the axioms to just: ... S - 1-place function symbol ...
    (sci.logic)
  • Re: Can ZFC prove Addition is Associative?
    ... The Axiom of Infinity is Induction. ... The N of Peano world does not exist in the ZFC world. ... We can't get this far since you can't add the N given in the Peano ... axioms to the the sets given in the ZFC axioms. ...
    (sci.logic)