11 One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of 12 time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in 13 intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical 14 Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible 15 to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, 16 nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic 17 type theory along with a Beth-like model for it that provide some middle ground. On one hand 18 they incorporate a notion of progressing time and include evolving mathematical entities in the 19 form of choice sequences, and on the other hand they are consistent with a variant of the classical 20 LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian 21 intuitionistic type theory. 22 2012 ACM Subject Classification Replace ccsdesc macro with valid one 23

How do we convey the remarkable truth that the ancient study of logic, dating to Aristotle over two thousand four hundred years ago, is now more relevant than ever? It is especially important in one of the youngest academic disciplines, computer science, roughly only fifty years old. Our goal is to understand this relevance to computer science and its potential. Aristotle gave us a dozen books to build on – Prior Analytics (2 books), Posterior Analytics (two more books), and Topics (eight books). He undertook the earliest known formal study of logic and introduced the concept of variables . He studied for twenty years at Plato’s Academy. His wife Pythias taught Alexander the Great. Both constructive and intuitionistic mathematics are fundamentally about computation , as is computer science. Intuitionistic mathematics originates in the work of L.E.J. Brouwer, circa 1907 to 1966, and is primarily about understanding the continuum of real numbers and the logical principles that govern it. Oddly one of Brouwer’s earliest contributions was to logic, and remains controversial in some logic courses. He denied the law of excluded middle P ∨ ¬ P as he was working on his doctoral dissertation. It was a bold move for a young PhD student to challenge Aristotle. That was part of Brouwer’s character. We will begin to examine his reasoning and the responses to it in this lecture.

This course in Applied Logic is co-listed in the Computer Science and Mathematics Departments as CS4860 and Math4860. We have been jointly teaching it since at least 1994 [81]. Key elements of the subject have been taught since Aristotle [6] in 350 BC, so for 2,350 years. A lot can happen on that scale, and we can’t cover all of it. This offering of the course focuses on the modern period since Computer Science became an important new academic discipline, circa 1962 at Purdue University and then at Cornell University in 1965. Now in 2020, computer science is one of the most relevant and most popular subjects, attracting over 1,600 majors and requiring a large faculty, making CS departments among the largest in universities. Over its long history, logic has become a deep and broad subject with strong ties to mathematics, philosophy, and computer science. The steadily increasing capabilities of Artificial Intelligence (AI) have substantially enriched the role of computer science in both logic and mathematics. One reason for this is that computers are capable of supporting rigorous reasoning and checking proofs and programs for errors. Computers can check formal proofs for correctness without“understanding” any of the concepts the way humans do. As computers become more able to help in checking proofs we seek further ways to engage them in helping us discover proofs. The use of computers has opened a game changing period in the history of mathematics, logic, and computer science [76]. In this context we can see that some logical proofs also act as computer programs that perform the computations implicit in the formal proofs. This connection will be a theme of this course under the heading “proofs as programs” [10]. During world war II Alan Turing worked on building a computer called Colossus. For 32 years the existence of this machine was a secret. After the war Turing began to speak about mechanical intelligence. He famously said that“if a machine is expected to be infallible, it cannot also be intelligent,” (see page 70 of Darwin among the Machines which we discuss below). He also said that we want a machine that can learn from experience. This is a goal that we are working on at Cornell. We collect many fragments of successful formal proofs, and we apply them to help users make faster progress on creating other formal proofs. Our goal is to significantly speed up and extend this capability. It is one of many methods we are

In this lecture we present important results by Godel, Kleene, and others about the intuitionistic propositional calculus, iPC. Godel shows that iPC is only apparently narrower than classical PC. Kleene notes that the consistency of iPC secures the consistency of PC. Godel showed that there is no truth table decision procedure for iPC. Gentzen showed that there is a decision procedure for both PC and iPC Investigations into logical deduction by Gerhard Gentzen, 1969 [11]. Basically we we can prove that iPC is decidable using the same method that proves PC is decidable. These are important results by some of the best logicians. We draw heavily on Kleene’s book Introduction to Meta-Mathematics, ISHI Press International, 2009 [14]. 1 Intuitionistic Propositional Logic Axioms We recall the axioms given in Joan Moschovakis’ 2018 article in the Stanford Encyclopedia of Mathematics, SEP [19]. These axioms are listed below. 1. A⇒ (B ⇒ A). 2. (A⇒ B)⇒ ((A⇒ (B ⇒ C))⇒ (A⇒ C) 3. (A⇒ (B ⇒ (A & B)) 4. (A & B)⇒ A 5. (A & B)⇒ B 6. A⇒ (A ∨B) 7. B ⇒ (A ∨B) 8. (A⇒ C)⇒ ((B ⇒ C)⇒ ((A ∨B)⇒ C)) 9. (A⇒ B)⇒ ((A⇒ ¬B)⇒ ¬A) 10. ¬A⇒ (A⇒ B)

Powerful yet effective induction principles play an important role in computing, being a paramount component of programming languages, automated reasoning, and program verification systems. The Bar Induction (BI) principle is a fundamental concept of intuitionism, which is equivalent to the standard principle of transfinite induction. In this work, we investigate the compatibility of several variants of BI with Constructive Type Theory (CTT), a dependent type theory in the spirit of Martin-Löf’s extensional theory. We first show that CTT is compatible with a BI principle for sequences of numbers. Then, we establish the compatibility of CTT with a more general BI principle for sequences of name-free closed terms. The formalization of the latter principle within the theory involved enriching CTT’s term syntax with a limit constructor and showing that consistency is preserved. Furthermore, we provide novel insights regarding BI, such as the non-truncated version of BI on monotone bars being intuitionistically false. These enhancements are carried out formally using the Nuprl proof assistant that implements CTT and the formalization of CTT within the Coq proof assistant presented in previous works.

Constructions are central to the methodology of geometry presented in the Elements. This theory therefore poses a unique challenge to those concerned with the practice of constructive mathematics: can the Elements be faithfully captured in a modern constructive framework? In this paper, we outline our implementation of Euclidean geometry based on straightedge and compass constructions in the intuitionistic type theory of the Nuprl proof assistant. A result of our intuitionistic treatment of Euclidean geometry is a proof of the second proposition from Book I of the Elements in its full generality; a result that differs from other formally constructive accounts of Euclidean geometry. Our formalization of the straightedge and compass utilizes a predicate for orientation, which enables a concise and intuitive expression of Euclid’s constructions.

Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl.

We present an extension of the computation system and logic of the Nuprl proof assistant with intuitionistic principles, namely versions of Brouwer's bar induction principle, which is equivalent to transfinite induction. We have substantially extended the formalization of Nuprl's type theory within the Coq proof assistant to show that two such bar induction principles are valid w.r.t. Nuprl's semantics (the Good): one for sequences of numbers that involved only minor changes to the system, and a more general one for sequences of name-free (the Ugly) closed terms that involved adding a limit constructor to Nuprl's term syntax in our model of Nuprl's logic. We have proved that these additions preserve Nuprl's key metatheoretical properties such as consistency. Finally, we show some new insights regarding bar induction, such as the non-truncated version of bar induction on monotone bars is intuitionistically false (the Bad).

This article connects certain writings of Raymond Smullyan on logic and formal systems with current research on constructive type theory. It also considers aspects of teaching logic to computer science students. Those students require logic in order to precisely define programming tasks and demonstrate that programs meet logical specifications of these tasks. Smullyan's book First-Order Logic has been used for many years to teach logic to computer science students at Cornell. This article includes a brief account of an elegant result from this book. It is based on an extension of a fourteen page technical report that analyzes two pages on Boolean valuations in chapter one of his classic book. The analysis and results are formulated in a formal system of type theory and proved using the Nuprl proof assistant. The article also briefly considers the role of partial types, showing how they provide a new way to prove unsolvability results, another topic on which Smullyan has written with remarkable clarity. Partial types also provide a simple and faithful semantics for Hoare's partial correctness logic, widely used to reason about programs and taught in computer science as an important applied logic. They also make it possible to state a clean rule for defined functions in Hoare logic.

In the current problem set we are investigating two problems in computational geometry using concepts from our study of the computable real numbers and calculus. The main problem we are examining is the notion of a set of points in the plane and how to compute their convex hull. In the last lecture we briefly discussed how it is possible to investigate computational geometry in a more abstract manner, in the spirit of Euclidean geometry. In such an approach we start with an abstract type of Points. We do not need to think that these will be represented as real numbers. We can imagine them as “points in the plane” and state the properties of line segments, angles, triangles, polygons, and so forth using abstract axiomatic mathematics in the spirit of Euclid, but with more precision. This is the way algebra is usually presented as we have seen in looking about the algebraic properties of the rational and reals. Both of these types of numbers satisfy the algebraic properties of a field. We can define this concept without reference to any specific instances. We are interested in the general properties of any field.

Dr. Mark Bickford will discuss his implementation of the constructive reals in Nuprl, and we will discuss their significance both in practical applications and in the development of type theory. Supplementary material for this lecture is written by Dr. Bickford and included on the course web page for Lectures 16 and 17. He will also discuss his very insightful new result about the connectedness of the reals.

Lecture 3: More reduction rules, the notion of Currying and Uncurrying, and typing rules for some of the constructs. A key signature idea of the ML family of languages is introduced, the polymorphic types which in this version of the course are written with both the standard OCaml syntax ‘a, ‘b, ‘c, ... and with Greek letters as in the original articles on ML, e.g. α, β, γ, .... It would be good to know how to curry and uncurry functions.

This lecture continues our discussion of the constructive reals and intuitionistic reals. We look briefly at other options beyond the approach taken in the book Constructive Analysis by Bishop and Bridges which is a resource for this course available on the PRL project page (www.nuprl.org). Another resource is the calculator for the constructive reals provided in Nuprl as a public resource. It uses algorithms verified in Nuprl by Dr. Bickford. This calculator relies on an implementation of bignums and relies on the Nuprl software stack which includes Lisp at the lowest level. We have high confidence in this resource which we have been using for over a decade. It is likely that the very first verified implementation of the reals numbers was done in 1985 and reported on in Chapter 11 of the book Implementing Mathematics from 1986. In the next lecture we will look at nonstandard models of the reals which include elements called infinitessimals. We will consider them in a constructive setting as well.

We are gradually becoming familiar in the last three lectures with an approach to geometry in the style of Euclid, using abstract primitive concepts such as points, lines, polygons, congruence and so forth and with proving theorems that show the existence of geometric objects such as equilateral triangles and with performing certain constructions such as bisecting a line segment or an angle or with copying a line segment from one location to another. Euclid’s proofs are intended to provide constructions, but they are not always sufficiently complete to show all of the key steps. This approach to geometry does not rely on knowing about real numbers and the analytical approach to geometry. As we started to explore this approach to geometry CS3110 in 2016, we came across an intriguing small book by Turing Award winning computer scientist Donald Knuth called Axioms and Hulls[8].1 This book provides an excellent basis for a precise account of synthetic computational geometry. We have embarked on showing how this theory can be formalized in constructive type theory using the Nuprl proof assistant. Dr. Mark Bickford will illustrate the progress he has made on this in the next lecture (after spring break). In addition one of our post graduate researchers, Ariel Kellison, will show how we can formalize elements

We will present a very interesting theorem from Bishop and Bridges, and then we will briefly consider the nature of nonstandard models of the classical reals as presented in H.J. Keisler’s book, Elementary Calculus and his free 203 page instructor’s book entitled Foundations of the Infinitesimal Calculus [8] which is provided as a course resource with this lecture. We have not covered the basics of model theory on which the nonstandard models are based, and we will not attempt that because it is a subject not easily covered in constructive type theory.

Beginning in the early 1920’s, L.E.J. Brouwer proposed an intuitionsitic reformation of the foundations of mathematics.1 Among the key elements underlying this reconstruction were: (1) a complete rejection of the principle of the excluded middle, and (2) a collection of axioms culminating in what is commonly referred to as Brouwer’s Thesis on bars. The latter arose from Brouwer’s effort to redefine the continuum from an intuitionistic standpoint, that is, to characterize and analyze the continuum as a constructively defined object. Brouwer’s Thesis, which he proposed as an axiom on the nature of bars, resulted in the proof of the Bar Theorem and its corollary, the Fan Theorem. Interestingly, most mathematically significant consequences of the Bar Theorem can be proved using the Fan Theorem alone [14]. The fan, or finitely branching tree of potentially unbounded depth, can be viewed as the well-studied data structure from computer science, but it is important to understand that in the context of the Fan Theorem, the relevant "objects" within the tree are not the individual nodes and their hierarchical relations to one another, but rather the paths originating from the root of the tree and in particular, the paths of unbounded length. Such paths can be interpreted as unbounded sequences of successive choices, which can in turn be used to define the real numbers. Brouwer’s goal was to analyze the nature of these unbounded paths, and, in particular, to effectively characterize them using only collections of finite objects. Roughly speaking, the Fan Theorem states that the space of all unbounded binary sequences, i.e. the Cantor space C, can be "covered" by a finite set of finite sequences. In essence, this guarantees a form of compactness for C. As van Atten writes in [15, p. 41]:

These preliminary notes contain far more material that was covered in the first lecture. A redacted copy of the notes will be posted next week. We leave these longer notes up now to help students understand better the nature of the course. The actual lecture only covered material up to OCaml syntax.

It is well-known that concepts and methods of logic (more specifically constructive logic) occupy a central place in computer science. While it is quite common to identify ‘logic’ with ‘first-order logic’ (FOL), a careful examination of the various applications of logic in computer science reveals that FOL is insufficient for most of them, and that its most crucial shortcoming is its inability to provide inductive definitions in general, and the notion of the transitive closure in particular. The minimal logic that can serve for this goal is ancestral logic (AL). In this paper we define a constructive version of AL, pure intuitionistic ancestral logic (iAL), extending pure intuitionistic first-order logic (iFOL). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL, given by its realizer for the transitive closure operator TC, which corresponds to recursive programs. We derive this operator from the natural type theoretic definition of TC using intersection type. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further outline how iAL can serve as a natural framework for reasoning about programs.

Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal language that is intuitively clear to the programmers. We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system. This article focuses on the basic ideas of formal EventML programming illustrated by implementing a fault-tolerant consensus protocol and showing how we prove its safety properties with the Nuprl proof assistant.