Title: Introduction to Formal Logic
Number: 80-210
Prerequisites: None
Description: This is a self-paced, entirely computer-taught introduction
to formal logic. It covers an extensive curriculum ranging from sentential
and full first-order predicate logic, to integer arithmetic, probability
theory, and social choice theory. There are only three class meetings:
an introduction at the beginning of term, a midterm, and a final exam.
Human help is available at all times, and many of the exercises can be
completed on a state-of-the-art proof construction tutor now being developed
at CMU. Grading is based on how far one progresses in the computers curriculum
and on the two exams.
Title: Arguments and Inquiry
Number: 80-211
Prerequisites: None
Description: This course is an introduction to symbolic logic. The
development in this century of a rigorous, formal calculus for logical
reasoning is a significant scientific breakthrough -- the culmination of
a line of research stretching back literally to Aristotle. With it, reasoning
becomes amenable to treatment by formal methods and symbolic logic becomes
the science of correct reasoning. This watershed in the development of
logic has spurred its recent further development and opened the way for
numerous applications. This course introduces students to these modern
logical methods. We specify symbolic languages of propositional and quantificational
logic, in which large parts of ordinary English can be expressed. Logical
calculi for these languages then permit the analysis of arguments, leading
to the characterization of the important notion of logical validity. By
way of application, we systematically explore informal reasoning in natural
language and in elementary mathematics. Thus, students are also familiarized
with the basic techniques of set theory and arithmetic, in addition to
the methods of symbolic logic, with their many applications in mathematics,
computer science, linguistics and cognitive science. The course concludes
with an examination of the concept of computability (using Turing machines)
and its consequences regarding the limitations of formalized reasoning
(the theorems of Gödel and Church).
Title: Logic & Computation
Number: 80-310/610
Prerequisites: either 80-210, 80-211, or consent of the instructor.
DescriptionAn introduction to formal mathematical logic, with applications
to computer science. Topics include inductively defined structures, the
syntax and semantics of first-order logic, completeness, compactness, and
the Loewenheim-Skolem theorems. Topics may also include definability, nonstandard
models of arithmetic, intuitionistic, modal, and temporal logic, and automated
deduction.
Title: Computability & Incompleteness
Number: 80-311/611
Prerequisites: either 80-210, 80-211, or consent of the instructor.
Description: An introduction to computability theory and Gsdel's
incompleteness theorems. Topics include formal models of computation (Turing
machines, the lambda calculus, and the recursive functions), r.e and universal
r.e. sets, undecidability, formal systems, coding and self-reference, incompleteness,
and the undefinability of truth.
Title: Philosophy of Mathematics
Number: 80-312/612
Prerequisites: either 80-210, 80-211, or 36-202 or 36-217 or 36-226
or consent of the instructor.
Description: Problems in the foundations of mathematical analysis
prompted, around the turn of the century, renewed philosophical reflection
on mathematics and related mathematical and logical work. Set theoretic
and constructivist foundations for analysis are described; Hilberts program
is analyzed in detail. Finally, an attempt is made to defend a structuralist
position, influenced by Bernays and Bourbaki, that incorporates important
insights from the main foundational schools.
Title: Philosophy of Logic
Number: 80-313/613
Prerequisites: None
Description: The first part of this course analyzes the work in
and reflections on logic by Aristotle, Leibniz, and Frege. Tremendous progress
in clarifying and (partially) resolving problems has been made in this
century; most strikingly with respect to completeness and decidability
questions. These results will be discussed in the second part. Finally,
attention will be turned to theories of sets, classes, and properties.
Title: Logic in Artificial Intelligence
Number: 80-314/614
Prerequisites: either 80-211, 80-310/610, 21-600 or equivalent background
with consent of the instructor.
Description: An introduction to several formalisms used in knowledge
representation and database theory. The emphasis is placed on nonmonotonic
logic, conditional logic and belief revision methods. We will also study
epistemic and auto epistemic operators and consider applications in distributed
AI. Several methodological problems in AI are discussed.
Title: Modal Logic
Number: 80-315/615
Prerequisites: either 80-211, 80-310/610, 21-600 or equivalent background
with consent of the instructor.
Description: An introduction to first-order modal logic. The course
considers several modalities aside from the so-called alethic ones (necessity,
possibility). Epistemic, temporal or deontic modalities are studied, as
well as computationally motivated modals (like `after the computation terminates').
Several conceptual problems in formal ontology that motivated the field
are reviewed, as well as more recent applications in computer science and
linguistics. Kripke models are used throughout the course, but we also
study recent Kripkean-style systematizationÕs of the modals without
using possible worlds.
Title: Game Theory
Number: 80-405/705
Prerequisites: Undergraduates by permission only.
Description: The first part of course will be a standard introduction
Title: Recursion & Hierarchies
Number: 80-410/710
Prerequisites: 80-311/611 or equivalent, or consent of the instructor
Description: An advanced course in computability theory and recursion
theoretic hierarchies. Topics include finite-injury priority arguments,
the arithmetical and Borel hierarchies, and the projective and analytical
hierarchies.
Title: Proof Theory
Number: 80-411/711
Prerequisites: None
Description: An introduction to proof theory that addresses philosophical,
mathematical, and computational aspects of the subject. Topics may include:
the emergence of Hilbert's program, and proof theoryÕs more general
reductive goals; deductive systems, cut-elimination, and normalization;
the ordinal analysis of arithmetic; functional interpretation and the extraction
of computational information from proofs; and subsystems of second order
arithmetic.
Title: Intuitionism & Constructive Mathematics
Number: 80-412/712
Prerequisites: None
Description: The course first presents basic principles of constructive
mathematics (as formulated e.g. by Kronecker, Hilbert, Bishop) and the
distinctive features of Brouwers intuitionistic analysis. Then intuitionistic
logic and a variety of semantics are investigated. Finally, we discuss
the fundamental difference between a constructivist and realist position
in the foundations of mathematics.
Title: Category Theory
Number: 80-413/713
Prerequisites: either 80-310/610, 21-600, or consent of the instructor
Description: Category theory, a branch of abstract algebra, has
found many applications in mathematics, logic, and computer science. Like
such fields as elementary logic and set theory, category theory provides
a basic conceptual apparatus and a collection of formal methods useful
for addressing certain kinds of commonly occurring formal and informal
problems, particularly those involving structural and functional considerations.
This course is intended to acquaint students with these methods, and also
to encourage them to reflect on the interrelations between category theory
and the other basic formal disciplines.
Title: Topics in Logic & Mathematics
Number: 80-414/714
Prerequisites: None
Description: This course develops parts of the subjects that are
not covered in the regular offerings, for example, a detailed discussion
of geometry.
Title: Formal Semantics
Number: 80-481/781
Prerequisites: 80-210 or 80-211.
Description: This course is designed to provide the student with
a sound basis for intermediate and advanced work in the formal semantics
of natural language. The first part of the course will review set theory,
and propositional, predicate, and modal logic; and will introduce the student
to intentional logic and categorical grammar. In parallel with the presentation
of such formal systems, there will be a discussion of phenomena peculiar
to the semantics of natural language, including the distinctions between
sense and reference, direct and indirect quotation, propositional attitudes,
generic and specific reference, quantifiers, and adverbial. The second
part of the course will present one system for the semantics of English
Montague semantics in great detail.
Title: Logic & Computation Research Seminar
Number: 80-510/810
Prerequisites: None
Description: This seminar is intended for Logic&Computation
Majors and beginning graduate students. It covers, on the one hand, a particular
topic in logic, computation, or methodology; on the other hand, it introduces
students to current work in the department by "guest lectures"
of faculty members.
Title: Logic and Computation Research Symposium
Number: 80-511/811
Prerequisites: None
Description: This course provides a forum for the presentation and
detailed discussion of research done by students, be they undergraduates
working on their Senior Thesis or graduate students engaged with their
M.S. thesis.
Title: Seminar on the Foundations of Mathematics
Number: 80-513/813
Prerequisites: None
Description: The seminar will focus on mathematical and logical
work, important for foundational issues. For example, in the context of
Hilbert's program, fragments of first and second-order arithmetic are investigated.
The main questions are: (1) which parts of mathematical analysis can be
developed in weak subsystems of second order arithmetic, and (2) what computational
information can be extracted from proofs? This involves a presentation
of significant subclasses of recursive functions, the proof-theoretic analysis
of fragments of arithmetic, and of combinatorial principles. This course
is cross-listed with Mathematics and is open to undergraduates by permission
of the instructor.
Title: Seminar on Categorical Logic
Number: 80-520/820
Prerequisites: 80-413/713
Description: This course focuses on applications of category theory
in logic and computer science. A leading idea is functorial semantics,
according to which a model of a logical theory is a set-valued functor
on a category determined by the theory. This gives rise to a syntax-invariant
notion of a theory and introduces many algebraic methods into logic, leading
naturally to the universal and other general models that distinguish functorial
from classical semantics. Such categorical models occur, for example, in
denotational semantics. Another logical topic relevant to computation is
the lambda-calculus, and it is perhaps best treated via the theory of cartesian
closed categories. Similarly, higher-order logic receives elegant categorical
expression in the theory of topoi. Many other logical topics such as recursion
theory also have category-theoretical treatments, which invariably shed
light on their relations to other fields, both in logic and beyond.