[contravariant]

>my understanding is if you deduce something true from an assumption it means nothing.

That's not the case, even without axioms if you start at A and deduce B then this proves that "A => B". And usually you start with some axioms (i.e. statements that are true by definition; in the context of the article these are the types that have an implementation). Anything that follows from those is also true. At the end of the article the author stumbles upon the fact that you can add implementations / axioms for anything you want (however there's no guarantee that your theory will remain consistent).

>you need to deduce something false and thus the negation of your assumption is true.

Ironically it's precisely the reasoning "<contradiction> follows from B therefore not B" that's currently being questioned by mathematicians. Although in most context it is still a valid line of reasoning.

And what's entirely missing from the article is the distinction between true and provable. These aren't quite the same. Sure Goedel did prove that all statements that hold for every possible model (~implementation) of a theory are provable, but he also showed that no theory of arithmetic can have a unique model.

[thaumasiotes]

> 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)