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

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.
  • 2
    Its the "chicken-and.egg" (pseudo-problem): we have a mathematical theory about formal languages: their structure (syntax), their meaning (semantics), their properties (derivability, soundness, completeness). This mathematical theory is called mathematical logic. As every mathematical theory it uses our natural capabilities to speak (write), count and deduce. Jan 17, 2020 at 7:06
  • 2
    I strongly suggest you a careful reading of the two initial chapters of Yuri Manin, A Course in Mathematical Logic for Mathematicians (Springer, 2010); they are a good (but not so easy) exposition of basic mathematical logic with very subtle digressions regarding: language, logic and the world, truth that may help you to understand the "productive" aspect of the above perplexing circluarity. Jan 17, 2020 at 10:14
  • 2
    The first useful distinction is that between a formal theory (the object language level) and the mathematical theory of formal languages (the ,eta- level). Then, the key terminological distinction is that between a derivation in the calculus (the game performed with the formal language) and a proof of a theorem about the calculus (performed in the meta- with the usual math jargon and tools). Jan 17, 2020 at 13:12

2 Answers 2


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.

  • Perhaps I don't understand Gödel's theorem correctly, but is it meaningful to say whether undecidable statements are true or false? I thought for any undecidable statement G, either G or ¬G can be added to the system without causing inconsistencies. If truth (in pure logic) isn't defined rigorously relative to a formal system, then doesn't it become just a subjective and ill-defined notion?
    – WillG
    Jan 17, 2020 at 22:37
  • @WillG Good observation. It is true that formal systems can be constructed in which the Godel Sentence is true or false. But there are several interesting caveats. First, we can say whether some undecidable statements are true or not within the context of an analysis of the system. The Godel Sentence emphatically is true under such an analysis of arithmetic despite not being demonstrably so within arithmetic. Second, it is known that any formal system in which the Godel Sentence is false must be "non-standard," that is it must contain elements which do not correspond to any natural numbers.
    – Geoffrey
    Jan 17, 2020 at 22:52
  • Hmm I suppose this pushes the question down to the level of what makes the "standard" version correct and the "non-standard" version incorrect, i.e., who says that natural numbers alone constitute "true" arithmetic? But regardless, what types of "analysis of the system" are you referring to—something formal or informal?
    – WillG
    Jan 17, 2020 at 23:09
  • @WillG There are formal analyses of arithmetic and Godel which exist. You can find references to papers containing them on the Wikipedia page for the First Incompleteness Theorem. But you may ask how we know that those systems are any better or more trustworthy than the ones which they are being used to analyze. The reason always relies on intuition and whether or not the system appears to comport with reality. But of course you may ask how one can trust one's senses or one's collection of data. At some point you must accept a metric by which "truth" may be judged that can't itself be tested.
    – Geoffrey
    Jan 18, 2020 at 0:00

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.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .