As I discover the foundations of mathematics, I begin to understand that it is a matter of arbitrarily defining axioms and combining them - arriving at what we call theorems.
Having said that, it looks to me the following:
We could fix a finite number of symbols ($\lnot$, $\forall$,...) and state all the arbitrarily useful axioms with them (say the construction of natural numbers, the definition of the addition operation). Given that, let's say we define $n$ axioms, what would be left for us would be just to combine them in any possible way. For example, $n(n-1)$ statements would arrive by the combination of two (distinct and with order) of the original ones, $n(n-1)(n-2)$ by the combination of three. After that, for example, we could pick one of these $n(n-1)$ and combine with one of the original ones, with two of them. By construction, all provable (derivable by a combination of the axioms) statements would be achieved. Finally, we could state a statement with unknown truth value with the symbols and just combinatorially see if it is achievable.
The previous text is certainly bad written and not rigorous at all; in top of this, to try to clarify this thought that chases me, an analogy also comes to my mind: Given the rules of chess (our axioms), if we want to know if a certain configuration of the pieces (unknown statement) is provable (derivable by the rules), why can't we just go on trying all the moves from the beginning: moves pawn a, moves pawn b, ..., moves pawn a and knight b...
I know this is probably distant of making sense, but I can't see why this procedure would be so impracticable. Therefore I am humbly coming here in the seek for a glimpse of clarity to end this train of thought that chases my mind and that I simply can't develop in any sense.
This works ... in a sense. We can indeed perform brute force proof search given a sentence $\varphi$ and an appropriate axiom system $A$, and if $\varphi$ is provable (or disprovable) in $A$ we will eventually find a proof (or disproof) of $\varphi$ in $A$.
However, there are two serious drawbacks here. First, if $\varphi$ is independent of $A$ (= neither provable nor disprovable) we won't ever figure that out. Second, even if $\varphi$ is $A$-decidable it will take an extremely long time to find such a proof: roughly speaking, the number of $A$-proofs of a given length $n$ is exponential in $n$. So there's no hope of using brute-force proof search except to find extremely simple arguments.
What about improvements on brute-force search? Well, there is indeed such a subject as automated theorem proving; however, to my understanding it is very much in its infancy as far as proving new theorems (or even efficiently finding proofs of existing significant theorems) goes.
That said, there's the separate aspect of whether this captures the essence of mathematics. Is mathematics in fact just formal deduction? To a Platonist for example there really is such a thing as (say) $\mathbb{R}$, and we want to understand it. We're not particularly interested in questions of the form "Does $A$ prove $\varphi$" unless we already have reason to believe that $A$ is "correct" (although the question remains how we are supposed to know such a thing ...).
And even for the formalist the "mathematics-as-deductions" idea, if taken to its extreme, is missing something crucial. Namely, we don't consider all systems and all sentences to be equal but rather search for proofs of "interesting" sentences in "interesting" systems. If we reject the idea of a "mathematical universe" (or similar), this value judgment is difficult to understand. The big problem for the formalist is how to make sense of our extremely rich experiences surrounding "mere symbol games." The development of the theory of formal proofs convinces the formalist that mathematics-as-practiced is "coherent," but it doesn't provide an explanation of the mathematical experience which satisfies
methem.