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.
Or:
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).
Best Answer
Definition:
A waterfall is a system of differential equations of the form$\cdots\cdots\cdots$ [fluid mechanics stuff].
$\blacksquare$
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.