Introduction to (Formal) Logic (via, and also to, AI)

Terminology & General Orientation

• Terminology
  

  Note that sometimes `symbolic’ is used in place of `formal.’ This is bad practice, since formal logic include 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.

• 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, 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\(^{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 Shreyansh Nawlakha and Swapnil Khandekar.

  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 Shreyansh Nawlakha and Swapnil Khandekar; their email addresses, resp., are shreyanshnawlakha@gmail.com and khands2@rpi.edu.

  Please note again 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 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 in this class, it helps to have at least some command of it from high school. A much more robust treatment of prerequisites and a suitable background for this course is provided in the syllabus.

Texts/Readings

Syllabi

HyperSlate\(^{TM}\)

HyperGrader\(^{TM}\)

LAMA-BDLA Textbook

Class-Day Topic and Content (includes associated files; e.g., slide decks, lectures, tutorials, HyperSlate\(^{TM}\) files, etc.)

• January 10 2019: 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 learning under a different paradigm than that of LAMAe\(^{TM}\) should take Intro to Logic in a Fall semester, since the “Stanford paradigm” is in use then.

• January 14 2019: 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 17 2019: 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!

• January 21 2019: MLK Day!
  

  No class.

• January 24 2019: 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 28 2019: 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 oracle are given. The upshot is that proof discovery is a joint and indeed collaborative enterprise that unites superior human intelligence with inferior by invaluable machine intelligence.

• January 31 2019: 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 4 2019: 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 7 2019: Pure General Logic Programming (PGLP), Intro & Overview
  

  Every proof in HyperSlate, from the tiny to the elaborate, can be viewed as a PGLP program, and starting from an explanation of this fact, PGLP was presented.

• February 11 2019: The Pure Predicate Caclulus = \(\mathcal{L}_0\); Toward Quantification (Selmer Bringsjord)
  

  We begin by noting the 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, it regiments and allows.

• February 14 2019: Review and Interactive QAO Session for Test 1 (Selmer Bringsjord)
  

  Among other things, we covered the problem BiconditionalIntroByChaining, and reviewed proof by cases, indirect proof, and partial solutions/hints were given to a series of challenges on HyperGrader as an extension of this review.

Homeworks