“On the Meanings of the Logical Constants and the Justifications of the Logical Laws”
I know I tried to write up the Meetup announcement to draw people here with a computer science or programming background. And then I threw at you this dense philosophical paper which assumes you’re familiar with names like Gentzen and languages like German and Greek not Javascript or C#.
So, that was pretty unfair of me, I apologize. In order to amend for that let me tell you why I think this paper is important, why I love this paper, right now. Then we can dive in.
So first, you need to believe me when I say that logic and programming are actually the same task entirely. This is known as the “Proposition as Types” correspondance and it’s very deep. I’m not really going to talk about it here but instead merely assume its existence and hope that by the end of the talk you’ll have some hint as to why it’s meaningful and true—and then I suggest you read Wadler’s paper Propositions as Types to learn more.
Given p-a-t we can translate this entire long, dense philosophical paper about logic into a long, dense philosophical paper about programming. And then it is nothing more or less than a justification for the existence of programming and for key operations and notions we could not conceive of doing without.
You should care because p-a-t tells us that when logics and (programming) languages align nicely then they’re probably catching on to something truly universal. Actually, Wadler suggests that such a thing might be too small—we call things like the gravitational constant “universal” to imply that they hold throughout our universe. But we can imagine such things varying, perhaps, just a bit, in another universe.
So Wadler suggests that when logic and programming align we’re hitting on something more than universal—it could not be possible for such a structure to fail to exist in any conceivable universe.
And so by studying p-a-t you can look at programming languages with a lens to what is utterly fundamental. And Per Martin-Löf’s goal here was to describe in painstaking detail, over the course of three lectures, what these utterly fundamental aspects were.
Recognizing them in your own programming will benefit your clarity of thought. Practically, people often say that learning Haskell will change the way you look at programming for the better. I program in Haskell a lot and I’d suggest that the concepts of this paper form a large chunk of that transformative factor.
So, with all that, maybe you’ll believe me that getting something from this paper is valuable. And so maybe you’ll give me a little rope to hang myself on those words for now because I need to talk about history and logic in order to properly contextualize what’s going on here and why PML is spending so much time to explain it in such painful detail.
PML is a Swedish logician and statistician born in 1942 who retired just a few years ago in 2009. His most relevant contribution is in the development of what’s called intuitionistic type theory—his particular formulation is called, unimaginatively, “Martin-Löf’s Type Theory” (MLTT).
If you’ve heard of interactive theorem provers or languages like Agda, Coq, or Idris then you’ve technically heard of MLTT as they are usually elaborations and modifications of MLTT. While this isn’t totally true, for the purposes of this talk I’m going to just say that dependent types are all due to MLTT and its ancestors.
So, if you’re interested in advanced types you cannot ignore this man.
The next thing I’d like to talk about is MLTT itself, but, honestly, it’s unnecessarily complex for the point of this paper. Instead, what I really need to explain is constructivism in logic.
Really, this may be entire point of the first lecture.
But in order to talk about constructive logic I probably need to talk about classical logic.
I’m not a logician, so I’m going to be fairly gestural here.
One way of thinking about logic, sometimes called “classical logic” is concerned with things called propositions like “A and B” or “D implies Q”. Moreover, it’s concerned with a relationship between propositions called consequence. Consequence defines what it means for one proposition to entail another. For instance, we might say “A” entails “A” or we might say “P and Q” entails “P”.
Users of classical logic want to specify a set of elementary propositions called axioms and then study the entire space of entailed propositions. It turns out that with well-chosen axioms you end up with a set of consequences which describes much of what we’d like to talk about in mathematics.
For much of modern history people have considered what the proper design of consequence and entailment is. Some standard ones will be immediately recognizable—they’ve been around since Aristotle!
- Law of non-contradiction: It cannot be that both “A” and “Not A” are simultaneously entailed
- Commutativity of And: For all propositions “P” and “Q”, the proposition “P And Q” entails “Q And P”
- Modus ponens: The propositions “P leads to Q” and “P” together entail “Q”
- Law of excluded middle: For all propositions “P”, one of “P” or “Not P” must be entailed
These arise in a very natural way from considering propositions as either “True” or “False”. Most likely you’ve seen truth tables in high school so this idea should be very familiar.
This idea was really popular in the early 1900s as pre-eminent mathematician David Hilbert was organizing the world’s mathematicians into a program of research aimed to find the one true axiomatic basis for all of mathematics and then an “efficient program” for computing each and every mathematical truth by tracing consequence on and on.
This program ended in the 1930s when Kurt Gödel proved it impossible. It turns out that any system of finite axiomatization like what I just described, should it ever get too powerful, either violates non-contradiction or is incomplete—mathematics always escapes it.
Sadly, Gödel announced his result the very day before Hilbert gave his retirement address galvanizing his Program onward: “We must know; we will know!” That line ended up engraved on his gravestone in what I consider to be a little bit of dark irony—although it certainly represents Hilbert’s mathematical charisma. Even if Gödel threw disaster to his particular program, Hilbert’s desire to explain the universe in mathematics is a fundamental value that lives on today.
Anyway, I told you that stuff mostly to say that PML finds it absurd.
PML writes from a camp called the “constructivists” or the “intuitionists”. This was invented by one of Hilbert’s star pupils, Brouwer, who sneakily rose to prominence under Hilbert’s wing before publishing a paper entitled “The untrustworthiness of the principles of logic” where he claimed that the Principle of Excluded Middle was, well, untrustworthy and so any system which depends upon it or anything that entails it is flawed.
Hilbert, seeing that he was currently engaged in a career-defining program to use such a system to its fullest extent, was less than pleased and spent years arguing publically and vehemently with Brouwer.
But what we’d like to get to here is why Brouwer distrusted PEM.
The thing that defines an intuitionist is their belief that mathematics is an activity, an action, a force produced by the person who writes it or consumes it.
To talk about this, I’ll use a notation from Frege’s Begriffsschrift that I like.
To an intuitionist, propositions in the sense of classical logic are things that may be considered. In my adopted use of Frege’s notation, you write them like this
— P and Q
where the horizontal line (“Inhaltsstrich”) means “what follows is a statement”. An intuitionist is not satisfied with consideration, though, and so they seek to complete this notation like so
\|— P and Q
where the vertical stroke (“Urteilsstrich”) represents the act of assertion. It means that not only does that proposition hold content but I also assert its truth.
RAWR! Urteil!
More importantly that just the subjective act of assertion, however, is the need to construct some reason for your assertion to be true—an artifact of that assertion, a proof.
So ultimately, this is the problem.
The Law of Excluded middle asserts that for any proposition “P” we have “P Or (Not P)”.
Brouwer and his camp of Intuitionists dislike that because it doesn’t indicate which of the two holds—is it “P” or “Not P”? I don’t know what I’m asserting. I don’t know how to construct my proof.
Which might seem kind of silly at first sight. Lots of the time it ought to be very easy to determine whether “P” or “Not P” holds. When this is the case, we call “P” decidable (which ought to sound familiar).
But we often want to talk about things in logic which are not so easily decidable. Brouwer and Hilbert fought because Hilbert wanted to prove things about infinite, complex mathematical objects using LEM and Brouwer claimed those proofs were untrustworthy, nearly vacuous. Fightin’ words.
So, anyway, that’s intuitionism. A big part of PML’s paper is about justifying intuitionism. He spends most of Lecture 1 distinguishing propositions and assertions (which he calls judgements).
So now we’ve touched upon another sensitive topic—the notion of undecidability and infinity. The reasons for stressing out so much about intutionism may not be clear without examining infinity a bit closer. We’ll also see how infinity is closely tied to computer science and why mathematician’s historical fear of infinity kept them from discovering this for a while.
In particular, it’s worth noting that types, static types to be clear, were originally invented by mathematicians for exactly this purpose.
Around 30 years prior to Gödel’s announcement, Bertrand Russell discovered something annoying about recursive mathematical sets: they were pretty trivially inconsistent with themselves—they violated the logical principle of non-contradiction!
In particular Russell constructed the following set
R = { x | x is not an element of x }
such that: If R is an element of R then R is not an element of R and If R is not an element of R then R is an element of R
This was an especially big blow in the nascent Hilbert Program since mathematicians had been using (recursive) sets as the very bedrock foundation to “prove all of mathematics”. The problem was resolved by more clearly defining the axioms of set theory into a system called Zermelo-Frenkel Set Theory (with the “Axiom of Choice”).
But Russell also invented another way to avoid this strange recursion: it was a little bit annoying and verbose and required mathematicians to write down more things which ought to be pretty obvious so, as with all such things, is was doomed to languish in obscurity as the more dynamic ZFC took central stage.
Russell invented the “first” static type system: he called it the Extensional Hierarchy and it, more or less, declared that set theory has to obey a typing discipline such as to outlaw “R”. Frege had been doing this as well.
Around the same time people were battling with the Extensional Hierarchy (and shortly after Gödel’s announcement), Alonzo Church produced his Lambda Calculus and discovered a similar problem.
Church’s original goal with LC was to clarify one of Hilbert’s goals with his Program—Hilbert wanted mathematics to be “effectively computable”, but nobody knew what that meant yet. Church discovered the LC, determined how one could encode arithmetic into it, and eventually declared that propositions which could be encoded in the LC were exactly those which are “effectively computable” (later Turing showed that the same idea could be encoded in his Turing Machines, btw).
Unfortunately, LC has a problem with respect to serving as a notion of computability of mathematical truth—we’re all probably familiar with it, too: you can encode infinite loops!
Y = λ f . (λ x . f (x x)) (λ x . f (x x))
This is a major part of how we compute today, but it feels a lot like Russell’s paradox—very tight self-reference causes formal systems of sufficient power to explode. In logical terms, an infinite loop entails “P” for any proposition “P” which lets us violate non-contradiction.
Church resolved this explosive problem in much the same way that Russell did: he invented the Simply Typed Lambda Calculus which, through clever typing discipline, makes illegal the exact kind of tight self-reference which causes explosions. Subsequently, the LC was shown, by the very beginnings of Propositions As Types, to be a consistent encoding of logic.
So now we have the relevant pieces:
- Intuitionism requires that we construct and prove and assert things especially when dealing with infinities
- Types are shown to be a mechanism for carefully constraining our assertions so as to respect the troubles of infinity as described by Gödel and Russell (and Kleene)
This is the atmosphere that Per Martin-Löf came into as he wrote this paper. The goal was to justify, from the very beginnings, the necessity of points 1 and 2 and to use them to construct a viable way of reasoning. While we’ll also take as being a viable way of programming.
Lectures 1 and 2 concern themselves mostly with justifying intuitionism. Lecture 1 asserts the need to distinguish propositions and judgements in a way kind of in-line with Frege. Lecture 2 discusses two important judgements and their relation: first “P prop” which indicates knowledge of what is required to prove “P” and then “P true” which indicates how to prove “P”.
Under p-a-t we can see these as follows:
- A judgement is the physical act of constructing a program, writing it down, and checking its validity. If we believe our compiler then our construction of the relevant program text is exactly the act of judging its meaning.
- The judgement “A prop” corresponds to “A type” and indicates that we’ve written a valid type for which we might wish to seek to instantiate via a program.
- The judgement “A true” corresponds to “m : A” where “m” is our program which we’ve constructed and typechecked thus proving the inhabitability of “A”, it’s truth.
So that brings us up to Lecture 3. This one is probably the most notation heavy and strange. It uses a language and syntax created by Gentzen called “Natural Deduction” to describe the actual rules for forming proposition judgements and truth judgements. These are much like the rules of entailment that described consequence back in classical logic, but, as PML stresses, they do not describe consequence but instead inference—they give us the “allowable moves” to go from constructions of proof of one type to another.
They describe the very, very, very, very basics of the programming language of the universe.
What is this language? Roughly, if you’re familiar with Haskell or OCaml (or F#, or Rust, or Scala, or Racket, or Swift, or really any language if you have a little discipline), PML describes non-recursive algebraic data types. Technically, we need to add a better story for existential quantification to Haskell and we have to throw out Haskell or OCaml’s recursivity because they’re too liberal and run afoul of paradoxes of infinity.
And so, PML’s presentation of this language here is a little immature. Later formulations which give rise to Agda and Coq and Idris are much more refined.
But the goal of this paper isn’t to describe this language. Instead, PML describes the language in order to serve an example of how evident this mode of reasoning is. It arises as a natural progression of the investigation of consequence, construction, infinity, and types that was conducted all throughout the 20th century. To his eyes, there could be no other sane way of reasoning than to construct proofs via rules like this. It is a line of reasoning beginning with nothing more than immediate evidence of how logic works.
- PML invented modern dependent type theory (MLTT)
- The word “programming” is used 1 times—and under a totally different definition
- PML writes in the language of “logic”, but logic and programming turn out to be identical, so it’s completely valid to read everything in this paper as being about programming.
- PML’s goal is to say that logic is not about talking about truth and falsity, but instead about the physical action of proof
- Ultimately, that physical action ends up being exactly programming.
- So, PML is describing why programming must exist and, then, why it works.
- He forces us to view programming as full of life instead of dead, syntactic, formal
- He starts at the beginnings of logic and arrives at programming, so it starts off slow.
- Let me justify why that needed to happen
- Hilbert wanted to make things dead, mechanistic, completely
formal; Gödel proved that mathematics could not be so
circumscribed
- Constructivism is the notion that mathematics/programming requires work and force—it must be done!
- Comes in three parts
- “I have merely wanted to give a preliminary hint at the
difference between [judgement and proposition] by showing how
the terminology has evolved.”
- This section leaves us thinking Judgement is either “assertion of truth” or “assertion of falsehood”
- Or non-existence altogether—“unknowing”
- Justify the need to formally define “proposition”
- “This immediately implies that the traditional definition of the act of judging as an affirming or denying and of the judgement, that is, the proposition in the terminology then used, as an affirmation or denial has to be rejected, because ‘A prop’ is certainly neither an affirmation nor a denial.”
- “And the definition would simply be that, when understood as an act of judging, a judgement is nothing but an act of knowing, and, when understood as that which is judged, it is a piece or, more solemnly, an object of knowledge”
- “To judge” is “to know”, “judgement” is “knowledge”. Spoken abstractly these are things, but when you make it your own it becomes “evident judgement” and “evident knowledge”
- We must aquire evidence in order to judge
- Brouwer: “there are no unexperienced [judgements (truths)]”
- “For example, if we consider the two forms of judgement
A is a proposition
and
A is true,
then there is something that you must know in order to have the right to make a judgement of the first form, and there is something else which you must know, in addition, in order to have the right to make a judgement of the second form. And what you must know depends in neither case on A, but only on the form of the judgement, “… is a proposition” or “… is true”, respectively”
- “Thus, if proof theory is construed, not in Hilbert’s sense, as metamathematics, but simply as the study of proofs in the original sense of the word, then proof theory is the same as theory of knowledge, which, in turn, is the same as logic in the original sense of the word, as the study of reasoning, or proof, not as metamathematics.”
- “Thus, if we do not have the notion of evidence, we do not have the notion of proof.”
- “Since, as I said earlier, the law of the excluded middle, indeed, all the laws of the classical propositional calculus, are doubtlessly valid on this conception of the notion of proposition, this means that the rejection of the law of excluded middle is implicitly also a rejection of the conception of a proposition as something which is true or false.”
- “What would an example be? If you take a proposition like, The sun is shining,to know that proposition, you must know what counts as a verification of it, which in this case would be the direct seeing of the shining sun.”
- “The important point to observe here is the change from is in A is true to can in A can be verified, or A is verifiable. Thus what is expressed in terms of being in the first formulation really has the modal character of possibility”
- “The difference between an inference and a logical consequence, or hypothetical judgement, is that an inference is a proof of a logical consequence. Thus an inference is the same as a hypothetical proof.”