Introduction to Formal Logic (with AI)
Spring 2026 Edition of IFLWAI (“eye” • “full” • “way”)
Selmer Bringsjord

Terminology & General Orientation

• Terminology
  

  Note that sometimes ‘symbolic’ is used in place of ‘formal.’ This is bad practice, since formal logic includes the aforementioned 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 formalization 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, in connection mostly with number theory.

• What Next?
  

  After this class, the student can proceed to the intermediate level in formal deductive and inductive logic (computational or otherwise), 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, computational cognitive science, formal/theoretical computer science, and in-depth 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.) Present matters expressed a bit more boldly, and in keeping with S Bringsjord’s views, amount to saying that formal logic is the field that allows formalization of anything at all that is sufficiently precise, and thus all disciplines that are sufficiently precise can in fact for reduced to and subsumed by formal logic.

• 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, S Bringsjord thinks he has with others in Motalen invented a better way to define, specify, and present formal logic with AI, and to use computational formal logic for AI, and he is toiling to explain this invention to others, and to disseminate the invention in question. The better way in question is denoted (i) by the phrase ‘Logic: A Modern Approach^®,’ or simply by the abbreviation ‘LAMA^®,’ pronounced so as to rhyme with ‘llama;’ and (ii) by the word ‘HyperLogic.’

• 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 any and all TAs and graduate students. As to what these other thinkers hold in connection with LAMA^®, that is an open question. You are free and indeed encouraged to inquire!

• Graduate Teaching Assistants; Further Help
  

  The TA for this Spring 2026 edition of the course is PhD student Brandon Rozek, an expert on computational logic and AI, and especially automated planning (rozekb@rpi.edu). 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-CLAIGHS Textbook

Class-Day Content

• January 12 2026: 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 and a different collection of software systems than that of LAMA^® and its patented and Pat. Pend. AI systems should take Intro to Logic in a Fall semester, since the “Stanford paradigm” is in use then.

• January 15 2026: 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. ∀ Φ, φ, ψ: if Φ ⊢ φ ∧ ¬ φ, then Φ ⊢ ψ], which is needed at a key juncture in this lecture.

• January 19 2026: MLK Day! No class.
  

• January 22 2026: Motivating Paradoxes, Puzzles, Part II (S Bringsjord & Brandon Rozek)
  

  We start by briefly taking note of the excellent contrarian Wall Street Journal essay “No, AI Machines Can’t Think” by A. Kessler (Jan 7 2024), and a better-than-the-Turing-Test test mentioned within in it: the Lovelace Test, presented here. And we consider some vintage “AI In The News”: whether AI’s should be conscious, as illogically asserted in a NY Times opinion piece (“Without Consciousness, AIs Will Be Sociopaths,” Jan 13 2023). (Illogically? Yes: Contra the author, Princeton’s Prof. Graziano, from φ → ψ one cannot validly deduce ¬ φ → ¬ ψ!) Next, after review of more puzzlers, including 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?

• January 29 2026: 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 reasoner LogicTheorist stole the show. (We analyzed a theorem that LT automatically proved.) The class includes discussion of The Singularity, and ends with Bringsjordian skepticism about The Singularity in light of (Turing-level) machine impotence in the face of the Entscheidungsproblem, a landmark, must-be-understood problem in the history of formal logic (and of computer science, cognitive science, and AI).

• February 2 2026: Propositional Calculus I, Emphasis on Our First Oracle (S Bringsjord)
  

  We first return to the topic of The Singularity, and observe that D Amodei’s recent essay on “Confronting and Overcoming the Risks of Powerful AI” (available Confronting and Overcoming the Risks of Powerful AI surely contains a premeditated reference to the driving mecahnism in The Singularity; e.g. see

  [This] picture probably underestimates the likely rate of progress. Because AI is now writing much of the code at Anthropic, it is already substantially accelerating the rate of our progress in building the next generation of AI systems. This feedback loop is gathering steam month by month, and may be only 1–2 years away from a point where the current generation of AI autonomously builds the next. This loop has already started, and will accelerate rapidly in the coming months and years. Watching the last 5 years of progress from within Anthropic, and looking at how even the next few months of models are shaping up, I can feel the pace of progress, and the clock ticking down. (Paragraph #6)

  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. 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 and automated verification. A full, live, hands-on tutorial regarding the UI of HyperSlate^® is given, and HyperSlate^®’s PC-provability oracle is covered as well.

  • A video showing the use of the PC provability oracle (in an older but still-pedagogically-sufficient-here version of HyperSlate^®) solving the “NYS 3” logic problem is available here.

• February 5 2026: Propositional Calculus II (S Bringsjord)
  

  The simple but cornerstone inference rule of modus ponens [a.k.a. conditional elimination, in the natural-reasoning tradition (specifically the branch inaugurated by Gentzen) we are following] is introduced, and claimed (by S Bringsjord) 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.

• February 9 2026: Propositional Calculus III (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 even this level there is in fact excellent coverage of indirect proof, and then see how reductio ad absurdum is formalized in HyperSlate^®. The foregoing is Part I; in Part II, Selmer recounts James Oswald’s strategies and tips for proof-construction in HyperSlate^®, the slide deck for which is available here.

• February 12 2026: Darwin’s Mistake+; The Pure Predicate Calculus = ℒ₀; 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 = ℒ₀. ℒ₀ is introduced specifically in connection with (1), which, in contrast to the weaker propositional calculus = ℒ_pc, it regiments and allows. Presentation and discussion is rendered concrete by use of HyperSlate^®.

• February 17–24 2026: Test 1, Introduced via This Slide Deck
  

  Test 1 consists of six problems, two personalized, AI-generated ℒ₀ problems, and two personalized, AI-generated ℒ_pc problems. Grades on Test 1 will be computed by this simple logic: Winning one trophy yields a letter grade of C, two a B, 3 and A, and all an $A+*; but of course the competition on Test 1, which is entirely separate from a grade, as maintained and reported on the relevant leaderboard, is another matter.

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

  Here begins coverage of ℒ₁ and we thereby begin Part III of the course. We start by noting the need for quantification in syome very simple arguments, then explicitly introduce the two simplest inference rules/schemata for quantifiers in ℒ₁. 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 significant 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ödelian Essays on Artificial Versus Personal Inteligence: Pretenders Versus Persons.

• Feb 23 2026: FOL II (including universal intro) (S Bringsjord)
  

  After the usual pointer to an AI-in-the-News issue, 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 intos action to reach some theorems (including three regarding the relative smartness of different Scandinavian countries). In Part II of our class meeting we analyze how to prove DeMorgan’s Theorems in natural deduction, and here we look at some attempts by OpenAI’s LRMs to generate these proofs.

• February 26 2026: 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 (and trickiest) 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.

Tutorials (expands as semester unfolds)

• Getting Registered with HyperGrader^®/HyperSlate^®
  

  A vintage-but-still-helpful simple tutorial is available here, in which someone registers into the HyperGrader^® platform, and then activates HyperSlate^® to prove 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.

• Switching Disjuncts is Fine (under 90 sec)
  
  • Just click here.
• 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.

Live Logic

Homeworks

Tests

Card Logic

• Pair 1:
  
  • 🂴 🃅 🃖 🃗
  • 🂥 🂶 🃗 🃈
• Pair 2:
  
  • 🂱 🃒 🂳 🃄
  • 🂲 🃃 🂤 🂵
• Incomplete Pair With Mystery Card:
  
  • 🃉 🃚 🂫 🃍
  • 🂺 🃋 🂭 🂠
• Options For Mystery Card:
  
  • 🃝 🃍 🃞 🃑