syll intlog s19

Transcript

1 Introduction to (Formal ) Logic (via, and also to, AI ) Spring 19, M R 12–1:50 DCC308 Selmer Bringsjord Rensselaer AI & Reasoning (RAIR) Lab Department of Cognitive Science Department of Computer Science Lally School of Management Rensselaer Polytechnic Institute (RPI) Troy NY 12180 USA Office Hours: M R 345–5 CA 3rd flr; & by appointment (518) 276-6472 [email protected] version 0407192130NY Contents 1 1 General Orientation 2 2 Assistance to Bringsjord 2 3 Prerequisites 2 4 Textbook/Courseware 5 Schedule 3 5.1 Why Study Logic?; Its History (I) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 5.2 Propositional Calculus ( L ) & pc “Pure” Predicate Calculus ( L 4 ) (II) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 0 5.3 First-Order Logic (FOL = L ); 1 Glimpse of SOL = 5 , TOL = L L (III) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 3 5.4 Theories (= Axiom Systems) (IV) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 5.5 Deontic Logic and Killer Robots (V) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 5.6 Beginning Heterogenous Logic & Beginning ductive Logic (BIL): Glimpses (VI) . . . . . . . . . . . 5 In 5.7 G ̈odel (VII) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 6 Grading 7 7 Some Learning Outcomes 7 8 Academic Honesty 7 References 8

2 1 General Orientation 1 tm This course is an accelerated, advanced introduction, within the LAMA to deductive paradigm, in ductive and heterogeneous formal logic (with at least some brief but informative pointers to both 2 The phrase we use to describe what the student is principally introduced to in formal logic). beginning deductive logic, advanced (BDLA). AI plays a significant role in advancing this class is: learning in the class; and the class includes an introduction to logicist aspects of AI and computer programming. 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 , which are all based on formal logic. The formal sciences include e.g. theoretical formal sciences the computer science (e.g., computability theory, complexity theory, rigorous coverage of programming and programming languages), mathematics in its traditional branches (analysis, topology, algebra, etc), decision theory, game theory, set theory, probability theory, mathematical statistics, etc. (and of course formal logic itself). tm paradigm.” What is that? This question will be We have referred above to “the LAMA tm answered in more detail later, but we do say here that while the LAMA paradigm is based upon a number of pedagogical principles, first and foremost among them is what can be labelled the 3 Driving Dictum: If you can’t prove it, you don’t get it. Turning back to the nature of formal logic, it can accurately be said that it’s the science and 4 engineering of reasoning, but even this supremely general slogan 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 indeed tm experimenting with in the HyperSlate system) expressed in the formal logic known as ‘first-order logic’ (= FOL = L be hearing more about), and, as we shall see and discuss , which you’ll also 1 1 tm ’ is an acronym for ‘Logic: A Modern Approach,” and is pronounced to rhyme with ‘llama’ in contem- ‘LAMA Lama glama , and has in fact porary English, the name of the exotic and sure-footed camelid whose binomial name is been referred to in the past by the single-l ‘lama.’ 2 Sometimes ‘symbolic’ is used in place of ‘formal,’ but that’s a bad practice, since — as students in this class pictorial will soon see — formal logic includes the representation of and systematic reasoning over information, and such information is decidedly not symbolic. For a discussion of the stark difference between the pictorial vs. the symbolic, and presentation of a formal logic that enables representation of and reasoning over both, see (Arkoudas & Bringsjord 2009), which directly informs Chapter 8 of our textbook. 3 It’s profitable to ponder a variant of this dictum, applicable in venues [e.g. legal hearings, courtrooms, reports by analysts in various domains that are not exclusively formal (e.g. fundamental investing, intelligence, etc.)] in which reasoning is not only deductive, but inductive, viz. “If you can’t show by explicit argument that it’s likelihood reaches a sufficient level, you don’t get it.” 4 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 declarative 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 . 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 and its LAMA-BDLA textbook, 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. 1

3 in class, computer science emerged from and is in large part based upon logic (for cogent coverage of this emergence, see Glymour 1992, Halpern, Harper, Immerman, Kolaitis, Vardi & Vianu 2001). all at once rational-and-rigorous intellectual pursuits. (If you Logic is indeed the foundation for 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.) 2 Assistance to Bringsjord [email protected] ; and Shreyansh The TAs for this course are: Swapnil Khandekar; email address: Nawlakha; email address [email protected] . Swapnil will hold office hours on Tues 10a–12p on CA 3rd flr (and by appointment). Shreyansh will hold office hours on Fri 2p–4p also on CA 3rd flr (and by appointment). Some guest lectures may be provided by researchers working in the RAIR Lab, a logic-based AI lab. 3 Prerequisites formal logic, There are no formal prerequisites. However, as said above, this course introduces and does so in an accelerated, advanced way. This implies that — for want of a better phrase — students are expected to have a degree of logico-mathematical maturity. You have this on the assumption that you understood the math you were supposed to learn in order to make it where you 5 are. For example, to get to where you are now, you were supposed to have learned the technique indirect proof (= proof by contradiction = reductio ad absurdum of ). 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 (Bass & Johnson 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 (Bellman, Bragg & Handlin 2012). It’s recommended that during the first two weeks of the class, students review their high-school coverage of formal logic, which includes 6 L . at minimum the rudiments of the propositional calculus = pc 4 Textbook/Courseware Students will purchase the inseparable and symbiotic triadic combination published by Motalen: • Logic: A Modern Approach; Beginning Deductive Logic, Advanced via Hyper- the e-textbook tm Slate (LAMA-BDLA); tm • AI system (for, among other things, assessing student access to and use of the HyperGrader work); and 5 If you happen to be a student reading this as one wanting to be introduced to formal logic, from outside RPI, please examine your own case realistically. If you are not in command of the traditional high-school-level content for algebra, geometry, trigonometry, and at least some (differential and integral) calculus, you will need to go with a tm standard, non-advanced introduction to logic in the LAMA paradigm, or in some other paradigm. Specifically, if tm ’ paradigm, you will need the LAMA-BDL textbook, not LAMA-BDL A . The ‘A’ in ‘LAMA-BDL A in the LAMA is for ‘Advanced.’ Check which textbook you have! 6 Sometimes referred to as ‘sentential logic’ or ‘zeroth-order logic.’ (For us, zeroth-order logic, L , includes relation 0 symbols and function symbols, as well as identity.) If you are at all confused about how these terms were used before reaching the present course, please discuss asap with the instructor or TAs. 2

4 tm • AI system (for, among other things, engineering proofs access to and use of the HyperSlate in collaboration with AI); All three items will be available after purchase in the RPI Bookstore of an envelope with a per- sonalized starting code for registration. Logistics of the purchase, and the contents of the envelope that purchase will secure, will be encapsulated in the first class meeting, Jan 10 2019, and then gone over in more detail on Jan 14 2019, after which the envelopes in question will soon be on sale tm tm in the Rensselaer Bookstore. The first use in earnest of HyperSlate and HyperGrader will happen in class on Jan 28 2019, so by the start of class on that day students should have LAMA- tm tm on their laptops in class. BDLA, and be able to open both HyperSlate and HyperGrader Updates to LAMA-BDLA, and additional exercises, will be provided by listing on the course web page (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/arguments/truth-trees etc. so that you can use them as building blocks in harder proofs; in other words, building up your own “logical library” will be crucial. tm tm Please note that HyperSlate are copyrighted software: copying and/or and HyperGrader reverse-engineering and/or distributing this software to others is strictly prohibited. You will need to submit online a signed version of a License Agreement. This agreement will also reference the textbook, which is copyrighted as well, and since it’s an ebook, cannot be copied or distributed or resold in any way. In addition, occasionally papers may be assigned as reading. Two background ones, indeed, are hereby assigned: (Bringsjord, Taylor, Shilliday, Clark & Arkoudas 2008, Bringsjord 2008). Finally, slide decks used in class will contain crucial additional content above and beyond tm tm LAMA-BDLA and HyperSlate content, and will be available on the web and HyperGrader site for course for study. Along with slide decks, video and audio tutorials and mini-lectures will be provided as well. 5 Schedule The progression of class meetings is divided into seven parts: first a motivation/history stretch I, during which we show that the logically untrained have great trouble reasoning well, and set an historical context for modern logic and AI, and then six additional parts II–VII. In the first of these remaining parts we’ll focus in II on the (= L propositional calculus ); in III on first-order pc second-order logic logic ) and beyond; and in ), with a brief look at (= FOL = (= SOL = L L 2 1 IV we’ll cover modal logic (in the form, specifically, of four closely related modal logics: T , S4 , D (= ), and S5 , with the emphasis on SDL as a formalism for AI/machine ethics). Emphasis will SDL be on learning how to construct proofs in each system. Part V of the course looks at formal axiom systems, or as they are often called in mathematical logic, theories . Part VI of the course looks at formal in ductive logic, and to a degree at logics for reasoning over visual content (e.g., diagrams). The seventh (VII) and final part of the course is a synoptic look at some of the astonishing work of perhaps the greatest logician: Kurt G ̈odel. 7 A more fine-grained schedule now follows. 7 Note that the Rensselaer Academic Calendar is available here. 3

5 5.1 Why Study Logic?; Its History (I) instructions for purchase of a personalized code in the Bookstore, which will enable students to tm : Jan 10 General Orientation to the LAMA • obtain LAMA-BDLA and gain access to both Paradigm, Logistics, Mechanics . The syllabus tm tm . Codes, and HyperGrader HyperSlate is reviewed in detail. It’s made clear to the stu- in laser-tagged, sealed envelopes, should be on dents that, in this class, there is a very definite, sale after this class meeting. comprehensive, theoretical position on formal logic and the teaching thereof; this position tm 5.2 Propositional Calculus ( ) & L pc corresponds to the affirmation of the LAMA “Pure” Predicate Calculus ( L ) (II) (= Logic: A Modern Approach) paradigm, and 0 that in lockstep with this position the tightly Jan 28 : Review from High School: Variables • integrated trio of . This & Connectives; Propositional Calculus I meeting will tie up any loose ends on the his- 1. the LAMA-BDLA textbook, tory side of things. Students by this point tm proof-construction system, 2. HyperSlate tm should have HyperSlate running on their and laptops, have their codes registered, and have tm 3. HyperGrader system for (among other signed and accepted their LA. This is the start things) automated assessment of proofs, of coverage of the propositional calculus, L . pc are used. Students wishing to learn under the : Propositional Calculus II: The Formal • Jan 31 “Stanford” paradigm are encouraged to drop Language, First Rules of Inference/Inference tm -based course and take PHIL 2140 this LAMA . Application to Schemata, and Immaterialism in its alternating spot (i.e., Fall semester, an- some of the original problems used to motivate nually). the course (meetings Jan 14 & 17). Simple proofs settle these problems. The view that • Motivating Puzzles, Problems, Para- : Jan 14 formal logic, in particular some of the rudi- . Here we among other R doxes, H , , Part I ments of the propositional calculus, is based on things tackle problems which, if solvable be- immaterial world, a view defended by the late fore further learning, obviate taking the course. James Ross (1992), is presented and defended. We also discuss Bringsjord’s “elevated” view of the human mind as potentially near-perfectly Feb 4 Propositional Calculus III: Remaining : • rational, and specifically capable of systematic . Here Rules of Inference/Inference Schemata and productive reasoning about the infinite. we discuss the “harder” inference schemata; e.g. proof-by-cases/disjunction elimination. More • Jan 17 : Motivating Puzzles, Problems, Para- substantive proofs achieved. In addition, indi- . A continuation of Part H , R doxes, , Part II rect proof is introduced in earnest. I; the problems in question get harder. Feb 7 : Propositional Calculus IV: Pure Gen- • • No Class: Martin Luther King Day : Jan 21 eral Logic Programming (PGLP) at the Level Whirlwind History and Overview of • Jan 24 : L of . Some harder proofs obtained. This pc Formal Logic (in intimate connection with com- class meeting will probably be the first time tm puter science and AI), From Euclid to today’s HyperSlate is used in conjunction with tm . In one class Cutting-Edge Computational Logic HyperGrader . Demonstrations will be given. meeting we surf the timeline of all of formal By this time students should be set up to use tm logic, from Euclid to the present. A particular HyperGrader to win trophies. Coverage here emphasis is placed on Leibniz, the inventor of of resolution, and PGLP at the level of the modern formal logic. Aristotle is cast as the in- propositional calculus. ventor of formal logic in its original form (syllo- Feb 11 • : The Pure Predicate Calculus . This is gistic deduction). The crucial timepoint of the zeroth-order logic, or L , for us. What kind of 0 Entschei- discovery of the unsolvability of the logic do we get if we add to the propositional dungsproblem by Turing-level computers fig- calculus machinery for relation symbols, func- ures prominently, and supports a skeptical po- tion symbols, and identity (=)? The result is sition on The Singularity. The class ends with 4

6 L , and we explore some problems and proofs 5.4 Theories (= Axiom Systems) (IV) 0 in this logic. EA Theories of Arithmetic I (e.g., : Mar 28 • ). • Feb 14 : Review, taking stock, prep for first : Apr 1 • ). Theories of Arithmetic II (e.g., PA test (next class), sustained Q&A. • Feb 18 : No class (President’s Day Holiday) Test #1 . Note that this is a Tuesday! • : Feb 19 5.5 Deontic Logic and Killer Robots (V) Modal Logic: What and Why : Apr 4 . This • ); 5.3 First-Order Logic (FOL = L 1 is a general introduction to the crucial differ- extensional ence between logic versus inten- L , TOL = L Glimpse of SOL = 3 2 L logic. The logics , L L , sional , , L L 3 2 1 0 pc (III) are all extensional. Now we move to the inten- The Need for Quantification, and the : • Feb 21 sional category, which includes modal logics. Centrality Thereof in Human Thought and Com- Five modal logics are introduced, rapidly for munication . = T , K now: , D , M S4 , and S5 . Feb 25 : New Inference Schemata in • L = 1 D Apr 8 . After a quick SDL = : The System • FOL, I . We here introduce, discuss, and em- peek ahead at the PAID Problem and “The universal elim ; ploy existential intro and Four Steps” that — we claim — can solve it, these are the two easy ones. But easy as they D SDL . we proceed to consider deontic logic = might be, do they suffice to enable us to prove This is the basic system of logic intended to that God exists? capture central categories in ethics (e.g., obli- gation, permissibiity, etc.). It will turn out • : A New (Harder) Inference Schema Feb 28 that is in need of major improvement, if SDL . We introduce FOL, II = in L universal 1 not outright replacement, because (for starters) , the first of the two harder new infer- intro of two paradoxes: Chisholm’s Paradox and the ence schemata for FOL. Free-Choice Permission Paradox. : Mar 4–Mar 8 Spring Break • • Apr 11 : The Threat of “Killer” Robots . Here : Proofs/Problems in = L Mar 11 • . FOl, III 1 again is presented the “PAID” problem: artifi- We here cover the inference schema existential a owerful, p cial agents/robots that are utonomous, . elim angerous (if not capable d ntelligent, are i and d of estroying us). : Mar 14 . FOl, IV = • L Proofs/Problems in 1 Now we’re ready for some challenges in FOL! . Af- • : Apr 15 Logic Can Save Us; Here’s How (origi- ter taking note of the fact that Star Trek The Liar; Russell’s Paradox; Skolem’s : • Mar 18 nal) teaches us that logic can save us, this class . Paradox introduces an engineered quantified multi-operator ∗ : ZFC; Second-Order Logic (SOL), Third- Mar 21 • , developed at Rensselaer, modal logic, DCEC Order Logic (TOL), and Beyond (e.g. Type The- and explains how use of the computational ver- ory) . We return here to the failed attempt sion thereof, implemented, can be used to en- to prove God’s existence, and with some help able an AI/robot to adjudicate thorny ethical from Kurt G ̈odel, try again. dilemmas. : • Test #2 Mar 25 5

7 5.6 Beginning Heterogenous Logic & Beginning ductive Logic (BIL): In Glimpses (VI) • : Heterogeneous Logic; Whirlwind His- Apr 18 tory & Overview Beginning (Formal) Inductive tm Logic (LAMA-BIL) in the LAMA . Paradigm A solution to the Lottery Paradox is provided, and recent work in the RAIR Lab devoted to solving the St Petersburg Paradox will also be covered. 5.7 G ̈odel (VII) • : G ̈odel’s Completeness Theorem & First Apr 22 Incompleteness Theorem . We seek here to un- derstand the brilliant core of G ̈odel’s CT, from his doctoral dissertation. In addition, we pro- vide the class with a glimpse of G ̈odel’s stun- ning in completeness theorems, and briefly take up the question: Could an AI ever match G ̈odel? • Apr 25 : Test #3 6

8 6 Grading Grades are based in part on three in-class tests. Each of these tests will call for in-class use of tm tm . The three tests are weighted 10%, 15%, and in conjunction with HyperGrader HyperSlate 25%, respectively. In addition, grades are based on a series of required problems to be done in tm tm . Every problem in the series must be the HyperSlate system, and verified by HyperGrader tm certified 100% correct by HyperGrader in order to pass the course, and a grade of ‘A’ is earned tm must for the series, which is 40% of the final grade. All required assignments on HyperGrader be completed and submitted in order to receive a final grade. The remaining 10% of one’s grade is tm based on performance on “pop” problems given in class, to be solved in HyperSlate and graded tm . Finally, please note that class attendance is mandatory. Any more than two by HyperGrader unexcused absences will result in a failing grade. 7 Some Learning Outcomes There are four desired outcomes. One : Students will be able to carry out formal proofs and tm disproofs, within the HyperSlate system and its workspaces, at the level of the propositional and predicate calculi, and propositional modal logic (the aforementioned systems T , S4 , D , and S5 ). Two : Students will be able to translate suitable reasoning in English into interconnected formulae in the languages of these four calculi, and assess this reasoning by determining if the desired structures are present in the formulae and relationships between them. , students will Three Four be able to carry out informal proofs. , students will demonstrate significant understanding of the advanced topics covered. 8 Academic Honesty Student-teacher relationships are built on mutual respect and trust. Students must be able to trust that their teachers have made responsible decisions about the structure and content of the course, and that they’re conscientiously making their best effort to help students learn. Teachers must be able to trust that students do their work conscientiously and honestly, making their best effort to learn. Acts that violate this mutual respect and trust undermine the educational process; they counteract and contradict our very reason for being at Rensselaer and will not be tolerated. Any student who engages in any form of academic dishonesty will receive an F in this course and will be reported to the Dean of Students for further disciplinary action. (The Rensselaer Handbook defines various forms of Academic Dishonesty and procedures for responding to them. All of these forms are violations of trust between students and teachers. Please familiarize yourself with this portion tm for course credit under of the handbook.) In particular, all solutions submitted to HyperGrader a student id are to be the work of the student associated with that id alone, and not in any way copied or based on the work of anyone else. References Arkoudas, K. & Bringsjord, S. (2009), ‘Vivid: An AI Framework for Heterogeneous Problem Solving’, Artificial Intelligence 173 (15), 1367–1405. URL: http://kryten.mm.rpi.edu/KA SB Vivid offprint AIJ.pdf 7

9 Bass, L. & Johnson, A. (2012), Geometry: Common Core , Pearson, Upper Saddle River, NJ. Series Authors: Charles, R., Kennedy, D. & Hall, B. Consulting Authors: Murphy, S. & Wiggins, G. Bellman, A., Bragg, S. & Handlin, W. (2012), , Pearson, Upper Saddle River, NJ. Algebra 2: Common Core Series Authors: Charles, R., Kennedy, D. & Hall, B. Consulting Authors: Murphy, S. & Wiggins, G. Bringsjord, S. (2008), Declarative/Logic-Based Cognitive Modeling, in R. Sun, ed., ‘The Handbook of Com- putational Psychology’, Cambridge University Press, Cambridge, UK, pp. 127–169. lccm ab-toc 031607.pdf URL: http://kryten.mm.rpi.edu/sb Bringsjord, S., Taylor, J., Shilliday, A., Clark, M. & Arkoudas, K. (2008), Slate: An Argument-Centered Intelligent Assistant to Human Reasoners, in F. Grasso, N. Green, R. Kibble & C. Reed, eds, ‘Proceed- ings of the 8th International Workshop on Computational Models of Natural Argument (CMNA 8)’, University of Patras, Patras, Greece, pp. 1–10. etal Slate cmna crc 061708.pdf http://kryten.mm.rpi.edu/Bringsjord URL: Glymour, C. (1992), Thinking Things Through , MIT Press, Cambridge, MA. Halpern, J., Harper, R., Immerman, N., Kolaitis, P., Vardi, M. & Vianu, V. (2001), ‘On the Unusual Effectiveness of Logic in Computer Science’, The Bulletin of Symbolic Logic 7 (2), 213–236. Ross, J. (1992), ‘Immaterial Aspects of Thought’, The Journal of Philosophy 89 (3), 136–150. 8

Related documents