Logic & Proofs (Copy)


An introductory logic course, designed for students from a broad range of disciplines, from mathematics and computer science to drama and creative writing.


Logic is a remarkable discipline. It is deeply rooted in the past going back to its first systematic presentation in Aristotle’s work. In its modern form, it has not only expanded Aristotelian Logic in dramatic ways, but it has also become foundational, e.g., for linguistics, computer science, cognitive science, and artificial intelligence. It is, of course, deeply intertwined with philosophy and mathematics as correctness of argumentation is particularly crucial for these abstract disciplines.

The relationship of logic to other subjects and disciplines.

Logic & Proofs is a rigorous introduction to modern symbolic logic that covers both sentential and predicate logic (including identity). The crucial skills of recognizing the (in-)correctness of arguments are honed by working in the LogicLab: in derivation or proof problems, students learn to construct complex arguments in a strategically guided way; in truth table and truth-tree problems, the emphasis is on systematically finding counterexamples.

The LogicLab with an active truth-table problem.

The LogicLab is a central part in bringing these core topics to vivid life. Indeed, the course has been constructed to provide support for individual learning through active engagement; that is a most important feature and applies across all versions and is reflected in all features of Logic & Proofs, whether using the course as an individual learner or as a student at an academic institution.

Active engagement

Logic & Proofs is designed for students from a broad range of disciplines, from mathematics and computer science to drama and creative writing. It is also designed for someone who would like to get a real insight into modern symbolic logic. The course is highly interactive and engaging; it brings a fresh perspective to classical material. These features make it possible for any student to master the material — by supporting their individual learning. After all, students in such introductory courses have quite diverse backgrounds and strikingly different perspectives on the courses’ formal aspects. Students from the arts or from the humanities may need more examples and, very importantly, more time to absorb material and to practice with helpful feedback; it is remarkable how well they actually can do.

The presentation is multi-modal: each chapter is introduced by a concise lecture that formulates its central notions and techniques and motivates its learning objectives. In the main text, each central concept is also introduced by a brief lecture; each important technique is examined and used in a particular example. That kind of discussion is followed by interactive learning environments, namely, “Did I get this?” exercises that are essentially multiple-choice problems, and “Learn by doing” exercises that are genuine cognitive tutors. The most sophisticated ILE is the LogicLab.

A 'Learn By Doing' problem in the course text.

The course material is carefully scaffolded and has been iteratively improved — using the feedback of both the many students who have taken the course and their instructors. Each chapter features review materials and assignments that include both quizzes and lab problems. The quizzes and practice questions provide fully automated feedback to students. The practice lab problems offer support by the Dynamic Tutor. In sum, the course and all its ILEs support the individual learning of students.

A portion of a 'Practice Lab Problems' page from the course text.

NEXT TAB: LogicLab and the Dynamic Tutor

LogicLab and the Dynamic Tutor

The central logical skills are developed in the LogicLab lab environment mentioned earlier. In derivation problems, students practice proof construction in a natural deduction framework.

The LogicLab with an active derivation problem.

Here, their learning is supported by an intelligent automated tutor. This Proof Tutor helps students, on demand and dynamically, to think through arguments in a systematic and strategic fashion. The Proof Tutor uses the automated proof search mechanism AProS to provide, as part of the dialogue with the student, strategically informed hints for solving proof problems.

The LogicLab with an active derivation problem and the Tutor in use.

In the semantic truth-table and truth-tree problems, students practice techniques for a semantic analysis of formulae and arguments. They begin with “chasing truth up the tree of grammar”, in Quine’s vivid language; then they complete truth-tables and build truth-trees for sentential and predicate formulae involving identity. Ultimately, they learn how to define counterexamples to incorrect arguments using a completed truth-tree.

The LogicLab with an active truth-tree problem.

Individual Learner

Logic & Proofs is available for individual learners in two different modes. The first mode is the completely free version. This version does not include the chapter assignments or any exams; it is to be used for a detailed, free exploration of modern logic and this novel approach to logic instruction. In particular, the chapters’ practice problems for the construction of proofs allow appeals to the supportive Dynamic Proof Tutor.

Then there is, secondly, the certificate version that carries a small registration fee of $80. Here the individual student has access to the full course content of Logic & Proofs (but without Instructor or TA support, and not including any exams). As in the free version, the chapters’ practice problems allow, when involving the construction of proofs, appeals to the Proof Tutor. The assignments do not; they give students the opportunity to demonstrate the mastery of their logical skills. All the chapter assignments are graded automatically and provide informative feedback.


A Carnegie Mellon Certificate is obtained by solving more than 75% of the Quizzes and Lab problems; if learners solve more than 90%, they obtain a Certificate with distinction.

Finally, in the certificate version, the learner has also access to the standalone version of the LogicLab, i.e., a free-standing application that has all the features of the online version. The standalone LogicLab goes beyond the course labs in that it allows students to formulate their own problems and then to solve them in the same fashion as the problems contained in the course material.

The problem editor in the standalone version of the LogicLab.

Academic Use

At Carnegie Mellon and elsewhere, Logic & Proofs is offered as a semester-long or quarter-long course with varying degrees of instructor and TA support.

  • At CMU, in addition to working through the online material at a specified rate (approximately one chapter per week), the class meets in small groups once a week for an instructor-led discussion session. Active student participation is not only encouraged, but required.
  • At some institutions, Logic & Proofs is used as the main resource for a course with traditional weekly lectures, as well as meetings with a TA.
  • At yet other institutions, Logic & Proofs has been offered as a fully self-paced course, with online and drop-in instructor and/or TA support, but without regular class meetings.

In all three modes of use, Logic & Proofs has been found pedagogically effective. See the relevant research by Patchan, Schunn, Sieg, and McLaughlin at the AProS project site.

The course has been taken since 2007 by more than 13,000 students for credit at various institutions including Carnegie Mellon University, Carnegie Mellon Qatar, IUPUI, Francisco Marroquín University (Guatemala), Habib University (Pakistan), Haverford College, University of British Columbia, University of Nevada in Las Vegas, Kent State University, College of Lake County, University of Washington, University of Maryland (College Park), and the University of South Florida.

Instructor Options and Choices

For instructors wishing to try out or start using Logic & Proofs, there are several versions of the material available in the OLI Course Builder, accessible via an instructor’s account on OLI:

  1. The full course, designed for the semester system (13+ weeks), including identity as a core chapter and with functions available as an additional topic. This version includes three midterms and one final exam.
  2. The full course, designed for the semester system (13+ weeks), including predicate logic only in the core topics, with both identity and functions available as additional topics. This version includes three midterms and one final exam
  3. A slightly reduced course, designed for the quarter system (10 weeks), including identity as a core chapter and with functions available as an additional topic. This version includes one midterm and one final exam.
  4. Sentential logic only. This version includes a final exam.

The exams included in these versions are optional. They can be removed from the course syllabus in the Course Builder, or left in but not assigned, instead serving as optional practice activities. We also have available versions of the material that include different numbers of exams, with the exam timing being somewhat different. Please contact us for details if you are interested in the possibility of using a different exam suite.

For instructors wishing to include functions as a core topic, or make any other alterations to the selection of core vs additional material, we are able to accomodate most such requests (given advance notice), and are happy to work with you to determine the best selection of core material to suit your needs.

The versions of the material mentioned above make all lab problems available to students at all times. We also offer precondition versions with the same content and exam options as those above that restrict access to lab problems as follows: students must complete in-chapter lab activities to unlock the chapter review problems, and must complete the review problem sets (by finishing at least one problem in each set) in order to unlock the chapter lab assignment. Instructors interested in using these additional preconditions in their sections should please contact us for more information and assistance setting up a course that uses them.

Detailed Content

Statements and Arguments
The central logical notions of statements and arguments are introduced. The notion of the standard form of an argument is presented, as are the criteria adopted for judging the quality of an argument.
Learning objectives:
  • Explain what a statement is, and discuss how statements are related to sentences.
  • Determine whether or not a sentence of English expresses a statement, and if so, to identify the statement expressed.
  • Explain what an argument is, and determine whether or not a given
    passage constitutes an argument.
  • Identify the premises and conclusion of an argument, and
    represent the argument in standard form.
  • List the criteria an argument must meet in order to be considered
    a good argument, and explain why each criterion is necessary.
  • Determine whether premises support the conclusion jointly or independently.
  • Determine whether a given argument is a bad or a good argument, and why this is the case.
Sentential Logic
Syntax and Symbolization
The syntax of the language of sentential logic is introduced. Translation to and from sentential formulae and syntactic analysis of expressions is the focus.
Learning objectives:
  • Discern the logical structure of English sentences.
  • Symbolize English sentences as formulae of sentential logic.
  • Explain the grammar of the logical language of sentential logic.
  • Construct and identify formulae of sentential logic.
  • Construct and use parse trees.
The semantics of the language of sentential logic are discussed. The notions of truth-values and truth-functions are introduced, and a number of semantics tools for the evaluation of both formulae and arguments are presented.
Learning objectives:
  • Explain what a truth-value assignment is.
  • Give the truth-conditions for the logical connectives.
  • Determine the truth-value of a formula relative to a given truth-value assignment.
  • Construct a truth-table for a given formula or argument.
  • Use truth-tables to analyze arguments and formulae.
  • Explain what tautological, contingent, and contradictory formulae are.
  • Find a counterexample to an invalid argument, using a truth-table or truth-tree.
The notion of a derivation is introduced, and the inference rules for the binary connectives are presented.
Learning objectives:
  • Explain the structure of derivations.
  • Apply and identify applications of rules of inference within a derivation.
  • Establish the validity of rules of inference.
Indirect Rules
The inference rules relating to negation are introduced.
Learning objectives:
  • Apply and identify applications of the inference rules for negation.
  • Explain the structure of indirect rules of inference.
  • Find contradictions to use in applications of indirect rules.
Strategies and Derived Rules
Strategies for completing derivations efficiently and easily are discussed, and a number of derived rules of inference are presented.
Learning objectives:
  • Approach proof construction problems in a strategic fashion.
  • Apply and identify applications of derived rules.
  • Provide explanations of and explain some significant properties of the logical connectives.
Elementary Metamathematics
A number of metamathematical notions are introduced and a new connective is added to the language.
Learning objectives:
  • Show that two formulae are logically equivalent just in case their biconditional is a tautology.
  • Explain how a biconditional can be considered logically equivalent to a formula in disjunctive normal form.
  • Find a disjunctive normal form equivalent to any formula.
  • Explain the connection between truth-tables and Boolean circuits.
Predicate Logic
Syntax and Semantics I
The first step in the transition from sentential to predicate logic is taken, by introducing the notions of predicates and singular terms.
Learning objectives:
  • Identify and distinguish between predicates and singular terms.
  • Analyze the internal logical structure of English sentences.
  • Construct atomic formulae from predicates and singular terms according to syntactic rules.
  • Semantically interpret and evaluate formulae constructed using predicates and singular terms.
Syntax and Semantics II
The transition from sentential to predicate logic is completed by introducing the notions of quantifiers and variables.
Learning objectives:
  • Analyze the internal logical structure of English sentences involving quantity terms.
  • Construct arbitrary predicate formulae according to the syntactic rules.
  • Semantically interpret and evaluate predicate formulae.
The derivation system for sentential logic is expanded to cover predicate arguments, by adding introduction and elimination rules for the quantifiers.
Learning objectives:
  • Apply and identify applications of the inference rules for the quantifiers.
Strategies and Derived Rules
The strategies for efficient derivation completion are reconsidered in the predicate context, and a number of derived rules for predicate logic are presented. A normal form for predicate logic, called prenex normal form, is also introduced.
Learning objectives:
  • Extend the strategic considerations for the construction of proofs to predicate logic.
  • Develop, apply, and identify applications of derived rules.
  • Convert an arbitrary formula into an equivalent formula in prenex normal form.
The notion of identity is introduced and discussed, and additions are made to the syntax, semantics, and derivation system in order to incorporate this notion.
Learning objectives:
  • Translate English sentences involving identity into the extended language of predicate logic.
  • Apply and identify applications of the inference rules for identity.
  • Give the Russellian analysis of sentences involving definite descriptions.
The notion of functions is introduced and discussed, and additions are made to the syntax and semantics in order to incorporate this notion.
Learning objectives:
  • Use function symbols in translating both English sentences and mathematical statements.
  • Use syntactic and semantic techniques with function symbols.

Versions and Features

Features Individual Use Academic Use
Independent Certificate Sentential Full Course
Logic Only Quarter Semester
free $80 $40/student $80/student
Sentential Logic
Predicate Logic
End-of-Chapter Practice
Quiz Questions
Lab Exercises
End-of-Chapter Assignments
Chapter Quiz
Lab Assignment
Proof Tutor available on selected practice problems
Standalone Version
Midterm Exams 1 1 3
Final Exam
OLI Website:
New look and
New student registration process

OLI’s website has undergone a refresh, and so has the student registration process. Watch the video to see how easily students can register with a Course Key.