Re:There's a mathematician in your compiler
by thaumasiotes on Tuesday March 31, 2020 @01:05PM
(#22739686)
> That's not the case, even without axioms if you start at A and deduce B then this proves that "A => B".
As I already pointed out in this thread, you're not right here. It is true that if you start at A and deduce B you've proven A ⟹ B. But if you're deducing something true, it's not necessary to start with A. If B is true, then A ⟹ B for all A, so you've proven nothing you didn't already have. It is quite literally correct to say that "if you deduce something true from an assumption, it means nothing".
You can see a nice visual illustration of the meaninglessness of the premise by completing the proof of "A→B" from "B" at http://incredible.pm (session 2)
As I already pointed out in this thread, you're not right here. It is true that if you start at A and deduce B you've proven A ⟹ B. But if you're deducing something true, it's not necessary to start with A. If B is true, then A ⟹ B for all A, so you've proven nothing you didn't already have. It is quite literally correct to say that "if you deduce something true from an assumption, it means nothing".
You can see a nice visual illustration of the meaninglessness of the premise by completing the proof of "A→B" from "B" at http://incredible.pm (session 2)