# Intermediate Formal Logic and AI (= IFLAI2)

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

Selmer Bringsjord
with Naveen Sundar G. $$\wedge$$ …

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

## General Orientation

This course gives advanced, accelerated coverage of intermediate formal logic and logic-based (= logicist) AI. This course makes crucial use of AI for learning, and also provides coverage of selected “big questions” in and arising from logicist AI. In addition, students are exposed to a pure and general form of logic programming, 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.

• What is Formal Logic?

In general, formal logic is the science and engineering of reasoning,1 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

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 HyperSlate® and HyperGrader®, Advanced/ (LAMA-BDLHSHGA);
2. the HyperSlate® software system for (among other things) proof and program construction in collaboration with AI technology (= the “oralces”); and
3. HyperGrader®, an AI-infused online system for assessing student progress.

Each member of this trio will be available online after purchase of 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-BDLHSHGA, 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 the course of this course, and e-housekeeping and e-orderliness are of paramount importance. You will specifically need to assemble a library of completed and partially completed proofs 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 HyperSlateHyperGrader® and HyperGrader® are each copyrighted and trademarked: copying and/or distributing this software to others is strictly prohibited. You will need to AGRRE online after the time of registration to a License Agreement. This agreement will also cover the textbook, which is copyrighted as well, and cannot be copied or distributed in any way, even in part.

In addition, occasionally papers may be assigned as reading.

Finally, slide decks used in class will contain crucial additional content above and beyond LAMA-BDLHSHGA, 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.

## Syllabus

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

## HyperSlate®

This is the interactive software system used for constructing proofs and arguments, and Clojure functions, in collaboration with AI technology, and is available here after registering, agreeing to the license agreement, and signing into HyperGrader®.

## HyperGrader®

This is the AI system for submitting, getting assessed, and earning trophies and learderboard points for proofs, arguments, and Clojure functions constructed in HyperSlate®, and is available here after registration and by sign-in.

## LAMA-BDLAHSHG Textbook

This is the e-textbook for the course, and is obtained after registration and sign-in to HyperGrader®, via download.

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

Please note that for each class 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.

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

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

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

• 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 forthcoming.

Forthcoming!

## Footnotes:

1

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.

Created: 2020-09-17 Thu 14:33

Emacs 25.3.50.1 (Org mode 8.2.10)

Validate