Reading this thread:
http://math.stackexchange.com/questions/397972/what-is-a-proof
Sparks many questions, that I think would be good for people to discuss here.
===
I think the most interesting question that arises from there, is what or who determines the set of axioms that we base off all of our mathematics on.
According to some people in the thread, it is possible to construct a base set of axioms and derive whatever they want from that, is this plausible?
A proof is just a formal sequence of manipulations of strings of symbols by some predetermined rules to obtain various logical expressions. The strings we are allowed to start with are our axioms (written in a formal language, see
http://en.wikipedia.org/wiki/Formal_system).
Who decides which formal systems we should work in? Anyone can! Over time useful concepts become formalised by mathematicians and a sensible set of definitions/axioms become pretty universally accepted. But nothing is stopping you from constructing your own formal system, choosing a set of axioms, and proving theorems in this system. Of course, if you choose your axioms poorly, your system might be contradictory! (Both a theorem and its negation can be proven in your system).
For example
http://en.wikipedia.org/wiki/ZFC formalises a very ubiquitous concept, that of forming collections of objects. The axioms are ideally a small set of self evident low-level statements from which we can construct a theory. (Note that even in this example there is controversy though, not every mathematician accepts the axiom of choice (the C in ZFC), which is a crucial tool in many mathematical arguments.)
One advantage of formalising a theory is that we can view theorems as purely syntactic entities (a formal string of symbols, not some deeper truth about the universe). This way, one does not have to worry about the nature of "truth" and "reality" whilst doing mathematics. This distinction between "truth" and "theoremhood" allows us to view mathematics as simply a game of seeing what we can create in the imaginary perfect universe governed by a particular formal system we have chosen to work in.
This is my philosophy anyway, I know there are many differing views on this and I am no expert.
Note:
One of the original purposes of formalism was to study formal systems themselves due to the rigorous nature of their definitions and "prove" (in a different sense of the word, see
http://en.wikipedia.org/wiki/Metamathematics) that the formal systems underpinning mathematics had some desirable properties (such as
http://en.wikipedia.org/wiki/Completeness#Logical_completeness and being non-contradictory). Sadly this goal was partially shattered by Kurt Gödel and his two incompleteness theorems which are quite deep and technical but very interesting. Basically, we can never show that ALL of mathematics under the formalist view is as nice as we would like so we just have to accept the state that the foundations are currently in and actually prove things. ZFC together with first-order logic form a satisfactory formalism for most of mathematics.
For more information see
http://en.wikipedia.org/wiki/Foundations_of_mathematics and things it links to.
Apologies if I got anything wrong here, it has been quite some time since I read about these sorts of things.
