Why do we need/use proof theory?

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.

• What would be an example of a "model-theoretic method" that could be used for, say, arithmetic? It's not like we can write out all the natural numbers and test them all, the way we can with a truth table... – Eric Wofsey Nov 29 '18 at 4:46
• While it's not entirely clear to me what you are proposing, I think a key point to keep in mind is that the incompleteness theorem isn't restricted to notions of "provability" that follow the axioms-and-deductive-rules paradigm. There is simply no algorithm at all that can decide truth in first-order arithmetic. Any algorithmic method of determining whether a sentence in first-order arithmetic is true must fail on some sentences. – Eric Wofsey Nov 29 '18 at 5:24
• @EricWofsey Thanks for your comments. About your first comment - sure, we can't write truth table for all natural numbers but we can still intuitively reason that, for example, for some predicate $P(x)$ it is a valid formula that $P(x) \Rightarrow \exists x(P(x))$. If $P(x)$ is false for all $x$ (which could be members of an infinite collection) then $P(x)$ is false and by truth table $P(x) \Rightarrow \exists x(P(x))$ evaluates to true. On the other hand, if $P(x)$ is true for some $x$ then $\exists x(P(x))$ is true. By truth table we see that again the whole formula is true. So, it is valid. – Daniels Krimans Nov 29 '18 at 5:35
• @EricWofsey I am not sure if there is any proposal from my side because I have no idea about neither proof theory nor model theory. One of my confusions is formula being provable means that formula is true. Then, it seems redundant to reason about formulas being provable, if we can reason about formulas being true in the first place. – Daniels Krimans Nov 29 '18 at 5:42
• When you say set theory uses (i) axioms instead of (ii) saying which statements we accept as true, how do you think those differ? But I think you'll learn some things of interest to you if you research second-order arithmetic, whose models are isomorphic. – J.G. Nov 29 '18 at 6:51

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.

• Thank you for your answer! I have to read it carefully and think about it. – Daniels Krimans Nov 29 '18 at 7:14
• Would I be correct in saying that, to conclude that some undecidable statement in some system is true, we have to move to a larger system? If something is true but unprovable in an axiomatic system, we can only be sure it's true by using a "bigger" axiomatic system? – Sambo Nov 29 '18 at 15:20
• @DanielsKrimans 1) Yes, truth in a finite structure is decidable by brute force, but not so for an infinite structure. But there is no such thing as 'truth in PA': PA is a formal system that proves things, not a structure in which things are true or false. The structure $(\mathbb N,0,1,+,\cdot)$ is a model for PA, so the things PA proves are true in this structure. Truth in $\mathbb N$ is the notion I'm saying is formalizable in set theory. And if ZFC can prove a sentence is true in $\mathbb N,$ then most mathematicians believe it. (But ZFC can't decide everything: just more stuff than PA). – spaceisdarkgreen Nov 30 '18 at 0:58
• @DanielsKrimans 2) Again, ZFC is a system, not a structure. The 'standard model' for ZFC is the cumulative hierarchy $V$, and Tarski's theorem says that we cannot define truth in $V$ within the language of set theory, just like it says we can't define truth in $\mathbb N$ in the language of arithmetic. We can talk about the truth or falsity of first order statements about $V,$ but again, we have to go outside (say, to Morse-Kelley) if we want to formalize this notion of truth. It is the nature of assumptions that you must assume them. – spaceisdarkgreen Nov 30 '18 at 1:09
• @DanielsKrimans For instance, many set theorists believe that various large cardinal axioms are 'clearly true' in the cumulative hierarchy even though we know we cannot prove them in ZFC. So, when they need them, they assume them and believe the results of their proofs are true of the cumulative hierarchy. It is not generally agreed upon whether the cumulative hierarchy is a sharp concept such that 'set theoretical truth' is well defined. (It's certainly nowhere near as sharp as the natural numbers.) – spaceisdarkgreen Nov 30 '18 at 1:20