« first day (1299 days earlier)      last day (1184 days later) » 

12:45
@MaxH Put a space after "not". Your first error is at "contradiction". But why are you not fixing your earlier incorrect proofs?
@F.Zer It's correct but not ideal. You are really using a lot of little lemmas to manipulate the statements. This makes your proof less transparent and also less constructive. I can make the same complaint about @Prithubiswas 's proof here, so I'll complain about both at the same time. =)
@user21820 So you mean not A instead of notA? Why is there an error at contradiction? Would I have to write B after not B and before contradiction as a restate? If so then that is because I sometimes forget the restates...
I did not post fixed proofs because I wanted to do something else and I only had limited time.
@F.Zer @Prithubiswas: Although such lemmas are important and useful when searching for a proof, after finding a proof it is also good to try to simplify it to use as little as possible without bloating it. So I think both of you should try rearranging the argument to use less lemmas. For example, you want to prove "∀k∈ℕ ( P(k) )" and you can do so via ∀intro, pushing your argument further in under "If ¬P(k):" instead.
@MaxH Yes "not A". Your error is again because you violated the rule; "at the same indentation level".
No, it is not because you forget restates; omitting restate-lines never causes the proof to become wrong. But yours is actually wrong.
Then I am not immediately sure where the error is. Let me see...
13:03
@MaxH This other one is a correct proof of half the exercise.
@user21820 Yes, I only did half because of limited time.
@MaxH Sure.
I will have to go soon, so I dont know if I can do much today.
@MaxH No problem. There's no hurry to complete these.
I also need to do lots of homework unfortunately...
But I will post as soon as I can
13:05
No problem. As I said, there's no hurry. =)
Bye for now!
Thanks and bye!
13:21
Prove Strong induction from Well-ordering:
  If ∀k ∈ ℕ ( ∀i ∈ ℕ ( i < k ⇒ P(i) ) ⇒ P(k) ):
    Given k ∈ ℕ:
      If ¬P(k):
        ∃k ∈ ℕ ( ¬P(k) )
        Let m ∈ ℕ such that ¬P(m) ∧ ∀k ∈ ℕ ( ¬P(k) ⇒ k ≥ m ) [well-ordering]
        ∀i ∈ ℕ ( i < m ⇒ P(i) ) ⇒ P(m)
        ¬∀i ∈ ℕ ( i < m ⇒ P(i) )
        ∃i ∈ ℕ ( i < m ∧ ¬P(i) )
        Let a ∈ ℕ such that a < m ∧ ¬P(a)
        ¬P(a) ⇒ a ≥ m
        a ≥ m
        ⊥
    ∀k ∈ ℕ ( P(k) )
@user21820 Fixed attempt. Is it better now ?
 
2 hours later…
14:59
@user21820 So intuitively your recursion theorem is something like this?
So meaning there exists a sequence (s1,s2,s3,s4,...) such that the above criterion is satisfied?
15:16
@Prithubiswas That's right, and that sequence is g in the recursion theorem.
@F.Zer "a lot of little lemmas".
 
2 hours later…
17:01
@user21820 Sorry. What do you think now ?
Prove Strong induction from Well-ordering:
  If ∀k ∈ ℕ ( ∀i ∈ ℕ ( i < k ⇒ P(i) ) ⇒ P(k) ):
    Given k ∈ ℕ:
      If ¬P(k):
        ∃k ∈ ℕ ( ¬P(k) )
        Let m ∈ ℕ such that ¬P(m) ∧ ∀k ∈ ℕ ( ¬P(k) ⇒ k ≥ m ) [well-ordering]
        ∀i ∈ ℕ ( i < m ⇒ P(i) ) ⇒ P(m)
        Given i ∈ ℕ:
          If i < m:
            If ¬P(i):
              i ≥ m
              ⊥
            P(i)
        ∀i ∈ ℕ ( i < m ⇒ P(i) )
        P(m)
        ¬P(m)
        ⊥
    ∀k ∈ ℕ ( P(k) )
17:25
@F.Zer Exactly!
I'm not saying you should always do this, by the way.
I'm just saying that it can be sometimes helpful to see a proof that uses only the basic tools.
Obviously, for more complicated problems what is "basic" would be correspondingly more complicated.
Got it ! Thank you ! I see how that is useful.
You're welcome!
@user21820 After looking at the recursion theorem , my first reaction was:
"Oh I can prove this. I think I just need definitional expansion , function notation , and maybe induction (because ... recursion I guess?)".
But then you said "let me know if you wish to see a proof of the recursion theorem"
So it means the recursion theorem would be quite hard for me to prove , and my naive thought wouldn't work at all. But I fail to see intuitively why it wouldn't work.
It is the case that I know that it is hard , but don't know why it is hard.
@F.Zer I also like this proof. It is a lot more transparent than mine.
@user21820 Another way to say it might be: "My intuition is saying that proving the recursion theorem requires only a trivial use of induction , but my sixth sense is telling that it is hard."
17:46
@Prithubiswas Induction only gets you to any arbitrary finite point. It never gets you all the way.
You can of course try and see what you get and what you can't get, when using what you said you at first thought you need.
And actually I don't think it's impossible for you to prove on your own. But you need to use comprehension at some point, because the other stuff even with definitional expansion and function-notation aren't powerful enough.
If you want to try proving it yourself, maybe you could follow my hint: First observe that you can by induction prove the existence of finite approximations of arbitrary length, namely finite sequences that follow the recursive relation. Then use comprehension to glue all finite approximations together, namely construct the set of all pairs such that each one is in some finite approximation. Finally prove that the result is a function that satisfies the desired property.
18:34
If (A implies not B) and B:
	A implies notB.
	B.
	If not (not A):
		A.
		B.
		A implies not B.
		If A:
			not B.
			B.
		contradiction.
		not A.
		contradiction.
	not (not A) implies contradiction.
	not A.
(A implies not B) and B implies not A.
@user21820 Would that be a fix?

« first day (1299 days earlier)      last day (1184 days later) »