Intermediate Formal Logic and AI (= IFLAI2)
Fall 2023 edition of IFLAI2
Selmer Bringsjord

General Orientation

• What is Formal Computational Logic?
  

  In general, formal logic is the science and engineering of reasoning,¹ 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.) As to computational formal logic, well, for now let’s just say that computation itself can be taken to consist of reasoning in a logic — a fact that we shall be exploring.

• 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 intermediate 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^®,’ or simply by the abbreviation ‘LAMA^®,’ 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^® paradigm.

  As to what these thinkers hold in connection with LAMA^®, that is an open question. You are free to inquire!

• Prerequisites
  

  Students must have had a previous, rigorous, comprehensive first course in formal logic, preferably including computational logic. It is highly beneficial that the student have had in this prior course, or from some other source, modal logic. Realistically, some students will have only studied mathematical logic or standard extensional logics in their prior coursework. There is nothing to be done about this save to include early on some coverage of modal logic via independent work by the student in HyperSlate^® on some modal-logic problems.

Texts/Readings

Syllabus

HyperSlate^®

HyperGrader^®

LAMA-BDLHGHSA Textbook

Class-Day Topic and Content (includes associated slide decks, video lectures, and — sometimes — tutorials, etc.)

• August 28 2023: General Orientation to the LAMA^® 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 LAMA^® should take “straight” Intermediate Logic from another instructor, since probably the “Stanford paradigm” is in use then, and in that case the course will not be based upon or cover AI and AI-based topics, and will not be based on Motalen’s technology.

• August 31 2023: Tutorial, Mechanics; Historical and Scientific Context re. Formal Logic, AI, and Logic Machines (S Bringsjord)
  

  We begin by considering, armed with formal logic, the question “What is school for?,” taken up (9/1/22) in a symposium hosted by the New York Times. Then, after a brief review of some course mechanics, we remind students that prowess in cracking problems in \(\mathscr{L}_{PC}\), \(\mathscr{L}_1\), and \(\mathscr{L}_2\) is assumed, and may need to be refreshed. (Review Problems for these logics will, starting today, be published with deadlines on the HyperGrader^®; platfor, due either on Sept 7 or Sept 11.)

  We then take a time-traveling tour of computational formal logic and AI, going from Euclid, three centuries BC, to — possibly? — The Singularity in our future, and put some emphasis on the Entscheidungsproblem. The final phase of this session has a focus on form of AI and computer programming based on formal logic: viz. “The Terrific Triad” of circa 1965, resurrected, refined, and reenergized.

  • A (past) Corresponding Video Lecture by S Bringsjord, “The Terrific Triad,” is available here.

• September 5 2023: Review of Extensional Logics (contrasted with intensional logics) (S Bringsjord)
  

  We use the case of Blinky (Lost in Space) to explain the core difference between extensional versus intensional logics. (Later in the class we shall employ the infinitary version of the False Belief Task to further display what’s unreachable for extensional logics, and why.) We end by returning to the extensional trio of \(\mathscr{L}_{PC}\), \(\mathscr{L}_1\), and \(\mathscr{L}_2\). In the second of these extensional logics, and using our AI oracles in HG^®, we first explore an example from 1957 by Layman Allen, who dreamed of formal logic capturing the U.S. tax code, and then explore SpecialLlamasDisjunction, introduced in our previous meeting. We end with coverage of \(\mathscr{L}_2\), second-order logic, and the so-called \(k\)-order ladder.

  • Recommended Reading (for contrast, and to set up for our next class): “Intensional Logic” in SEP

• September 7 2023: Review of/Entry to Intensional/Modal Logics (S Bringsjord)
  

  We first take a look at some personalized AI-generated problems in our respective HyperGrader^® accounts, and move from there into a full GUI tutorial. Then we briefly inquire as to whether there are any questions about the \(k\)-order logic ladder, and then return to the case of Blinky (of Lost in Space fame) to begin to probe relevant s-expressions in modal logic in HS^®. Next, we look at the most demanding versions of the False Belief Task that anyone in AI and/or computational CogSci has attempted; this coverage includes even the infinitary FBT. Handling these taks requires, certainly, intensional/modal logics. Finally, we encapsulate the modal logics K, T, D, 4, and 5, focus a bit on D, an early deontic logic, in connection with Chisholm’s Paradox, but end up targeting 5 = S5 in this class. After reading the relevant portion of the textbook, the following are recommended for exceptionally sedulous students (focus on proof theory/inference):

  • Recommended Reading #1: “Intensional Logic” in SEP
  • Recommended Reading #2: “Modal Logic” in SEP
  • Recommended Reading #1: “Deontic Logic” in SEP

• September 11 2023: Church’s Theorem (S Bringsjord, w Naveen Sundar G on Turing machines)
  

  We first explore some advanced topics (e.g. automated planning) in HyperGrader^® and HyperSlate^®. We then present and prove Church’s Theorem, which says that the Entscheidungsproblem is unsolvable by Turing-level machines; i.e. that theoremhood in \(\mathscr{L}_1\) = FOL is Turing-unsolvable. We make use of the Halting Problem to obtain CT (and look at the kernel of reasoning in a HyperSlate^® workspace.

  • Recommended Background Reading: “Turing Machines” in SEP

• September 14 2023: Completeness Theorems (S Bringsjord)
  

  A video of this entire lecture, replete with use of HyperSlate to show how in it one can prove the completeness of the propositional calculus, and — following Gödel’s dissertation — of first-order logic, is provided via the link given here. As to our sequence, we begin with an overview of S Bringsjord’s forthcoming Gödel’s Great Theorems, and then pass directly to coverage the first of these theorems: the completeness theorem for \(\mathscr{L}_1\), which was the heart of Gödel’s dissertation. It turns out that because of the power of HyperSlate we can instantly convey the proof-kernel of completeness for both the propositional calculus and FOL, in line with what Gödel did. Our coverage here includes a characterization of completeness in general, and then in specific terms for \(\mathscr{L}_1\). We include some remarks about Leon Henkin, well known for devising a simpler, smoother proof of the completeness theorem.

• September 18 2023: Gödel’s First Incompleteness Theorem (S Bringsjord)
  

  We here cover the second of Gödel’s great theorems, the one that has been most discussed and revered among those he obtained: viz., his first incompleteness theorem (G1), taking at its core Peano Arithmetic (PA). After first making sure that we have a handle on PA via exploration of it in HyperSlate^®, we visit a Bringsjordian proof-oriented version of the Liar Paradox, then get clear on Gödel Numbering by simply taking note of how standard dictionaries work, and then we prove the theorem. We end by considering “astrologic” in connection with Goodstein’s Theorem, which is an example the kind of mysterious arithmetic sentences that Gödel showed in G1 must exist.

• September 21 2023: Gödel’s Second Incompleteness Theorem (S Bringsjord)
  

  We here prove Gödel’s second incompleteness theorem (G2), which is a corollary of G1 (Gödel didn’t bother to prove it directly in his proof of G1).

• September 25 2023: Gödel’s Speedup Theorem (James Oswald)
  

  We introduce different levels of acceleration, from fast cars (such as electric ones from Tesla and Lucid) to the space shuttle to light-gas guns from NASA to the Ackermann Function to the beyond-recursive speedup of Rado’s \(\Sigma\) (= “Busy Beaver”) function. Then we explain and prove that moving from one logic to a more expressive one can secure speedup that, like \(\Sigma\), gives non-recursive acceleration! This is Gödel’s Speedup Theorem, the engineering consequences of which (inquisitive and wise) modern minds are still sorting out.

Tutorials

• Getting off the Ground into HyperGrader^® and HyperSlate^® (Aug 2020)
  

  This short, simple “blast-from-the-past” tutorial explains how to register if you purchased a code from a collegiate bookstore, and then includes solving a very simple proof challenge (show that if you’re given a conjunction you can deduce in HS^® that \(\psi \wedge \phi\)).

Informal Exercises and Metalogical Homeworks