mathematical proof vs. first-order logic deductions

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).

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.

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.

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.