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

Table of Contents

A "fully fungible" (in-person ∨ online ∨ hybrid) course, thanks to singular AI technology.

Selmer Bringsjord
with Naveen Sundar G. ∧ …



Figure 2: Larry


Figure 3: Lucy

[All artwork (all of which is copyrighted) for the LAMA paradigm by KB Foushée.]

General Orientation

This course gives advanced, accelerated coverage of intermediate computational formal logic, and — to an appreciable degree — logic-based (= logicist) AI. The course makes crucial use of AI for learning, and also provides coverage of selected “big questions” in and arising from logicist (= logic-based) AI. The course also covers the abject failure of brands of AI that are based on purely non-logical, numerical (artificial) neural-network techniques (e.g., deep learning). These failures can be summed up by saying, with Arkoudas, that such AI simply can’t reason (see e.g. his “GPT-4 Can’t Reason”). In addition, students are exposed to a pure and general form of logic programming invented by S Bringsjord under ANR support in his capacity of working in the PROGRAMme project, so-called Pure General Logic Programming (PGLP), and will be able to themselves write not only proofs, but proofs that include functional code written in Clojure, in the new logic-programming language HyperLog®.


First, students new to AI should read this overview of the field.

Next, students will purchase access to and obtain the symbiotically interconnected trio of

  1. the e-text Logic: A Modern Approach; Beginning Deductive Logic via HyperGrader® and HyperSlate®, Advanced (LAMA-BDLHGHSA);
  2. the HyperSlate® interactive AI-infused environment for (among other things) proof and program construction in collaboration with AI technology (= the “oralces”); and
  3. HyperGrader®, an AI-infused online platform for assessing student progress (HG® comprises HS®)

published by Motalen. Each member of this trio will be available online after purchase of a license, via 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-BDLHGHSA, and additional exercises, will be provided by listing on relevant HyperGrader® web pages upon signing in (and sometimes by email) through the course of the semester. You will need to manage many electronic files in this course, and e-housekeeping and e-orderliness are of paramount importance. You will specifically need to assemble a library in HyperGrader® of completed and partially completed proofs and other files in 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 HyperGrader® and HyperSlate® are each copyrighted, trademarked, and patented: copying and/or distributing this software to others is strictly prohibited. You will be asked to AGREE online after the time of registration to a License Agreement. This agreement will also cover the etextbook, which is copyrighted as well, and cannot be copied or distributed in any way, even in part.

In addition, occasionally papers will be assigned as reading.

Finally, slide decks used in class will contain crucial additional content above and beyond LAMA-BDLHGHSA, information posted on HyperGrader®, and in your library for HyperSlate®; this additional content will be available on the web site as the course unfolds through time.


The version of the course now underway is the Fall 2023 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.


This is the interactive environemnt system used for constructing proofs and arguments, and — in HyperLog® — pure logic programs (Clojure is available in order to make function symbols in formulae “live”), in collaboration with AI technology (our “oracles”), and is available here after registering, agreeing to the license agreement, and signing into HyperGrader®.


This is Motalen’s overarching AI platform for submitting, getting assessed, and earning trophies and learderboard points for proofs, arguments, and — in HyperLog® — pure logic programs (along with Clojure functions to make function symbols “live”) constructed in HyperSlate®, and is available here after registration and by sign-in.


This is the e-textbook for the course, and is obtained after registration and sign-in to HyperGrader®, via download. New versions of the book will appear directly in HyperGrader® for download.

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

Please note that for some classes there will be a slide deck and a video lecture (but the video lecture often will not be posted until after synchronous in-person instruction, and in some cases may not be posted, in order to prevent certain data from being fully public).


Informal Exercises and Metalogical Homeworks

These are assigned and discussed by direct point-to-point communication in in-person class meetings, on the HyperGrader® platform, and sometimes by email.



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 schemata 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.

Author: Selmer Bringsjord

Created: 2023-12-04 Mon 12:31

Emacs (Org mode 8.2.10)