[1] All math axioms can be expressed as grammar rules like the following:
A -> B (directed)
A <-> BC (undirected)
See [6].
[2] Given axiom length of n (total symbols in your axioms) this has polynomial worst-case lengthening your axioms. See [13].
[3] We can introduce two non-terminals, ( and ), and rewrite the rules in [1] as follows:
( A ) -> ( B ) (directed)
( A ) <-> ( ( B ) ( C ) ) (undirected)
[4] Given a target string, S = A1 A2 ... Am for rules in [1] (S is something we'd like to prove), the problem becomes, "find a permutation of parenthesis for S such that rules in [2] generates S."
[5] The parenthesis will put A1 A2 ... Am into a binary tree.
[6] There are exponential worst-case combinations of parenthesis to consider: If A1 A2 ... Am are vertices in a graph, there are m^2 possible edges to consider. If it's a tree, there are m-1 vertices. There are (at most) (m^2 choose m-1) ways to put that into a tree. That is exponential worst-case.
[7] Each non-terminal may, via directed rules, be substituted for another non-terminal. Checking directed reachability is polynomial. This is in proportion to the number of non-terminals you have (which is worst-case total axiom length polynomial(n)). This adds a polynomial overhead to each non-terminal you check.
[8] There are m non-terminals to check in S. As you replace ((B)(C)) with (A), you have a new non-terminal to check.
[9] This feels like an exhaustive search for each combination of parenthesis: You start with m symbols. You have polynomial(n) choices (by [7]). Each choice replaces 2 symbols with a new symbol (by [8]) that has polynomial(n) choices (by [7]).
Does this come out to 2^(polynomial(n+m)) worst-case time complexity?
I can't really follow your argument, but it's not hard to show that its conclusion is wrong:
This is a direct consequence of Godel's first incompleteness theorem:
If there were such an $f$, we could computably decide whether a given sentence $\sigma$ is consistent.
We can use this to build a computable completion of Robinson arithmetic $Q$:
Let $(\varphi_i)_{i\in\mathbb{N}}$ be the usual enumeration of the sentences of arithmetic.
Let $\sigma_0$ be the usual conjunction of the finitely many axioms of $Q$.
Having defined $\sigma_i$, let $\sigma_{i+1}=\sigma_i\wedge\varphi_i$ if that's consistent and $\sigma_{i+1}=\sigma_i\wedge\neg\varphi_i$ otherwise.
The set $\{\sigma_i: i\in\mathbb{N}\}$ is then computable, complete, consistent, and extends $Q$; contradicting Godel.
Perhaps you're implicitly thinking of (or in your argument you have implicit assumptions which are only valid for) propositional logic, where things are better behaved (in particular, propositional logic is decidable). There we do indeed only need to "look exponentially far," and the general topic of lengths of propositional proofs is an important aspect of modern complexity theory.
But then, propositional logic is not sufficient for mathematics (precisely since it's too simple).