# Introduction to (Formal) Logic (and AI)

(= IFLAI; pronounced: “eye” “fly”)

## Table of Contents

Selmer Bringsjord

with Naveen Sundar G.

\(\wedge\) Joshua Taylor \(\wedge\) \(\ldots\)

Figure 2: Larry

Figure 3: Lucy

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

## Terminology & General Orientation

This course is an advanced, accelerated introduction to deductive
formal logic, with some substantive coverage of
*in*ductive formal logic, in which formalisms
for dealing with uncertainty (e.g. probability theory, and also the
likelihood calculus) are included, and to heterogeneous formal logic
(which allows reasoning over not only textual/linguistic content, but
visual content as well). The course conforms to the
LAMA^{TM} paradigm in general, and is
specifically based on **Hyperlogic**, which among other things (all of
which are explained and covered) is based on the view that proofs and
arguments are best cast as **hypergraphs**. Since the present course is
focused on deduction, the course is specifically based on
**hypergraphical natural deduction**. To our knowledge, this is the
only robust treatment of formal logic based on this form of deduction,
which as many unique advantages.

The course makes crucial use of AI for learning, and also provides an
introduction to AI itself, at least AI of the logicist variety. In
particular, students are exposed to a pure and general form of logic
programming (so-called **PGLP**) that is particularly well-suited for
pursuing logicist AI.

The last part of the class includes distinctive coverage of some of the great theorems of humanity’s greatest logician: Kurt Gödel.

- 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,

^{1}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 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\(^{TM}\),’ or simply by the abbreviation ‘LAMA\(^{TM}\),’ 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

^{TM}paradigm. This thus applies specifically to TAs Aayush Masheshwarkar and Hariharan Sreenivas. As to what these thinkers hold in connection with LAMA^{TM}, that is an open question. You are free to inquire! - Graduate Teaching Assistants; Further Help
The TAs for this course are the most-capable duo of Aayush Masheshwarkar and Hariharan Sreenivas; their email addresses, resp., are

`aayushnmaheshwarkar@gmail.com`

and`harhara4698@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

Students will purchase access to and obtain the inseperably interconnected trio of

- the e-text
*Logic: A Modern Approach; Beginning Deductive Logic via HyperSlate*(LAMA-BDLA);^{TM}, Advanced - the HyperSlate
^{TM}software system for (among other things) proof construction in collaboration with AI technology; and - HyperGrader
^{TM}, an AI-infused online system for assessing, tracking, and broadcasting (in anonymized form on leaderboards) 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-BDLA, and additional
exercises, will be provided by listing on relevant
LAMA^{TM} web pages upon signing in (and
sometimes by email) through the course of the semester. You will need
to manage many electronic files as this course proceeds, 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 HyperSlate^{TM} is

copyrighted: copying and/or distributing this software to others is strictly prohibited. You will need to AGREE online (after registration) 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. Two, indeed, were assigned in the syllabus, on the first day of class.

As to AI, it’s strongly recommended that students read the online summary of AI provided by Bringsjord & Govindarajulu, available here.

Finally, slide decks used in class will contain crucial additional
content above and beyond LAMA-BDLA, information posted on
HyperGrader^{TM}, and on
HyperSlate^{TM}; 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 Spring **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^{TM}

This is the software system used for constructing proofs and arguments in collaboration with AI technology, and is available here after registration and sign-in.

## HyperGrader^{TM}

This is the AI system for submitting, getting assessed, and earning
points for proofs and arguments constructed in
HyperSlate^{TM}, and is available here after
registration and by sign-in.

## LAMA-BDLA Textbook

This is the textbook for the course, and is obtained after registration and sign-in, by downloading.

## Lectures

**January 13 2020**: General Orientation to the LAMA\(^{TM}\) 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

^{TM}should take*Intro to Logic*in a Fall semester, since the “Stanford paradigm” is in use then.**January 16 2020**: 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 is included. For a full video of the

**2018**version of this session done in 1:1 style, replete with audio proofs of some of the rather tricky problems presented, click here. Students for whom 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 Φ \(\vdash\) φ ∧ ¬ φ, then Φ \(\vdash\) ψ].**January 21 2020**: MLK Day!No class.

**January 23 2020**: Motivating Paradoxes, Puzzles, and \(\mathcal{R}\), Part II (S Bringsjord)This slide deck, expanded over that used in the previous class, shows some of solutions expressed as informal proofs, and contains Moriarty’s ticking-bomb challenge! — and also Special Llamas Disjunction.

**January 27 2020**: 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*.**January 30 2020**: Propositional Calculus I (S Bringsjord)This class meeting introduces one of the central tenets of LAMA\(^{TM}\): 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\(^{TM}\)’s oracles are given. The upshot is that proof discovery is a joint and indeed collaborative enterprise that unites superior human intelligence with inferior but invaluable machine intelligence.

**February 3 2020**: Propositional Calculus II (S Bringsjord)The simple but cornerstone inference rule of

*modus ponens*(a.ka. /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\(^{TM}\) corresponds to*disjunction elimination*. Tutorials are provided via real-time use of HyperSlate\(^{TM}\) on key exercises.**February 6 2020**: 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 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 regimented in HyperSlate.**February 10 2020**: Pure General Logic Programming (PGLP)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, PGLP was presented, in its historical context.

**February 13 2020**: The Pure Predicate Caclulus = \(\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.

## Tutorials

- Thwarting Dr M’s Fiendish Challenge
The AI in HyperSlate

^{TM}is used here to confirm that the blue wire is the right one to snip, in order to save life on Earth.

## Pop Problems

These problems are presented in class in the absence of any preceding announcement that they are coming. Please see the syllabus for more information.

## Homeworks

Homework consists of solving *all* required problems listed on
HyperGrader^{TM}’s web pages. (Non-required
problems are clearly marked as such, e.g. as **Bonus Problems**.) All
solutions are created in their final form in
HyperSlate^{TM}.
HyperGrader^{TM} for interactive use via its
underlying AI technology opens for its Spring 2020 stint on or about
Jan 27 2020, and an orientation/introduction to the system is given in
class that day. Note that homeworks cannot be done without access to,
and sustained and continuous use of,
HyperSlate^{TM} and
HyperGrader^{TM}.

## Tests

There are three tests. Please see the syllabus for their dates.

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