Introduction to (Formal) Logic (and AI)
Spring 2022 edition of IFLAI1
Selmer Bringsjord

Terminology & General Orientation

• Terminology
  

  Note that sometimes ‘symbolic’ is used in place of ‘formal.’ This is bad practice, since formal logic includes 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. The class also serves as a stepping stone to further study of AI, of formal/theoretical computer science, and of logic programming.

• 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, the vast majority of classical mathematics can be deductively derived from a small set of formulae (including, e.g., ZFC set theory, which you’ll be hearing more about, and exploring) expressed in the particular formal logics known as ‘first-order logic’ (FOL = \(\mathscr{L}_1\)) and ‘second-order logic’ (= SOL = \(\mathscr{L}_2\)); you’ll also be hearing more about both of these logics as well. In addition, 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 to use computational formal logic for AI, 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. This thus applies specifically to TAs Dhruva and Harshaa. As to what these other thinkers hold in connection with LAMA^®, that is an open question. You are free to inquire!

• Graduate Teaching Assistants; Further Help
  

  The TAs for this Sp 2022 edition of the course are Dhruva Hiremagalur Naraya (dhruva.hnarayan@gmail.com) and Harshaa Narayan (harshahnarayan@gmail.com). Please note again the subsection 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 the courses 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 from scratch in this class, it helps to have at least some command of it from high school, since our pace will be a rapid one. A much more robust treatment of prerequisites and a suitable background for this course is provided in the syllabus.

Texts/Readings

Syllabus

HyperSlate^®

HyperGrader^®

LAMA-BDLAHS Textbook

Lectures

• January 10 2022: 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 for learning under a different paradigm than that of LAMA^® should take Intro to Logic in a Fall semester, since the “Stanford paradigm” is in use then.

• January 13 2022: The Immaterial Paradise; 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 and human cognition is included.

  Students for whom all 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. $∀ Φ, φ, ψ: \mbox{if} Φ \vdash φ ∧ ¬ φ, \mbox{then} Φ \vdash ψ$], which is needed at a key juncture in this lecture.

  • Video of the entire lecture, curated and refined, is available here.

• January 17 2022: MLK Day!
  

  No class.

• January 20 2022: The Balderdash That is GPT-3 AI; Motivating Paradoxes, and Puzzles, Part II (S Bringsjord)
  

  We explore whether or not the AI GPT-3, appearing in an interview (watchable here) through its humanoid avatar, is as logical as it claims to be. (Result: GPT-3 has a decidedly inflated view of its logical powers.) Next, after review of a puzzler involving boolean operators and the inference schema explosion, we then move to Moriarty’s fiendish ticking-bomb challenge! Can you solve it in time to save the world?

  • Video of the entire lecture, curated and refined, is available here.
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Mtg Info for:  "The Balderdash that if GPT-3 AI; Motivating Paradoxes & Puzzles, Part II"
  Time: Jan 20, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• January 24 2022: 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.

  • Video of the entire lecture, curated and refined, is available here.
  • Video of the automation of a (now!) simple theorem (shown during the synchronous lecture) obtained by Logic Theorist at the 1956 dawn of AI after 10 seconds of work automatically proved instantly by HyperSlate^® here.
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info for Jan 24 2022 IFLAI1 Class Mtg:  "Whirlwind History & Overview of Formal Logic"
  Time: Jan 24, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• January 27 2022: Propositional Calculus I, Emphasis on Our First Oracle (S Bringsjord)
  

  This class meeting introduces one of the central tenets of LAMA^®: 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^®’s oracles are given. The immediate upshot to note is that proof discovery is a joint and indeed collaborative enterprise that unites superior human intelligence with inferior but nonetheless invaluable machine intelligence in the form of automated reasoning.

  • Video of this crucial lecture, curated and refined, is available here.
  • A video showing the use of the PC provability oracle in HyperSlate^® solving the “NYS 3” logic problem is available here.
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info for IFLAI1 Class Mtg:  "Propositional Calculus I:  Our First Oracle"
  Time: Jan 27, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• January 31 2022: Propositional Calculus II (S Bringsjord)
  

  The simple but cornerstone inference rule of modus ponens (a.k.a. /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^® corresponds to disjunction elimination. Tutorials are provided via real-time use of HyperSlate^® on key exercises.

  • A curated video lecture, replete with plenty of HyperSlate^® use, can be found here.
  • Zoom-mtg Info here:

  Topic: IFLAI1 Zoom Mtg:  "Propositional Calculus II:  Two More Rules of Inference; Applying Them"
  Time: Jan 31, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• February 3 2022: 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 (and also Geometry) 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 formalized in HyperSlate^®.

  • A curated video lecture, replete with plenty of HyperSlate^® use, can be found here.
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info IFLAI1 Class Mtg:  "Propositional Calculus III: Reductio ad Absurdum Proofs"
  Time: Feb 3, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• February 7 2022: Pure General Logic Programming (PGLP), and Hyperlog, Part 1
  

  Every proof in HyperSlate, from the tiny to the elaborate, can be viewed as a Pure General Logic Programming (PGLP) program, and starting from an explanation of this fact (with some look-ahead- discussion of the Turing-completeness of the first three elementary deductive logics covered in this class), PGLP, invented by S Bringsjord under support from both AFOSR and France’s ANR, is presented, in its historical context. This lecture also serves as a first introduction to the novel programming language and environment Hyperlog^TM; this new language is an instance of PGLP available in HyperSlate^®, and is integrated with Clojure.

  • A curated video lecture corresponding to this class meeting and the slide deck used is available here. (Note this is a 2021 lecture, but try as S Bringsjord might, he could not improve upon it for the 2022 edition of the class.)
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Info for IFLAI1 Class Mtg:  "General Logic Programming (PGLP), and Hyperlog, Part I"
  Time: Feb 7, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• February 10 2022: Darwin’s Mistake+; The Pure Predicate Calculus = \(\mathscr{L}_0\); Toward Quantification (Selmer Bringsjord)
  

  We begin by noting that 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 = \(\mathscr{L}_0\) is introduced specifically in connection with (1), which, in contrast to the weaker propositional calculus = \(\mathscr{L}_{pc}\), it regiments and allows. Presentation and discussion is rendered concrete by use of HyperSlate^®.

  • A full video lecture, replete with explanation of the two new inference rules that distinguish zero-order logic from the mere propositional calculus, is available here.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info for IFLAI1 Class Mtg:  "Darwin's Mistake+; The Pure Predicate Caclulus; Toward Quantification"
  Time: Feb 10, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• February 14–18 2022: Test 1
  

  Test 1 consists of six problems, four “core” problems, and two Bonus problems. The Bonus problems are human-authored, entirely optional, have absolutely no negative effect on your grade if not attempted (let alone solved); they do result in extra credit in the form of points on the master leaderboard (and are of course good for learning!). Of the four core problems, one is human-authored, and three are AI-authored (personalized for each student individually).

  For some help, some solution videos for some earlier-year problems (in earlier, less-powerful versions of HyperSlate^®) are given immediately below, but note that Selmer is here 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 the 2019 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^®$, and expressed specifically as the proof-by-cases proof plan.

  • The solution to one of Selmer’s personalized problems (from a few years back), which 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.
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Z Mtg on Test 1 for IFLAI1
  Time: Feb 14, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

  And now, we begin Part III of the course …

• February 17 2022: Quantification; FOL I; “Proving” God’s Existence (S Bringsjord)
  

  Here begins coverage of \(\mathscr{L}_1\). We start by noting the need for quantification in some very simple arguments, then explicitly introduce the two simplest inference rules/schemata for quantifiers in \(\mathscr{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ödel. Analysis of Gödel’s proof will need to wait for a later date; it’s by the way analyzed in a chapter in Bringsjord’s forthcoming Gödel’s Great Theorems, from Oxford University Press.

  • The full video lecture, replete with explanation of the first two new inference rules/schemata for first-order logic, is available here.
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Z Mtg on Test 1 for IFLAI1
  Time: Feb 14, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• Feb 22 2022: FOL II (including universal intro) (S Bringsjord)
  

  After the new inference rule/schema universal intro is introduced, we move to HyperSlate^® in order to bring to life a simple but esemplastic example. We end by looking at some excercises that require putting it into action to reach some theorems (including three regarding the relative smartness of different Scandinavian countries).

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-mtg Info for IFLAI1:  "Test-1 Strategy Session; FOL II (universal intro)"
  Time: Feb 22, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• February 24 2022: FOL III (existential elim); Logic, AI, Games, and the (Powerful!) Human Mind (S Bringsjord)
  

  We first visit a ranking of the “hardness” of problems for humans and AIs based on formal logic. Next, the fourth and final new inference schema for FOL, existential elim, is covered. In addition, after setting context by reviewing AI’s unimpressive victories in checkers, chess, Jeopardy!, and Go, some remarks are made on the nature of grid-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. We also discuss Motalen’s latest game: LogiNim.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-mtg Info IFLAI1 Class:  "Remarks re Logic & Games; Existential Introduction"
  Time: Feb 24, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• February 28 2022: Exhortation; Truth Trees; Measuring Human/Machine Intelligence; and FOL IV (S Bringsjord)
  

  Truth trees are introduced, their superiority over truth tables is explained, and it’s shown that HyperSlate^® easily allows for the construction, testing, and certification of truth trees — in the very same environment used for the construction and testing of formal hypergraphical proofs. A challenge to Singularity-affirming thinkers, in the form of a very humble set of problems involving numerical quantification, is issued. This challenge comes after a high-altitude view of the basic machinery of this quantification, directly related to a relevant section in the LAMA-BDLA textbook. We end by looking at an artificial multi-agent, embodied in RAIR-Lab robots, solving a challenge that involves robust quantification. This challenge is planned to be one the new RAIR-Lab robot PERI.2 will be able to eventually handle!

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info for IFLAI1 Class:  "Truth Trees In HyperSlate® and ..."
  Time: Feb 28, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom now meeting expired.
  

• March 3 2022: The Liar; Russell’s Paradox; (Toward, only) Thoraf’s Paradox (S Bringsjord)
  

  We introduce our first paradox, perhaps the primogenitor of all paradoxes: The Liar Paradox, or just simply: The Liar. Next, we proceed to Russell’s Paradox, including the Norwegian barberesque version of it, which will soon be a Required Problem on HyperGrader^®. In fact, we mention two forthcoming problems in HyperSlate^®, ChimericalBarber, and the problem that asks you to create the proof that Russell mailed Frege, and left a large part of the latter’s work in shambles as a result (RusselsLetter2Frege). Finally, we consider two problems that pave the way toward (Thoraf) Skolem’s Paradox (which we don’t directly engage).

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info for IFLAI1 Class Mtg:  "The Great Paradoxes and ..."
  Time: Mar 3, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting has expired.
  

• Spring Break!
  

• March 14 2022 Test 2, Introduced and Explained (of course via HyperGrader^®)
  

  One of the Test-2 problems is a creativity challenge: The student creates his/her own problem, and HyperGrader^®’s AI measures the problem based on how difficult it is for this AI to discover a proof that cracks the problem.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Test 2 Introduction/Presentation/Orientation, for IFLAI1 Spring 22
  Time: Mar 14, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• March 17 2022: Climbing the k-Order Ladder (S Bringsjord)
  
  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: IFLAI1S22 Mtg for Mar 17:  "Climbing the k-Order Ladder (& possible discussion of Test 2)"
  Time: Mar 17, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom Meeting now expired.
  https://us02web.zoom.us/j/86243484960?pwd=N29EYWxwSTJzZGRRRDEwT2ZjdXlMZz09
  

• March 21 2022: Rebuilding the Foundations of Math via ZFC; Baby Arithmetic (BA) and Peano Arithmetic (PA) (S Bringsjord)
  

  After a quick review of the damage done by Russell’s Paradox, we present and discuss the fascinating and fiendishly clever Richard’s Paradox, which joins with Russell’s Theorem in destroying naïve set theory (including specifically Frege’s Axiom V). Then we take a look for the first time at Zermelo-Franenkel set theory (= ZFC), which saves the day when substituted for Frege’s axiomatization, and we specifically take a look at the Axiom Schema of Separation (SEP) in ZFC, and then look at SEP in HyperSlate^®. We end by taking a look at the first part of classical mathematics that can now be confidently built out from the foundation of ZFC: elementary arithmetic, expressed in formal logic. Here we look at Baby Arithmetic (BA) and Peano Arithmetic (PA), and in the case of the former explore a new excercise in HyperGrader^®.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: IFLAI1S22 Mtg:  "Rebuilding the Foundations of Math via ZFC; Baby Arithmetic (BA) and Peano Arithmetic (PA)"
  Time: Mar 21, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• March 24 2022 On to Intensional Logics
  

  This is a general introduction, using the robot Blinky and a shell game, along with the False Belief task at level 5 and beyond, to the crucial difference between extensional logics versus intensional logics. The logics \(\mathscr{L}_{pc}\), \(\mathscr{L}_0\), \(\mathscr{L}_1\), \(\mathscr{L}_2\), \(\mathscr{L}_3\) are all extensional. Now we move to the intensional category, which includes modal logics. Six modal logics are introduced, rapidly for now: K, T = M, D, S4, S5, and \(\mathcal{DCEC}\). A first proof in K of its characteristic axiom is constructed in HyperSlate^®.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: IFLAI1 Class Mtg:  "On to Intensional Logics"
  Time: Mar 24, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• March 28 2021: Against Killer Robots, Standard Deontic Logic (SDL = D) Isn’t Going to Cut It! (Chisholm’s Paradox; The Free Choice Permission Paradox; Ross’s Paradox) (S Bringsjord)
  

  In this lecture, to first show 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 powerful, autonomous, and intelligent, and conclude that these machines are dangerous. This is what I have dubbed “The PAID Problem.” We also quickly introduce the RAIR Lab’s proposed solution, in the form of The Four Steps. But The Four Steps solution requires for its basis a computational logic that can capture ethical theories and codes, as well as legal theories and codes. We introduce and discuss as a candidate logic for this, so-called Standard Deontic Logic (SDL) = D = M, which is available in HyperSlate^®. Unfortunately, three paradoxes (from among many) lead us to reject D, and return to the drawing board, PAID still a looming threat.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Info for IFLAI1:  "Against Killer Robots, Standard Deontic Logic (SDL = D) Isn't Going to Cut It! (Chisholm's Paradox; The Free Choice Permission Paradox)"
  Time: Mar 28, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• March 31 2022: Logic Can Save Us (Selmer Bringsjord & Naveen Sundar G)
  

  Replete with robot demos, in this lecture Selmer Bringsjord provides the RAIR Lab’s solution to the PAID Problem (and along the way briefly discusses another existential threat, that of pandemics), one that makes use not of the deficient deontic logic like D, but rather \(\mathcal{DCEC}^\ast\). Demos are shown. The presentation concludes with the robot version of the “Jungle Jim” ethical super-dilemma, which demands moral creativity in machines.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom-Mtg Info for IFLAI1 Class:  "Logic Can Save Us From Killer Robots"
  from “Killer Robots”
  Time: Mar 31, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• April 4 2022: Intro to Inductive Logic via The Monty Hall Problem, The Paradox of Grue, The Lottery Paradox, and AI for Drone Strikes (S Bringsjord)
  

  We begin by making the crucial distinction between deductive logic versus inductive logic, and take note of the fact that we’ve been (and will again after today) learning the former, not the latter. We then review The Monty Hall Problem to see that for at least some applications/domains formal logic must include both deduction over bivalent propositions and some machinery to cover uncertainty values (e.g. probability values between 0 and 1). Next, we briefly visit The Paradox of Grue, which is solved in detail in Bringsjord’s intermediate logic-and-AI class (IFLAI2), in order to explain that this paradox serves to divide and define three fundamentally different approaches to formal inductive logic, one that originates in Carnap and is mathematical, traditionally non-computational, and not proof-/argument-based (pure inductive logic); one that is rooted in philosophy and informal argumentation/informal logic; and the third approach, the one pursued by S Bringsjord:

  Base inductive logic on argument and proof, but do so in a formal/mathematical manner, and include not only probability theory and its relatives, but likelihood as well.

  This third approach enables S Bringsjord to provide a superior solution to The Lottery Paradox, by introducing a multi-valued inductive logic based on likelihood values that does the trick, lickety split. We end with some discussion of AI based on computational inductive logic of the third type for enabling AI to make rational, ethical decisions about drone strikes.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: IFLAI1 Apr 4 Mtg:  “Inductive Logic via The Monty Hall Problem, The Paradox of Grue, The Lottery Paradox, & AI for Drone Strikes”
  Time: Apr 4, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting now expired.
  

• April 7 2022: Overview of GGT Book; Gödel’s Completeness Theorem (S Bringsjord)
  

  After setting some context with a brief overview of the peerless collection of Gödel’s greatest theorems (each of which is covered in the forthcoming Gödel’s Great Theorems (by S Bringsjord; Oxford University Press), we cover the first of these theorems, which was achieved in Gödel’s dissertation. This is Gödel’s Completeness Theorem, and as part of it, König’s Lemma (which Gö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 hand-drawn content to allow some examples to be worked out; these 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 not possible.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Info for IFLAI1's Class Mtg:  "Overview of /Gödel's Great Theorems/ Book; Gödel's Completeness Theorem"
  Time: Apr 7, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• April 11 2022: Gödel’s First Incompleteness Theorem (S Bringsjord; extracted from his Gödel’s Great Theorems)
  

  This lecture covers the theorem for which Gödel is celebrated in the semi-popular literature and media; it says that, unfortunately, mathematics, indeed even just elementary arithmetic, contains an infinite number of propositions that will remain mysterious forever: unproved, with negations unproved as well (unless we turn to infinitary techniques: we assume that our axiom systems and our proof techniques are limited in certain ways — ways that yours truly, generally following Zermelo, rejects.) You have what you need to fully understand the theorem and proof, but if you are a mere mortal, will need to have your thinking cap on, and to be ready to ask questions as needed.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Info for IFLAI1 Class Mtg:  "Gödel's Famous First Incompleteness Theorem"
  Time: Apr 11, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• April 14 2022: Gödel’s Second Incompleteness Theorem (S Bringsjord)
  

  We here cover Gödel’s second incompleteness theorem (G2), which is a corollary of G1. As a matter of fact, armed with the Fixed Point Theorem, and G1, G2 really is rather a piece of cake to prove!

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Mtg for IFLAI1:  "Gödel's Second Incompleteness Theorem"
  Time: Apr 14, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• April 18 2022: Gödel’s Silver Blaze Theorem: $ZFC ¬\vdash ¬ CH (S Bringsjord)
  

  We here cover Gödel’s Greatest Theorem, in which he shows that ZFC set theory doesn’t deductively entail the Continuum Hypothesis (CH). [We leave aside the Generalized CH (GCH).] Without making any use of transfinite numbers, we set out and reflect upon both CH and the 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 results (put informally) that mathematics can’t be used to prove mathematics free of contradiction.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Info for IFLAI1 Class Mtg:  "Gödel's Greatest Theorem"
  Time: Apr 18, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• April 21 2022: 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.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Mtg for IFLAI1 Class Mtg:  "Gödel’s Time-Travel Theorem
  (and an 'insoluble problem' arising therefrom)"
  Time: Apr 21, 2022 12:00 PM Eastern Time (US and Canada)
  
  Zoom meeting expired.
  

• April 25 2022 Final IFLAI 2022 Lecture: Could AI Ever Match Gödel’s Greatness? (S Bringsjord; based on Part II of final chap his Gödel’s Great Theorems)
  

  In this lecture, the final one in IFLAI 2022, we explore the possibility of AI so powerful that it can reach Gödelian heights. Our investigation of this possibility includes reflection up a profound Either/Or proposition that Gödel introduced in a 1951 lecture at Brown University: either we are infinitely more powerful than any finite computing machine (e.g. a standard Turing machine, or the machines that underlie HyperSlate^®), or else there are absolutely (human-)unsolvable Diophantine problems. The lecture (proper) ends with the AI vs. Gödel “Scorecard,” and then discussion of the number and type of problems in forthcoming Test 3, and the grading scheme thereof.

  • Zoom-mtg Info here:

  Selmer Bringsjord is inviting you to a scheduled Zoom meeting.
  
  Topic: Zoom Info for IFLAI1 Final Class Mtg:  "Could AI Ever Match Gödel’s Greatness?"
  Time: Apr 25, 2022 12:00 PM Eastern Time (US and Canada)
  
  Join Zoom Meeting
  https://us02web.zoom.us/j/84063834369?pwd=TlpIWnlTOFlQWGlPQ3o4RjBOWHZGQT09
  
  Meeting ID: 840 6383 4369
  Passcode: 714766
  One tap mobile
  +19292056099,,84063834369#,,,,*714766# US (New York)
  +13126266799,,84063834369#,,,,*714766# US (Chicago)
  
  Dial by your location
          +1 929 205 6099 US (New York)
          +1 312 626 6799 US (Chicago)
          +1 301 715 8592 US (Washington DC)
          +1 253 215 8782 US (Tacoma)
          +1 346 248 7799 US (Houston)
          +1 669 900 6833 US (San Jose)
  Meeting ID: 840 6383 4369
  Passcode: 714766
  Find your local number: https://us02web.zoom.us/u/kxvVFn3Yk
  

Tutorials

• Getting Registered with HyperGrader^®/HyperSlate^®
  

  A simple tutorial, available here, in which someone registers into HyperGrader^® and proves that switching the order of conjuncts is provable in the propositional calculus = \(\mathscr{L}_{PC}\). This proof wins a trophy and earns a leaderboard spot for the Exercise switching_conjuncts_fine.

• Getting Started with HyperSlate^®: Propositional Calculus
  

  In this tutorial, available here, S Bringsjord starts from scratch with a blank workspace and uses HyperSlate^® and the PC provability oracle available therein to show that the atomic proposition \(h\) can be deduced from \(\{\neg \neg c, c \rightarrow a, \neg a \vee b, b \rightarrow d, \neg (d \vee e)\}\). The main purpose of this video is coverage of the intuitive interface and basic moves therein.

Pop Problems

Homeworks

Tests