Re: Peano's second axiom.

On Jun 30, 12:54 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:
On Jun 30, 11:05 am, Zaljo...@xxxxxxxxx wrote:

Primitives: 0,number,S
Axiom: number(0)
Axiom: Ax( number(x) -> number(Sx) )
Axiom: Axy( (number(x) & number(y)) -> ((Sx = Sy) -> x=y) )
Axiom: Ax ( number(x) -> ~0=Sx )
Axiom: Ax (( Ay( yex -> number(y)) & 0ex & Ay( yex->Syex ) ) ->
Az( number(z)-> zex ) ).

You used the symbol 'e' but neither declared it as primitive nor
defined it.

Oh, yes, e is among the primitives sure.

Zuhair





One thing I don't really understand is why 0 is among the list of
primitives in PA.

Why not having only two primitives: Number and Successor 'S'.

having the axiom:

Axiom of first number : E!x(number(x) & Ay(number(y) -> ~x=S(y))).

and then defining 0 as

x=0 <-> (number(x) & Ay(number(y) -> ~x=S(y))).

There is no need to put 0 among the list of primitives.

In this way we'll have four axioms and two primitives.

In first order PA, there is no need to have 'is a number' as a
primitive. And your theory doesn't cover addition and multiplication.
And your symbol 'e' is unaccounted for.

In first order PA we don't need a primitive 'is a number' as in set
theory we don't need a primitive 'is a set'.

MoeBlee- Hide quoted text -

- Show quoted text -


.

Relevant Pages

  • Re: A type theory with a universal set in it.
    ... primitives: N,S,k,<,e,F. ... N is a primitive one place predicate symbole that stands for 'natural ... is an axiom. ... is inconsistent. ...
    (sci.logic)
  • Re: Peanos second axiom.
    ... Ok, suppose you have a set theory T, that is extension of first order ... S. And you have the following axiom in T ... you use the symbol 'e' as well as primitives 'M' and 'S' ... Your theory T doesn't prove ~xeM, ...
    (sci.logic)
  • Theory X.
    ... primitives: N,S,k,<,e,F,G. ... N is a primitive one place predicate symbole that stands for 'natural ... is an axiom. ... Axiom schema of Comprehension: for every formula Q in which x is ...
    (sci.logic)
  • A type theory with a universal set in it.
    ... primitives: N,S,k,<,e,F. ... N is a primitive one place predicate symbole that stands for 'natural ... is an axiom. ... Also Frege's definition of cardinality as an equivalence class of all ...
    (sci.logic)
  • Re: A type theory with a universal set in it.
    ... primitives: N,S,k,<,e,F. ... N is a primitive one place predicate symbole that stands for 'natural ... is an axiom. ... Also Frege's definition of cardinality as an equivalence class of all ...
    (sci.logic)