Intuitionistic Logic for Type Theory

I’ve written about intuitionistic logic before. In fact, there’s a whole section about it in my book. But now that I’m reading a lot about type theory, I’m starting to look at it diferently.

When you study classical axiomatic set theory, you’re necessarily also studying classical first order predicate logic. You have to be doing that, because classical axiomatic set theory is deeply and intimately intertwined with FOPL. Similarly, the semantics of FOPL as it’s used in modern math are inextricably tangled with set theory. Sets are specified by predicates; predicates get their meaning from the sets of objects that they satisfy.

You can view type theory – or at least Martin-Loff’s intuitionistic type theory – as having nearly the same relationship to intuitionistic logic. We’ll see that in detail in later posts, but for now, intuitionistic type theory is a fundamental mathematical framework which is built on intuitionistic logic. So you can’t talk about this kind of type theory unless you understand the basics of the logic.

In this post, I’m going to try to explain what intuitionistic logic is, and how it differs from FOPL. (We’ll see all of this in more detail later.)

Intuitionistic logic is a modal predicate logic, which is built around a constructivist idea of truth. The intuitionistic idea of truth ends up being much stronger than what most of us are used to from standard FOPL: it means that nothing exists unless there is a concrete way of constructing it.

For a concrete example of what that means: in standard FOPL with the ZFC axioms, you can prove the Banach-Tarski paradox. Banach-Tarski (which I wrote about HERE) says that it’s possible to take a sphere the size of an orange, cut it into pieces, and then re-assemble those pieces into two spheres the same size as the original orange. Or, alternatively, that you can take those pieces that you sliced an orange-sized sphere into, and re-assemble them into a sphere the size of the sun.

Many people would say that this is, clearly, ridiculous. Others would point out a variety of rationalizations: that a sphere the size of an orange and a sphere the size of the sun contain the same number of points; or that the slicing process transitioned from a metric topology to a collection of non-metric topologies, or several other possible explanations.

But what no one can dispute is that there is one very important property of this proof. Those slices are unconstructable. That is, they exist based on a proof using the axiom of choice, but the sets of points in those topologies can’t be constructed by any process. They exist as a necessary implication of the axiom of choice, but we can’t construct them, and even given a pair of sets, one of which is one of those slices, and one of which isn’t, we can’t identify which one is.

According to intuitionism, this is ridiculous. Saying that something exists, but that it is forever beyond our reach is foolishness. If we can’t construct it, if we can’t describe how to identify it, what does it mean to say that it must exist?

When you’re working in intuitionistic logic, every proof that a type of thing exists consists of either a concrete example of the thing, or a process for constructing an example of the thing. A proof of a negative is a concrete counterexample, or a process for creating one. In computer-sciency-terms, the process doesn’t need to terminate. You don’t have to be able to construct something in finite time. But you need to have a process that describes how to contsruct it. So you can, for example, still do Cantor’s diagonalization in intuitionistic logic: if someone gives you an alleged complete 1:1 mapping between the real numbers and the integers, the proof tells you how to create a counterexample. But you can’t do the proof of Banach-Tarski, because it relies on an axiom-of-choice existence proof of something non-constructable.

The way that intuitionistic logic creates that constructivist requirement is not what you might expect. When I first heard about it, I assumed that it was based on a statement of principle: a proof has to create a concrete example. But that approach has an obvious problem: how do you mathematically define it? Logic is supposed to be purely symbolic. How can you take an abstract statement about what a proof should be, and make it work in logic?

Logic is built on inference rules. You have a collection of statements, and a collection of rules about how to use those statements to produce proofs. It turns out that by making a couple of simple changes to the rules of inference that you can get exactly the constructivist requirements that we’d want. It’s based on two real changes compared to standard FOPL.

Intuitionistic logic is modal. In FOPL, any given statement is either true or false. If it’s not true, then it’s false. If it’s true, it’s always true, and always was true. There’s no other choice. In intuitionistic logic, that’s not really the case: intuitionistic logic has three states: true, false, and unknown. If you know nothing about it, then it’s formally unknown, and it will stay unknown until there’s a proof about it; once you find a proof, it’s truth value changes from unknown to either true or false. All of the inference rules of intuitionistic logic only allow inference from proven statements. You can’t reason about an unknown – you need to have a proof that moves it from unknown to either true or false first.

The semantics of this are quite simple: it’s a tiny change in the definition of truth. In FOPL, a statement is true if there exists a proof of that statement, and it’s false if there’s a proof of the negation of that statement. In intuitionistic logic, a statement is true if you have a proof of that statement; and it’s false if you can prove that there is no proof of the statement If you haven’t proven A, then A is unknown. If A is unknown, then \lnot A is also unknown. A \lor \lnot A is, similarly, not true until you have a proof of either A or \lnot A: it means that either “There is a proof of A or there is a proof of \lnot A“. But if we don’t know if there’s a proof of either one, then it’s unknown! You could argue that this is true in FOPL as well – but in FOPL, you can rely on the fact that A \lor \lnot A, and you can use that in a proof, and explore both options. In intuitionistic logic, you can’t: you can’t do anything with A \lor \lnot A until you’ve got a proof.

It’s amazing how small the change to FOPL is to produce something that is so strongly constructionist. The easiest way to appreciate it is to just look at the rules, and how they change. To do that, I’m going to quickly walk through the inference rules of intuitionistic logic, and then show you what you’d need to change to get classical FOPL. Most of the time, when I’ve written about logics, I used sequents to write the inference rules; for ease of typesetting (and for the fun of doing something just a bit different), this time, I’m going to use Hilbert calculus (the same method that Gödel used in his incompleteness proof.) In HC, you define axioms and inference rules. For intuitionistic logic, we need to define three inference rules:

  1. Modus Ponens: Given \alpha and \alpha \rightarrow \beta, you can infer \alpha.
  2. Universal Generation: Given \alpha \rightarrow \beta, you can infer \alpha \rightarrow (\forall x: \beta) if x is not free in \beta.
  3. Existential Generation: Given \alpha \rightarrow \beta, you can infer (\exists x: \alpha) \rightarrow \beta, if x is not free in \beta.

With the inference rules out of the way, there’s a collection of axioms. Each axiom is actually a schema: you can substitute any valid statement for any of the variables in the axioms.

  1. Then-1: \alpha \rightarrow (\beta \rightarrow \alpha).
  2. Then-2: (\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma))
  3. And-1: \alpha \land \beta \rightarrow \alpha
  4. And-2: \alpha \land \beta \rightarrow \beta
  5. And-3: \alpha \rightarrow (\beta \rightarrow (\alpha \land \beta))
  6. Or-1: \alpha \rightarrow \alpha \lor \beta
  7. Or-2: \beta \rightarrow \alpha \lor \beta
  8. Or-3: (\alpha \rightarrow \beta) \rightarrow ((\gamma \rightarrow \beta) \rightarrow (\alpha \lor \gamma) \rightarrow \beta)
  9. False: \text{False} \rightarrow \alpha. (For a bit of explanation, this rule means that we don’t need to have \lnot rules – \lnot \alpha can be treated as \text{False} \rightarrow \alpha.)
  10. Universal: (\forall x: \alpha(x)) \rightarrow \alpha(t), if t is not bound by instantiating \alpha(t).
  11. Existential: \alpha(x) \rightarrow (\exists x \alpha(x) if t is not bound by instantiating \alpha(t).

That’s intuitionistic logic. What’s the difference between that and FOPL? What kinds of powerful reasoning features did you need to give up from FOPL to get this strongly constructivist logic?

Just one simple axiom: the law of the excluded middle, \alpha \lor \lnot \alpha.

That’s it. Get rid of the excluded middle, and you’ve got the beautiful constructivist intuitionistic logic. All we had to give up is one of the most intuitionnally obvious rules in all of logic.

12 thoughts on “Intuitionistic Logic for Type Theory

  1. Steve Reilly

    One minor correction–in your definition of modus ponens, you use an alpha at the end when you mean beta

    Reply
  2. Mostermand

    Intuitionistic logic is not modal.

    >intuitionistic logic has three states: true, false, and unknown.

    This is true for modal logic, but not for intuitionistic logic.
    Just like FOPL, intuitionistic logic has proven statements, unproven statements and unprovable statements, so in that sense you could argue that you are right.
    But intuitionistic logic does not talk about necessary and possible truths, like modal logic.

    Reply
    1. John Armstrong

      Well, it depends.

      See, there are two different techniques that BOTH get called “proof by contradiction”, and it’s easy to get confused between them when speaking colloquially.

      One approach is really “proof by contrapositive”. That is, in order to prove a -> b, you assume !b and prove !a. Then since you’ve shown that !b -> !a, you conclude that the contrapositive is also true: a -> b

      The other approach — the real “proof by contradiction” — attempts to prove a by assuming !a and deriving an absurdity. What this really proves is that !!a is true. Now, in FOPL we have that !!a a, so we can conclude a from !!a, but in intuitionistic logic all you know is that a -> !!a. That is, if a is provable, then the statement that a is falsifiable is itself falsifiable; the proof of a provides the evidence, since a statement cannot be falsifiable if it has a proof. The upshot is that “proof by contradiction” — in this specific sense — is actually IMPOSSIBLE, not just hard.

      Reply
  3. decourse

    “In intuitionistic logic, that’s not really the case: intuitionistic logic has three states: true, false, and unknown.”

    I think it’s incorrect to talk about “true” and “false” here. I think of the three states as “provable”, “refutable”, and “neither”.

    Oh, and when you say “~a can be treated as False -> a”, you meant “~a can be treated as a -> False”. Or, rather, that’s its definition.

    Reply
  4. reinpost

    You’re glossing over the difference in classical logic between a proposition being true or false and it being provable or unprovable. Truth and falsehood are defined in terms of models, using model theory (at least in the logic classes I took). Inference rules are for proving statements: they define provability, not (classical) truth. Truth and provability are only equivalent if your rules for proving statements are sound and complete. As the Wikipedia page on First-order logic explains, there are plenty such systems for FOPC, which is why you can safely gloss over the difference here – but you can’t in general.

    Reply
    1. markcc Post author

      Yes, I am absolutely glossing over that distinction, and doing it deliberately.

      What I try to do on this blog is take beautiful, complex mathematical ideas, and explain them in ways that help people like me, who aren’t mathematicians, understand what makes the math so beautiful and fascinating.

      That’s the goal. In order to do that, I’ve got to simplify. I’ve written about models before, and I don’t want to discount their importance. But I thought that in this article, getting in to model theory in order to make the distinction between model-truth and logical-provability was just piling too much complexity. For an informal description of intuitionistic logic, I didn’t think it was necessary, and adding it would make the article that much harder to follow.

      Reply
  5. jdkbrown

    Mostermind:

    The models for intuitionistic logic are isomorphic to the models of Kripke’s possible worlds semantics for S4 modal logics. Intuitionism really is modal.

    Reply
  6. Doug Spoonwood

    In addition to the point about modus ponens getting misrepresented, those aren’t axioms, nor axiom schema (an axiom doesn’t include any substitution instances of the axiom, while an axiom schema does include all of its substitution instances). They are simply not well-formed formulas in any formal language, as the formation rules for binary connectives tell you. They may abbreviate such, but if you want to show formal logic, then you need to show what axioms actually look like first, or at least provide the means for the reader to construct those formal axioms/axiom schema.

    Also, in your explanation of what would be axiom 9 if corrected to become an axiom, which I’ll denote using Polish/Lukasiewicz notation “C0p”, your parenthetical comment is incorrect. “C0p” is logically equivalent to “1”. We don’t need to have N (negation) rules, because Np is logically equivalent to Cp0.

    Also, this is just one possible axiom set for intuitionistic logic. And no, the difference doesn’t lie in just one simple axiom (nor is ApNp a rule of inference… rules of inference are metalingustic, axioms lie in the object language). The difference lies in the addition of any axiom, axiom schema, or axiom set which allows us to deduce ApNp.

    Let “#” stand for a variable function of one argument. Suppose we had the following axiom set:

    1 C p Cqp.

    2 C CpCqr C Cpq Cpr.

    3 C CNpq C CNpNq p

    4 C #Apq #CNpq.

    5 C #Kpq #NCpNq.

    We do *not* have ApNp as an axiom, but this axiom set is still not intuitionist, because we can deduce ApNp in this system.

    As a historical note, Hilbert didn’t invent these systems. Frege was the first to study one of them. Consequently, Frege Calculus, or Frege-Hilbert Calculus are more accurate terms.

    Reply

Leave a Reply