For a long time I thought that the standard mathematical proofs, only were an informal or imperfect way of writing the proof in the language of first-order logic.

When I say standard mathematical proof I mean all the proofs in analysis, topology etc. that goes like this:

Let x be an element of A.
Hence x is an element of B.


Let epsilon be bigger than 0.
Hence f is continious.

etc etc.

But when we prove things in first-order logic, the deduction always have the matehmatical symbols and connectives etc.($\forall,\neg,(,),\vee$,etc..)

I always thought that these proof were just an informal way of presenting the correct way of the proof as it is in mathematical logic.

But now I am reading first-order logic. And here they formalize these deduction rules etc. However, when they prove something about the language, they still use the ordinary way of proving things as we do in mathematics.

So it is not clear what is the correct, or most basic, or "most perfect" way of proving things of these two. I mean, since we must use this standard mathematical way in order to prove things about first-order logic, does this mean that this way of proving things is just as valid, or maybe even more so valid, than the formal way in mathematical logic, because to even create mathematical logic, we need these proof techniques?

So when a standard calculus text proves that a function is continuous in the ordinary way, this may be a more basic way to prove it, than if it was written in the language of first-order logic, because this technique is needed to create first order logic?

A simple way to state the question: Does the proof writing in first-order logic "precede" the ordinary proof writing used in mathematics, or does the ordinary proof writing used in mathematics "precede" the deduction writing used in first-order logic?

When I say precede I mean, is it more basic, is it more atomic, is it closer to the foundation, is it closer to the "ground"? (This is very imprecise, but I hope you see my point).

  • $\begingroup$ I dont understand what are you talking about... first order logic is used in all proofs... And why you says "matematical logic" as it is different of first order logic? The "ordinary" proof is first order logic too. $\endgroup$
    – Masacroso
    Jul 5, 2015 at 17:39
  • $\begingroup$ I don't mean to distinguish between mathematcal logic and first-order logic, I distinguish between mathematical logic/first-order logic and the way proofs are written in math textbooks. But what I mean is that the proofs in math books are not written in the language of first-order logic, they are written in text instead, and this way of proving things is used to prove things about first order logic when we create first order logic, so is then this way of proving things a more "basic" way of doing it? $\endgroup$
    – user119615
    Jul 5, 2015 at 17:41
  • 1
    $\begingroup$ The basic laws of thinking are ground zero, it doesn't get more basic than that. And yes, it's informal, tough luck. $\endgroup$
    – Git Gud
    Jul 5, 2015 at 17:42
  • 2
    $\begingroup$ @Masacroso I think you're missing the OP's point. I will rephrase the question: Some mathematics is formalized in FOL, but when you study FOL you use mathematical reasoning. So why formalize it if you're going to have to stand on informal ground sooner or later? $\endgroup$
    – Git Gud
    Jul 5, 2015 at 17:47
  • 2
    $\begingroup$ It is the other way round ... mathematical proof dates back to Euclid and before him, while first-order logic dates from the end of XIX century. First-order logic is (also) a mathematical model of "mathematical proof" as well as calculus is (also) a mathematical model of some physical phenomenon. $\endgroup$ Jul 5, 2015 at 18:17

4 Answers 4



A waterfall is a system of differential equations of the form$\cdots\cdots\cdots$ [fluid mechanics stuff].


But that's not a waterfall; that a mathematical model of a waterfall. Likewise proofs studied in mathematical logic, written in a form suitable to submit them to proof-checking software, are not proofs; rather, formal logic is a mathematical model of what logical proofs are. What certain logicians call "metamathematics" is really mathematics and what they call mathematics is really really only a mathematical model of mathematics. It's really a more complicated and icky situation than one might suspect before one thinks about it.

  • $\begingroup$ Thank you very much for your answer. It is hard to know what the foundation of mathematics then is, since logic is just a model of the theory, and ZFC is inside logic. So I guess it is a very shaky thing what is the foundation, I think we can construct a lot from the natural numbers, but we can't say that the peano axioms are the foundations either?, because these axioms is a part of first-order logic? So the natural numbers, and so the rest of mathematics just exist?(I thought the natural numbers was constructed from set theory, and set theory from logic, but since logic is not the found.. $\endgroup$
    – user119615
    Jul 5, 2015 at 21:04
  • $\begingroup$ ation, the natural numbers can't come from there?) $\endgroup$
    – user119615
    Jul 5, 2015 at 21:04
  • 2
    $\begingroup$ @DougSpoonwood : It is people's understanding of the output that proves something. ${}\qquad{}$ $\endgroup$ Jul 5, 2015 at 23:40
  • 1
    $\begingroup$ @MichaelHardy So, given that computers can never understand anything, the possibility of a computer ever proving something is impossible in principle? EQP didn't prove anything at all, it just indicated symbols to get printed to the screen? I certainly don't agree that understanding proves something. Understanding is psychological. Proofs on the other hand are objective, and thus I think you've made a category error. $\endgroup$ Jul 6, 2015 at 0:14
  • 1
    $\begingroup$ I agree with Mike Hardy. Re: computer proofs: If there were no conscious beings, and a 'computer' popped into existence and went through the same series of operations, it wouldn't prove anything. However, given that there are human beings who know how the computer works and know how its outputs correspond to certain objective facts, the computer succeeds in proving something, because we can know that A is true on the basis of a certain output of the computer program. $\endgroup$
    – Owl
    Jul 6, 2015 at 20:27

Your question as asked prompts good answers pointing to the study of foundations, the history of mathematics and the philosophy of mathematics.

You may be asking (as a student) about how working mathematicians answer your question. I think the answer is that most don't. You write proofs to convince yourself and other mathematicians that what you've discovered about some mathematical structure is correct - without really trying to argue further about what "correct" really means.

When my students ask me how to write a proof I tell them they should write something that convinces me that they have convinced themselves for good reason. The level of formality depends on the level of difficulty of the problem and the level of understanding of the student. In elementary school some kids can prove that the sum of two odd integers is even.

In some sense proof is a social construct, created by the society of mathematicians. It evolves over time.As the subject matter of mathematics has become more general and more abstract the work required to create a convincing argument for professionals has matured. Machine assisted proofs are at the edge of what's controversial today.

I hope this rambling helps. It may generate downvotes too.

  • $\begingroup$ "You write proofs to convince yourself..." No, I don't always write proofs to convince myself of something. Even in say number theory, one might try to prove some theorem which we already know to hold as true, just in a different way. Some constructivist mathematicians might do this regularly, because they may well feel convinced by non-constructive proofs and most mathematicians stand convinced by those proofs also. Also, if proof is a construct created by the society of mathematicians, then how do certain programs generate proofs? Are the programs mathematicians? $\endgroup$ Jul 5, 2015 at 22:17
  • $\begingroup$ @DougSpoonwood Fair enough on your first point - looking for new proofs is part of the fun. The last questions about programs that generate proofs are interesting. I don't think any answers would really contradict my sense that what constitutes a proof is determined by the mathematicians of the day. $\endgroup$ Jul 6, 2015 at 1:03

Does the proof writing in first-order logic "precede" the ordinary proof writing used in mathematics [. . .]

I think there are different understandings of "proof" and of "precede". "Proof" in formal logic has a technical sense referring to a symbol sequence satisfying certain formal rules. However, "proof" in ordinary English (the original sense of the word) refers to a certain way of coming to know something.

"Proof" in the ordinary sense means something like: thing that provides conclusive reasons for believing something else (as in "Look, footprints! That's proof that someone else was here!"). In a related sense, a "proof" is a verbal explanation of the conclusive reasons for believing something.

(Note: mathematicians might deny that the footprints would count as proof. That is because the standards in mathematics are stricter than in most other contexts, so that a reason won't count as conclusive unless it is logically impossible for the conclusion to fail to be true, given the reason.)

Now, the "ordinary proof writing" that you're talking about really does, I think, give the reader who understands it conclusive reasons for believing the conclusion; hence, I would say it counts as a perfectly legitimate kind of proof.

What about the formal-logic proofs; what do they have to do with proof in the ordinary sense? Well, a person who understands the rules of a formal system (and knows that they really correspond to valid inference forms) does indeed acquire conclusive reasons to believe a conclusion, when he sees that (the formal-logic symbolization of) that conclusion is the final line in a formal-logic "proof". Thus, formal logic proofs (given that understanding and knowledge) are a species of proofs in the ordinary sense. If you have the formal logic proof, then you have conclusive reasons to believe the conclusion; but you can also have conclusive reasons without having the formal logic proof.

By the way, as an example of the latter, consider Godel's Theorem, which was originally about a certain formal system (the system of Russell & Whitehead's Principia Mathematica). Godel proved that (assuming the PM system was cosistent) there was a sentence that had to be true but could not be proved within the system. Godel's method generalizes to any consistent formal system, and the method actually enables you to construct the true-but-unprovable sentence, given any (consistent) formal system.

This shows that the notion of proof cannot be exhausted by any formal system, since for any formal system, if we know that the system is consistent, we can prove a sentence that cannot be proven in that system. And if we don't know that the system is consistent, then I would say that we can't prove anything using the system. So, for any formal system, the "proofs" that exist in that system cannot exhaust all the proofs (in the ordinary sense) that there are.


The formal logic proofs qualify as more basic.

A formal logic proof of a mathematical statement of a conjecture which is not known whether it holds or not, given that the deductive system used is sound, will qualify as a mathematical proof. For example, the proof of the Robbins conjecture though produced via McCune's input and EQP's reasoning, did qualify as a proof of a mathematical result.

On the other hand, a mathematical proof might NOT qualify as capable of getting translated into a formal proof, because it might not qualify as correct. For example, some of Euclid's old proofs arguably still qualify as mathematical, or at least for a very, very long time they did qualify as mathematical, but they were not correct. Also, the mathematical proof has to get translated into formal logic to make sense from the perspective of formal logic. A formal proof does not have to get translated to "ordinary" mathematics in order to make sense from the perspective of "ordinary" mathematics, it just requires that the "ordinary" mathematician learn the relevant formal system.

  • $\begingroup$ Thank you very much for your answer. But may I please ask you about two comments then. 1. What is your comment to the fact that in order to prove things about first-order logic, we use informal mathematics, should these proofs also be formalized?, will there be circularity? 2. And may I also please ask you about your opinion about the other answers, it seems like they are opposite of what you give. Maybe there is no clear answer to this. $\endgroup$
    – user119615
    Jul 5, 2015 at 21:06
  • $\begingroup$ 1. Go ahead and try to formalize meta-theoretic proofs if you want to. I believe that many experts would consider that a difficult exercise. You'll need a different meta-theory to avoid circularity. 2. I whole heartedly disagree with Ethan Bolker's comment that proof is a social construct, and I believe that the people like Russell, Frege, Lukasiewcz, etc. who founded mathematical logic would resolutely stand against such an instance of social psychologism. I also have the opinion that, strictly speaking, proofs qualify as logical entities, not mathematical entities. $\endgroup$ Jul 5, 2015 at 21:59
  • $\begingroup$ Also, I don't write proofs just to convince myself of the truth of some theorem, or that it appears in some system. One problem consists of finding the shortest proof or a shorter proof under some fixed axioms and rule(s) of inference. In those cases, I'm almost always already convinced that the theorem exists in the system, and I'm not trying to convince myself again that such holds! I'm trying to find a shorter proof. Or maybe I'll try to find a proof that uses fewer variables, fewer axioms, or comes as more easily followed, say by only requiring a unification to occur in one way. $\endgroup$ Jul 5, 2015 at 22:02
  • $\begingroup$ Michael Hardy's comment "Likewise proofs studied in mathematical logic, written in a form suitable to submit them to proof-checking software, are not proofs" makes no sense at all and probably could accurately get said to consist of little more than posturing. A logician could similarly posture and say that no proofs in mathematics exist, and that proof is a logical concept, and thus only proofs exist inside the context of logic. Also, the comment makes no sense in light of the fact of computer generated proofs which have produced new mathematical results. $\endgroup$ Jul 5, 2015 at 22:09
  • $\begingroup$ Thank you, but there is one thing I would like to ask you about. You say it is difficult to formalize meta-theoretic proofs, aren't then these proofs in a way more basic then the ones written in first-order logic? And aren't the type of proofs they do in meta-theory in regards to logic the same type of proof-style as they do in classical mathematics? $\endgroup$
    – user119615
    Jul 5, 2015 at 22:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .