Yakk wrote:The thing that is created when we do mathematics is the proof that connects axiom to theorem. The space of "true statements" that are implied even by axioms (and the conceptual framework that lets you prove things with them) is vast, and speaking of the consequences as being "already there, just not discovered yet" is questionable.

It is like saying that all books in existence are implied by the existence of a printing press, and any book after that point was merely a discovery of the arrangement of characters. Or if you dislike that, the existence of number based encoding of books (where a book is represented by a single number, and all possible books are listed in this index uniquely) made the act of writing one of discovery of those numbers.

There is one critical difference that your analogy passes over however: The semantic content of books is not a function of the semantic content of letters, the characters which comprise the books. In math on the other hand, the opposite of this is true. Once a few axioms and their symbolic representations are agreed upon, the exact meaning of a mathematical statement can be read off (at least in theory) from the arrangements of these symbols, even though in practice that's not quite how things are done. Just knowing what "c", "a", and "t" are does not tell you what "cat" means as an English word, but knowing what [imath]P,Q,\Rightarrow[/imath] mean allows you to deduce the meaning of [imath]P\Rightarrow Q[/imath].