1. Introduction
When we investigate logic, there is an immediate "logical issue," namely we must use logic to study any subject, including logic. So how do we start?
One solution is that everyday naive logic plus basic knowledge about elementary computing allows us to bootstrap our understanding — first to achieve a clearer sense of the naive logical primitives we normally use in everyday discourse. The new clarity is based on the intuitive computational meaning of the logical operators. Building on this first step, we can achieve a more precise understanding of extensions of the simplest logics to understand reasoning that requires finer distinctions about computation.
A computational understanding of logic has allowed computer scientists to build proof constructing programs and assemble software systems called proof assistants that execute the computations that logic requires. Those assistants in turn help people use formal logic to solve important mathematical and computational problems. Some of these problems concern logic itself.
A similar bootstrapping mechanism enables high-level programming languages to execute on low-level hardware. We use this approach to impart knowledge of logic and mathematics to proof assistants. This is an autocatalytic process, one that steadily improves itself. In these logical investigations we will use the bootstrapping process to achieve a technical understanding of logical systems and learn what it means to implement them and use them to formalize and solve mathematical and computational problems.
Propositions and Evidence
The central objects of logic are propositions or equivalently questions or problems. We are fundamentally interested in whether we can solve problems, answer questions, and find evidence for propositions. These are essentially equivalent tasks. To a first approximation, these tasks require precise declarative thoughts. In ordinary discourse they are the kind of thoughts that constitute assertions, statements or claims or they are used to pose questions.
For example, 1 = 1 is a very simple declarative thought about the natural number 1. We can ask the question "does 1 = 1?". This question is so primitive that we don't need to justify our answer once we see it. We call it a basic fact or a trivial question because we can immediately and intuitively see the answer once we understand the meaning of equality. Indeed we know from the very meaning of equality that every mathematical object is equal to itself, so the question has a trivial answer, yes by definition of equality.
We will avoid saying that a proposition is true, even for 1 = 1. We avoid speaking about "truth" because we are primarily concerned with the reasons we believe a proposition or the grounds we have for asserting it or the solutions we accept to a problem. These notions are all based on intuitive mental acts and our natural ability to experience them as solutions, reasons or evidence. When we understand a proposition and experience evidence for it, we say that the proposition is true based on this evidence.
Prior to "recognizing the evidence" or "seeing the solution" or "experiencing the evidence" or "finding the evidence," we need to understand the meaning of the proposition; that means we must know its sense. To understand an idea or a written expression of an idea such as 1 = 1 or any thought A, we need to first know its meaning or sense. For example, we probably don't know the sense of (0/0)! < 1, so we would not recognize evidence for asserting it or be able to produce evidence for believing it or answer the question (0/0)! < 1?. We call a thought or an attempted expression of a thought or formulation of a problem well formed if we can explain its sense. Such a thought or written expression of it is called a proposition or a meaningful question or a well defined problem.
Once we know that A is a proposition, we are in a position to seek evidence for believing it or asserting it. For some propositions, questions or problems, such as 0 = 1, we know that there is no solution or there cannot be evidence by the very sense of the thought. It is absurd that 0 = 1 for two natural numbers 0 and 1 by the very meaning of these numbers and the sense of equality. These very basic propositions, 0 = 0 and 0 = 1, suggest that we might want to have two atomic thoughts that are the most general examples of trivial propositions. So we introduce the proposition True to mean the proposition that has evidence by its very nature, trivial evidence. So we pick some symbolic representation as trivial evidence, say ★ or yes or obviously.
In a similar spirit of reducing our explanations to something very elementary, we can introduce False and say that this is a proposition that by definition has no correct or meaningful evidence. We could also say that any hypothetical evidence for False in a context of assumptions is a mistake. In this case we imagine that some hypothetical combination of ideas that we thought provided evidence for some other proposition A are wrong or mistaken and could be used to show False in the sense of revealing the mistake. For example, if someone claimed arithmetical evidence for 0 = 1, we would expect to be able to analyze that evidence and find a mistake in it, and that mistake once revealed is evidence for False.
A sufficiently interesting mathematical proposition is called a theorem. Very important theorems have names such as the Pythagorean Theorem or the Fundamental Theorem of Arithmetic or the Fundamental Theorem of Algebra. Less interesting ones may simply be called facts, e.g. it is a fact that 0 < 1 or even more basically that 0 = 0.
Proof Assistants
To know a proposition does not necessarily mean that we have a proof of it in the strict formal logical sense. A proof in the strict sense requires that we have specified the axioms and rules of inference that allow us to prove the proposition from the axioms.
Over the past three decades mathematicians and computer scientists have developed the concept of a publicly implemented formal proof [Con09]. This means that the proof is built by a person and a proof assistant working together in a logical system that is open to public scrutiny and available for general use.1 Moreover, the proof assistant is explained in detail in a users manual and in an expository book that is widely available. It also means that the formal proofs can be checked by independent programs written by interested parties who are not the ones who built and maintain the proof assistant. Furthermore it means that the formal proofs can be precisely related to informal proofs and to precise evidence assembled by other means, e.g., perhaps by a computer program that can execute the evidence terms.
In these notes we reserve the word formal proof of a proposition to apply to machine checked (or generated) proofs in specific completely defined systems of formal logic. We use the term informal proof for arguments that people believe could be made formal in some logic that they could specify. We will see that the idea of computational evidence can be made quite precise as well, using concepts from constructive logic and computing theory without translating them into a specific completely formal logic. We will see that computational evidence can be given in the form of a program and its data types. We can know enough to believe an assertion based on very precise computational evidence without knowing exactly how to formally prove it. Indeed, we think there will be an interesting activity in translating such evidence terms into proofs in a particular formal logic, perhaps into several of them.
This existential circumstance that we can know enough about a proposition to assert it and defend our knowledge claim with very precise computational evidence before we can turn that evidence into a precise proof is a novel aspect of modern mathematical knowledge that is new to the world. Perhaps the major "existential feature" of modern mathematical knowledge is that now we have proof assistants that can help us turn computational evidence into computer checked formal proofs. So the modern standard of proof has created a new category of knowledge called formal knowledge and a new system of integrating that into our informal knowledge.
Outline of the Notes
The typical modern account of logic in a textbook or lecture series starts with the propositional calculus, PC. This calculus is concerned with a few simple ways of combining atomic propositions using the propositional connectives of and, or, implies, and not. Accounts first define the formulas of the logic, then explain the meaning of the operators and the notion of evidence required for knowing propositions built from them. We start with an especially simple propositional logic that uses only the implication operator, denoted ⇒. The symbol ⊃ is used for implication in some logic books.
The topic usually covered next is called First-Order Logic (FOL), and it deals with two additional logical operators called quantifiers. These quantifiers are all and exists, as in saying "for all natural numbers there exists a larger one," symbolically we write ∀n:ℕ. ∃m:ℕ. n < m.
1 Proof assistants are also called interactive theorem provers or provers for short.
Table of Contents