Note that my knowledge of both proof theory and model theory is incredibly weak. I just started learning about them using Kleene's "Mathematical logic".
If I understand it correctly then one of the tasks of logic is to be explicit about our reasoning in mathematics and to understand what reasoning is valid and which is not. Model theory in Kleene's book is described as a way to think about logic where (classically) you assume that there are some objects for which we do not care about their internal structure, but the only thing that matters is that each of them is either true or false, but not both. Also, we assume that from these objects we can construct formulas, such as "A and B", "A or B" and so forth. Then we are interested in how the truth and falsity of these formulas depend on truth and falsity of our basic objects. We define this using truth tables. Then, we can always compute the truth or falsity of formulas depending on truth and falsity of our basic objects. Then we can say that logical consequence from A to B is valid if whenever A is true then B is true. Then, in principle, we could use this as a criterion whether we do mathematics right – if every logical consequence we are making is valid then it is correct and we can use it.
Now, another point of view mentioned in the book is a proof theory. There, we do not think about the truth of the objects, but about provability. By that we mean that we choose some formulas which we call axioms and we choose deduction rules which we assume can be used in our deductions, and then we say formula is provable if there is a sequence of formulas where each is either axiom or obtained from deduction rules that use formulas that appear previously in the deduction. Note that there is no truth notion here. I am concerned here because the way we choose axioms is exactly by taking into account our interpretation. For propositional calculus, for example, we can prove that formula is valid if and only if it is provable from suitably chosen axioms. So, for me, it seems that for propositional calculus proof theory is just an alternative method obtaining formulas that are valid and obtaining logical consequences that are valid. Probably, it is more convenient and less lengthy than reason about truth values, but still, we do not gain any new insight conceptually.
But my biggest concern is when we consider stronger theories, say, those for which Godel's incompleteness theorem applies. There we can show that the truth is not the same thing as provability. If I am not mistaken, you can show that things that are provable are true but not the other way around. But, we are interested in the truth in the first place. We, therefore, see that method of proving from axioms and deductive rules can give us true formulas, but we will never be able to use this method to get all of the truths. So, why do we not forget proof theory? Why don't we just argue using model-theoretic methods like truth tables or other methods that are concerned with truth? Why is it true that, for example, modern set theory is given using axioms and deductive rules, but not by saying which statements we accept as true and then we do mathematics using logical consequences which are valid. It seems to me that by restricting ourselves by axioms and deductive rules, we restrict the number of true results we can obtain.
I hope that I am not confusing you too much and that the question makes a little bit of sense. I would appreciate any comments or advice about this topic. If you want me to be more careful with what I am trying to say, please let me know and I will edit my question accordingly.
Best Answer
Your question makes sense to me, but it's a bit hard to answer concisely. The short answer is that for the most part, when mathematicians decide to accept anything as true, it is because it has been proven rigorously. And as you allude to, rigorous reasoning lends itself to an analysis where we convert the reasoning into a formal proof in some system (say PA, or ZFC). When you come up with a semantic proof for the truth of something by considering models (or truth tables for propositional logic), you are using reasoning that can be formalized in ZFC or in rare cases, some somewhat stronger system. In fact 'mathematically accepted fact' roughly correlates with 'has a proof formalizable in ZFC.' Thus, formal proofs are always there... it's really the only way we know to clearly establish mathematical truth.
Some of your thinking seems to stem from overgeneralizing from the example of propositional logic. Frankly, I'm a bit surprised your instinct was that formal proofs are the more convenient method here. A formal proof can be tedious to find, even in the case of propositional logic, especially if you're using an inconvenient Hilbert-style system. On the other hand, what could be easier than just plugging in some values to a truth table? (conceptually... computationally, the problem does not scale well).
However, this is an artifact of the fact that propositional logic is decidable. If we move on to first order logic, we're faced with difficulty: how do we decide if every $m\in M$ satisfies $\phi(m)$ for $M$ some structure and $\phi$ some formula of its language? We no longer necessarily have a decidible problem. The "brute force solution" would be checking $\phi(m)$ for every $m\in M,$ which cannot be done if $M$ is infinite (and who knows if $\phi(m)$ is decidible itself). It turns out that this basic difficulty is not surmountable in general, and Godel's theorem and the halting problem are ways of seeing this.
To show that a sentence is true in the structure $\mathbb N,$ we must have some way of proving things about $\mathbb N.$ Finding a proof formalizable in some system like PA or ZFC are the only accepted ways of doing so, although the incompleteness theorem tells us we can't decide every statement in some fixed system.
So what of these "true but unprovable" statements of Godel? How can we determine it's true if it isn't provable? Well, if we're considering the Godel sentence $G$ for PA, we haven't shown it isn't provable, only that it isn't provable in PA. The proof that the Godel sentence is true is done in a stronger system than PA. The basic argument is this: Recall that $G$ essentially says of itself that it is not provable in PA. Now, assuming PA only proves correct things (i.e. it is sound), we can see that it can't be provable in PA, and thus that it is true (since it says it is not provable in PA). It turns out the premise of soundness can be weakened to just consistency.
Godel's first theorem "if PA is consistent, then $G$ is not provable in PA" can be shown in a fairly weak system. The first step toward proving $G$ by the logic above is showing PA is consistent and a closer look reveals this must be the step at which PA fails (this is Godel's second theorem). However, you can prove PA is consistent in ZFC, and the easiest way to do this is to show that $\mathbb N$ is a model for PA. Then the rest of the reasoning falls into place, and proceed to prove $G$ is true. You believe this since your reasoning is formalizable in ZFC and you believe ZFC (or the fragment you used, anyway).
So semantics are not some black box that generates truths that you cannot get from formal proof. Philosophical worries notwithstanding, the truths are there, but there's no way to see what they are without proof. Instead, ZFC is a formal system that proves some things that you cannot prove in PA. And ZFC is also incomplete: in order to believe that its 'true but unprovable statements' (like its Godel sentence or Con(ZFC)) are in fact true, we need to believe assumptions beyond those made in ZFC.