Can transfinite (strong) induction for N be derived from Peano's Axioms?
Dan Christensen
Dan
Barb Knox
"Dan Christensen" <dch...@allstream.net> wrote:
>I[f] so, can someone stetch out a proof starting from PA?
Transfinite induction can not even be EXPRESSED in PA. In the standard
model, it only expresses finite values.
AIUI, ZF minus the Axiom of Infinity is equivalent to PA.
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------
Ken Pledger
> Is so, can someone stetch out a proof starting from PA?
>
> Dan
Edmund Landau, "Grundlagen der Analysis" (also available in
English translation), Satz 27, proves that N is well-ordered. This can
easily be modified to give you strong induction.
Ken Pledger.
Ken Pledger
Ken Pledger <Ken.P...@mcs.vuw.ac.nz> wrote:
>
> .... This can
> easily be modified to give you strong induction....
I was assuming that Dan's "transfinite" was a slip, and he really
meant "strong".
Ken Pledger.
Arturo Magidin
Dan Christensen <dch...@allstream.net> wrote:
>If so, can someone sketch out a proof starting from PA?
If by "transfinite induction for N" you mean
"Let S be a subset of natural numbers such that
for all n, if ({k in N: k<n} is contained in S) then (n is in S).
Then S=N"
then this is equivalent to regular induction in N (which is Peano's
fifth axiom), and to the well-ordering principle.
THEOREM: The following are equivalent:
(i) Peano's fifth axiom
(ii) Strong induction for N (as stated above).
(iii) N is well-ordered.
Proof. (i)->(ii). Assume S satisfies the conditions given.
Let S' = { n in S: for all k in N, k<n -> k in S}.
We show that S' satisfies the assumptions of Peano's fifth axiom.
0 is in S, since {k in N: k<0} is empty. Since 0 is in S and so are
all "smaller natural numbers", it follows that 0 is in S'.
Assume n is in S'. Then n and all k<n are in S. Therefore, all k<n+1
are in S. By assumption on S, this means that n+1 is in S. Hence s+1
and all k<n+1 are in S, so n+1 is in S'.
Therefore, by Peano's fifth axiom, S' is equal to N. Since S' is
contained in S, and S is contained in N, it follows that N=S, as
desired.
(ii)->(iii) Let A be a nonempty subset of N. Then S=N-A is not all of
N, so by the contrapositive of (ii) there must exist n in S such that
{k in N : k<n } is contained in S and n is not in S.
Thus n is in A, and for all k in N, k<n -> k not in A.
Therefore, n is in A, and for all k in N, k in A -> n<= k; that is, A
has a least element. This is what we wanted to prove.
(iii)->(i). Let S be a subset of N such that 0 is in S, and for all n
in N, n in S -> (n+1) in S. We want to show that S=N.
Let A=N-S. If A is nonempty, then by well ordering it has a least
element k.
k is not equal to 0, since 0 is in S by assumption. So k = n+1 for
some n. Since n<k, and k is the least element of A, n is not in A.
So n is in S. Therefore, n+1 is in S. But n+1 = k is not in S. This
contradiction arises from assuming that A is nonempty. Therefore A is
empty, so N=S as desired.
QED
--
======================================================================
"It's not denial. I'm just very selective about
what I accept as reality."
--- Calvin ("Calvin and Hobbes")
======================================================================
Arturo Magidin
mag...@math.berkeley.edu
Bill Dubuque
>Dan Christensen <dch...@allstream.net> wrote:
>>
>> Can transfinite (strong) induction for N be derived from Peano's Axioms?
>> If so, can someone sketch out a proof starting from PA?
>
> If by "transfinite induction for N" you mean
>
> "Let S be a subset of natural numbers such that
>
> for all n, if ({k in N: k<n} is contained in S) then (n is in S).
>
> Then S=N"
>
> then this is equivalent to regular induction in N (which is
> Peano's fifth axiom), and to the well-ordering principle.
>
> THEOREM: The following are equivalent:
>
> (i) Peano's fifth axiom
> (ii) Strong induction for N (as stated above).
> (iii) N is well-ordered.
A subtle yet serious error lurks here - one that's quite common
in such logically naive arguments, as I mentioned here before [1].
First, the above theorem is meaningless without stating precisely
what base theory T you're assuming implicitly in the background.
I.e. what you're really proving is T,i => T,ii => T,iii => T,i.
Now T cannot include (i) = Peano's 5th axiom for else you would
be begging the principle when you prove T,iii => i. Therefore
your proof (iii)->(i) is erroneous because you have assumed that
every nonzero integer is a successor, a statement that requires
induction (Peano's 5th) in the standard Peano axiomatization
(a well-known fact - you even mentioned it here previously [2]).
Indeed, replacing Peano's 5th axiom with (iii) N is well-ordered
does not yield equivalent axioms for N since it is easily seen
to have other ordinal models, e.g. w + w = 1,2,3,...w,w+1,w+2,...
Note that in this model w is not a successor so that your proof
(iii) -> (i) does not apply, as expected since induction fails
on w + w. For much further discussion and references see my
prior post [1] of 1998/5/7. It also mentions other principles
often naively deemed equivalent to induction, e.g. pigeonhole.
--Bill Dubuque
[1] http://groups-beta.google.com/group/sci.math/msg/7d553d98e3f2d45c
http://google.com/groups?selm=y8zogx9...@nestle.ai.mit.edu
[2] http://groups-beta.google.com/group/sci.math/msg/f07ae64614c37c00
http://google.com/groups?selm=b8jrqa$2o0h$1...@agate.berkeley.edu
> Proof. (i)->(ii). Assume S satisfies the conditions given.
>
> Let S' = { n in S: for all k in N, k<n -> k in S}.
>
> We show that S' satisfies the assumptions of Peano's fifth axiom.
>
> 0 is in S, since {k in N: k<0} is empty. Since 0 is in S and so are
> all "smaller natural numbers", it follows that 0 is in S'.
>
> Assume n is in S'. Then n and all k<n are in S. Therefore, all k<n+1
> are in S. By assumption on S, this means that n+1 is in S. Hence s+1
> and all k<n+1 are in S, so n+1 is in S'.
>
> Therefore, by Peano's fifth axiom, S' is equal to N. Since S' is
> contained in S, and S is contained in N, it follows that N=S, as
> desired.
>
> (ii)->(iii) Let A be a nonempty subset of N. Then S=N-A is not all of
> N, so by the contrapositive of (ii) there must exist n in S such that
>
> {k in N : k<n } is contained in S and n is not in S.
>
> Thus n is in A, and for all k in N, k<n -> k not in A.
>
> Therefore, n is in A, and for all k in N, k in A -> n<= k; that is,
> A has a least element. This is what we wanted to prove.
>
> (iii)->(i). Let S be a subset of N such that 0 is in S, and for all n
> in N, n in S -> (n+1) in S. We want to show that S=N.
>
> Let A=N-S. If A is nonempty, then by well ordering it has a least
> element k.
>
> k is not equal to 0, since 0 is in S by assumption. So k = n+1 for
> some n. Since n<k, and k is the least element of A, n is not in A.
** ERROR ** your hypotheses needn't imply k is a successor, see above.
David C. Ullrich
<dch...@allstream.net> wrote:
>Is so, can someone stetch out a proof starting from PA?
Exactly what do you mean by "transfinite induction for N",
strong or otherwise?
>Dan
>
************************
David C. Ullrich
H. Enderton
>If so, can someone sketch out a proof starting from PA?
First of all, I'm assuming "transfinite" was unintended.
And that the topic is the strong induction schema:
If (forall n)[(forall m < n)phi(m) --> phi(n)], then (forall n)phi(n)
If my assumption is wrong, you can stop reading here.
Yes, all instances of strong induction are provable in PA.
Arturo Magidin already covered this, but let me rephrase the
argument.
Suppose we (working in PA) know
(*) (forall n)[(forall m < n)phi(m) --> phi(n)].
The key is to apply ordinary indunction to the statement
theta(n):
(forall m < n)phi(m).
Basis: theta(0). Vacuous; PA knows that nothing is less than 0.
Inductive step: Suppose we have theta(k). Then (*) is exactly
what we need to get theta(k+1). Details easy to fill in.
So we conclude forall n theta(n).
And then we get phi(n) from theta(n+1).
Done.
--Herb Enderton
Mitch Harris
>Dan Christensen <dch...@allstream.net> wrote:
>>If so, can someone sketch out a proof starting from PA?
>
>First of all, I'm assuming "transfinite" was unintended.
>And that the topic is the strong induction schema:
> If (forall n)[(forall m < n)phi(m) --> phi(n)], then (forall n)phi(n)
>If my assumption is wrong, you can stop reading here.
>
>Yes, all instances of strong induction are provable in PA.
How do you reconcile Bill Dubuque's complaints then?
--
Mitch (remove the q to email)
Arturo Magidin
Bill Dubuque correctly pointed out that I was mistaken in claiming
that PA1-PA4 + Well Ordering implied regular induction. However, the
proofs that PA1-PA4 + PA5 -> Strong induction and that PA1-PA4 +
Strong induction -> Well ordering were correct.
Dan Christensen
"Arturo Magidin" <mag...@math.berkeley.edu> wrote in message
news:cvj6rd$1m72$1...@agate.berkeley.edu...
> In article <ng8Td.29$g4....@tor-nn1.netcom.ca>,
> Dan Christensen <dch...@allstream.net> wrote:
>>If so, can someone sketch out a proof starting from PA?
>
> If by "transfinite induction for N" you mean
>
Yes, I did mean "STRONG induction." Sorry about the confusion.
>
> "Let S be a subset of natural numbers such that
>
> for all n, if ({k in N: k<n} is contained in S) then (n is in S).
>
> Then S=N"
>
> then this is equivalent to regular induction in N (which is Peano's
> fifth axiom), and to the well-ordering principle.
>
>
> THEOREM: The following are equivalent:
>
> (i) Peano's fifth axiom
> (ii) Strong induction for N (as stated above).
> (iii) N is well-ordered.
>
>
> Proof. (i)->(ii). Assume S satisfies the conditions given.
>
> Let S' = { n in S: for all k in N, k<n -> k in S}.
>
> We show that S' satisfies the assumptions of Peano's fifth axiom.
>
> 0 is in S, since {k in N: k<0} is empty. Since 0 is in S and so are
> all "smaller natural numbers", it follows that 0 is in S'.
>
> Assume n is in S'. Then n and all k<n are in S. Therefore, all k<n+1
> are in S.
It seems an intuitively "obvious" point, but what specific property of N can
be used here to prove all k<n+1 are in S?
Dan
Arturo Magidin
Dan Christensen <dch...@allstream.net> wrote:
>
>"Arturo Magidin" <mag...@math.berkeley.edu> wrote in message
>news:cvj6rd$1m72$1...@agate.berkeley.edu...
>> In article <ng8Td.29$g4....@tor-nn1.netcom.ca>,
>> Dan Christensen <dch...@allstream.net> wrote:
>>>If so, can someone sketch out a proof starting from PA?
>>
>> If by "transfinite induction for N" you mean
>>
>
>Yes, I did mean "STRONG induction." Sorry about the confusion.
>
>
>>
>> "Let S be a subset of natural numbers such that
>>
>> for all n, if ({k in N: k<n} is contained in S) then (n is in S).
>>
>> Then S=N"
>>
>> then this is equivalent to regular induction in N (which is Peano's
>> fifth axiom), and to the well-ordering principle.
>>
>>
>> THEOREM: The following are equivalent:
>>
>> (i) Peano's fifth axiom
>> (ii) Strong induction for N (as stated above).
>> (iii) N is well-ordered.
Please note Bill Dubuque's correction of the implication (iii)->(i)
(which does not hold as stated).
>> Proof. (i)->(ii). Assume S satisfies the conditions given.
>>
>> Let S' = { n in S: for all k in N, k<n -> k in S}.
>>
>> We show that S' satisfies the assumptions of Peano's fifth axiom.
>>
>> 0 is in S, since {k in N: k<0} is empty. Since 0 is in S and so are
>> all "smaller natural numbers", it follows that 0 is in S'.
>>
>> Assume n is in S'. Then n and all k<n are in S. Therefore, all k<n+1
>> are in S.
>
>It seems an intuitively "obvious" point, but what specific property of N can
>be used here to prove all k<n+1 are in S?
First prove by regular induction that there is no natural number
between n and n+1 for every natural number n. Also prove that the
natural order is a total ordering.
Then we can prove that:
{k in N : k<n} U {n} = {k in N : k< n+1}.
The left hand side is always included on the right hand side.
If they are not equal, then there exists m in N such that m<n+1, but m
is not smaller than n and m is not equal to n. By trichotomy (which
follows from the total ordering), m>n. Since there is no natural
number between n and n+1, then m> n+1 or m=n+1. But both possibilities
are impossible, since m<n+1. Therefore, the right hand side must be
included in the left hand side, proving equality.
(I hope...)
Dan Christensen
Perhaps there is an easier way, but I used induction to first prove that no
natural number is <1. Then it was easy to prove that there is no natural
number between n and n+1 using a simple proof by contradiction:
Suppose p<x<p+1
Then p+u=x and x+v=p+1 for some u and v in N.
Substituting, (p+u)+v=p+1
By associativity, p+(u+v)=p+1
Cancelling, u+v=1 and u<1, a contradiction.
Also prove that the
> natural order is a total ordering.
>
> Then we can prove that:
> {k in N : k<n} U {n} = {k in N : k< n+1}.
>
> The left hand side is always included on the right hand side.
>
> If they are not equal, then there exists m in N such that m<n+1, but m
> is not smaller than n and m is not equal to n. By trichotomy (which
> follows from the total ordering), m>n. Since there is no natural
> number between n and n+1, then m> n+1 or m=n+1. But both possibilities
> are impossible, since m<n+1. Therefore, the right hand side must be
> included in the left hand side, proving equality.
>
> (I hope...)
>
I was stuck on this proof for several days. Thanks again, Arturo.
Dan
Download DC Proof 1.0 at http://www.dcproof.com
Mitch Harris
>
>... I used induction to first prove that no natural number is <1.
Isn't 0 less than 1?
Arturo Magidin
Mitch Harris <har...@tcs.inf.tu-dresden.de> wrote:
>Dan Christensen <dch...@allstream.net> wrote:
>>
>>... I used induction to first prove that no natural number is <1.
>
>Isn't 0 less than 1?
Some people include 0 as a natural number; some people do not. It is
clear that Dan does not. It should be trivial for anybody to figure
out how to translate between elementary proofs done assuming 0 is a
natural number and ones assuming it is not.
Mitch Harris
> In article <38ena7F...@news.dfncis.de>,
> Mitch Harris <har...@tcs.inf.tu-dresden.de> wrote:
>
>>Dan Christensen <dch...@allstream.net> wrote:
>>
>>>... I used induction to first prove that no natural number is <1.
>>
>>Isn't 0 less than 1?
>
>
> Some people include 0 as a natural number; some people do not. It is
> clear that Dan does not.
Sure. But Peano did include 0 in his axioms.
> It should be trivial for anybody to figure
> out how to translate between elementary proofs done assuming 0 is a
> natural number and ones assuming it is not.
Sure, but you could do the same for "17" (*): all your proofs would
need special cases to deal with it.
(*) or some other arbitrary ..uh... number that simplifies theorem
staements and proofs considerably if you consider it part of the naturals.
--
Mitch Harris
(remove q to reply)
Arturo Magidin
Mitch Harris <har...@tcs.inf.tu-dresden.de> wrote:
>Arturo Magidin wrote:
>> In article <38ena7F...@news.dfncis.de>,
>> Mitch Harris <har...@tcs.inf.tu-dresden.de> wrote:
>>
>>>Dan Christensen <dch...@allstream.net> wrote:
>>>
>>>>... I used induction to first prove that no natural number is <1.
>>>
>>>Isn't 0 less than 1?
>>
>>
>> Some people include 0 as a natural number; some people do not. It is
>> clear that Dan does not.
>
>Sure. But Peano did include 0 in his axioms.
>
>> It should be trivial for anybody to figure
>> out how to translate between elementary proofs done assuming 0 is a
>> natural number and ones assuming it is not.
>
>Sure, but you could do the same for "17" (*): all your proofs would
>need special cases to deal with it.
Indeed, the collection of natural numbers greater than 17 are order
isomorphic to the natural numbers, so you can do that.
But the choices of starting at 0 or at 1 are both extremely common;
starting at 0 is more natural if you are coming from set theory, for
example, but traditionally the natural numbers did NOT include 0
(natural numbers were the positive integers).
G. A. Edgar
> >> Some people include 0 as a natural number; some people do not. It is
> >> clear that Dan does not.
> >
> >Sure. But Peano did include 0 in his axioms.
No, I think he started with 1.
What is the actual Peano reference?
--
G. A. Edgar http://www.math.ohio-state.edu/~edgar/
Dave Seaman
> Arturo Magidin wrote:
>> In article <38ena7F...@news.dfncis.de>,
>> Mitch Harris <har...@tcs.inf.tu-dresden.de> wrote:
>>
>>>Dan Christensen <dch...@allstream.net> wrote:
>>>
>>>>... I used induction to first prove that no natural number is <1.
>>>
>>>Isn't 0 less than 1?
>>
>>
>> Some people include 0 as a natural number; some people do not. It is
>> clear that Dan does not.
> Sure. But Peano did include 0 in his axioms.
No, he didn't.
>> It should be trivial for anybody to figure
>> out how to translate between elementary proofs done assuming 0 is a
>> natural number and ones assuming it is not.
> Sure, but you could do the same for "17" (*): all your proofs would
> need special cases to deal with it.
> (*) or some other arbitrary ..uh... number that simplifies theorem
> staements and proofs considerably if you consider it part of the naturals.
You could exclude all the numbers from 0 through 17 and still have an
inductive set. Just excluding 17 while keeping 16 would violate the
Peano axioms.
--
Dave Seaman
Judge Yohn's mistakes revealed in Mumia Abu-Jamal ruling.
<http://www.commoncouragepress.com/index.cfm?action=book&bookid=228>
Mitch Harris
>>>>Some people include 0 as a natural number; some people do not. It is
>>>>clear that Dan does not.
>>>
>>>Sure. But Peano did include 0 in his axioms.
>
> No, I think he started with 1.
> What is the actual Peano reference?
OK, I don't have the original reference.
Checking the references I do have (Kleene, Intro to Metamathematics,
ch 2, #7, Ebbinghaus, Flum, Thomas, Intro to Logic, sec 7.3) say 0.
Bill Dubuque
>Mitch Harris <har...@tcs.inf.tu-dresden.de> wrote:
>>Arturo Magidin wrote:
>>>
>>> Some people include 0 as a natural number; some people do not.
>>>
>>> out how to translate between elementary proofs done assuming
>>> 0 is a natural number and ones assuming it is not.
>>
>> Sure, but you could do the same for "17" (*): all your proofs would
>> need special cases to deal with it.
>
> Indeed, the collection of natural numbers greater than 17 are order
> isomorphic to the natural numbers, so you can do that.
Recall N may be presented as free algebra.
I quote from my prior post [1]:
Richard Carr <r...@columbia.edu> wrote:
|
| ... The Peano axioms are axioms for a model of the language <N;S;e>
| (or an extensions, thereof) where N is a set, S is a unary function
| symbol and e is a constant symbol.
| The axioms state that the interpretation of S, S^N is injective, that the
| interpretation of e, e^N is not in in the range of S^N and that if A is a
| subset of N such that e^N is in A and for every a in A, S^N(a) is in A,
| then A=N.
More elegantly a Peano algebra is simply the free P-algebra generated
by the empty set, where P is an algebra class comprised of one nullary
operation (the constant 0) and one unary operation (the successor S).
Note that no axioms are needed: a Peano algebra consists of the terms
0, S(0), S(S(0)), ... and freeness implies no two terms are equal.
One advantage of this viewpoint is that one may now apply general
results from the theory of free algebras, e.g. definition by
induction (recursion) is available, and Peano algebras are
unique up to isomorphism. Many good algebra textbooks present
this viewpoint, e.g. see Paul Cohn's Universal Algebra, Ch. VII.1.
--Bill Dubuque
[1] http://groups-beta.google.com/group/sci.math/msg/374d5af053fea0c2
http://google.com/groups?selm=y8zogwemw...@nestle.ai.mit.edu
Mitch Harris
> On Mon, 28 Feb 2005 10:57:26 +0100, Mitch Harris wrote:
>>Arturo Magidin wrote:
>>>
>>>Some people include 0 as a natural number; some people do not. It is
>>>clear that Dan does not.
>
>>Sure. But Peano did include 0 in his axioms.
>
> No, he didn't.
I didn't know that. Every presentation that I've seen uses 0 as the
base case. But I have no idea what Peano's original formulation was.
>>>It should be trivial for anybody to figure
>>>out how to translate between elementary proofs done assuming 0 is a
>>>natural number and ones assuming it is not.
>
>>Sure, but you could do the same for "17" (*): all your proofs would
>>need special cases to deal with it.
>
>>(*) or some other arbitrary ..uh... number that simplifies theorem
>>staements and proofs considerably if you consider it part of the naturals.
>
> You could exclude all the numbers from 0 through 17 and still have an
> inductive set. Just excluding 17 while keeping 16 would violate the
> Peano axioms.
I was just addressing the naming problem, whether it is more useful to
have 0 as a member of the naturals or not. The analogy with 17 is more
explicitly this: we could, by fiat, define X to be the numbers up to
16 and then all numbers reachable by successor from 18 (so that 17 is
not a member of X), and then we could rewrite all proofs about numbers
using X union {17} (because 16+1 = 17 and 17+1=18). And that would be
silly because we'd need all sorts of ugly cases to deal with the the
thing that just happens, by fiat, not to be named appropriately.
My point is (I suppose) that is, in the religious war between the "N
starts with 1" and "N starts with 0" camp, I side with the latter.
Or if that is troublesome, since excluding 0 from the naturals doesn't
break anything (it'll prevent lots of thms), but including it makes
lots more thms, why not just include 0?
r.e.s.
> Mitch Harris wrote:
>> Sure. But Peano did include 0 in his axioms.
>
> No, he didn't.
First he didn't, then later he did.
In 1889, when he first published them, he apparently didn't use 0:
"G. Peano, Principles of Arithmetic, Presented by a New Method. 1889.
[transl. in From Frege to Gödel, van Heijenoort, Harvard Univ. Press,
1971.]"
at http://www.math.uwaterloo.ca/~snburris/htdocs/scav/peano/peano.html
(The publication is cited in References. There is an obvious typo
re "1989" in the text of the webpage.)
In 1895 he did use 0, according to a Rivista di matematica extract at
http://www-gap.dcs.st-and.ac.uk/~history/Mathematicians/Peano.html
(which that site apparently incorrectly calls the "original" axioms).
--r.e.s.
Herman Rubin
G. A. Edgar <ed...@math.ohio-state.edu.invalid> wrote:
>> >> Some people include 0 as a natural number; some people do not. It is
>> >> clear that Dan does not.
>> >Sure. But Peano did include 0 in his axioms.
>No, I think he started with 1.
>What is the actual Peano reference?
If you use the formulation in Landau, the starting point
is not mentioned in the axioms themselves. One can then
start anywhere; Landau starts with 1 to postpone the
problem of not being able to divide by zero as long as
possible, to the real numbers.
Starting with 0, this problem will arise, and also the
characterization of x > y becomes
for some z NOT ZERO, x = y + z
and there are other similar problems. On the other hand,
if it is to be used to teach arithmetic, as it should,
it is important to have zero to discuss representations.
--
This address is for information only. I do not claim that these views
are those of the Statistics Department or of Purdue University.
Herman Rubin, Department of Statistics, Purdue University
hru...@stat.purdue.edu Phone: (765)494-6054 FAX: (765)494-0558
Arturo Magidin
Herman Rubin <hru...@odds.stat.purdue.edu> wrote:
>In article <280220050952480238%ed...@math.ohio-state.edu.invalid>,
>G. A. Edgar <ed...@math.ohio-state.edu.invalid> wrote:
>
>>> >> Some people include 0 as a natural number; some people do not. It is
>>> >> clear that Dan does not.
>
>>> >Sure. But Peano did include 0 in his axioms.
>
>>No, I think he started with 1.
>>What is the actual Peano reference?
>
>If you use the formulation in Landau, the starting point
>is not mentioned in the axioms themselves. One can then
>start anywhere; Landau starts with 1 to postpone the
>problem of not being able to divide by zero as long as
>possible, to the real numbers.
>
>Starting with 0, this problem will arise, and also the
>characterization of x > y becomes
>
> for some z NOT ZERO, x = y + z
>
>and there are other similar problems.
Though, if you are including zero because you are coming from set
theory, then chances are you will take the non-strict inequality
x >= y as the primitive order relation (and leave strict inequality as
the derived one), in which case you simply have
x>= y if and only if there exists some z such that x = y+z
and then you can define x>y as "x>=y and x not equal to y".
It's really just six of one and half a dozen of the other; they are
both common, in my experience.