« first day (217 days earlier)      last day (2266 days later) » 

09:39
@Secret What is the original problem?
 
3 hours later…
12:16
Mar 24 at 15:11, by user21820
Let Q(n) denote "Forall k in N ( k<n implies P(k) )".
Then Q is a property on N.
If Forall n in N ( Forall k in N ( k<n implies P(k) ) implies P(n) ):
	Forall n in N ( Q(n) implies P(n) ).
	// Now we shall prove "Forall n in N ( Q(n) )" by ordinary induction //
	...
	Thus Q(0).
	Given n in N:
		If Q(n):
			Forall k in N ( k<n implies P(k) ).
			Given k in N:
				If k<n+1:
					k<n or k=n.	// Are you convinced this follows from "k<n+1"?
					If k<n:
						...
					If k=n:
						...
					P(k).
			Forall k in N ( k<n+1 implies P(k) ).
@user21820 It is the homework you gave me last year, which because of my PhD work I don't have time to do it until now
The proof of strong induction
12:43
@Secret Ah okay, but what you wrote doesn't follow the outline I gave.
let me tidy that up into your format...
The first "..." you basically understand, though you should learn to use the rules rather than say "vacuous truth". The question of "k<n or k=n" you also more or less get it (this can be shown rigorously from the axioms of PA, crucially axiom 14), and I don't need you to explain that at the moment.
But after that, you got lost in the second "..." under "If k<n:", which should have been easy, because you have "Q(n)".
@Secret You need to reach the last two lines in my outline, because that is what you need to use induction on Q.
But Q(n) is "Forall k in N ( k<n implies P(k) )". The thing I need to use is "k<n implies P(k)" but it is stuck inside the "Forall k in N and I cannot take it out to use it with"k<n" within the context "if k < n" to conclude "P(k)"
Also how does one deal with empty statements when there isn't a k to plug into "k<0" to give it a truth value, and likewise for P(0)?
I don't recall seeing a sentence of the form "(empty set) implies (empty set)"
If Forall n in N ( Forall k in N ( k<n implies P(k) ) implies P(n) ):
	Forall n in N ( Q(n) implies P(n) ).
	...
	Thus Q(0).
	Given n in N:
		If Q(n):
			Given k in N:
				If k<n+1:
					...
					P(k). // Here onwards is obtained by working backward.
			Forall k in N ( k<n+1 implies P(k) ).
			Q(n+1).
	Therefore Forall n in N ( Q(n) ). // by induction on Q
@Secret The variables conflict, so you need to rename it. But intuitively it should be obvious that Q(n) says something about every k < n.
@Secret There are no sets. You can directly prove Q(0) using the rules.
hmm... Q(0) is "Forall k in N ( k<0 implies P(k) )". But such a k does not exist. Then how can I determine the truth value of "k<0"? Or do you mean I need to expand "<" also?
If I think of this as a program, then the nonexistence of k will mean the program saw only ?<0, which it cannot determine its truth value because there is no input for "?" to complete the instruction
I mean, the only rule I can see to use here is to invoke contradiction somehow, but why it is sound to assume "k<0" is a false statement if there is no k to plug in?
12:59
Use the rules.
You should know by now that if a forall-statement can be proven the last step can always be forall-intro.
@Secret Axiom 15.
If you want to be rigorous, you need to pick a definition for "x ≤ y". For example if you define it to be "x<y ∨ x=y", then you use axioms 8,9,15 to show "∀x∈N ( ¬x<0 )".
For now you can just use what I wrote as a fact, though you should of course know how to do it all rigorously.
13:46
ok, let me try again (I initially failed to find Axiom 15 because I thought you are referring to the fitch style logic rules and there is no rule11-15 numbered, and only very later I realise you are referring to the Peano axioms.
I think next time when I get confused, I should just wipe my brain clean and just scan the last 10 messages on this chat to ensure I do not miss out important information due to my brain trying to look for a preconceived information and hence susceptible to confirmation bias)
13:59
@Secret Ah, in my post I changed axioms 14 and 15 (the last two), and was careful to use only the non-logical symbols 0,1,+,·,<.
Both versions are equivalent, so you can use my version if you wish.

« first day (217 days earlier)      last day (2266 days later) »