Strong Induction Follows From Weak Induction: Formal Proof

[Dan Christensen]

THEOREM

Strong induction follows from weak (ordinary) induction


Weak Induction:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in a => b+1 in a]
=> ALL(b):[b in n => b in a]]]


Strong Induction:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n => [c<=b => c in a]] => b+1 in a]]
=> ALL(b):[b in n => b in a]]]


Full Text (99 lines) at https://www.dcproof.com/StrongInductionHolds.htm


Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[j4n bur53]

You should also give credit that this was asked by
me some weeks ago.

Actually its only Weak => Pseudo Strong.

How about Weak => Real Strong AND Real Strong => Weal.
Where Real Strong is this one:

Real Strong:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>

[c<b => c in a]] => b in a]]

=> ALL(b):[b in n => b in a]]]

Can you do it in DC Proof?

[j4n bur53]

Any way, cool to see you doing new proofs, instead
of hunting cranks. Keep up the good work!

[Dan Christensen]

On Monday, April 15, 2019 at 2:22:48 AM UTC-4, j4n bur53 wrote:

> On Monday, April 15, 2019 at 7:15:17 AM UTC+2, Dan Christensen wrote:
> > THEOREM
> >
> > Strong induction follows from weak (ordinary) induction
> >
> >
> > Weak Induction:
> >
> > ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in a => b+1 in a]
> > => ALL(b):[b in n => b in a]]]
> >
> >
> > Strong Induction:
> >
> > ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> > => [0 in a & ALL(b):[b in n => [ALL(c):[c in n => [c<=b => c in a]] => b+1 in a]]
> > => ALL(b):[b in n => b in a]]]
> >
> >
> > Full Text (99 lines) at https://www.dcproof.com/StrongInductionHolds.htm
> >
> >

> Actually its only Weak => Pseudo Strong.
>

Wrong.

> How about Weak => Real Strong AND Real Strong => Weal.
> Where Real Strong is this one:
>
> Real Strong:
>
> ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> => [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
> [c<b => c in a]] => b in a]]
> => ALL(b):[b in n => b in a]]]
>

I think you will find that the partial ordering on N is implicit in most definitions.

[Dan Christensen]

Along with the use of b+1 as in weak induction.

[j4n bur53]

Well the are two things missing:

- The backward direction, strong induction
implies weak induction,

- The the correct forward direction, weak
induction implies strong induction, where
strong induction is this here:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
[c<b => c in a]] => b in a]]
=> ALL(b):[b in n => b in a]]]

Otherwise my challenge is not satsified.

[j4n bur53]

The challenge is to use no weak induction
when proving strong induction implies weak
induction, and to adhere to strong induction

defined as here, where we dont have any
+1. So you would need to define +1 from <,
or somesuch not sure.

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
[c<b => c in a]] => b in a]]
=> ALL(b):[b in n => b in a]]]

Some fellow Arturo Magidin, who has posted in the
past on sci.logic:
https://groups.google.com/d/msg/sci.logic/BKSQBjm6Jjs/B74b7zipAgAJ

Has some opinion how the two relate. But I have
some doubts that without further axioms about
< things work out:

Strong Induction proofs done with Weak Induction
https://math.stackexchange.com/a/108377/4414

[j4n bur53]

You can also read on MSE how strong induction, the
one I was refering to, was defined:

Strong induction: Let S⊆N be such that:
For all n∈N , if {k∈N∣k<n}⊆S then n∈S.
Then S=N.

Strong Induction proofs done with Weak Induction
https://math.stackexchange.com/a/108377/4414

I don't see any =< and +1. I only see <.
With =< and +1 it is much too simple. Also
doing only one direction is simple.

[Dan Christensen]

> Well the are two things missing:
>
> - The backward direction, strong induction
> implies weak induction,
>

Not going to happen. Strong induction requires addition to be defined on N. And to construct addition on N, you require weak induction (from Peano's Axioms).

> - The the correct forward direction, weak
> induction implies strong induction, where
> strong induction is this here:
>
> ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> => [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
> [c<b => c in a]] => b in a]]
> => ALL(b):[b in n => b in a]]]
>

This is an equivalent definition, but I haven't seen it in a quick search of online sources. Informal definitions usually have an inductive hypothesis something like supposing P(n) for n<= k and then requiring proof of P(k+1).

> Otherwise my challenge is not satsified.
>

Challenge??? I left it as a homework assignment for you, Jan. I even gave you a helpful link to get you started. I'm afraid I will have to give you a zero on this one. You might be get partial credit if you can recast my proof using your unusual definition of strong induction.

[j4n bur53]

Actually its possible to prove. Strong => Weak.
Arturo Magidin says so, but he doesn't deliever
all the information to do so.

I agree with Arturo Magidin on other grounds,
its just a theorem from set theory about
omega, just recall that x e y means x < y.

But well, it wouldn't be a challenge if it would
be too obvious, without some fill in the blanks
puzzling. Right?

[j4n bur53]

If you follow all the theorems about omega
on metamath.org, you will get an idea how
to do it.

But I didn't have enough time myself to do a
write up, and strip down the metamath.org
stuff so that it

happens in a smaller world, with < .

[Dan Christensen]

On Monday, April 15, 2019 at 12:54:25 PM UTC-4, j4n bur53 wrote:
> Actually its possible to prove. Strong => Weak.

I think you would have to arbitrarily define addition on N to start with. Give it a try, though it seems pointless to me.

[j4n bur53]

I don't know, I don't think having seen addition
in meta math concerning omega.

This could be a pointless obsession of yours?

[Dan Christensen]

On Monday, April 15, 2019 at 1:25:29 PM UTC-4, j4n bur53 wrote:

>
> On Monday, April 15, 2019 at 7:07:21 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 15, 2019 at 12:54:25 PM UTC-4, j4n bur53 wrote:
> > > Actually its possible to prove. Strong => Weak.
> >
> > I think you would have to arbitrarily define addition on N to start with. Give it a try, though it seems pointless to me.

> I don't know, I don't think having seen addition
> in meta math concerning omega.
>

I don't think I have seen a definition of strong induction that does not make use of addition on N.

[j4n bur53]

Well I guess you havent seen much in your life.
This definition here doesn't use any addition:

https://en.wikipedia.org/wiki/Epsilon-induction

Restrict it to omega, and you get strong
induction. Where do you see addition?

[j4n bur53]

Oh, I forgot, you don't have a regularity axiom
in DC Proof. Thats indeed a blind spot.

[j4n bur53]

You are not batshit stupid, aren't you? This is
not another Dan-O-Matic? I am not talking to a
plastic tree?

I'm talking to a plastic tree...
https://www.youtube.com/watch?v=TDX3X5iC3nc

I mean you are not John Gabriel, that has only seen
books from the outside. Did you ever see a set
theory book from the inside?

But I must admit, I don't know yet how it all
works out. There are different candidates for
axioms about < to make strong induction work.

Unfortunately the fellow Arturo Magidin isn't
precise and complete enough on MSE. But concerning
the strong induction schema, its like Arturo

Magidin wrote, without addition, even not the
least addition, like a successor +1:

"Strong induction: Let S⊆N be such that:
For all n∈N , if {k∈N∣k<n}⊆S then n∈S.
Then S=N."
Strong Induction proofs done with Weak Induction
https://math.stackexchange.com/a/108377/4414

You can easily verify that the above is epsilon
induction, since in von Neuman ordinals,
x e y is the same as x < y.

[Dan Christensen]

On Monday, April 15, 2019 at 2:41:41 PM UTC-4, j4n bur53 wrote:

> On Monday, April 15, 2019 at 8:25:34 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 15, 2019 at 1:25:29 PM UTC-4, j4n bur53 wrote:
> >
> > >
> > > On Monday, April 15, 2019 at 7:07:21 PM UTC+2, Dan Christensen wrote:
> > > > On Monday, April 15, 2019 at 12:54:25 PM UTC-4, j4n bur53 wrote:
> > > > > Actually its possible to prove. Strong => Weak.
> > > >
> > > > I think you would have to arbitrarily define addition on N to start with. Give it a try, though it seems pointless to me.
> >
> > > I don't know, I don't think having seen addition
> > > in meta math concerning omega.
> > >
> >
> > I don't think I have seen a definition of strong induction that does not make use of addition on N.
> >

> Well I guess you havent seen much in your life.
> This definition here doesn't use any addition:
>
> https://en.wikipedia.org/wiki/Epsilon-induction
>

Nice try. It might work if you want to play around with von Neumann ordinals (not everyone's cup of tea as you must know). I will stick to the ordinary natural numbers that you find in most math textbooks. There, you must at least implicitly define addition before you can do strong induction. Thanks anyway.

[Dan Christensen]

On Monday, April 15, 2019 at 2:57:13 PM UTC-4, j4n bur53 wrote:

> Magidin wrote, without addition, even not the
> least addition, like a successor +1:
>
> "Strong induction: Let S⊆N be such that:
> For all n∈N , if {k∈N∣k<n}⊆S then n∈S.
> Then S=N."

In this case, addition is buried in the definition of <. Usually something like:

A x, y in N: [x < y <=> E z in N: [z=/=0 & x+z=y]]

> Strong Induction proofs done with Weak Induction
> https://math.stackexchange.com/a/108377/4414
>
> You can easily verify that the above is epsilon
> induction, since in von Neuman ordinals,
> x e y is the same as x < y.
>

Too weird for most. Thanks anyway.

[j4n bur53]

I have never seen element hood x e y, defined
from addition. How do you define addition in
set theory and from it element hood?

How do you show that addition is well defined,
if you only have strong induction,

and the following is missing:
- successor
- weak induction

Recall the backward task is: Strong => Weak,
and not Weak+Strong => Weak.

Canadian Big Foot, you are as usual tripping
along some Dan-O-Matik, and do not understand
the challenge, even not a micro ounze of it.

[j4n bur53]

Again these are the two tasks:

- Strong => Weak,
and not Weak+Strong => Weak (Dan-O-Matik nonsense)
- Weak => Strong

Where Strong means:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
[c<b => c in a]] => b in a]]
=> ALL(b):[b in n => b in a]]]

This is usually proved by use of another principle.
The least element principle which says:

LeastElementPrinciple:
Every non empty set of natural numbers S,
has a least element n, n e S.

The proof then usually works its way as follows:

1) Weak => LeastElementPrinciple
2) LeastElementPrinciple => Strong
3) Strong => Weak

Or maybe the other way around, don't remember. This
is the classical text book way to show these things.
You find plenty PDFs about it on the internet.

[j4n bur53]

If you google you find really plenty PDFs, involving
the Least Element Principle as well. Thats not a lie.
I just made a test, and quickly got, and a proof that

your are just an ingnorant bastard not knowing the
real strong induction principle, only your pseudo form,
here is the real strong induction principle again:

THE LEAST ELEMENT PRINCIPLE AND STRONG INDUCTION
The Strong Induction Principle says:
Let P(n) be a proposition form over N. If for each n ∈ N,
(P(m) for all m ∈ N such that m < n) implies P(n)
then P(n) is true for each n ∈ N.
http://people.reed.edu/~jerry/131/leastelt.pdf

So the approach and claims by Arturo Magidin are
a little unusual. But maybe through a formalization
we can shed more light on the issue from all sides.

[j4n bur53]

In Arturo Magidin its not apparent whether he invokes
the LEAST ELEMENT PRINCIPLE. I have to check, maybe it
can be extracted, seen somehow in the

extra axiom he demands. Of course a formalization would
also have the advantage over an informal verbose proof,
that we would clearer see what

is demanded from set theory.

For example in your present proof "Pseudo Strong =>
Weak", you use set theory to get the set q from
the set p, you use comprehension:

18 ALL(a):[a e q <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]

Split, 16

Comprehension is called subset axiom in DC Proof.
But your "Pseudo Strong => Weak" proof is pretty
useless, to say the least.

It is pointless since it doesn't show something
for Real Strong induction, only something much
easier for Pseudo Strong induction.

[j4n bur53]

The LEAST ELEMENT PRINCIPLE is of course the same
as well ordering, which brings us back to epsilon
induction. But again talking to a plastic

tree here is pretty useless. Maybe another time,
in 10 years or so, when you have grown up,
together with your DC proof.

[j4n bur53]

Prior hint:

On Monday, March 18, 2019 at 12:34:48 AM UTC+1, j4n bur53 wrote:
> If you have a day without Herpes Pimples, you
> could prove the following 1)=>2)=>3)=>1)
> 1) Weak induction on N
> 2) Wellordering of N
> 3) Strong induction on N

https://groups.google.com/d/msg/sci.math/BoFgMITP5XQ/9C3rh9FqAAAJ

[Dan Christensen]

On Monday, April 15, 2019 at 4:02:51 PM UTC-4, j4n bur53 wrote:
> I have never seen element hood x e y, defined
> from addition. How do you define addition in
> set theory and from it element hood?
>

No idea. And don't really care. Sorry.

> How do you show that addition is well defined,
> if you only have strong induction,
>

As above.

> and the following is missing:
> - successor
> - weak induction
>
> Recall the backward task is: Strong => Weak,
> and not Weak+Strong => Weak.
>

It is not a question that interests me very much, so I have assigned it to you as homework, Jan. Check out the link I gave you originally. I find that people just want proof that strong induction is valid. They generally accept ordinary (weak) induction as given in Peano's Axioms.

[j4n bur53]

Well of course, its difficult to admit an
error. But fact is, despite that you found a
link to pseudo strong induction,

even from www.oxfordmathcenter.com what ever
this means, its not real strong induction.
Thats just some nonsense, I dont know who

wrote it, Ms. Christina Lee?

You should better check your sources...

On Monday, April 15, 2019 at 10:34:17 PM UTC+2, Dan Christensen wrote:
> ... faux excuses ...

[j4n bur53]

Thats just a godaddy website from some chipmunks:

whois.godaddy.com
Domain Name: OXFORDMATHCENTER.COM
Registry Domain ID: 1734012901_DOMAIN_COM-VRSN
Registrar WHOIS Server: whois.godaddy.com
Registrar URL: http://www.godaddy.com
Registrant Organization:
Registrant State/Province: Georgia
Registrant Country: US

beautiful campus in Atlanta, Georgia's
historic Druid Hills neighborhood
http://www.emory.edu/home/index.html

Oxford is somewhere else:
http://www.ox.ac.uk/

[j4n bur53]

I don't know whether its even legal that
they call themselves oxford math center.

I didn't check other stuff on their website,
about the quality of its content.

[j4n bur53]

They repeat the same error here:
http://www.oxfordmathcenter.com/drupal7/node/114

but they mention well ordering.

[Dan Christensen]

On Monday, April 15, 2019 at 4:57:48 PM UTC-4, j4n bur53 wrote:

> even from www.oxfordmathcenter.com what ever
> this means, its not real strong induction.
> Thats just some nonsense, I dont know who
>

Bullshit. Nothing wrong with it. Certainly nothing eccentric about it. N

> wrote it, Ms. Christina Lee?
>
> You should better check your sources...
>

I looked at several, top-rated websites, looking for definitions and proofs of strong induction. The only variations seem to be the "first number" (either 0, 1 or an arbitrary number m_0). All seemed to use addition implicitly, e.g. P(k+1).

[j4n bur53]

Well this here has the correct strong induction:

THE LEAST ELEMENT PRINCIPLE AND STRONG INDUCTION
The Strong Induction Principle says:
Let P(n) be a proposition form over N. If for each n ∈ N,
(P(m) for all m ∈ N such that m < n) implies P(n)
then P(n) is true for each n ∈ N.
http://people.reed.edu/~jerry/131/leastelt.pdf

So successor used. Correct strong induction is more
challenging and more interesting. There are a lot of
fine points, you don't get

with pseudo strong induction. But who am I talking
to, a plastic tree. Anyway no use to explain to a
Canadian bigfoot what strong induction is.

[j4n bur53]

Corr.:

No successor used

[j4n bur53]

Canadian bigfoot principle:

The canadian bigfoot does not understand something at t=0

You can explain a canadian bigfoot that his view at
t=n was wrong, and he might change his view at t=n+1,
but nevertheless he will be still wrong at t=n+1

---------------------------------------------------------

The canadian bigfoot will never understand

[j4n bur53]

In correct strong induction, all there is, is <, there
is no successor. Successor is something from weak
induction.

If you mix the two, like you do in pseudo strong
induction, you mix two principles. You mix these
two principles:

- Strong, for two numbers n and m, I can say
whhether one is smaller than the other, i.e. n < m.

- Weak, for two numbers n and m, I can say
whether one directly follows the other, i.e. n+1 = m

In real strong induction makes exclusively use of
the first principle, saying whether something is
smaller or not.

Pseudo strong induction mixes both principles,
saying whether something is smaller or equal or
not and saying whether something directly follows

something else. You get problems to perform
proper back and forth proofs, when you use pseudo
strong induction.

Pseudo strong induction doesn't allow you to
analyse the situation properly.

[Dan Christensen]

On Monday, April 15, 2019 at 5:38:43 PM UTC-4, j4n bur53 wrote:
> In correct strong induction, all there is, is <, there
> is no successor. Successor is something from weak
> induction.
>

If the top-rated sites are any indication, you usually have something like:

P(0) & P(1) & ... P(k) => P(k+1)

Perhaps you are upset that I had to do your homework for you? Get over it, Jan. It's OK.

[j4n bur53]

Nope you don't have this, because you have no successor.
Successor is forbidden in strong induction. Strong
induction doesn't know about such a principle.

You even don't know that there is a predecessor.
You would first need to prove this. What you wrote
makes use of a predecessor:

P(0) & P(1) & ... P(k-1) => P(k)

Read Arturo Magidin please:

However, if we add a further property, namely
For every 𝑛∈ℕ, either 𝑛=0 or else there exists
𝑚∈ℕ such that 𝑛=𝑠(𝑚);

Thats the predecessor property. But this would
be already a derived property, which only holds
inside omega.

Strong induction is not based on predecessor,
it only says:

forall n(n<k => P(n)) => P(k)

I don't know. Whats wrong with you? Dan-O-Matik
stupidity again?

[j4n bur53]

Normally you are not batshit stupid. But now
your are really blind as a bat. I mean we already
did here on sci.logic prove

that every number has a predecessor. How did you
prove it, via weak induction or via strong induction?
Can you prove it in proper correct strong induction?

When you can prove that every number has predecessor
in proper correct strong induction, then you are
already half way of:

Proper Correct Strong => Weak

But proving pseudo strong induction implies weak
induction is nothing. You have already predecessor,
and therefore its not interesting.

The only interesting thing is proving proper
correct strong induction implies weak induction,
and not some nonsense pseodo strong induction

implies weak induction, as you did now. Thats
just chipmunk irrelevant nonsense, without any
true mathematical content.

[j4n bur53]

Corr.:

You proved weak => pseodo strong. Well also
not very interesting. Everything which is pseodo
strong is not extremly interesting.

It is practically relevant, since in practice,
in many proves one falls back to pseodo
strong, whereby it is doubtfull what

the sequence P(0),..,P(n-1) should be. Do we
suddently have lists? Or inference rules with
arbitrary premisses, even varying (variadic)?

See also:

Course-of-Value Induction in Cedille
Denis Firsov, Larry Diehl, Christopher Jenkins, and Aaron Stump
https://arxiv.org/pdf/1811.11961.pdf

[Dan Christensen]

On Monday, April 15, 2019 at 6:10:54 PM UTC-4, j4n bur53 wrote:

> On Monday, April 15, 2019 at 11:57:58 PM UTC+2, Dan Christensen wrote:
> > On Monday, April 15, 2019 at 5:38:43 PM UTC-4, j4n bur53 wrote:
> > > In correct strong induction, all there is, is <, there
> > > is no successor. Successor is something from weak
> > > induction.
> > >
> >
> > If the top-rated sites are any indication, you usually have something like:
> >
> > P(0) & P(1) & ... P(k) => P(k+1)
> >
> > Perhaps you are upset that I had to do your homework for you? Get over it, Jan. It's OK.
> >

> Nope you don't have this, because you have no successor.

Yeah, I really do.

ALL(a):[Set(a) & ALL(b):[b in a => b in n]

=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n => [c<=b => c in a]] => b+1 in a]]

=> ALL(b):[b in n => b in a]]]

> Successor is forbidden in strong induction.

You REALLY seem to be losing it here, Jan. Get a grip, man!

[j4n bur53]

Thats forbidden in strong induction. Strong induction
doesn't read as follows:

Pseudo Strong Induction:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
[c<=b => c in a]] => b+1 in a]]
=> ALL(b):[b in n => b in a]]]

Strong induction doesn't make any use of successor.
Its only this one:

Real Strong Induction:

ALL(a):[Set(a) & ALL(b):[b in a => b in n]
=> [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>

[c<b => c in a]] => b in a]]

=> ALL(b):[b in n => b in a]]]

Can you proof "Weak => Real Strong" AND "Real Strong
=> Weak". Can you do this in DC Proof? This was
the challenge.

Can you do it, yes or no?

Dan Christensen schrieb:

[j4n bur53]

Take your time. How many weeks did it take you to
prove "Weak => Pseodo Strong". 4 Weeks?

So lets check back in Summer 2019 again.

j4n bur53 schrieb:

[j4n bur53]

Hint Nr. 2: You don't need +1 if you have <.

This is quite standard and stereotypical found in
some of the set theory proofs, don't remember "Zorns
lemma" or something.

If you have well ordering, respectively LEAST ELEMENT
PRINCIPLE, then every non-empty S, has a least element
n, n e S. We can write n = min(S).

Now successor is simply:

m+1 := min({k e N | m < k})

(In one of the proofs of Zorns lemma the role of min is
replaced by choice function, but the idea is the same,
how do we get some successors? See also:
https://en.wikipedia.org/wiki/Zorn's_lemma#Proof_sketch )

j4n bur53 schrieb:

[j4n bur53]

And further:

n = min(S)

Is easily formalizable as:

n e S /\ forall j (j e S => n < j \/ n = j)

j4n bur53 schrieb:

[Dan Christensen]

On Monday, April 15, 2019 at 7:50:00 PM UTC-4, j4n bur53 wrote:
> Hint Nr. 2: You don't need +1 if you have <.
>

I wondered about that, too, but the usual practice does seem to be to use +1 and =<. Maybe because it makes strong induction look superficially more like what students are used to in regular (weak) induction -- a good reason IMHO. Students have a hard enough time with regular induction.

> This is quite standard and stereotypical found in
> some of the set theory proofs, don't remember "Zorns
> lemma" or something.
>
> If you have well ordering, respectively LEAST ELEMENT
> PRINCIPLE, then every non-empty S, has a least element
> n, n e S. We can write n = min(S).
>
> Now successor is simply:
>
> m+1 := min({k e N | m < k})

Not interested in von Neumann's ordinals. Neither are most math textbooks it would seem, and for good reason. It seems like something cooked up by someone who doesn't spend a lot of their time actually writing mathematical proofs, and can get away with making simple things needlessly complicated. IMHO for what it's worth.

[Dan Christensen]

On Monday, April 15, 2019 at 6:59:36 PM UTC-4, j4n bur53 wrote:
>
> Dan Christensen schrieb:
> > On Monday, April 15, 2019 at 2:41:41 PM UTC-4, j4n bur53 wrote:
> >
> >> On Monday, April 15, 2019 at 8:25:34 PM UTC+2, Dan Christensen wrote:
> >>> On Monday, April 15, 2019 at 1:25:29 PM UTC-4, j4n bur53 wrote:
> >>>
> >>>>
> >>>> On Monday, April 15, 2019 at 7:07:21 PM UTC+2, Dan Christensen wrote:
> >>>>> On Monday, April 15, 2019 at 12:54:25 PM UTC-4, j4n bur53 wrote:
> >>>>>> Actually its possible to prove. Strong => Weak.
> >>>>>
> >>>>> I think you would have to arbitrarily define addition on N to start with. Give it a try, though it seems pointless to me.
> >>>
> >>>> I don't know, I don't think having seen addition
> >>>> in meta math concerning omega.
> >>>>
> >>>
> >>> I don't think I have seen a definition of strong induction that does not make use of addition on N.
> >>>
> >
> >> Well I guess you havent seen much in your life.
> >> This definition here doesn't use any addition:
> >>
> >> https://en.wikipedia.org/wiki/Epsilon-induction
> >>
> >
> > Nice try. It might work if you want to play around with von Neumann ordinals (not everyone's cup of tea as you must know). I will stick to the ordinary natural numbers that you find in most math textbooks. There, you must at least implicitly define addition before you can do strong induction. Thanks anyway.
> >

> Thats forbidden in strong induction. Strong induction
> doesn't read as follows:
>
> Pseudo Strong Induction:
>
> ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> => [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
> [c<=b => c in a]] => b+1 in a]]
> => ALL(b):[b in n => b in a]]]
>
> Strong induction doesn't make any use of successor.
> Its only this one:
>
> Real Strong Induction:
>
> ALL(a):[Set(a) & ALL(b):[b in a => b in n]
> => [0 in a & ALL(b):[b in n => [ALL(c):[c in n =>
> [c<b => c in a]] => b in a]]
> => ALL(b):[b in n => b in a]]]
>

Again, if the top-rated website on the proofs of strong induction are anything to go by, this is NOT the usual presentation. Google it yourself if you don't believe me. Usually, definitions of strong induction seem to use successors (e.g. k+1) and implicitly at least make use of the usual partial ordering on N. More like my proof.

Deal with it, Jan. It's so weird how you are obsessing over this simple fact.

[j4n bur53]

What top-rated sites are you refering to. Can you show
us? Meanwhile, what is so difficult in a justification
of "Real Strong <=> Weak"?

Can you do it DC Proof, or not?

[j4n bur53]

Easter holidays comming, no regular work on friday and
monday, once of a lifetime chance to use your brains,

instead of posting a shitload of nonsense about
top-rated sites and other irrelevant lame excuses.

[Dan Christensen]

> What top-rated sites are you refering to. Can you show
> us?

Here are the top 4 on Google:

http://www.math.ucsd.edu/~benchow/Week2notesmore.pdf

http://www.cs.cornell.edu/courses/cs2800/2011fa/Lectures/induction.pdf

http://www.oxfordmathcenter.com/drupal7/node/485

https://brilliant.org/wiki/strong-induction/

> Meanwhile, what is so difficult in a justification
> of "Real Strong <=> Weak"?
>
> Can you do it DC Proof, or not?
>

Haven't tried. Seems pointless since I would need to use weak induction from Peano's Axioms to construct addition and the usual ordering on N on which strong induction is based.

You seem to have a lot of time on your hands. Why don't you try to prove it in DC Proof? You can use my proof as a template. The Oxford College page has an informal proof. I've done all the hard work for you. As I recall, I had assigned both proofs to you as homework several weeks ago. Time to start pulling your weight, Jan. ;^)

[j4n bur53]

Your on the wrong track with your addition obsession.
And what is so top-rated on these 4 sites, showing
pseudo strong induction?

Here are 4 sites, that show the real strong induction:

Jerry Shurman Professor
http://people.reed.edu/~jerry/131/leastelt.pdf

Jireh Loreaux Assistant Professor
http://siue.edu/~jloreau/courses/math-223/notes/sec-well-ordering.html

MATC project at Dartmouth
http://www.dartmouth.edu/~matc/DiscreteMath/IV.7.pdf

Karen E. Smith, Keeler Professor
http://www.math.lsa.umich.edu/~kesmith/295handout3.pdf

Your are just a lazy ass. If you solve the problem
during easter holiday, this would show that your
are not the slow poke, that you have demonstrated

so far. Do we need to wait till summer 2019?

[FredJeffries]

Real shame that someone can pose as a computer programmer in the 21st century and not know the difference between the increment operation and the addition operation nor understand the concepts behind them...

[Dan Christensen]

On Wednesday, April 17, 2019 at 5:28:18 PM UTC-4, j4n bur53 wrote:
> Your on the wrong track with your addition obsession.
> And what is so top-rated on these 4 sites, showing
> pseudo strong induction?
>
> Here are 4 sites, that show the real strong induction:
>

"Real" strong induction??? Wow! You must have looked long and hard for these links, but I think I will stick to what appears to be the most commonly used form of the definition. Thanks anyway.

[j4n bur53]

So you only give us one direction of pseudo strong
induction. Even not both direction. And even not
for real strong induction. Thats pretty poor.

Whats the teaching behind DC proof? Lean and
cheap, like Mc Donalds?

[j4n bur53]

Also I agree with FredJeffries, there must be some
further confusion involved. Weak uses only successor,
and not addition.

I guess you mean addition because you want define
less than equal from it? This might work for one
direction, but the other direction,

I dont know. One road map to get proofs would be,
to split the proof into 3 sub proofs:

1) Weak => LeastElementPrinciple

2) LeastElementPrinciple => Strong

3) Strong => Weak

Or maybe the other way around, don't remember. This
is the classical text book way to show these things.
You find plenty PDFs about it on the internet.

Can you do this classical text book in DC Proof?

[Dan Christensen]

On Wednesday, April 17, 2019 at 8:04:05 PM UTC-4, j4n bur53 wrote:
> Also I agree with FredJeffries, there must be some
> further confusion involved. Weak uses only successor,
> and not addition.
>

No confusion on my part. Using Peano's Axioms and a bit of set theory you can prove the existence of the addition function on N. You will also be able to define 1=S(0) and prove S(x)=x+1. Then you can recast induction in terms of x+1 instead of S(x) as I did in my proof. You can also then define <= (or <) in terms of addition on N.

> I guess you mean addition because you want define
> less than equal from it?

[snip]

Yes. Ax, y in N: [x<=y <=> Ez in N: x+z=y]

Or Ax, y in N: [x<y <=> Ez in N: [z=/=0 & x+z=y]].

Where would addition, < and <= on N come from without Peano's 5 Axioms and its weak induction? Maybe YOU could start with first-order PA that defines addition from the start -- not something that interests me.

[j4n bur53]

Canadian Bigfoot wrote: "> Where would addition, <

and <= on N come from without Peano's 5 Axioms
and its weak induction?"

Thats the challenge, one way to prove it,
is to split the proof into 3 sub proofs:

1) Weak => LeastElementPrinciple

2) LeastElementPrinciple => Strong

3) Strong => Weak

Can you do it in DC Proof? This is the

classical text book way to show these
things. You find plenty PDFs about

it on the internet.

[FredJeffries]

On Wednesday, April 17, 2019 at 7:49:25 PM UTC-7, Dan Christensen wrote:
> On Wednesday, April 17, 2019 at 8:04:05 PM UTC-4, j4n bur53 wrote:
> > Also I agree with FredJeffries, there must be some
> > further confusion involved. Weak uses only successor,
> > and not addition.
> >
>
> No confusion on my part. Using Peano's Axioms and a bit of set theory you can prove the existence of the addition function on N. You will also be able to define 1=S(0) and prove S(x)=x+1. Then you can recast induction in terms of x+1 instead of S(x) as I did in my proof. You can also then define <= (or <) in terms of addition on N.
>
>
> > I guess you mean addition because you want define
> > less than equal from it?
>
> [snip]
>
> Yes. Ax, y in N: [x<=y <=> Ez in N: x+z=y]
>
> Or Ax, y in N: [x<y <=> Ez in N: [z=/=0 & x+z=y]].
>
> Where would addition, < and <= on N come from without Peano's 5 Axioms and its weak induction? Maybe YOU could start with first-order PA that defines addition from the start -- not something that interests me.

Why do they need to come from anywhere?

Where do YOUR 5 Peano 'Axioms' and that 'little bit of set theory' come from? Presumably, you were handed them on tablets of titanium from out of the holy volcano.

https://www.futilitycloset.com/2019/04/18/unquote-602/

[Dan Christensen]

On Thursday, April 18, 2019 at 5:19:10 AM UTC-4, j4n bur53 wrote:

> On Thursday, April 18, 2019 at 4:49:25 AM UTC+2, Dan Christensen wrote:
> > On Wednesday, April 17, 2019 at 8:04:05 PM UTC-4, j4n bur53 wrote:
> > > Also I agree with FredJeffries, there must be some
> > > further confusion involved. Weak uses only successor,
> > > and not addition.
> > >
> >
> > No confusion on my part. Using Peano's Axioms and a bit of set theory you can prove the existence of the addition function on N. You will also be able to define 1=S(0) and prove S(x)=x+1. Then you can recast induction in terms of x+1 instead of S(x) as I did in my proof. You can also then define <= (or <) in terms of addition on N.
> >
> >
> > > I guess you mean addition because you want define
> > > less than equal from it?
> >
> > [snip]
> >
> > Yes. Ax, y in N: [x<=y <=> Ez in N: x+z=y]
> >
> > Or Ax, y in N: [x<y <=> Ez in N: [z=/=0 & x+z=y]].
> >
> > Where would addition, < and <= on N come from without Peano's 5 Axioms and its weak induction? Maybe YOU could start with first-order PA that defines addition from the start -- not something that interests me.
> >

>

> Thats the challenge, one way to prove it,
> is to split the proof into 3 sub proofs:
>
> 1) Weak => LeastElementPrinciple
>
> 2) LeastElementPrinciple => Strong
>
> 3) Strong => Weak
>

If you want to formally develop number theory without Peano's axioms, have at it. I prefer doing things the easy way. Thanks any way.

> Can you do it in DC Proof? This is the
> classical text book way to show these
> things.

In my experience, most if not all textbooks that present an axiomatic approach developing number theory will start in Peano's 5 Axioms (including weak induction) and set theory. But you are, of course, free to try out your unconventional approach and see if it works.

[Dan Christensen]

On Thursday, April 18, 2019 at 8:27:42 AM UTC-4, FredJeffries wrote:
> On Wednesday, April 17, 2019 at 7:49:25 PM UTC-7, Dan Christensen wrote:
> > On Wednesday, April 17, 2019 at 8:04:05 PM UTC-4, j4n bur53 wrote:
> > > Also I agree with FredJeffries, there must be some
> > > further confusion involved. Weak uses only successor,
> > > and not addition.
> > >
> >
> > No confusion on my part. Using Peano's Axioms and a bit of set theory you can prove the existence of the addition function on N. You will also be able to define 1=S(0) and prove S(x)=x+1. Then you can recast induction in terms of x+1 instead of S(x) as I did in my proof. You can also then define <= (or <) in terms of addition on N.
> >
> >
> > > I guess you mean addition because you want define
> > > less than equal from it?
> >
> > [snip]
> >
> > Yes. Ax, y in N: [x<=y <=> Ez in N: x+z=y]
> >
> > Or Ax, y in N: [x<y <=> Ez in N: [z=/=0 & x+z=y]].
> >
> > Where would addition, < and <= on N come from without Peano's 5 Axioms and its weak induction? Maybe YOU could start with first-order PA that defines addition from the start -- not something that interests me.
>
> Why do they need to come from anywhere?
>
> Where do YOUR 5 Peano 'Axioms' and that 'little bit of set theory' come from?

Mostly Cantor, Dedekind and Peano.

[Dan Christensen]

It's so weird, almost crank-like, that you can find anything controversial in such a commonly used definition.

[FredJeffries]

I find nothing controversial in the definition.

[Dan Christensen]

Ummmm... OK. Perhaps you are in the wrong thread, Fred?


Dan

[j4n bur53]

This threads new title is ingnorance is bliss.
Come on, you can do it a proof "Real Strong <=>
Weak". I mean what is DC Proof worth?

[j4n bur53]

Well you could do your DC proofs blindly,
like most of your DC proofs, without much
deeper understanding. Or as Timothy

Gowers's puts it:

"fluency first and understanding later"

How Craig Barton wishes he’d taught maths
Timothy, Gowers's - December 22, 2018
https://gowers.wordpress.com/2018/12/22/how-craig-barton-wishes-hed-taught-maths/#more-6435

There are a lot of DC proofs around, which
are just nonsense. For example the "verification"
of modal logic in DC proof. They also

lack a backward direction. Pretty useless.

[Julio Di Egidio]

On Friday, 19 April 2019 16:54:40 UTC+2, j4n bur53 wrote:

> Well you could do your DC proofs blindly,
> like most of your DC proofs, without much
> deeper understanding.

Sure, but your objections without substance are at least as uninteresting.

Can you point out any specific issues with his system or results?
Conversely, can we learn anything by looking more carefully at the
putative line that separates a bunch of essentially arbitrary symbols
from a mathematical formal system proper??

I mean, he is a fucking spammer and always in denial, but just empty
polemics aren't useful either, and eventually become the other side
of the same spamming coin...

Julio

[Dan Christensen]

On Friday, April 19, 2019 at 10:54:40 AM UTC-4, j4n bur53 wrote:

>
> On Friday, April 19, 2019 at 2:52:19 AM UTC+2, j4n bur53 wrote:
> > This threads new title is ingnorance is bliss.
> > Come on, you can do it a proof "Real Strong <=>
> > Weak". I mean what is DC Proof worth?
> >

> Well you could do your DC proofs blindly,
> like most of your DC proofs, without much
> deeper understanding. Or as Timothy
>
> Gowers's puts it:
>
> "fluency first and understanding later"
>
> How Craig Barton wishes he’d taught maths
> Timothy, Gowers's - December 22, 2018
> https://gowers.wordpress.com/2018/12/22/how-craig-barton-wishes-hed-taught-maths/#more-6435
>
> There are a lot of DC proofs around, which
> are just nonsense. For example the "verification"
> of modal logic in DC proof. They also
>
> lack a backward direction. Pretty useless.

I see you are STILL struggling with the definition of strong induction, Jan.

If you want to develop number theory without Peano Axioms (with its weak induction), maybe our friend WM can help you. (HA, HA, HA!!!)

[Me]

On Friday, April 19, 2019 at 6:31:32 PM UTC+2, Dan Christensen wrote:

> If you want to develop number theory without Peano Axioms (with its weak
> induction), maybe our friend WM can help you. (HA, HA, HA!!!)

Agree, Jan and WM really should join forces! :-)

[j4n bur53]

What makes you think I struggle with a definition?
There are two definitions:

Definition 1:

ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e a]] => b+1 e a]]
=> ALL(b):[b e n => b e a]]]

Definition 2:

ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e n => [ALL(c):[c e n => [c<b => c e a]] => b e a]]
=> ALL(b):[b e n => b e a]]]

A proof based on defintion 1 is rather trivial. And
further a proof based on definition 1, without the
reverse direction is pretty useless.

What would show some proficiency would be a proof
based on defintion 2, and both directions. In such
a proof for strong induction, < would

be the only primitive.

[j4n bur53]

You understand what "both directions" means,
don't you? Showing only one direction means

proving only "A => B". Showing "both directions"
means proving "A <=> B", respectivaly "A => B"

and "B => A". If you have questions feel free to ask.

[j4n bur53]

Why is a one direction based on definition 1 trivial?
Well it contains already +1, the successor.
But the point of showing "Strong <=> Weak" is not

to obtain a rather trival result, and it is
not only proving one direction. So the real challenge
here is to use definition 2, and of course showing

both direction, and not only one direction.

[Dan Christensen]

See my reply to your identical posting at The Zoo (sci.math) just now.


Dan

[j4n bur53]

Dan-O-Matik wrote:
> > Definition 2:
> >
> > ALL(a):[Set(a) & ALL(b):[b e a => b e n]
> > => [0 e a & ALL(b):[b e n => [ALL(c):[c e n => [c<b => c e a]] => b e a]]
> > => ALL(b):[b e n => b e a]]]
> >
>

> Requires addition and related <. Essentially equivalent definitions.

How do you define addition, if you have only
Strong Induction, Definition 2?

You don't have Weak Induction already. Strong
Induction means this axiom is missing:

Induction Principle Peano, is missing in Strong Induction
x e S /\ forall x (x e N => x e S => x+1 e S) =>
forall y (y e N => x e S)

Can you show us? Why is addition a+b needed,
and not successor +1?

[j4n bur53]

When you have Peano Induction aka Weak
Induction, you can define addition via

this here for example:

x + 0 = x
x + y' = (x + y)'

But you also need successor. And you can show
that + is uniquely defined.(*)

But in Strong induction you have only <, no
successor and no addition +.

(*) Famously proved by Dedekind 1888
126. Satz der Definition durch Induction
http://www.opera-platonis.de/dedekind/Dedekind_Was_sind_2.pdf

https://de.wikipedia.org/wiki/Richard_Dedekind#Werk

What happened after 1888?

[Dan Christensen]

On Friday, April 19, 2019 at 3:27:46 PM UTC-4, j4n bur53 wrote:
> Dan...

See my reply to your identical posting just now in The Zoo (sci.math)


Dan

[j4n bur53]

Dan-O-Matik halucinated:

> > You don't have Weak Induction already.

> You do actually. You should really acquaint
> yourself with Peano's Axioms at
> http://mathworld.wolfram.com/PeanosAxioms.html (see Axiom 5)

Well the problem setup is such that you do
not have weak induction, if you prove
this direction:

Strong Induction => Weak Induction

You only have weak induction, if you prove
this direction:

Weak Induction => Strong Induction

Whats wrong with you?

[Dan Christensen]

On Friday, April 19, 2019 at 5:48:46 PM UTC-4, j4n bur53 wrote:
> Dan...

See my reply to your identical posting just now at The Zoo (sci.math)


Dan

[j4n bur53]

Canadian Bigfoot halucinated from within his
Zoo. As a crank, he likes to be in the sci.math
crank Zoo:
> Like I said, if you want to develop number
> theory without Peano's Axiom's, I suggest
> you team up with WM.

Well if you prove "Strong => Weak", you recreate
Peano from something else.

Is this some Dan-O-Matik nonsense again?

The proof is not that difficult. You can do it,
maybe use your brains.

[j4n bur53]

Hint: Have a closer look at ordinals maybe.
They are also based on <, since e is <.

[j4n bur53]

Here is the answer what happened after 1888:

A kind of cambrian explosion happened, in
formal methods AND arithmetic. To mention
a few approachs that are not good old Peano:

- Frege, Humes Principle, its more
cardinality based arithmetic

- Cantor, Zermelo, set theory, its more
ordinals based arithmetic

- Conway, surreals, its more
tree based arithmetic

- What else?

- Other stuff, Gödels incompletness deals
with arithmetic, some Recursion theory deals
with arithmetic.

Anyway, maybe the hurdle "Strong => Weak" problem
can be solved via Conway? I find

4. Preliminaries III: s-hierarchical ordered structures
<A,+,0> abelian group and <A,<> ordered binary trees.
https://arxiv.org/pdf/1512.04001.pdf

Not sure. Was more expecting something towards Cantor.

[j4n bur53]

"The Cambrian explosion or Cambrian radiation was
an event approximately 541 million years ago in
the Cambrian period when most major animal phyla
appeared in the fossil record. It lasted for about
20–25 million years and resulted in the divergence
of most modern metazoan phyla. The event was
accompanied by major diversification of
other organisms."
https://en.wikipedia.org/wiki/Cambrian_explosion

What happened in formal methods AND arithmetic is
only around 100 years old.

[j4n bur53]

Canadian bigfoot, may I ask you a question. Since you
idolize Peanos axiom so much, and since Peanos axiom 5
is weak induction, why can you not proof:

1) Weak => Least Element Principle

This would bring us already closer to "Strong <=>
Weak". You sure you know anything about Peano?
For "Strong <=> Weak" we would only need these
missing pieces:

2) Least Element Principle => (Real) Strong

3) (Real) Strong => Weak

You could also try other paths, to arrive at
"Strong <=> Weak".

[Dan Christensen]

On Friday, April 19, 2019 at 6:40:53 PM UTC-4, j4n bur53 wrote:
> Hint: Have a closer look at ordinals maybe.
> They are also based on <, since e is <.
>

Thanks, but no thanks. I prefer to develop number theory starting from Peano's Axioms (including weak induction) as most textbooks seem to do. None start with strong induction. And very few start with von Neumann ordinals -- for very good reasons.

[j4n bur53]

I dont think you did anything with Peano so far. Can
you prove at least the following:

1) Weak => Least Element Principle

Or is DC proof totally useless?

[j4n bur53]

I dont find a lot of applications of Peano via DC
Proof, although you do repeatedly do name dropping

of it. Friedrich Gauss is attributed the following quote:

Mathematics is the queen of the sciences
and arithmetic is the queen of mathematics.

[j4n bur53]

Here is a proof sketch "Weak => Least Element Principle".
Dont know whether this is the classical text book
approach, thats just a morning shower idea.

a) Separation lemma. The Least Element Principle
says that every non empty set S has a minimal
element. We could first proof that a non
empty set S, has at least some element k,

we do not need to know what element it is,
but we can proof that any of these
elements k, separates the set S into two
sets S' and S'' where:

S' = { j e S | j<k \/ k=j }

S'' = { j e S | j>k }

b) Finite set lemma: We could prove via induction
that for finite sets the Least Element Principle
holds. So we take sets with n-elements, and
show by Weak induction, that if an n-elements set
has a minimum than an n+1 element set has a minium

Since a 1 element set has a minimum, via Weak
induction it should follow that every finite
set has a minum.

c) Combine a) and b) for an arbitrary set S,
which can now be finite or infinite, we can
separate it into S' and S''. S' will be finite,
and has a minimum. We can show that the minimum
is also the mimimum of S.

Q.E.D.

[j4n bur53]

But possibly, by googling, we could compare the
proof idea, with other proof ideas floating around.

This would bring us closer to check off one sub proof.

[j4n bur53]

Here are other proof ideas:

Well-Ordering and Mathematical Induction
https://math.stackexchange.com/q/432293/4414

[j4n bur53]

My morning shower proof is this proof:

When can we do induction? - Tobias Kildetoft

Proof: Let A⊆X be a non-empty subset and
let a∈A. Now the set {x∈X∣x≤a}∩A is finite
and non-empty and thus has a minimal element,
which is a minimal element in A.

https://math.blogoverflow.com/2015/03/10/when-can-we-do-induction/?cb=1

He also writes:

"So my claim is that if X is a totally ordered
set, then we can do induction on X if and only
if X is well-ordered. But this then refers to
the “strong” induction.

What happened to the other kind? Can we make sense
of the other kind if we just have a total order?
The answer to the last question is: Almost.

If we have a well-ordered set (with a small
additional condition), then we can in fact make
sense of the usual kind of induction."

What is the small additional condition?
I did not yet read the full blog. So I
currently don't know.

[FredJeffries]

On Friday, April 19, 2019 at 10:06:56 PM UTC-7, Dan Christensen demonstrated that he has never seen a Number Theory textbook:

> On Friday, April 19, 2019 at 6:40:53 PM UTC-4, j4n bur53 wrote:
> > Hint: Have a closer look at ordinals maybe.
> > They are also based on <, since e is <.
> >
>
> Thanks, but no thanks. I prefer to develop number theory starting from Peano's Axioms (including weak induction) as most textbooks seem to do.

No, (almost) none of them do

> None start with strong induction.

(Almost) All start with divisibility

> And very few start with von Neumann ordinals -- for very good reasons.

Correct -- the same reason that they do not start with (or even mention) the Peano axioms.

[FredJeffries]

On Saturday, April 20, 2019 at 1:52:39 AM UTC-7, j4n bur53 wrote:
>
> is DC proof totally useless?

You are blaming the tool for the shortcomings of the craftsperson

[Dan Christensen]

On Saturday, April 20, 2019 at 4:57:51 AM UTC-4, j4n bur53 wrote:
> I dont find a lot of applications of Peano via DC

> Proof...


You haven't been paying attention, Jan. See lines 15-84 of my proof here.

[Dan Christensen]

On Saturday, April 20, 2019 at 10:05:42 AM UTC-4, FredJeffries wrote:
> On Friday, April 19, 2019 at 10:06:56 PM UTC-7, Dan Christensen demonstrated that he has never seen a Number Theory textbook:
> > On Friday, April 19, 2019 at 6:40:53 PM UTC-4, j4n bur53 wrote:
> > > Hint: Have a closer look at ordinals maybe.
> > > They are also based on <, since e is <.
> > >
> >
> > Thanks, but no thanks. I prefer to develop number theory starting from Peano's Axioms (including weak induction) as most textbooks seem to do.
>
> No, (almost) none of them do
>
> > None start with strong induction.
>
> (Almost) All start with divisibility
>

Any that I have seen that present an axiomatic approach to the foundations of number theory will start with Peano's 5 Axioms and use some very basic set theory.

> > And very few start with von Neumann ordinals -- for very good reasons.
>
> Correct -- the same reason that they do not start with (or even mention) the Peano axioms.

Not really. I would think that von Neumann ordinals would be pedagogical disaster in most cases. Peano's Axioms, on the other hand, are quite accessible and are based on common sense about the natural numbers:

1. 0 is a natural number (the "first" natural number).
2. Every natural number has a unique successor (the "next" number)
3. If a natural number has a predecessor, that predecessor is unique (the "previous" number).
4. 0 has no predecessor.
5. Any natural number can be reached by going from one number to next starting at 0.

Common sense number facts.

[FredJeffries]

On Saturday, April 20, 2019 at 7:50:03 AM UTC-7, Dan Christensen wrote:
> On Saturday, April 20, 2019 at 10:05:42 AM UTC-4, FredJeffries wrote:
> > On Friday, April 19, 2019 at 10:06:56 PM UTC-7, Dan Christensen demonstrated that he has never seen a Number Theory textbook:
> > > On Friday, April 19, 2019 at 6:40:53 PM UTC-4, j4n bur53 wrote:
> > > > Hint: Have a closer look at ordinals maybe.
> > > > They are also based on <, since e is <.
> > > >
> > >
> > > Thanks, but no thanks. I prefer to develop number theory starting from Peano's Axioms (including weak induction) as most textbooks seem to do.
> >
> > No, (almost) none of them do
> >
> > > None start with strong induction.
> >
> > (Almost) All start with divisibility
> >
>
> Any that I have seen that present an axiomatic approach to the foundations of number theory will start with Peano's 5 Axioms and use some very basic set theory.

Vacuously true, since you have never seen any.

[j4n bur53]

Well DC proof very much reflects the creator. For
example his "set theory" doesn't have a regularity axiom.

Of course this could be mitigated, by adding a reguarity
axiom in a proof. But usually if you bundle "set theory"

with your tool, you should bundle full "set theory",
not only some fragment. Etc.. etc..

[j4n bur53]

Similarly with many of his worked out proofs.
He just stops were it would become interesting.

Now he proofs "Weak => Strong". He could also
prove "Weak => True", which is trivially true

for any formula A, i.e. "A => true" is always
provable. Just check the truth table:

A B A => B
0 0 1
0 1 1 %%% here
1 0 0
1 1 1 %%% here

So in general proving only "A => B", and not
discussing "B => A" at the same time, is pretty

useless. If you prove "A => B", you should either
also prove "B => A", or give an example where

"B => A" doesn't hold.

[Dan Christensen]

Strange then that there are 176,000 hits on Google for "peano axioms" at the moment.

[Jim Burns]

On 4/20/2019 5:29 AM, j4n bur53 wrote:

> My morning shower proof is this proof:
>
> When can we do induction? - Tobias Kildetoft
>
> Proof: Let A⊆X be a non-empty subset and
> let a∈A. Now the set {x∈X∣x≤a}∩A is finite
> and non-empty and thus has a minimal element,
> which is a minimal element in A.
>
> https://math.blogoverflow.com/2015/03/10/when-can-we-do-induction/?cb=1
>
> He also writes:
>
> "So my claim is that if X is a totally ordered
> set, then we can do induction on X if and only
> if X is well-ordered. But this then refers to
> the “strong” induction.
>
> What happened to the other kind? Can we make sense
> of the other kind if we just have a total order?
> The answer to the last question is: Almost.
>
> If we have a well-ordered set (with a small
> additional condition), then we can in fact make
> sense of the usual kind of induction."
>
> What is the small additional condition?
> I did not yet read the full blog. So I
> currently don't know.

The additional condition Kildetoft gives is that
anything other than 0 has an immediate predecessor.

I suspect that there are lots of different ways to give
an equivalent condition. The one that makes the most sense
to me is to require everything in the well-order to be a
finite element.
Ay e X: Finite({ z e X | z < y })

If all y in X are finite, then all y must have an immediate
predecessor or be 0.
(Suppose w e X has no immediate predecessor. Then w is
infinite or is 0.)

If not all y in X are finite, then, for some y ~= 0,
y does not have an immediate predecessor.
(omega is the first infinite ordinal and it does not have
an immediate predecessor. If an infinite y is in X,
omega is also in X.)

----
The transfinite version of induction is
| If there is a counter-example to property P(x), then
| there is a _first_ counter-example to property P(x).

This is basically just the Least Element Principle.
It looks better written as its contrapositive.
| If there is no _first_ counter-example to P(x),
| then there is no counter-example to P(x) _at all_ .

More formally:
| ~Ex:( ~P(x) & Ay:( y < x -> P(y) ) ) -> Az:P(z)
Or:
| Ax,Ay:( ( y < x -> P(y) ) -> P(x) ) -> Az:P(z)

If we add to that the requirement that every non-zero
element have an immediate predecessor (that every element
be finite, as I think of it), then, for a first _non-zero_
counter-example x, ~P(x) and P(x-1).
| If there is a counter-example to property P(x), then
| there is a _first_ counter-example x, and either
| ~P(0) for x = 0, or ~P(x) and P(x-1) for x ~= 0.

The contrapositive of _this_ is the familiar Peano-style
induction rule.
| If P(0) and, for all x ~= 0, ~P(x-1) or P(x), then
| there is no counter-example to P(x) at all:
| for all x, P(x).

Or, even better:
| ( P(0) & Ay:(P(y) -> P(y+1)) ) -> Ax:P(x)

[FredJeffries]

It's nice to see that you finally have acknowledged that you have never seen a Number Theory textbook.

[FredJeffries]

On Saturday, April 20, 2019 at 9:06:51 AM UTC-7, Dan Christensen wrote:

> Strange then that there are 176,000 hits on Google for "peano axioms" at the moment.

And not one of them is a Number Theory textbook...