# 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^{®}.

- What is Formal Computational 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.) As to*computational*formal logic, well, for now let’s just say that computation*itself*can be taken to consist of reasoning in a logic — a fact that we shall be exploring. - 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 intermediate 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 first course in formal logic, preferably including computational 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 include 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

- the e-text
*Logic: A Modern Approach; Beginning Deductive Logic via*HyperGrader^{®}*and*HyperSlate^{®},*Advanced*(LAMA-BDLHGHSA); - the HyperSlate
^{®}interactive AI-infused environment for (among other things) proof and program construction in collaboration with AI technology (= the “oralces”); and - 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.

## Syllabus

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.

## HyperSlate^{®}

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^{®}.

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

## LAMA-BDLHGHSA Textbook

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

**August 28 2023**: 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, and will not be based on Motalen’s technology.**August 31 2023**: Tutorial, Mechanics; Historical and Scientific Context re. Formal Logic, AI, and Logic Machines (S Bringsjord)We begin by considering, armed with formal logic, the question “What is school for?,” taken up (9/1/22) in a symposium hosted by the

*New York Times*. Then, 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. (Review Problems for these logics will, starting today, be published with deadlines on the HyperGrader^{®}; platfor, due either on Sept 7 or Sept 11.)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 emphasis 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.**A (past) Corresponding Video Lecture**by S Bringsjord, “The Terrific Triad,” is available here.

**September 5 2023**: 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. (Later in the class we shall employ 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**(for contrast, and to set up for our next class): “Intensional Logic” in SEP

**September 7 2023**: Review of/Entry to Intensional/Modal Logics (S Bringsjord)We first take a look at some personalized AI-generated problems in our respective HyperGrader

^{®}accounts, and move from there into a full GUI tutorial. Then we briefly inquire as to whether there are any questions about the \(k\)-order logic ladder, and then return to the case of Blinky (of*Lost in Space*fame) 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; this coverage includes even the*infinitary*FBT. Handling these taks requires, certainly, intensional/modal logics. Finally, we encapsulate the modal logics**K**,**T**,**D**,**4**, and**5**, focus a bit on**D**, an early deontic logic, in connection with Chisholm’s Paradox, but end up targeting**5**=**S5**in this class. After reading the relevant portion of the textbook, the following are recommended for exceptionally sedulous students (focus on proof theory/inference):**Recommended Reading #1**: “Intensional Logic” in SEP**Recommended Reading #2**: “Modal Logic” in SEP**Recommended Reading #1**: “Deontic Logic” in SEP

**September 11 2023**: Church’s Theorem (S Bringsjord, w Naveen Sundar G on Turing machines)We first explore some advanced topics (e.g. automated planning) in HyperGrader

^{®}and HyperSlate^{®}. We then 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. We make use of the Halting Problem to obtain CT (and look at the kernel of reasoning in a HyperSlate^{®}workspace.**Recommended Background Reading**: “Turing Machines” in SEP

**September 14 2023**: Completeness Theorems (S Bringsjord)A video of this entire lecture, replete with use of HyperSlate to show how in it one can prove the completeness of the propositional calculus, and — following Gödel’s dissertation — of first-order logic, is provided via the link given here. As to our sequence, we begin with an overview of S Bringsjord’s forthcoming

*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. It turns out that because of the power of HyperSlate we can instantly convey the proof-kernel of completeness for both the propositional calculus and FOL, in line with what Gödel did. Our coverage here includes a characterization of completeness in general, and then in specific terms for \(\mathscr{L}_1\). We include some remarks about Leon Henkin, well known for devising a simpler, smoother proof of the completeness theorem.**September 18 2023**: Gödel’s First Incompleteness Theorem (S Bringsjord)We here cover the second 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 21 2023**: Gödel’s Second Incompleteness Theorem (S Bringsjord)We here prove Gödel’s

*second*incompleteness theorem (G2), which is a corollary of G1 (Gödel didn’t bother to prove it directly in his proof of G1).**September 25 2023**: Gödel’s Speedup Theorem (James Oswald)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! This is Gödel’s Speedup Theorem, the engineering consequences of which (inquisitive and wise) modern minds are still sorting out.

**September 28 2023**: An Introduction to Non-Axiomatic Logic and Some Quantification (James Oswald)James Oswald gives an introduction to some levels of Pei Wang’s Non-Axiomatic Reasoning System (NARS).

**October 2 2023**: Formal Logic, AI, Computer Science, and the Immaterial (S Bringsjord)Formal logic, AI, and computer science all at least appear to entail some non-physical things (e.g. algorithms, infinite cardinal numbers, etc.) exist. Does the entailment go through? And if it does, does this in turn entail that we are immaterial as well? Affirmative answers to both questions are defended by Bringsjord, based directly on this forthcoming paper. In addition, a particular view of computer science as dealing with the immaterial is discussed, with this paper as background.

**October 5 2023**: Machine-Learning Machines Don’t Learn; AI Needs … Real Learning (\(\mathcal{RL}\)) in the Form of Learning*Ex Nihilo*(S Bringsjord)AI of today has given the world so-called “machine learning,” or just ‘ML’ for short. But do machines doing ML actually learn? A negative answer is given, and defended; and a genuine form of learning (for natural and artificial agents), \(\mathcal{RL}\), is introduced and defended. The negative answer is based on (indeed can be found in) “Do Machine-Learning Machines Learn?”. The kind of deep, genuinely human-level learning that AI

*should*be based on is*Learning*, introduced in this paper.**Ex Nihilo****October 9 2023**No class: Columbus Day. (Why do we not celebrate Leiv Eiriksson Day?!)**October 12 2023**: Can We Ensure That AIs are Ethically Correct? (S Bringsjord)This class is to a significant degree based on S Bringsjord’s keynote at the 46th annual German national AI conference. The answer given to the title/question, in a word, is: When the AI in question is logicist, yes; and here’s how; but in the case of today’s so-called “generative” AI, the question is disturbingly open.

**October 16 2023**: AI, Consciousness, and Lambda (\(\Lambda\)) (S Bringsjord)This class is based on work by Bringsjord \& Govindarajulu as set out in this paper (a rough preprint; you should study first), and this second one (also a rough preprint), in which a new theory of machine consciousness is set out and associated with a scheme (\(\Lambda\)) for measuring this consciousness. B\&G also here articulate and analyze purported refutations of the Integrated Information Theory of consciousness advanced by Tononi \& Koch, and its associated scheme (\(\Phi\)) for measuring consciousness. In addition, it is explained how the concept of \textit{cognitive intelligence} can be based upon \(\Lambda\), and how this has substantive bearing on artificial \emph{general} intelligence = AGI.

**October 19 2023**: AI to Surmount Arrow’s (Impossibility) Theorem and Adjudicate Military Decision-Making (S Bringsjord)S Bringsjord presents and discusses/debates with the class two papers, (i) the 2021 paper

“Automated Argument Adjudication to Solve Ethical Problems in Multi-Agent Environments” Bringsjord, S., Govindarajulu, N.S. & Giancola, M.

*Paladyn, Journal of Behavioral Robotics***12.1**: 310–335. https://www.degruyter.com/document/doi/10.1515/pjbr-2021-0009/pdfas AI science & technology able to prevent such things as this tragedy, by surmounting Arrow’s Theorem, and a subsequent paper that initiates in earnest the need to capture testimonial evidence (in the broad sense not restricted in any way to legal contexts), viz.

“A Framework for Testimony-Infused Automated Adjudicative Dynamic Multi-Agent Reasoning in Ethically Charged Scenarios” Bringsjord, S., Rozek, B., Giancola, M., Bringsjord, S. & Govindarajulu, N.S. A Framework for Testimony-Infused Automated Adjudicative Dynamic Multi-Agent Reasoning in

*Value Sharing Between Humans and Robots*, Syun, S., Toki, M.O., Ferreira, M.I.A., Govindarajulu, N.S., Silva, M. & Goher, K.,eds. (London, UK: CLAWAR), pp. 47–66.**October 23 2023**: S5 Modal Logic And The Standard Translation (James Oswald)Class is structured as follows: 1) An overview of the universe of modal logics is given; 2) an axiomatic approach to S5, and interpretations of the axioms in different modalities, are provided; 3) the hypergraphical natural-deduction approach (HND) to S5 (overview of all S5 HyperSlate rules) is given; 4) a 15-minute exercise is carried out, in which the goal is to prove one direction of equivalence between the axiomatic S5 and HND S5 (students are asked to prove the 3 S5 axioms in a HyperSlate HND S5 workspace); next, 5) a very short discussion of possible-world semantics to ground what R is in the standard translation is carried out; then 6) the standard translation is presented; and finally 7) an exercise that calls for translating axioms 4 and B to FOL, and proving they are equivalent to axiom 5 in FOL, is conducted.

**October 26 2023**: What are We, Rigorously Speaking? (S Bringsjord)Class begins with a quick overview of a presentation by S Bringsjord at the Center for New American Security on AI from Motalen to help US nuclear strategists. Next, we look at a preview of our next metalogical problem (see the slides for details). And then we pass to the main question for the day: 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. We also briefly discuss Rapaport’s position that,*contra*Bringsjord, cognition is computation/computable.**October 30 2023**: 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.**November 2 2023**: 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.**November 6 2023**: Off Script: Autonomy-Trust Theorems (Planned: Introducing HyperLog (v .75)) (S Bringsjord)Selmer went “off script” here: He showed and discussed in-progress paper on a family of theorems relating levels of autonomy in AIs to levels of trust it’s rational to have in them.

2022 slide deck remains available here, in correspondence with this plan, carried out in 2022: 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.

**November 9 2023**: Off Script: Rapaport vs. Bringsjord (Planned: On Quantificational Modal Logic (S5-centric)) (S Bringsjord)Selmer goes off script again, to encapsulate the debate between Bill Rapaport and Bringsjord on the question “Will AI Match (or Even Exceed) Human Intelligence?” Rapaport has changed the question, but his “Yes” position, in draft form that will continue to be refined, is presented here. Selmer explains, and in part shows, that his “No” position is based on three cases, where each case includes multiple arguments. The three cases are:

*The Balloon-Bursting Case*. Many in AI have long been afflicted with an irrational level of optimism about human-level AI, with prediction after prediction that a certain year will bring human-level AI on stage. It never happens. What can inferred from these repeated failures?*The Superminds Case*. Logico-mathematically, we know well that there are modes of information-processing that far exceed in power what a standard Turing machine (and any equivalent, e.g. a Register machine) is capable of. If the human mind is capable of such processing, then, since AI is bound to Turing machines and less, Rapaport is wrong.*The Sledgehammers Case*. Even were the prior two cases to fail, just one of the sledgehammers in this case would suffice to obliterate the “Yes” position of Rapaport. One sledgehammer is*phenomenal consciousness*; we have it (which is why life is worth living) and enlist such consciousness to achieve intelligent behavior that’s otherwise unattainable; no mere computing machine, however it may compute, can have p-consciousness; ergo our level of intelligence is beyond the reach of AI.

The former plan, for which past slides are provided, was as follows. 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.**November 13 2023**: Off Script: White Paper on Engineering Ethical Control of Large Language Models (Formerly: Killer Robots & The PAID Problem in Star Trek TOS, D, and Beyond to DCEC* (in HyperSlate®)) (S Bringsjord)Going off script, Bringsjord strives to outline the start of a planned white paper on how to achieve ethical control of large language models, by extending prior work that can be used for ethical/legal control of AIs/robots that are logic-based.

Formerly: 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 turn to

*Star Trek TOS*to see this dynamic in action. 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.**November 16 2023**: Off Script: Session 2 on the White Paper (Formerly: DDE (Doctrine of Double Effect) => DDE* (with self-sacrifice) => DTripleE) (S Bringsjord)To start, we return to 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.**November 20 2023**: Gödel’s Silver Blaze Theorem, Part I: Further Context and Proof SketchIn 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. (All student should read the mystery story in question.)

- November 23 2023*: Thanksgiving!
**November 28 2021**: 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 single-slide! proof-sketch of Gödel’s stunning result.**November 30 2023**: Gödel’s Time Travel Theorem; Toward Selmer’s Solution of an “Insoluble” Time-Travel Puzzle (S Bringsjord)We now proceed to a more rigorous look at so-called video proofs for the possibility of backwards time travel, and then to consideration of a supposedly “insoluble” time-travel paradox from Storrs McCall, which Selmer recasts as “The Paradox of Proust,” and then proceeds to solve.

**December 4 2023**: Gödel’s God Theorem (Scott-Benzmüller edition) (S Bringsjord)Selmer reminisces about Prof James Ross’ public presentations at Penn of his claimed proof of God’s existence, and then we turn to the Scott-Benzmüller version of Gödel’s God Theorem, which is expressed in S5-modal third-order logic. Selmer then gives a glimpse of his new family of mental arguments.

## Tutorials

- Getting off the Ground into HyperGrader
^{®}and HyperSlate^{®}(Aug 2020)This short, simple “blast-from-the-past” 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 you can deduce in HS^{®}that \(\psi \wedge \phi\)).

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

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