Introduction to (Formal) Logic (via, and also to, AI)
Table of Contents
Selmer Bringsjord
with Naveen Sundar G.
\(\wedge\) Joshua Taylor \(\wedge\) \(\ldots\)
Figure 2: Larry
Figure 3: Lucy
[All artwork (all of which is copyrighted) for the LAMA paradigm by KB Foushee.]
Terminology & General Orientation
This course is an advanced, accelerated introduction to deductive formal logic, with at least some informative pointers to inductive formal logic, in which formalisms for dealing with uncertainty (e.g. probability theory) are included, and to heterogeneous formal logic (which allows reasoning over visual content) as well. This course makes crucial use of AI for learning, and also provides an introduction to AI itself, at least AI of the logicist variety. In particular, students are exposed to a pure and general form of logic programming (so-called PGLP).
- Terminology
Note that sometimes `symbolic’ is used in place of `formal.’ This is bad practice, since formal logic include heterogeneous logics in which not only symbolic, but also pictorial information, figures. Deductive formal logic is a superset of mathematical logic; the latter is the part of deductive formal logic devoted to the mathematical analysis of mathematics itself (which is why some also use the term ‘meta-mathematics’ to denote mathematical logic). Part of the present course is devoted to mathematical logic. The specific phrase used to describe what the student is principally introduced to in this class is: beginning deductive logic, advanced (BDLA); hence the title of our textbook (see below).
- What Next?
After this class, the student can proceed to the intermediate level in formal deductive logic, and — with a deeper understanding and better prepared to flourish — to various areas within the formal sciences, which are invariably based on formal logic, at least to a high degree. The formal sciences include e.g. theoretical computer science (e.g., computability theory, complexity theory, rigorous coverage of programming and programming languages), mathematics in all its traditional branches (analysis, geometry, topology, etc), decision theory, (economic) game theory, set theory, probability theory, etc.
- What is Formal Logic?
In general, formal logic is the science and engineering of reasoning,1 but even this supremely general description fails to convey the flexibility and enormity of the field. For example, all of classical mathematics can be deductively derived from a small set of formulae (e.g., ZFC set theory, which you’ll be hearing more about, and exploring) expressed in the particular formal logic known as `first-order logic’ (FOL = \(\mathscr{L}_1\), which you’ll also be hearing more about), and computer science emerged from and is in large part based upon logic (for peerlessly cogent yet non-technical coverage of this emergence, see C Glymour’s Thinking Things Through). Logic is indeed the foundation for all at once rational-and-rigorous intellectual pursuits. (If you can find a counter-example, i.e. such a pursuit that doesn’t directly and crucially partake of logic, S Bringsjord would be very interested to see it.)
- Context: A Research University
You have wisely decided to attend a technical research university, with a faculty-led mission to create new knowledge and technology in collaboration with students. RPI is the oldest such place in the English-speaking world; it may know a thing or two about this mission. The mission drives those who teach you in this class. The last thing we want to do is simply convey to you how others present and teach introductory formal logic. As should be obvious by now, we think we have invented a better way to define, specify, and present formal logic, and are working hard to explain this invention, to explain it to others, and to disseminate the invention in question. The better way in question is denoted by the phrase `Logic: A Modern Approach\(^{TM}\),’ or simply by the abbreviation `LAMA\(^{TM}\),’ pronounced so as to rhyme with `llama.’
- A Disclaimer!
Please note that guest lecturers other than NS Govindarajulu and A Bringsjord should not be assumed to have fully affirmed the LAMA\(^{TM}\) paradigm. This thus applies specifically to TAs Shreyansh Nawlakha and Swapnil Khandekar.
As to what these thinkers hold in connection with LAMA\(^{TM}\), that is an open question. You are free to inquire.
- Graduate Teaching Assistants; Further Help
The TAs for this course are the most-capable duo of Shreyansh Nawlakha and Swapnil Khandekar; their email addresses, resp., are
shreyanshnawlakha@gmail.com
andkhands2@rpi.edu
.Please note again A Disclaimer!.
- Prerequisites
There are no formal prerequisites. However, as said above, this course covers formal logic, and though the course is an introduction, it has also been said above that it’s an advanced, accelerated one. This implies that — for want of a better phrase — students are expected to have a degree of logico-mathematical maturity, achieved for example through mastery of first-rate coverage of high-school mathematics. You have this maturity and mastery on the assumption that you understood the math you were supposed to learn in order to make it where you are. For example, to get to where you are now, you were supposed to have learned the technique of indirect proof (= proof by contradiction = reductio ad absurdum), from either or both of Algebra 2 and Geometry. An example of the list of concepts and techniques you are assumed to be familiar with from high-school geometry can be found in the common-core-connected Geometry: Common Core by Bass et al., published by Pearson in 2012. An example of the list of concepts and techniques you are assumed to be familiar with from high-school Algebra 2 can be found in the common-core-connected Algebra 2: Common Core by Bellman et al., published by Pearson, 2012. It’s recommended that during the first two weeks of the class, students review their high-school coverage of formal logic. While this material will be covered in this class, it helps to have at least some command of it from high school. A much more robust treatment of prerequisites and a suitable background for this course is provided in the syllabus.
Texts/Readings
Students will purchase access to and obtain the inseperably interconnected trio of
- the e-text Logic: A Modern Approach; Beginning Deductive Logic via HyperSlatee\(^{TM}\), Advanced (LAMA-BDLA);
- the HyperSlate\(^{TM}\) software system for (among other things) proof construction in collaboration with AI technology; and
- HyperGrader\(^{TM}\), an AI-infused online system for assessing student progress.
Each member of this trio will be available online after purchase of the relevant code-carrying envelope in the RPI Bookstore. Full logistics of this purchase, and the content of the envelope and how to proceed from this content, will be explained the first class (and subsequently, as needed). Updates to LAMA-BDLA, and additional exercises, will be provided by listing on relevant LAMAe\(^{TM}\) web pages upon signing in (and sometimes by email) through the course of the semester. You will need to manage many electronic files in the course of this course, and e-housekeeping and e-orderliness are of paramount importance. You will specifically need to assemble a library of completed and partially completed proofs so that you can use them as building blocks in harder proofs; in other words, building up your own “logical library” will be crucial.
Please note that HyperSlatee\(^{TM}\) and Slatee\(^{TM}\) are each copyrighted: copying and/or distributing this software to others is strictly prohibited. You will need to AGRRE online after are the time of registration a License Agreement. This agreement will also cover the textbook, which is copyrighted as well, and cannot be copied or distributed in any way, even in part.
In addition, occasionally papers may be assigned as reading. Two, indeed, were assigned in the syllabus, on the first day of class.
Finally, slide decks used in class will contain crucial additional content above and beyond LAMA-BDLA, information posted on HyperGrader\(^{TM}\), and HyperSlate\(^{TM}\); this additional content will be available on the web site as the course unfolds through time.
Syllabi
The version of the course now underway is the Spring 2019 edition, the syllabus for which is available here. This is a robust, detailed syllabus, and is required reading — and reading that will pay off, for sure. Syllabi for some prior years are given in this enumeration:
HyperSlate\(^{TM}\)
This is the software system used for constructing proofs and arguments in collaboration with AI technology, and is available here after registration and sign-in. The older, locally-run-only Slatee\(^{TM}\) system will also be available for those who care to explore it.
HyperGrader\(^{TM}\)
This is the AI system for submitting, getting assessed, and earning points for proofs and arguments constructed in HyperSlate\(^{TM}\) (and Slatee\(^{TM}\)), and is available here after registration and by sign-in.
LAMA-BDLA Textbook
This is the textbook for the course, and is obtained after registration and sign-in, by downloading.
Class-Day Topic and Content (includes associated files; e.g., slide decks, lectures, tutorials, HyperSlate\(^{TM}\) files, etc.)
- January 10 2019: General Orientation to the LAMA\(^{TM}\) Paradigm, Logistics, Mechanics. (S Bringsjord)
The syllabus was projected and presented, and discussed, in detail. Please note that the syllabus, in particular, makes clear that students who wish to opt learning under a different paradigm than that of LAMAe\(^{TM}\) should take Intro to Logic in a Fall semester, since the “Stanford paradigm” is in use then.
- January 14 2019: Motivating Paradoxes, Puzzles, and \(\mathcal{R}\), Part I (a.k.a. “Why Study Logic?”; S Bringsjord)
The many answers to the “Why study formal logic?” question are enumerated, and explained. An avowal of Bringsjord’s immaterialist position on formal logic is included. For a full video of the 2018 version of this session done in 1:1 style, replete with audio proofs of some of the rather tricky problems presented, click here. Students for whom the problems presented are a breeze, can conceivably test out of the course, but one specific requirement in that regard is that such a student must’ve arrived from high school math and/or computer science with full command of explosion [viz. ∀ Φ, φ, ψ: if Φ \(\vdash\) φ ∧ ¬ φ, then Φ \(\vdash\) ψ].
- January 17 2019: Motivating Paradoxes, Puzzles, and \(\mathcal{R}\), Part II (S Bringsjord)
This slide deck, expanded over that used in the previous class, shows some of solutions expressed as informal proofs, and contains Moriarty’s ticking-bomb challenge!
- January 21 2019: MLK Day!
No class.
- January 24 2019: Whirlwind History of Logic — With Skepticism About The Singularity Derived Therefrom (S Bringsjord)
In our time-traveling tour of computational formal logic and AI, we go from Euclid, three centuries BC, to — possibly? — The Singularity in our future, and along the way note that Leibniz, peerless polymath and autodidact, is the inventor of modern formal logic, and that at AI’s DARPA-sponsored dawn in 1956, the automated reasoning Logic Theorist stole the show. The presentation ends with Bringsjordian skepticism about The Singularity in light of (Turing-level) machine impotence in the face of the Entscheidungsproblem.
- January 28 2019: Propositional Calculus I (S Bringsjord)
This class meeting introduces one of the central tenets of LAMA\(^{TM}\): viz., that making immediate and continuous use of AI in the form of provabiity oracles (here, at the level of the propositional calculus) is indispendable for discovering valid proofs that solve problems. Examples using one of HyperSlate\(^{TM}\)’s oracle are given. The upshot is that proof discovery is a joint and indeed collaborative enterprise that unites superior human intelligence with inferior by invaluable machine intelligence.
- January 31 2019: Propositional Calculus II (S Bringsjord)
The simple but cornerstone inference rule of modus ponens (a.ka. /conditional elimination) is introduced, and claimed to be an element of the immaterial universe of of formal logic. This class meeting also introduces the powerful and — at least when it comes to precise, verifiable, valid reasoning — ubiquitous proof technique proof by cases, which in HyperSlate\(^{TM}\) corresponds to disjunction elimination. Tutorials are provided via real-time use of HyperSlate\(^{TM}\) on key exercises.
- February 4 2019: Propositional Calculus III: Reductio ad Absurdum Proofs (S Bringsjord)
A crucial class, in which, harkening back to the astounding Euclid, we look at his still-edifying indirect proof that there must be infinitely many prime numbers, visit Algebra 2 from high school and note that in decent textbooks at this level there is in fact excellent coverage of indirect proof, and then see how reductio ad absurdum is regimented in HyperSlate.
- February 7 2019: Pure General Logic Programming (PGLP), Intro & Overview
Every proof in HyperSlate, from the tiny to the elaborate, can be viewed as a PGLP program, and starting from an explanation of this fact, PGLP was presented.
- February 11 2019: The Pure Predicate Caclulus = \(\mathcal{L}_0\); Toward Quantification (Selmer Bringsjord)
We begin by noting the formal logic provides a way of seeing, contra Darwin (in Descent of Man), that H. sapiens sapiens is qualitatively distinct, intellectually speaking, from nonhuman animals, in light of the former’s ability to reason (1) with abstract relations and functions, (2) with quantifiers, (3) recursively, and (4) over and with infinite structures. The pure predicate calculus = zeroth-order logic is introduced specifically in connection with (1), which, in contrast to the weaker propositional calculus, it regiments and allows.
- February 14 2019: Review and Interactive QAJ Session for Test 1 (Selmer Bringsjord)
Among other things, we covered the problem BiconditionalIntroByChaining, and reviewed proof by cases, indirect proof, and partial solutions/hints were given in HyperSlate\(^{TM}\) to a series of challenges on HyperGrader\(^{TM}\) as an extension of this review.
- February 19–22 2019: Test 1
Test 1 consisted of three human-authored problems and one AI-authored problem (personalized for each student individually). Solution videos for the quartet follow immediately, but note that Selmer is solving his own fourth problem, personalized just for him. One will learn a lot from watching these videos (and stopping and studying them along the way).
- The solution to problem of showing \(\vdash_{L_{pc}} (A \rightarrow B) \rightarrow (B \rightarrow C) \rightarrow (A \rightarrow C)\) is available here.
- Phase 1 of the solution to EmmaHelpedToo, in which a proof-by-cases proof plan is created, is available here. EmmaHelpedToo was first presented in the “motivation” part (Part I) of the class; we have seen in class a valid informal proof that cracks this problem, and that prof is mapped into a formal correlate in HyperSlate\(^{TM}\), and expressed specifically as the proof-by-cases proof plan. Phase 2 of solution, in which it’s shown in a sub-proof how to deduce one side of the needed contradiction for Case 2 in the overarching proof, is given in this video.
- The solution to the Smullyan knight-knave problem (a formalized version of Problem 1.1 in Smullyan’s KK) will be given in a forthcoming video.
- The solution to Selmer’s personalized problem, which as he says is rather “creative” on the part of the AI that produced it, is available here. As shown in the video, surisingly, three different routes are available for derving the GOAL from a subset of the GIVENs.
And now we begin Part III of the course …
- February 25 2019: FOL I (S Bringsjord)
Here begins coverage of $\mathcal{L}_1$! We begin by noting the need for quantification in some very simple arguments, then explicitly introduce the two simplest inference rules/schemata for quantifiers in \(\mathcal{L}_1\). This meeting starts our coverage of the long-inseparable link between formal logic and purported proofs of God’s existence. We start with two such “proofs,” neither of which is intended to be taken seriously, but both of which have pedagogical value. Along the way we note that a serious series of purported proofs of God’s existence have been given by Anselm, Descartes, Leibniz, and — in the 20th century — by the greatest logician so far: G$\"{o}$del. Analysis of G$\"{o}$del’s proof will need to wait for a later date.
- February 28 2019: FOL II (Including
Universal Intro
) (S Bringsjord)After the new inference schema
universal intro
is introduced, we end with some excercises that require putting it into action to reach some theorems (including three regarding the relative smartness of different Scandinavian countries). - Spring Break!
Time to ski or sun …
- March 11 2019: FOL III (with a “countdown” HyperGrader problem, and remarks on games, formal logic, and AI) (S Bringsjord)
The fourth and final new inference schema for FOL,
existential elim
, is covered. Some remarks are made on the nature of grad-based logic-puzzle games; specifically, it’s pointed out that when such games are played without obtaining proofs for the moves made by the player, the efficacy of such games, learning-wise, is questionable. - March 15 2019: Exhortation; Truth Trees; Measuring Human/Machine Intelligence and FOL IV; Astrologic Coming (S Bringsjord)
Truth trees are introduced, their superiority over truth tables is explained, and it’s shown that HyperSlate easily allows for the construction and testing of truth trees — in the ver same environment used for the construction and testing of formal proofs. A challenge to Singularity-affirming thinkers, in the form of a very humble QAJ problem involving numerical quantification. This challenge comes after coverage of the basic machinery of this quantification, directly related to a relevant section in the LAMA-BDLA textbook.
- March 18 2019: The Liar; Russell’s Paradox; Pre-Skolmen Problems (S Bringsjord)
We here introduce our first paradox: The Liar. Then we proceed to Russell’s Paradox, including the barberesque version of it, which is now a Required Problem on HyperGrader\(^{TM}\). Finally, we consider two case problems that pave the way toward Skolem’s Paradox (which we don’t directly engage).
- March 21 2019: Rebuilding the Foundations of Math via ZFC; ZFC to Axiomatized Arithmetic (S Bringsjord)
After presenting and discussing Richard’s Paradox, which joins with Russell’s Theorem in destroying naive set theory (including specifically Frege’s Axiom V), we take a look for the first time at Zermelo-Franenkel set theory (= ZFC), and specifically therein at the Axiom Schema of Separation.
- March 25 2019: Test 2 (first of five problems) on HyperGrader released.
One of the five, to be released on March 28, is a peronalized problem automatically generated, a unique problems for each student. Another one of the five is a problem of a new type: it asks the student to created his/her own problem, and measures the problem based on how difficult it is for the background AI to discover a proof that cracks the problem.
- March 28 2019: Second-Order Logic and the k-order Ladder; Second-Order Axiomatized Arithmetic; G\"{o}del’s God Theorem and Speedup Theorem (S Bringsjord)
This class introduces a fair amount of (important) formal logic unfortunately rarely seen at the introductory level. Not only is second-order logic (SOL = \(\mathscr{L}_2\)) introduced, but the general method for climbing the higher-order-logic ladder is presented.
- April 1 2019: Tying Up Loose Ends in Extensional-Logic Coverage (S Bringsjord)
We tie up a number of loose ends before passing on to modal logic and discussion of “killer robots,” to wit:
- Status of Test 2: Let’s take a look at leaderboards etc.
- Questions about G’s a priori proof of God’s existence?
- New HyperGrader Bonus Problem (DoubleMindedMan1) Involving SOL
- ACA*\(_0\) in Astrologic: What the heck is it? In a word, it’s the theory of arithmetic between PA\(_1\) and PA\(_2\); see slide for technical info.
- What about the $1000 offer (for a set \(\Phi\) of first-order formulae s.t. a scenario renders all these formulae true if and only if the scenario’s domain is finite)?
- April 4 2019: Modal Logic: First Steps (S Bringsjord)
The main thrust of this class meeting is to introduce the (propositional) modal logics K, T = M, D, S4, and S5. Specifically:
- We revist the “The Universe of Logic” diagram, and before moving to modal logic, introduce the infinitary first-order logic \(\mathscr{L}_{\omega_1 \omega}\), which is shown in the “Infinitary” category of logics in the diagram.
- We next explain the fundamental divide between extensional versus intensional logics, which is also shown in the diagram.
- With this divide in hand, we proceed to quickly introduce the five modal logics ranging from K to S5.
- April 8 2019: Standard Deontic Logic (SDL = D) Isn’t Going to Cut It! (Chisholm’s Paradox; The Free Choice Permission Paradox) (S Bringsjord)
In order to create a context for why we would want to consider a computational deontic logic in the first place, we quickly look at the threat posed by AIs that are at once *p*owerful, *a*utonomous, and *i*ntelligent, and conclude that these machines are *d*angerous. We also quickly introduce that RAIR Lab’s proposed solution, in the form of The Four Steps. But The Four Steps requires for its basis an adequate compuational logic that captures ethical theories and ethical codes. We introduce and discuss as a candidate logic so-called Standard Deductive Logic (SDL) = D, which is now available in HyperSlate\(^{TM}\). Unfortunately, two paradoxes (from among many) lead us to reject D.
- April 11 2019: Logikk Kan Redde Oss Fra Onde Roboter (Atriya Sen; with Selmer Bringsjord & Naveen Sundar G)
Here Dr Atriya Sen provides the RAIR Lab’s solution to the PAID Problem, one that makes use not of a deficient deontic logic like D, but rather \(\mathcal{DCEC}^\ast\). Demos are shown. The presentation concludes with the robot version of the “Jungle Jim” moral dilemma.
- April 15 2019 Brief Remarks on Heterogeneous Logic (S Bringsjord)
Information often comes in visual, as opposed to linguistic/symbolic, form. The logics we have studied so far have been based, exclusively, on symbolic formulae. In this class we changes things up, rather dramatically: we consider heterogenous logics: logics that have traditional formulae, plus diagrams.
- April 18 2019: The Lottery Paradox and Introduction to /In/ductive Logic (S Bringsjord)
We provide a solution to the Lottery Paradox by introducing a multi-valued inductive logic that does the trick, lickety split.
#brought to life chiefly by Naveen Sundar G; see.
- April 22 2019: G\"{o}del’s Completeness Theorem (S Bringsjord)
After setting some context with a brief overview of G\"{o}del’s life, and the peerless collection of his greatest theorems (each of which is covered in the forthcoming G\"{o}del’s Great Theorems (by S Bringsjord; Oxford University Press), we cover the first of these theorems, which was achieved in G\"{o}del’s dissertation. This is G\"{o}del’s Completeness Theorem, and as part of it, K\"{o}nig’s Lemma (which G\"{o}del proved from scratch even though it has previously been proved); the theorem: Either (formula) \(\phi\) is satisfiable, or it’s refutable (here the formula is in FOL = \(\mathscr{L}_1\)). It will be necessary to make use of the doc can to allow some examples to be worked out; thesee examples involve a tree-based approach to establish satisfiability if doing so is possible; and reference to a deductive refutation of \(\phi\) if doing so is impossible.
Homeworks
Homework consists of solving all required problems listed on HyperGrader\(^{TM}\)’s RPI web page. (Non-required problems are clearly marked as such, e.g. as Bonus Problems.) All solutions are created in their final form in HyperSlatee\(^{TM}\). HyperGrader\(^{TM}\) for interactive use via its underlying AI technology opens for its Spring 2019 stint on or about Jan 28 2019, and an orientation/introduction to the system is given in class that day. Note that homeworks cannot be done without access to, and sustained and continuous use of, HyperSlatee\(^{TM}\) and HyperGradere\(^{TM}\).
Footnotes:
Warning: Increasingly, the term ‘reasoning’ is used by some who don’t really do anything related to reasoning, as traditionally understood, to nonetheless label what they do. Fortunately, it’s easy to verify that some reasoning is that which is covered by formal logic: If the reasoning is explicit; links declarative statements or formulae together via explicit, abstract reasoning schemata or rules of inference (giving rise to at least explicit arguments, and often proofs); is surveyable and inspectable, and ultimately machine-checkable; then the reasoning in question is what formal logic is the science and engineering of. (An immediate consequence of the characteristics just listed is that AIs based on artificial neural networks don’t reason, ever.) In order to characterize /in/formal logic, one can remove from the previous sentence the requirements that the links must conform to explicit reasoning schemas or rules of inference, and machine-checkability. It follows that so-called informal logic would revolve around arguments, but not proofs. An excellent overview of informal logic, which will be completely ignored in this class, is provided in “Informal Logic” in the Stanford Encyclopedia of Philosophy. In this article, it’s made clear that, yes, informal logic concentrates on the nature and uses of argument.