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

General Orientation

• What is Formal 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.)

• 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^®,’ 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 course in formal 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 inlude 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-BDLAHSHG Textbook

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

• August 31 2020: 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.

• September 3 2020: Tutorial, Mechanics; Historical and Scientific Context re. Formal Logic, AI, and Logic Machines (S Bringsjord)
  

  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. (A problem for each logic has been posted on HyperGrader^®; at this point, only switching_conjuncts_fine and these three problems are the pre-engineered problems posted on HG^®.) 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 ephasis 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.

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

• September 8 2020: 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, and then proceed to use 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: “Intensional Logic” in SEP
  • The Corresponding Video Lecture by S Bringsjord is under construction.

• September 10 2020: Review of Intensional/Modal Logics (S Bringsjord)
  

  We first briefly return to the case of Blinky (Lost in Space) 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, with this coverage including even the infinitary FBT. Handling these taks requires, certainly, intensional/modal logics. Finally, we encapsulate the modal logics K, T, D, 4, and 5, and focus on D, an early deontic logic, in connection with Chisholm’s Paradox.

  • Recommended Reading: “Intensional Logic” in SEP
  • The Corresponding Video Lecture by S Bringsjord is under construction.

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

  We here 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.

  • Recommended Background Reading: “Turing Machines” in SEP
  • The Corresponding Video Lecture by S Bringsjord is here.

• September 17 2020: Completeness Theorems (S Bringsjord)
  

  We begin with an overview of 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. Our coverage here includes a characterization of completeness in general, and then in specific terms for \(\mathscr{L}_1\). We end with some remarks about Leon Henkin, well known for devising a simpler, smoother proof of the completeness theorem.

  • The Corresponding Video Lecture by S Bringsjord is available here.

• September 21 2020: Gödel’s First Incompleteness Theorem (S Bringsjord)
  

  We here cover the first 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 24 2020: Gödel’s Second Incompleteness Theorem (S Bringsjord & Mike Giancola)
  

  We here cover Gödel’s second incompleteness theorem (G2), which is a corollary of G1. Bringsjord first sets the stage, and then Giancola present a tragic case study in which inconsistency brings a jet crashing to the ground, killing both pilot and co-pilot (his slide deck is available here). Then Bringsjord returns, and G2 is proved.

• September 28 2020: Real Learning (S Bringsjord)
  

  We here switched things up schedule-wise relative to our syllabus, for instead of continuing with our Gödelian sequence by covering the syllabus-scheduled Gödel’s Speedup Theorem, our topic is what S Bringsjord et al. calls Real Learning, or just \(\mathcal{RL}\), which is introduced in this paper, required reading for today’s class. The topic of Real Learning was slated for Oct 8 in our syllbaus.

  • The Corresponding Video Lecture by S Bringsjord, ``On International Paternalistic Taxation to Address The Mess That `Machine Learning’ is Making,” is available here. And the underlying slide deck is available in pdf format here.
  • Recommended Further Reading: Bringsjord et al. have introduced a form of learning that goes hand in hand with real learning: learning ex nihilo; the paper in question is available here.

• October 1 2020: Gödel’s Speedup Theorem (S Bringsjord)
  

  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!

• October 12 2020 No class: Columbus Day. (Why do we not celebrate Leiv Eiriksson Day?!)
  

• October 15 2020: No class (No power!)
  

• October 15 2020: Formal Inductive Logic (S Bringsjord)
  

  We begin our coverage of formal inductive logic by entering this branch of logic through the portal that is The Paradox of Grue, first presented by Neslon Goodman. The slide deck “Portal to Inductive Logic: The Paradox of Grue” is available here. Next, we solve The Lottery Paradox by bringing to bear an innovative inductive logic, one based upon relative strength factors, or likelihood measures. The slide deck “The Lottery Paradox can be obtained here. Next, we solve another paradox: The St Petersburg Paradox; the solution is given in this slide deck.

  • The Corresponding Video Lecture on The Paradox of Grue by S Bringsjord is available for watching here.

• ????
  

• October 26 2020: The Argument for God’s Existence from AI (S Bringsjord)
  

  A novel argument for God’s existence is given. This argument makes use of the concepts of the cognitive power (fleshed out in terms of formal logic) sufficient for hunting and gathering etc. in our forebears, at the level of AI as currently logico-mathematically defined in the the field itself (witness e.g. its textbooks), and needed for creating and using the branch of mathematics known as analysis.

  • The Corresponding Video Lecture in which the argument in question is given can be watched here.

• October 29 2020: What are We, Rigorously Speaking? (S Bringsjord)
  

  What are we? What are our brains? (The idea here, in keeping with the nature of both formal logic and AI, is that such questions are to be answered in formal, computational terms.) Prof Richard Granger eloquently and rigorously defends an answer to these questions that is directly at odds with the answer to them given by S Bringsjord. This class immediately grounds this clash by reference to opposing papers in Theoretical Computer Science, one by Bringsjord, and one by Granger.

  • The Corresponding Video Lecture in which the argument in question is given can be watched here.

• November 2 2020: Logic, AI, and Tax Technology (S Bringsjord)
  

  Selmer claims that a series of problems in the intersection of logic, AI, and taxation compose a set that is AI-complete. The discussion is anchored to a simple scenario, S, in which three agents must in some fashion have their incomes taxed in order to defend against a malicious invader.

  • The Corresponding Video Lecture is available for your viewing (pleasure?) here.

• November 5 2020: Pure General Logic Programming (PGLP) (S Bringsjord)
  

  The new logic-programming paradigm, Pure General Logic Programming (PGLP), invented by Selmer under support from ANR, AFOSR, and ONR, is here introduced and explained. PGLP subsumes Prolog and all its low-expressivity cousins, and renders program verification essentially effortless because (i) programs are specifications, and (ii) the verification of what is returned after execution consists simply in the checking of the proof of what is returned.

  • The Corresponding Video Lecture is here.

• November 9 2020: Killer Robots, D, Beyond to DCEC* in HyperSlate (S Bringsjord)
  

  We note The PAID Problem, in a nutshell that powerful, autonomous, intelligent machines are extremely dangerous, and might well eventually destroy us, unless The Four Steps are followed. We specifically note that the formal computational logic to be used in The Four Steps can’t be the deficient logic D or any of its cousins — but the /Deontic Cognitive Event Calculus/* (/DCEC/*) is instead the thing to use.

  • The Corresponding Video Lecture is here.

• November 12 2020: On Quantificational Modal Logic (S5-centric) (S Bringsjord)
  

  We begin by recalling why we need intensional logic in the first place, with some help from “Blinky,” of Lost in Space Fame. Then we zero in on propositional S5, take note of its elegance and economy (in light of e.g. the reduction principles it caps off). Finally, we consider a first version of quantificational S5, and end with a look at the notorious Barcan Formula, which it so happens is welcomed by S Bringsjord in his modal argument for *P=NP$, available here.

  • The Corresponding Video Lecture is in production.

• November 16 2020: DDE (Doctrine of Double Effect) => DDE* (with self-sacrifice) => DTripleE (S Bringsjord)
  

  To start, we review the Doctrine of Double Effect (DDE), used by Naveen Sundar Govindarajulu (NSG) and S Bringsjord to ensure that AIs (in relevant contexts) do the ethically correct thing, as shown in this IJCAI paper. It’s then explained that NSG discovered that DDE doesn’t work when the agent intending to save the day intends to do so via self-sacrifice; the new version of DDE, set out and explained in this paper, is then presented. Finally, the listener is invited to read about this Doctrine of Triple Effect in this paper, so that future discussion and debate will be possible.

  • The Corresponding Video Lecture is in production.

• November 19 2020: Introducing HyperLog (v .5) (S Bringsjord)
  

  After informing the audience that there are in fact some proposals for computing over the reals, with associated hierarchies, the new programming language HyperLog is introduced. This introduction includes, first, a sweeping overview of the history of formal logic and varous programming languages and their roots, and then passes to the mechanics of getting started in HyperLog, by defining Clojure functions, making inferences that compute relative to those defined functions, and employing a new oracle that can at once reason at the level of first-order logic and compute Clojure-defined functions.

  • The Corresponding Video Lecture is in production.

• November 23 2020: Gödel’s Silver Blaze Theorem, Part I: ZFC and Mathematics (S Bringsjord)
  

  In order to understand Gödel’s Greatest Theorem, which — for reasons to be explained — we shall regard to be “The Silver Blaze Theorem,” we need to have a firm understanding of axiomatic set theory, in the form, specifically, of ZFC. This session provides this understanding, and ends with a pointer to Cantor’s proof that the power-set operation, applied to the natural numbers, yields an even-larger set. This proof is also key to understanding The Silver Blaze Theorem.

  • The Corresponding Video Lecture is in production.

• November 26 2020*: Thanksgiving!
  

• November 30 2020: Gödel’s Silver Blaze Theorem, Part II: Further Context and Proof Sketch (S Bringsjord)
  

  In Part II of our coverage of Gödel’s Greatest Theorem, we begin in earnest by watching two videos of proofs by truth-trees in HyperSlate^®, in order to establish non-entailment. Next, without making any use of transfinite numbers, we set out and reflect upon both the Continuum Hypothesis (CH) and the Generalized Continuum Hypothesis (GCH). We then analyze the reasoning of Sherlock Holmes in the The Adventure of Silver Blaze, which is fundamentally a proof of non-entailment in its own right (and shows Scotland Yard, once again, to be, well, not exactly a place of ingenious detection). Finally, we pass to presentation and explanation of a proof-sketch of Gödel’s stunning result.

  • The Corresponding Video Lecture is in production.

• December 3 2020: Gödel’s Time Travel Theorem (S Bringsjord)
  

  We here look at the context, paradoxes related to and arising from, and diagrammatic justification for: Gödel’s birthday present to Einstein: a proof that backwards time travel in (Einstein’s) General Theory of Relativity is possible.

  • The slide deck provided as a movie, so that all diagrammatic/heterogeneous proofs can be viewed and experienced in the form devised by S Bringsjord is available here.
  • The Corresponding Video Lecture is in production.

• December 7 2020: Could a Finite Machine Every Match Gödel? Part I (S Bringsjord)
  

  We make first a few brief remarks regarding the “God Theorem” of Gödel, which end with a pointer to a better route to formalize the concept of a positive property than that taken by Gödel himself (and better as well, Selmer claims, than some others who have come after). We then answer the driving question by turning to games and game-playing, and end with an overview of the game Gödel played, which is Turing-undecidable.

  • The Corresponding Video Lecture is in production.

• December 10 2020: Could a Finite Machine Every Match Gödel? Part II (S Bringsjord)
  

  The 2020 edition of our course ends with consideration of Gödel’s “Either Or” claim, presented in 1951. The claims amounts to pointing out that either there’s a Diophantine Problem we (= the human mind) can’t possibly ever solve, or we are infinitely more powerful that any finite computing machine. At the very end of our session, Bringsjord takes stock of the four arguments for his No! to the question (contra William Rapaport), and issues a “scorecard” on Gödel’s own work w.r.t. to the fundamental question at hand.

  • The Corresponding Video Lecture is in production.

Tutorials

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

  This short, simple 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 \(\phi \wedge \psi\) you can deduce in HS^® that \(\psi \wedge \phi\).

• Special Llamas Disjunction (GUI pointers & use of FOL AI/oracle) (Sep 9 2020)
  

Informal Metalogical Homeworks