Could mathematical reasoning be non-axiomatic?

Question

"Mathematics is not a deductive science—that's a cliché. When you try to prove a theorem, you don't just list the hypotheses, and then start to reason. What you do is trial and error, experimentation, guesswork. You want to find out what the facts are, and what you do is in that respect similar to what a laboratory technician does."-Paul Halmos.

Following the argument of Paul Halmos, which I agree with, I don't think mathematics as done by mathematicians proceeds in an axiomatic manner. Now, I wonder whether we can provide foundations for mathematical reasoning as done by humans.

I think this might have relevance to automated theorem discovery or 'automated conjecturing' if such a field exists.

Answer 1

If I may quote Andres Caceido:

Mathematical theories are rarely developed axiomatically from the beginning. Instead, our axiomatizations tend to be the product of hindsight, using the experience accumulated through examples, guess work, and semi-rigorous reasoning.

This is true for almost all branches of mathematics:

1. Euclidean geometry: people were doing geometry long before Euclid's axiomatization of geometry
2. standard analysis: analysis originated from calculus which was done in an ad-hoc manner before Dedekind, Weierstrass, Cauchy and others tried to give it rigorous foundations.

Moreover, I'd like to say the following regarding axiomatisations:

1. Axiomatisations are not unique. Just look at the multiple axiomatisations of Euclidean geometry as an example.

2. Axiomatisations are necessary for proofs and they also help elucidate the structure of a mathematical theory so different theories can be compared.

3. Godel showed that the axiomatisation of any theory isn't sufficient to prove its consistency if it contains a theory of numbers.

It follows that mathematicians axiomatise branches of mathematics because of its practical value but many creative mathematicians(arguably the most creative) in history didn't use axioms as their starting point for the development of new mathematical objects. Think of Poincare and the birth of algebraic topology. Leibniz and the invention of Calculus. All of mathematical physics. ...etc.

Finally, I think that while the close analysis of a set of axioms can lead to many fruitful ideas a computer that aims to make mathematical discoveries should not be constrained by the set of axioms it's based on. Mistakes(guided by intuition) very often are fruitful, and the history of mathematics can offer plenty of examples.

I think it's for this reason that Poincare says:

Pure analysis puts at our disposal a multitude of procedures whose infallibility it guarantees; it opens to us a thousand different ways on which we can embark in all confidence; we are assured of meeting there no obstacles; but of all these ways, which will lead us most promptly to our goal? Who shall tell us which to choose? We need a faculty which makes us see the end from afar, and intuition is this faculty. It is necessary to the explorer for choosing his route; it is not less so to the one following his trail who wants to know why he chose it.

References:

1. Poincare on intuition in mathematics
2. A fully automatic problem solver with human style output

Note: As of this date most automated reasoning systems do brute force graph traversal over the grammar that defines the axioms of a particular system. Due to time and space constraints, this can't be the future of automated reasoning.