How False statement $\imples$ true statement is true?

please explain.

I have no Idea.

If the premise is false, it is sound that you can conclude anything

Or rather: If the premise is false, any conclusion can follow

@user21820 let's look at free groups

define a "step-reduction" to be where you reduce w1++[a,a^-1]++w2 to w1++w2

church-rosser: if w1 step-reduces to w2 and w3 respectively, then there is w4 such that w2 and w3 step-reduce to w4

(diamond of step-reduction)

I don't know how to prove this rigorously

and constructively

because e.g. w1=[a,b,a,a^-1,a,b,a,a^-1,b] can be step-reduced in three different manners

@LeakyNun By "step-reduce" you mean any number of step reductions, right? Then prove that there is a terminal point, which is easy because the length decreases at each step. Then prove that the terminal point is unique. The easiest way is to take the smallest counter-example (by total length), and then both must not share a prefix or suffix, and by induction you can move everything to one side, but by the definition of the free group by canonical reduction they cannot be equal.

one step

@user21820 I think you missed the word "constructively"

@LeakyNun Most proofs that go by "smallest counter-example" can be transformed to a strong-induction. But you're saying I'm answering the wrong question anyway.

sure

I think by cases.

I think strong-induction should really be called well-founded-induction

@LeakyNun Why did you think cases is not constructive, when the cases are concerning natural numbers?

If we accept PA−, it already has trichotomy for naturals.

which natural number?

The positions of the reductions.

If they don't overlap, we are done. If they do, we should be done too.

there are three cases...

and can it be done using only weak induction?

And it's false if you require step-reduce to be exactly 1 step, unless "w2" and "w3" are required to be distinct. a a' a -> a but cannot be further reduced, so there is no "w4" as required.

aha!

@LeakyNun Strong induction can only be proven from normal induction using LEM for a quantified sentence, so in general one who rejects LEM for quantified sentences may reject strong induction but not normal induction.

are you talking about natural numbers?

Yes.

I disagree

@LeakyNun Concerning well-founded induction, I wrote something similar here.

@LeakyNun Why? You cannot prove strong induction from normal induction without LEM for a quantifier...

I disagree :P

Then prove it; show meta-logically that any instance of strong induction can be proven from normal induction.

(∀n(∀k(k<n→p(k)))→p(n))→(∀np(n)) right

Right except you have some incorrect brackets.

alright

I don't have a proof that you can't do it, but I'm 100% sure you can't.

And I have to go now, sorry.

@user21820

@LeakyNun You're right. That's exactly the proof I wrote in my own notes 3 years ago. I know why I thought we need LEM; I mixed up with well-ordering.

Well-ordering: ∃n∈N ( P(n) ) ⇒ ∃m∈N ( P(m) ∧ ∀n∈N ( P(n) ⇒ n≥m) ).

Variant: ∃n∈N ( P(n) ) ⇒ ∃m∈N ( P(m) ∧ ∀n∈N ( n<m ⇒ ¬P(n) ) ).

can we instead define well-ordering using the well-ordered-induction, and then use it to prove your criterion?

Technically, what I just stated is really called the "well-ordering principle", so I think better not change existing terminology.

because in Lean, well-founded is not defined as in convention

I see.

Well you can do what you like, and state the translation later.

inductive acc {α : Sort u} (r : α → α → Prop) : α → Prop
| intro (x : α) (h : ∀ y, r y x → acc y) : acc x

inductive well_founded {α : Sort u} (r : α → α → Prop) : Prop
| intro (h : ∀ a, acc r a) : well_founded

lemma recursion {C : α → Sort v} (a : α) (h : Π x, (Π y, y ≺ x → C y) → C x) : C a :=
acc.rec_on (apply hwf a) (λ x₁ ac₁ ih, h x₁ ih)

acc stands for accessible

I'm really going off now. Will look at your messages later.

ok