How do proofs about logic fit into a logical framework?

Question

I'm learning logic from Michael O'Leary's A First Course in Mathematical Logic and Set Theory. In chapter 1 he carefully explains the meaning of logical implication (p ⊨ q), logical inference (p ⟹ q), proof (p ⊢ q), and "star" proof (p ⊢* q). (The "star" proof p ⊢* q means q is provable from p using only a certain restricted set of inference rules—I don't know if any of his terminology/notation is standard.)

As he introduces this material, he also states certain "theorems" and "proofs" about these logical structures. For example,

Theorem 1.4.2.

For all propositional forms p and q, p ⊢* q if and only if p ⊢ q.

Never mind for the moment exactly what his inference rules are and what the exact definition of ⊢* is. What concerns me is what it means exactly that we are "proving" the above result. To be sure, I understand his proof and even agree with it intuitively (he shows that all the inference rules of ⊢ can be achieved using only the restricted rules of ⊢*). What I don't understand is whether it is logically rigorous to say that we are "proving" anything about this logical system, which itself is supposed to be telling us precisely what it means to prove things.

These "meta" theorems and proofs (such as 1.4.2) are certainly not the kind of theorems/proofs that fit within this logical system and proof theory (which tells us nothing about how to formally manipulate strings involving ⊢). Here are some ideas about what they might be instead:

• Informal arguments that could serve as guides for some meta-logical system that is able to rigorously prove statements about this logical system.
• Informal arguments whose sole purpose is to guide how we casually think about, feel about, or interpret our formal logic.
• I'm missing something, and these really are theorems and proofs that could fit within the logical system and proof theory already laid out.

Answer 1

Deductive proofs in first-order logic are essentially transformations of one statement of the language into another. You start with some statement (or several or none at all) and then produce from it an ordered sequence of new statements derived by successive applications of the established rules of the system. You can end this sequence at any time and any new statement produced in this process is said to have been "derived" or "proven." This simple, highly structured process is why theorem proving can be automated: computers are really good at following rules.

Proofs are collections of statements in the system, and statements about proofs are not statements in the system - they are statements in natural language (e.g. English). Therefore, statements in English about statements in the system are not bound by the rules of the system and do not live within the system. However, just as it is possible to say whether $2+2=4$ is right or wrong within the context of arithmetic without using arithmetic, one can determine whether a proof is valid in the system without using the system to do it. This is because any impartial observer can check the rulebook to see whether or not the rules were followed correctly.

Here's the rub: it is reasonable to think that the logic of the system is also the logic we use to analyze statements about the system, but that's simply not the case. When we analyze the system, we are merely checking the rulebook, and the conclusions we draw are objectively true or false. Although, a different system with a different rulebook might lead to a different conclusion.

That said, I sympathize with (what I believe is) your concern - viz. "We are using logic to analyze logic, so isn't that circular? How can we use logic before we know how it works?" The answer is that natural, intuitionistic logic doesn't necessarily rely on a formal system because its truth is self-evident. Let me put it this way: Why do you believe in arithmetic? Is it because you've studied the rules and they seem internally consistent, or is it because its conclusions are patently obvious? 2 apples and 3 apples is 5 apples, ergo $2+3=5$. Don't fall into the trap of putting the cart before the horse. The system models reality, not vice versa. The model is imperfect, but we use the system because the model aligns with our intuitions.

As a final point, take for example the Incompleteness Theorem. The theorem is essentially a proof that the statement "This statement is not provable." exists in the system of arithmetic. This matters because such a statement is patently true (the alternative - i.e. being provable - would be a contradiction and is thus impossible), but it is not able to be proven to be true (by its very nature). However, its truth is not obvious within arithmetic since that would require a proof. It is only within our intuitive understanding of the statement's meaning that we can discern that it must be true regardless of what the system can or cannot say.

Answer 2

A formal logical system does not ever tell you what it means to prove something. It tells you what works in the model. The point is that you need to have faith that the model models your real thinking, and not something else. Otherwise, you can't use it to discuss the nature of thinking.

Without proof of a more casual sort that the proofs you are going to discuss map onto our ordinary understanding of real meaning, there is no reason for the formalism. If we don't have a really good faith that we are reliably representing the rudiments of language, we can prove all kinds of things about systems and models, and that will not really be saying anything about logic.

This is all part of Hilbert's program of Formalism to divorce basic math from a Platonic interpretation by proving that all there really is that makes logic work is a set of rules about manipulating symbols. But to do that, we would need to find a model of logic that is consistent and complete. Godel proves Hilbert is wrong. We can't have such a system, if we want to include arithmetic in our reasoning.

So reasoning must have a basis outside the axiomatic method, if it is to both make sense, and capture the boundaries of argumentation. You either need an outside reference that gives you a way to argue the virtues of both sides of various undecidable assertions. Or you need to accept that the boundaries of decision making extend beyond what can be established in precise language through strict argumentation.