I always wondered, we have many choices for choosing what kind of postulates – axioms, deduction rules, we choose for our formal system. For example, there are Hilbert style systems where there are many axioms but few deduction rules. On the other hand, in natural deduction systems there are few axioms but many deduction rules.
I have always felt that most of the working mathematicians never specify or even don't care about what formal system they are using. This might mean that most of the formal systems have the same tools. But is that so?
I am concerned because I want to be mathematician and I also want to make sure that there are as precisely defined rules for what I do as possible. I understand that formal system, for example, logical axioms and deductive rules, is taken so that axioms and deductive rules of it coincide with our intuition about proving. But how do I know that axioms that I write down for my deductive reasoning are correct? I guess that there is no way – the only thing is to assume that they are correct and see where it leads me to. But I am still concerned about the ambiguity of my choice.
Question 1: How does one choose formal system?
Question 2: Is there a proof that most of the formal systems are equivalent to one another?
Best Answer
It looks like what you're concerned about here is how to choose between, specifically, proof systems for classical first-order logic, with examples being Hilbert systems, natural deduction or sequent calculus, all in various variants.
You're not speaking about how to choose between classical first-order logic and, for example intuitionistic logic, nor about how to choose a foundational theory to reason about with your logic (such as ZFC or NF set theory, or perhaps PA for formal number theory).
We can then answer your second question quickly: Yes, all of the proof systems for classical first-order logic are equivalent to each other. Otherwise they wouldn't be proof systems for classical first-order logic! Namely, a proof system for classical first order logic has to prove exactly those entailments that are logically valid according to the usual model-theoretic semantics of first-order logic.
Generally it is fairly easy to prove that two of these systems are equivalent. You can rewrite a proof in one of them to a proof in another by working piece for piece -- each axiom or inference rule in each of the systems corresponds to a small piece of reasoning that we can see once and for all that a given other system can express. Translating a proof piece for piece generally won't produce an elegant proof in the target system, but it certainly will be a valid proof.
Now for the first question, which has two answers.
The first is, you choose the system that makes what you want to do easy. Some properties of proofs are particularly easy to express in sequent calculus. Hilbert systems have long and unwieldy proofs but a relatively small and short definition of what a good proof is, which makes them useful for settings where you need such a formalization. Natural deduction is relatively close to how working mathematicians actually write proofs, at least compared to the other styles.
Which of these properties you put the most weight on depends on what you want to actually do with your formal proofs. And asking that question in the first place presupposes that you are going to do something with them other than write them down and hope you'll get bragging rights from doing so. This assumption is often not true.
This leads us to the second, real, answer: As a working mathematician you don't choose a proof system to work in at all. Unless you are specifically a mathematical logician and do mathematics about logic, you won't be in the business of producing formal proofs at all.
Actual mathematical proofs are written in English (or another comparable natural language, of course) -- not as formal sequences of symbols in a proof system. What is allowed in such a proof is something you'll supposedly get an intuition for as a byproduct of your study of mathematics. That's how everybody did it before formal logic was invented in the decades around 1900, and they achieved, by and large, a pretty good consensus about what is a convincing proof step and what is not. It is to a large degree how everybody still does it.
This informal agreement of which proofs are convincing or not comes first. The rules of formal logic are an attempt to reproduce the informal consensus in the shape of precise, checkable rules. They're remarkably successful at that, but it's still just a map, not the actual territory of mathematical thought.