« first day (518 days earlier)      last day (2283 days later) » 

user21820
user21820
2:32 AM
@LeakyNun Har har... Very funny. But I'm serious; if you have some reason to not want it posted here, you should just say so otherwise I might post it here?
@LeakyNun Oh and I think I know what you're referring to. I do not know if it's true in the general population, but I am 100% sure that I would not be duped by anyone into making up a reason for some decision I was told I made but did not actually make.
It's partly because I always endeavour to use logical reasoning, so if it's a whim I identify it as a whim and do not attempt to rationalize it. I don't think you'd be duped by that experiment either.
 
 
3 hours later…
user131753
5:53 AM
You claim here that the post is wrong "because it implies that W&R managed to prove mathematical induction non-circularly". I don't see anything wrong in it. W&R did manage to prove mathematical induction non-circularly in the first edition of PM (but not in the second edition). Can you say exactly what is wrong with it and why it is "rubbish"?
 
Tung Nguyen
Tung Nguyen
7:02 AM
I have a quick question
Suppose I have this formula
( For all x P(x) )and ( there exists y Q/y) )
I can pull the quantifiers to the front, right ? because each clause has nothing to do with the other
So for example I pull For all x first
I get: For all x( P(x) and there exists y Q(y))
And then pull the existential quant
For all x, there exists y ( P(x) and Q(y) )
but on the other hand, i can pull the existential quant first and then the universal quant second
and get: There exists y, for all x ( P(x) and Q(Y) )
but the order of the quants matter, the 2 formula cant be equal, where am I wrong here ?
 
 
9 hours later…
Leaky Nun
Leaky Nun
3:59 PM
@TungNguyen actually they're equal
here's a proof in Lean, a proof assistant: 
example (α : Type u) (z : α) (P Q : α → Prop) : (∀ x, ∃ y, (P x ∧ Q y)) ↔ (∃ y, ∀ x, (P x ∧ Q y)) :=
⟨λ h, exists.elim (h z) (λ y hy, ⟨y, λ x, ⟨exists.elim (h x) (λ v, and.left), hy.2⟩⟩), λ h, exists.elim h (λ y hy x, ⟨y, hy x⟩)⟩
(you need the domain to be non-empty)
the second line is the proof, which I haven't tried to make readable
the first line is the statement. treat the things before : as initializing
actually I only typed this to convince you that it is true
actually, if A := ( For all x P(x) )and ( there exists y Q/y) ) and B := For all x( P(x) and there exists y Q(y)), then A implies B, but B does not imply A (unless the domain is non-empty)
 
 
6 hours later…
Leaky Nun
Leaky Nun
10:09 PM
@user21820 cauchy sequence is a Π3 sentence right
 

« first day (518 days earlier)      last day (2283 days later) »