Induction, Deduction, and the Collatz Conjecture: the Decidedly Undecidable Propositions.
The question I want to ask is “is there a proof for every statement about the natural numbers that seems to be inductively verifiable, but is a general recursive decision problem, provided your sample is large enough?” Simply, if we define a binary property ‘P’ that can only be tested by algorithms that might not halt, and show, say by computation, that every natural number up to some arbitrarily large number ‘N’ has the property P, does that mean that there must be a generalized deductive proof that for all natural numbers P holds?
How big can N get before there must be a deductive proof that P holds for all natural numbers? What if N was larger than Graham’s number[1]? What if we showed thousands of years from now—using computers that are unimaginably strong by today’s standards—that every number less than or equal to the number you get when you put Graham’s number as both of the inputs to the Ackermann function[2] has a property P. But they still have no generalized deductive proof that all numbers have P, is that enough for these future number theorists to state that it is a scientific fact that all natural numbers have the property P?
It may seem impossible for such a disagreement to come up between induction and deduction, but we are already at a similar (though admittedly less dramatic) impasse. The disagreement centers around the Collatz conjecture, which states that every number is a Collatz number. To test if some number n is a Collatz number, if n is even, divide it by 2 to get n / 2, if n is odd multiply it by 3 and add 1 to obtain 3n + 1, and repeat this process with the new number thus obtained, indefinitely, if you eventually reach the cycle 4, 2, 1, then n is a Collatz number. Every number up to 20 × 2^58 has been shown to be a Collatz number[3], and it has been shown that there are no cycles with a smaller period than 35400[4], yet there is still no deductive proof of the Collatz conjecture[5]. In fact, one method of generalized proof has already been shown to be undecidable[6]. If it was shown that no general proof could ever be found, but all numbers up to the unimaginably large ones described above were shown to be Collatz numbers, what epistemological status should we grant the conjecture?
It has been made clear by the history of mathematics that a lack of small counterexamples to a conjecture of the form “for all natural numbers P(n) = 1” where ‘P’ is a binary function (let’s call this an “inductive-conjecture”), is not at all a proof of that conjecture. There have been many inductive-conjectures with that sort of evidence in their favor that have later been shown not to be theorems, just because the counter examples were very large. But what if a proof of the undecidability of a conjecture of that form is given, what then if no counter example had been found up to the insanely large values described above?
If there is a binary property ‘R’ that holds for all natural numbers, i.e., there is no counter example, and it can be deductively shown that no proof of ‘R’ holding for all natural numbers exists, then the implications for epistemology, ontology and the scientific/rational endeavor in general are huge. If some facts about the natural numbers don’t follow from the application of valid inferences onto axiom and theorems, then what makes us think that all the facts about the natural world must follow from natural laws in combination with the initial state of the universe? If there is such a property, then that means that in a completely deterministic system where you have all the rules describing all the possible ways that things can change, and you have all the rest of the formally verifiable information about the system, there still might be some fact about this system which is true but does not follow from those rules. Those statements would only be verifiable by finite probabilistic sampling from an infinite population with an undetermined standard deviation, but still be true facts. Our crowning example of such a system would of course be the theory of the natural numbers itself if such a binary property were discovered. Suppose the Collatz conjecture were shown to be undecidable, that would mean that there is no counter example, i.e., all numbers are Collatz numbers (since the existence of a counter example would guarantee the conjecture’s decidability), but there would also be no generalized proof that no counter example exists (since the existence of such a proof would guarantee the decidability of the conjecture). So since we can’t verify the conjecture either way, should we call it meaningless/unverifiable? Or is logically undecidable somehow distinct from literally meaningless? What restrictions/expectations should we have if we believe that an inductive-conjecture is undecidable, and how would those restrictions change if we believed that conjecture was actually unverifiable.
Let’s call the claim that “there is a binary property R which holds for all natural numbers and that there is no counter example that can or will ever be found, but which also cannot be proven to hold for all natural numbers” the “first Potato conjecture”. How would one ever show the first potato conjecture, or even offer evidence in it’s favor? Let’s say we knew that some property ‘R_b’ held of all natural numbers that we might ever test. Then we would have a proof of this and R_b could not be our R. If we get a candidate property ‘R_c’ that isn’t capable of being proven or dis-proven of all natural numbers, then we will never know if it holds for all natural numbers. Could induction even offer us any evidence in this case? Is a finite sample ever representative of an infinite population with no standard deviation even in the case of simple succession? If not, then what evidence could we ever offer for or against the potato conjecture, if an undecidable inductive-conjecture were discovered? If the answer is no evidence one way or the other, does that mean that the potato conjecture is meaningless, or just undecidable?
(But no, really, I’m asking.)
[1]: http://en.wikipedia.org/wiki/Graham’s number
[2]: http://en.wikipedia.org/wiki/Ackermann_function
[3]: http://www.ieeta.pt/~tos/3x+1.html
[4]: http://www.jstor.org/pss/2044308
[5]: http://en.wikipedia.org/wiki/Collatz_conjecture
[6]: Quoting Lagarias 1985: “J. H. Conway proved the remarkable result that a simple generalization of the problem is algorithmically undecidable.” The work was reported in: J. H. Conway (1972). “Unpredictable Iterations”. Proceedings of the 1972 Number Theory Conference : University of Colorado, Boulder, Colorado, August 14–18, 1972. Boulder: University of Colorado. pp. 49–52.
I think the philosophical profoundness of undecidability is often exaggerated. I could be way off base here, but..
Consider, in group theory, the statement “There exists an element other than the identity which squares to give the identity”. This is “undecidable” in that you can’t prove it or disprove it from the group theory axioms, and there are are groups where it’s true and groups where it’s false. However, this doesn’t make people lie awake all night worrying whether it makes maths meaningless, or whether it’s true for the “real group”.
But as soon as you get an undecidable statement about a theory of arithmetic or sets, people start worrying about whether it’s true for the “real integers” or whatever.
What’s the difference?
There are two major differences:
First, Godel’s results are much stronger than the claim that one has undecidable statements within the axiomatic system. But one also has that there’s no algorithm which can in general say whether a given statement is provable in PA (assuming that PA is in fact consistent). This is a much stronger and weirder claim.
This is also different from your group example because the natural numbers are a very concrete object. So our intuition strongly suggests that there should really be only one thing that actually looks like N in some sense. Some (although not all) senses of that are shown to be wrong by Godel’s theorems. Although what is doing more of the work here in some sense are the non-standard models of arithmetic which strictly speaking are distinct from Godel’s results.
Couldn’t have said it better myself (vote up).
Godel’s result about incompleteness COULD mean just that PA is inconsistent.
It would be an interesting way for the incompleteness theorem to be fulfilled. And become quite obsolete at the same time also. Except maybe as an early warning or sign that something is deeply wrong with PA.
Sure, that could be the case but that still is a much weirder situation than what Khoth is talking about. (Also, note that Godel’s theorems apply not just to PA but to the much weaker system of Robinson arithmetic so if there is an inconsistency it is probably happening at an even more fundamental level.)
Robinson’s arithmetic is still an infinite one. That could be the root of all evils.
How do you feel about the infinite cyclic group?
I am skeptic about any infinity. I am not sure, if it is (always) paradoxical. But a theory which relates to an infinity related axiom is most likely too rich.
The concept of infinity and the concept an (infinite in any sense) god are both too ambitious for this finite world. But very persistent as we see.
Sets and Numbers are both much more central to our most basic beliefs than groups. Without an algorithmic way of determining truths about sets we may well have to adopt complete nominalism in our ontology, and interpreting modern science so as to be consistent with a nominalist ontology is no easy task.
The difference is this: Your claim about groups is independent of the axioms.
An unprovable proposition is NOT independent of the axioms. The axioms imply the truth of the statement, they just don’t allow a proof of it. That a claim is unprovable doesn’t mean it lacks a truth value.
By the way, in general, decidability is a property of languages (equivalently, of sets), not of specific sentences or claims.
In first-order logic, all valid statements are provable. The statements about natural numbers not provable from given axioms are also independent of the axioms. Both PA+Con(PA) and PA+NOT(Con(PA)) are consistent.
Does Con(PA) mean “the consequences of the peano axioms? That’s the only meaning I can think of, but then I don’t see how you could avoid inconsistency if you accept some axioms and then deny their consequences (PA + NOT (Con(PA)).
Con(PA) means the consistency of PA. It can be formalized within PA as a statement about integers, something like “there’s no integer encoding a proof in PA that 1=0”.
For an explanation of Nesov’s counterintuitive statement that PA+NOT(Con(PA)) is a consistent theory (or rather, equiconsistent with PA itself), see paragraph 48.2 in this PDF. For an explanation of how to build a model for that preposterous theory, see paragraph 2.1 in this PDF.
Is that really the case? How can the axioms imply the truth of a statement without allowing a proof of it? I thought for statements that are unprovable (and also undisprovable) there’s some model of the theory (often a pretty screwy one) where it’s true, and some model where it’s false.
There are statements that are disprovable without being provable. (Or vice-versa.) For example, a statement over the natural numbers with one universal quantifier: for all X, P(X) holds. If you find a counterexample, you’re done, but there might not be a proof. (Likewise, for finding an example of an existential claim.)
Many problems are in this category—the technical term is “semi-decidable.” For instance, the halting problem is semi-decidable. If you ever find a sequence of steps after which the machine is in a halting state, it provably halts. But there might not be any point at which you can prove that it won’t halt in the future.
Ah, I think we’re talking a bit at cross-purposes. I’m meaning proof of individual propositions in an axiomatic system, you’re meaning the algorithmic solving of a class of problems. Helpfully, the same terms can be used for both, leading to fun confusion for all.
Let P(x) be “x < N”.
Contrariwise, let N=BB(message_length(P)).
Aw ouch, why so cold? (though I admit quite clever.)
Cold?
Hmm, perhaps i misinterpreted your message. I thought “N=BB(message_length(P))” was some code referring to the string length of my message, I’ll feel stupid if it wasn’t.
On reflection, I’m not sure the formula is quite right, but...
message_length(P) is the size in bits of the shortest possible computer program that evaluates the property P.
BB is the busy beaver function, which gives the largest number that can be output by any program of a given length.
The general idea is that, given a formal notion of the complexity of the predicate, you can place a hard upper bound on which numbers it can ‘reach’. I don’t think the actual formula I gave was correct, but I don’t see how to fix it at the moment.
Ahh, yea good solution. I remember reading about this on wolfram mathworld, look it up there. If you don’t find it exactly it’ll be in a citation.
As I understand things though it isn’t a reasonable solution because the turing machine would have to have more states than the natural universe allows to actually find the answer for many non-halting problems.
Could you elaborate on what question that is your answer to? Is that an answer to one of my questions? I might just be confused.
Is there some fixed number of cases that is sufficient to establish conclusively an arbitrary proposition? Is there some fixed N that is large enough for any P?
I don’t think so. There are only O(k^N) strings of length N. It would be very strange if there were only finitely many true claims about the integers.
Here is a proposed proof sketch, by the way. Suppose for contradiction that there were some N such that all true claims about natural numbers had proofs of length less than N. Necessarily, there is a least such N, call it N’, for which that’s true. Take P as some proposition with a proof of length N’. Take P2 as some other proposition. The proof of (P and P’) is going to have length longer than N’, since it has to include P as a subproof and at least one additional line for P and P’.
This violates our assumption, QED.
P and P’ doesn’t seem like a very interesting proposition, but I don’t know a way to formalize “interesting”. I think there are probably are only finitely many claims that a finite mathematical mind can possibly find interesting.
I don’t think this necessarily follows. Suppose the last few lines of the proof of P read something like:
Pretty sure this can’t happen. We stipulated that we had the shortest proof for P. How did P and P’ get proved without proving P first? Or alternatively, without there being a shorter proof available for P without P’?
What if P = “The prime numbers are infinite or there are exactly 1337 of them” and P’ = “There are not exactly 1337 prime numbers.”
The shortest way to prove P involves proving (P and P’), which is the statement “The prime numbers are infinite.” It would take a roundabout argument indeed to exclude all finite cardinalities besides 1337, without also excluding 1337 and accidentally proving (P and P’).
I don’t have an example to hand. I just have a feeling that there might be some case where the shortest proof of (P and P’) is a component of the shortest proof of P, rather than the other way around.
Ha, I just got it. Pretty good, of course x<N holds for all numbers you try. But of course, there is a simple one line proof that ~P(N+1), so the inductive-conjecture with x<N certainly has a proof in the negative. This only applies to P where there is no proof of the existence of a counter example.
I understood (perhaps wrongly?) the original question to be “is there some fixed N that is sufficient regardless of P?” Did you mean instead “does there exist some P that has a finite sufficient N?”?
Wouldn’t a counterexample itself be proof of the existence of the counterexample?
If counterexamples are a subset of proofs of the existence of a counterexample, then:
(No counterexamples < N AND no simple proof of a counterexample) IMPLIES
(No counterexamples < N AND no counterexample) IMPLIES
(No counterexample)
But the absence of a counterexample is identical with the truth of the conjecture, which is what we were trying to prove. Once you are willing to look at N+1, by induction you are looking at all the positive integers, which takes forever.
Yes...
Unfortunately, very big, as a rule, and not explicitly computable.
Graham’s number would not be nearly large enough for “interesting” conjectures, “interesting” being more complex (by Kologomorov’s definition) than the specification of Graham’s number.
See http://en.wikipedia.org/wiki/Busy_beaver and the material referenced therein.
What if N is larger than the number you get when you plug graham’s as both of the inputs to the ackerman function?
Well, in such a case you can use the method to test somewhat more complex conjectures.
Unfortunately, the growth of the Busy Beaver function is so rapid that the number of bits of complexity of such provable conjectures added by your revised definition of N (I am ignoring the word “larger”, since that makes N undefined), is likely not very many.
What I’m really asking is, if some statement turns out to be undecidable for all of our Tarskian truth translation maps to models, does that make that conjecture meaningless, or is undecidable somehow distinct from unverifiable. What is the difference between believing “that conjecture is unverifiable” and believing “that conjecture is undecidable.”? Are the expectations/restrictions on experience that those two believes offer identical? If so does that mean that the difference between those two believes is a syntactic issue?
See Making Beliefs Pay Rent :
http://lesswrong.com/lw/i3/making_beliefs_pay_rent_in_anticipated_experiences/
Nitpick: you don’t mean “models” here, you mean “theories”.
Why should it?
Oh… you’re implicitly assuming a 1920s style verificationism whereby “meaningfulness” = “verifiability”. That’s a very bad idea because most/all statements turn out to be ‘unverifiable’ - certainly all laws of physics.
As for mathematics, the word ‘verifiable’ applied to a mathematical statement simply means ‘provable’ - either that or you’re using the word in a way guaranteed to cause confusion.
Or perhaps by “statement S is verifiable” what you really mean is “there exists an observation statement T such that P(T|S) is not equal to P(T|¬S)”?
Oh and I’m not talking about true or false in terms of provability (necessarily), don’t forget that there is a semantic theory of truth for formal languages called model theory. Falsification or verification of a statement from a language by semantic means works just as well.
You’re right I do mean theory. But importantly I’m including the first order language that holds for the model of the natural numbers. So the interpreted first order language of the natural numbers is included in this usage of “theory”.
I’m using a 1920′s (ish) style of verificationism that considers cases of P(T|S) ≠ P(T|~S) to be cases of a verifiable statement. See Ayler’s Language, Truth, and Logic. The positivists always held that inductively verifiable statements are still verifiable and thus meaningful.
What makes you say that all statements about the laws of physics are unverifiable? If it restricts your expectations for experience, it is a verifiable prediction. Certainly our hypothetical-deductive theories of the natural universe do in fact restrict our expected stimulus, and can be rejected on the grounds that the restrictions are not met.
I’m using the word “verifiable” as it is used in Positivism and Verificationism. A statement S is verifiable if and only if S is a tautology or there is a strong inductive argument with S as the conclusion, which if cogent gives us a probability for S.
“1+1=giraffe” is meaningless “Godel sentence” is undecidable
“1+1=giraffe” isn’t meaningless. It means that if you add one and one, you get a giraffe. Everyone knows that’s where giraffes come from.
If there is a difference between undecidable and meaningless, and a statement can be shown to be undecidable, then we need to accept that not every meaningful statement is true or false at least in the case of the natural numbers.
So does that mean that we should reject the principle of excluded middle? If so, that means that our standard logics are useless for dealing with mathematical (if not all) reasoning. Intuitionistic logic might be better suited at dealing with these sorts of issues, but it seems strange that some meaningful statements might be neither true nor false.
Well, you could do it like Goedel did. I don’t think you’re grokking the distinctions between different sorts of proofs, so reading up on Goedel’s proof might be what you want.
P.S. To get links to work on LW, replace problematic characters by a percent sign and then the ASCII hex code for the character, e.g. using %5F instead of an underscore ( _ ), or %2B instead of a plus sign ( + ). Or just put them inside brackets and use a link text, in which case you just need to know the ASCII codes for the brackets.
Quote
Sorry about the citations, I’m not good with format most of the time, I’ll work on it.
I fixed the URL that didn’t work. You needed to use tags and a bit of URL escaping, turning ‘+’ in the URL into ‘%2B’. Also, don’t indent first lines, this in not standard formatting on LW.
It would probably help to use [1], [2], [3] rather than *, **, ***.
On it
A statement can only be said to be provable or unprovable within some axiom system. Gödel’s first incompleteness theorem says that for any strong enough axiom system talking about the integers, there will exist true statements about the integers that the system cannot prove.
(ETA ignore the following, it’s wrong. Wow I’m really embarrassed right now. Whoever is reading this, please do me a favor and downvote my comment to oblivion—I don’t want to delete it because it has replies.)
If you proved the Collatz conjecture to be “undecidable either way” in some reasonable axiom system (as opposed to just unprovable in that system), that would imply the conjecture is true about the “actual integers”, because having no counterexamples is the same as being true.
Does undecidability really mean truth for the Collatz conjecture? Suppose it’s undecidable because in the “actual integers” there’s a starting value where the sequence grows indefinitely but there’s no way to prove that. Is that a possible situation?
I think that’s right. A better example here would be the Goldbach conjecture, there we really can claim that if there is a counter-example a sufficiently persistent brute-force search will find it within a finite amount of time.
I’m not sure if this is right, but I think that means that we will never prove Goldbach to be undecidable, since doing so would prove it was true and thereby contradict the claim that it is undecidable.
We could use one axiom system to prove that Goldbach is undecidable in Peano arithmetic. It would therefore be true.
That seems difficult to say, though I might just be confused. I assume your intuition is along the following lines (I’m sure you’ll correct me if I’m wrong ;) ): If Goldbach is shown to be undecidable, then this means that we can’t expect to find a counter example. Thus we can feel free to use Goldbachs conjecture, thus Goldbach’s is true. Contradiction.
The danger here seems to come from whether the intuition that “if we prove GB to be undecidable in PA, then we can safely assume that we will not ever find a counter example” is true, or if something stronger is needed to ensure the latter. I’m not sure about the truth of the claim, maybe someone can clarify?
If there is a counter-example to Goldbach then there is an even integer which cannot be expressed as the sum of two primes. This can in principle be proven simply by listing all the ways it can be expressed as the sum of two positive integers, there are only a finite number of possibilities, and in each case showing a non-trivial factorisation of one of the numbers. All this can easily be done in PA. Thus I’m pretty confident that if Goldbach is undecidable in PA then it is true.
The difficulty, as Endoself points out, it that if we prove it is undecidable without using PA, then we can’t then teleport this statement back into PA and use it in our proof.
Huh. So basically since (if you’ll excuse some sort of sloppy notation as well as sloppy formatting, I just can’t seem to get the latex to fit together nicely on this)
and
So then what is interesting (maybe totally useless in practice, but it hadn’t occurred to me) is that is seems like this generalizes to every proposition that has effectively computable counterexamples. As Khoth pointed out the reason this doesn’t carry over to Collatz is because a test for counterexamples is co-semicomputable.
I think so, it certainly generalises to any problem where counter-examples can always be proven in PA, I don’t know enough about the subject to know whether this is equivalent to computability.
Huh. So basically since (if you’ll excuse some notational sloppiness)
So then what is interesting (maybe totally useless in practice, but it hadn’t occurred to me) is that is seems like this generalizes to every proposition that has effectively computable counterexamples. As Khoth pointed out the reason this doesn’t carry over to Collatz is because a test for counterexamples is co-semicomputable.
Huh. So essentially since
So then what is interesting (maybe totally useless in practice, but it hadn’t occurred to me) is that is seems like this generalizes to every proposition that has effectively computable counterexamples. As Khoth pointed out the reason this doesn’t carry over to Collatz is because a test for counterexamples is co-semicomputable.
Argh! Sorry, in a hurry I got Collatz mixed up with something else, so the second half of my comment was completely stupid.
Only if you can’t proof that given that starting value the function will always rise, but that is an unlikely situation.
What about Godel’s first and second incompleteness theorems? They were not proven using any axiom system. Godel’s proof worked by substituting certain characters in PM with abbreviations, and then abbreviating those abbreviations, etc. He did so in a way that created a string of PM which stated that “this string’s Godel number is not a PM number.” He then used reasoning as old as the famous Cretan to show that that statement could never be consistently decided upon.
These results were shown about axiomatic systems of sufficient strength, but not inside of anyone system. Godel’s completeness theorem of first order logic functions in a similar way (reasoning about a formal system rather than within it). All of these results are achieved by model theoretic methods; if you want to know how you prove something outside of a proof theory look at model theory.
Gödel’s theorems can be formalized. Here’s a formal proof of the first one in Coq. Also, paragraph 8.4 there explains how the second incompleteness theorem can be proved by formalizing the proof of the first one within the system in question.
Model theory is not “platonic”, it lives within an ambient set theory. There are different axiomatizations of set theory, e.g. ZFC, which give rise to different “model theories”. An example from Wikipedia:
I know that you can formalize Godel’s incompleteness theorems, but they were not formalized originally, nor did they need to be formalized to be valid deductive arguments.
Now, you can’t really formalize Godel’s proof without abbreviation, this I know. The godel number of sentence G is a huge number that none of us could ever write down and that a computer would probably have a hard time holding as a value. Have you ever seen a proof of Euclid’s prime theorem in PA? Euclid gave a 6 step proof, in PA there are over 50 steps because every single peice of reasoning gets written down. To actually directly reference every peice of reasoning in godel’s proof is something Godel never does in undecidable props of PM and something that he has no need to do.
To be a valid deductive argument, a theorem must be formalizable. That doesn’t depend on accidental facts like whether its original presentation was formalized or not.
A statement can be proven outside of a formal system (I should have said from the beginning: “outside of a complete and consistent formal system) . There is no complete and consistent axiomatization of the differential calculus as shown by Godel’s first and second theorem, yet I think we can all agree that there are proofs in the calculus.
Your comment seems confused to me. There’s also no complete and consistent axiomatization of the integers, but the incomplete axiomatizations that we know allow us to formally prove statements like 2+2=4. Same for calculus.
The calculus was created before the innovation of formal systems in the 20th century. Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used. Any formal system that accurately modeled the calculus (regardless of its completeness or consistency) would be so much more austere and cluttered than the calculus itself, that it would be of no practical use.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation. Likewise, we don’t actually use PA to prove most statements about the natural numbers, we use the basic agreements we all have about what numbers act like and about what happens when you combine them by certain operators.
So was arithmetic. That is irrelevant to the possibility of formalising them.
Can you elucidate this precise sense? Calculus is just as formalisable as every other branch of mathematics.
What do you mean? I can prove d(x^2)/dx = 2x in as exhaustively complete detail as you want. So can these people and they probably have the proof online somewhere (the web site makes it very difficult to actually read their repository of formalised mathematics). Here’s a road map, starting from Peano arithmetic.
Construct the negative integers as equivalence classes of pairs of Peano integers: (a,b) and (c,d) are equivalent if a+d=b+c.
Do a similar extension to get the rational numbers.
Use Dedekind cuts to define real numbers.
Use epsilon-delta definitions to define limits.
With limits, define derivatives.
Calculate d(x^2)/dx: ((x+delta)^2 - x^2)/delta = 2x + x*delta --> 2x as delta --> 0. QED.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
What I meant by “there is a very formal sense in which the calculus cannot be formalized.” is that you can’t have a complete and consistent axiomatization of the reals. I apologize for the ambiguity. But unlike finitism, frst order logic, boolean arithmetic, category theory, and I’m sure many more, calculus and arithmetic cannot be completely and consistently axiomatized.
People built buildings before mechanics and materials science, but at some point in the development of the technology, you need those to get any further. It’s the same with mathematics. The formal apparatus isn’t what people do mathematics in, but it’s a necessary foundation. Without it you get informal arguments that no-one is quite sure are really valid, as was the case for calculus before the epsilon-delta definition of a limit was worked out. (It was more than a century later before someone was able to make rigorous the original talk of infinitesimals.)
You can proof something outside of a formal system. Algebra and the differential calculus are not formal systems, but you may have proofs within them. Look up model theory.