Introduction

We refer readers to Logical Investigations with the Nuprl Proof Assistant for a more detailed introduction on basic logic and logic rules, propositional calculus, first-order logic, evidence, Nuprl proofs, and more.

Constructive logic vs Classical logic

The central concept in logic is usually taken to be propositions, and the central questions are how do we understand them, i.e. grasp their sense, and how can we know them. The classical approach to knowledge is to define truth with respect to an ideal mathematical universe described in set theory.

The conventional account of mathematical logic is based on First-Order Logic (FOL), and its main story line is that axiomatic set theory is the standard language for defining all mathematical concepts. Set theory is expressed in FOL with only a few axioms, nine to be precise if Zermelo-Fraenkel axioms are used. To close the loop on the story, set theory is used to give the informal semantics of FOL.

This is a very compelling and elegant story that has served mathematics well for over a century. It is a story that does not require any mention of constructive or intuitionistic mathematics, and does not need to bother with explaining constructive logic at all.

In some textbooks, the constructive alternative is mentioned because it encourages students to think more carefully about the rules of logic. In most of these accounts, constructive logic is explained as a subsystem of FOL that does not use the Law of Excluded Middle (LEM), which is the law that says for any proposition P, it is either true or false. Written symbolically as P ∨ ~P.

This is not a very good explanation because the meaning of constructive logic is not given in terms of truth let alone in terms of sets. The intended interpretation of constructive logic reveals it as a richer logic in important ways. Constructive semantics is based on mental constructions, and among these is the notion of computable function. So constructive logic takes as basic a concept that is fundamental in computer science, the notion of a computable function. Indeed constructive logic axiomatizes features of computable functions. It makes computation part of the logic itself, not a derived notion from set theory. Indeed, set theory does not have among its primitives any notion of computation. In set theory, it is possible to model computation, but it is not possible to do computation.

In constructive logic, the situation is that it is possible to both express computation in the axioms and to do computation in the logic. On this reading of logic, first-order logic is a programming language. We use the term iFOL to describe the constructive (or intuitionistic) system. So the contrast is that FOL is a formal system of logic, and iFOL is a formally precise programming language. As we will see in these notes, it is possible to execute certain kinds of proofs in this logic and to interpret others as constructing data for the computations.

One technical novelty of this approach to first-order logic is that we can give a new meaning to the formulas, treating them as types. We can give a new meaning to the proof rules, treating them as basic constructors for programs and data. The primitive ideas of type theory are sufficiently rich to give this new semantics to classical logic. We call this a virtual evidence semantics because the evidence is not available for use in computations. It is interesting that we can explain classical logic in this manner, one that is very close to how constructive logic is explained, but just different enough that we can justify the classical rules such as ~~P => P and P v ~P" but we cannot compute with them. We say more about computation next.

Based on the constructive reading of logic, the proof rules are rules of programming. They are intuitive and useful. We interpret the rules as telling us how to give computational evidence for propositions. The evidence tells us what mental constructions we use to know a proposition. We understand a proposition once we understand exactly what constitutes evidence for knowing it. We don't know how to prove a proposition until we know what evidence is required to believe it.

In classical logic, the rules do not have a computational meaning. However, as we show in these notes, we can define classical logic in constructive logic once we understand what evidence counts for knowing the possible axioms that are accepted in classical logic but not in constructive logic. Essentially there are only two hard cases, understanding P ∨ ~P and understanding existence, ∃x:D.P(x). Existence is the easy case, we pretend we are from Missouri and demand to see the witness d in the domain of discourse D. Seeing the witness is believing.

For the Law of Excluded Middle (LEM), P ∨ ~P, it turns out to be easier, as Kolmogorov noted already when he was twenty years old, to first understand the rule of double negation elimination, namely ~~P ⇒ P. Kolmogorov suggested a unification of intuitionistic and classical logics based on his double negation embedding of classical logics into intuitionistic ones. These notes explain this in detail and then illustrate it in the propositions from Kleene's logic book, Introduction to Metamathematics [2].

Introduction to Virtual Evidence

The constructive approach to truth is to understand how knowledge is represented in logic and how we formalize it. The key idea is that the meaning of a proposition, say P, is given by a type whose elements can be understood as evidence for knowing P. It must be evidence that people and machines can produce, check, manipulate, communicate, and thus people can also experience. The summary here is based on enthusiasm for the idea that constructive mathematics is concerned with finding evidence that leads us to believe a proposition whose sense we grasp. Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning.

That method and its modifications do not provide a new semantic account of classical logic, rather they rely on syntactically translating classical propositions to constructive ones. The new idea proposed here is to define virtual constructive evidence for classical propositions using the refinement type of computational type theory to specify the classical computational content. The following refinement type, {Unit|P}, is critical.

The new axiom, ~~P ⇒ {Unit|P}, creates virtual evidence for P. Virtual constructive evidence carries more information than is provided by standard classical semantics.

Brouwer gave the following (unpublished) fully constructive argument for ~~(P ∨ ~P) which is reported on page 26 of Van Atten’s small 2004 book On Brouwer [4]:

"Can one ever prove of a proposition, that it can never be decided? No, because one would have to do so by reductio ad absurdum. So one would have to say: assume that the proposition has been decided in sense X, and from that deduce a contradiction. But then it would have been proved that not X is decided after all."

Now we introduce a simple but powerful new notion associated with the classical rule of logic favored by Kolmogorov and adopted by Kleene and others to express classical logic by adding one new law to constructive logic, the law of Double Negation Elimination (DNE): ~~P ⇒ P.

The New Axiom

The new idea presented here involves two steps. The first step is to hide (or suppress) the evidence for a proposition P using the refinement type. The classical meaning of P is based on the constructive refinement type {Unit|P} where Unit is the type with precisely one element, *. To know {Unit|P} constructively, one needs to know evidence p for P, but it is not included with the evidence type. Only * is an element of this type when it is non empty. The evidence p is virtual in this setting. We also call this refinement type squashed P. It is clear that there is evidence for P ⇒ {Unit|P}, so we know this implication constructively. However, we do not know {Unit|P} ⇒ P in general because we are only assuming that there is evidence for P, and even if we had known evidence for P and hidden it, to prove this proposition, we would need to reconstruct that evidence. Clearly we do not have evidence for {Unit|P ∨ ~P} ⇒ (P ∨ ~P) for all propositions P.

We can account for what people might mean when they believe that (P ∨ ~P) is obviously true. What they often say when asked to defend this axiom is that for every well defined proposition P, it is not possible to imagine any deeper explanation of LEM – it is just “obvious” and hence axiomatic. But it is far from universally obvious. So one approach is to simply say the following: we cannot imagine that ~(P ∨ ~P) could ever be true since accepting that would require us to exhibit a proposition P which we know to be unknowable. We cannot imagine how this would be done. Indeed, we constructively know that it cannot be done.

This step does not take us beyond constructive logic, but it introduces the idea that there is a type that is designed to hide evidence.

If we know ~P constructively, then we know that {Unit|P} is definitely empty – there is nothing to hide. When we know constructively that there is no evidence for ∼ P, then we know that {Unit| ~~P} cannot be empty. We also know that it can have only one possible unhidden element, namely *. We call this hidden evidence virtual because we can use {Unit|P} as if we had evidence for P when we are trying to prove other refinement types.

The second step is adding the following new axiom of Classical Introduction (CI): ~~P ⇒ {Unit|P}.

Our proposal is to forego including evidence for P when realizing the new axiom ~~P ⇒ {Unit|P}. This step agrees with the classical notion that evidence is not required for axioms. It agrees with the constructive notion that axioms should be realizable in that the constant function whose value is * is an adequate realizer for the only evidence that must be visible.

So this axiom is constructive in the sense that we have not lost the required computational meaning of the type. The constructive meaning is given in terms of evidence and computation which are entirely missing from the semantics of classical logic.

Outline of pages and Nuprl rules and proofs

The classical theorems presented in this math book are from the Introduction to Meta-Mathematics by Stephen Kleene. In this, he presents a list of about 100 theorems, starting with those of basic propositional logic and ending with first-order logic. He marks some from this list with a superscripted circle to indicate that they can't be constructively proved. However with the new proof tactics we can prove these in Nuprl. The ones we've chosen to be presented here require more attention and are more interesting to consider. Some are particularly interesting among these and have small descriptions to accopmany. The first theorem is not one of Kleene's, it is Pierce's Law. It is shown here because it is an interesting and more well known classical proof that is also known for not being constructively provable.

We can solve the classical proofs constructively in Nuprl by using new Nuprl rules that utilize the Law of Excluded Middle. If we have a squashed goal G, i.e. H ⊢ {G}, and we know the Law of Excluded Middle {G v ~G} has evidence *, then we can instantiate this into our hypotheses using the Nuprl rule ClassicalCase, inputting which proposition we want to apply this to. We would therefore have H,…, {G ∨ ~G} ⊢ {G}. We can then open {G ∨ ~G}, since our goal is still classical, and proceed by cases. However we can easily see that one case will be trivial: H,..,G ⊢ G. Doing many of these classical proofs we've seen that every proof has a trivial case like this. Thus we can simplify this idea to the Nuprl rule ClassicalContradiction, which will add the unsquashed nontrivial case to our hypotheses. If we had used this rule in our above example it would have looked like H,…, ~G ⊢ {G}, with the trivial steps omitted, from which we can proceed constructively.

Every proof done here uses ClassicalContradiction. We denote this in the extract as (CC;ng. ____), to signify that we've used classical contradiction on the current goal to get evidence not goal, ¬G. For example if we are at the goal ⊢ {A} and we need to use classical contradiction to proceed, then our next extract term would look like (CC;na.___).

The structure of the pages is as follows. Each proof is broken down step by step with the corresponding extract term to the right. The evidence for each hypothesis is given as e : H. The full extract term is located above the proof breakdown and is built bottom-up by filling in the fragment terms into the preceding blank.

Proofs that are if and only if are split into forward and backward direction and done separately. We present each case in the forward directio, and underneath we have the arrow direction to signify which direction it was presented in the theorem. In the second direction presented, evidence terms are reused and redefined, e.g. f : ___ in the first direction is not associated or equivalent to f : ___ in the second direction. It is always the case that one direction is constructive and one direction is classical. The direction presented first is always the constructive direction and there is an arrow next to the extract that indicates which direction it is as presented in the theorem. Since the direction is constructive there are no curly brackets around the proof. We could have left them on for consistency but we would remove them immediately in the proof since they're unnecessary. However, in Kleene 84,85,98, and 99 it was necessary to squash inner terms to be able to prove the classical direction, therefore the outermost curly brackets were left on in the constructive direction because they are necssary to open the inner squashed terms. At the bottom of the page is the proof of the theorem done in Nuprl. There is a version directly on the website and there is also a link to a PDF version.






Table of Contents