21-600 Mathematical Logic I
Instructor: Peter Andrews
MWF 11:30am-12:20pm
HH B131
12 Units
Description: The study of formal logical systems which model the
reasoning of mathematics, scientific disciplines, and everyday
discourse. Propositional calculus and first-order logic. Syntax,
axiomatic treatment, derived rules of
inference, proof techniques, computer-assisted formal proofs, normal
forms, consistency, independence, semantics, soundness, completeness,
the Lowenheim-Skolem and Downward Lowenheim-Skolem Theorems, compactness.
TEXTBOOK: Peter B. Andrews, An Introduction to Mathematical Logic and
Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic
Publishers, now published by Springer, 2002.

21-603 Model Theory I
Instructor: Rami Grossberg (rami@cmu.edu)
MWF 1:30
Room TBA
12 Units
DESCRIPTION: Model theory is one of the four major branches of
mathematical logic. There are many applications of model theory to
algebra (e.g. field theory, algebraic geometry, number theory, and group
theory), analysis (non-standard analysis, complex manifolds and the
geometry of Banach spaces) and theoretical computer science (via finite
model theory) as well as set theoretic topology and set theory. This
course is the first in a sequence. The purpose of this course to
introduce the student to some of the most important ideas of the field
with a special attention to "classification theory" which is the most
important subfield of modern model theory.  The main focus of the course is
Morely's categoricity theorem, the related conceptual infrastructure and
extensions.

Topics will include: compactness theorem, model completeness, elementary
decideability results,
Henkin's omitting types theorem, prime models. Elementary chains of
models, some basic two-cardinal theorems, saturated models
(characterization and existence), basic results on countable models
including Ryll-Nardzewski's theorem. Indiscernible sequences, and
connections with Ramsey theory, Ehrenfeucht-Mostowski models.
Introduction to stability (including the equivalence of the
order-property to instability), chain conditions in group theory
corresponding to stability/superstablity/omega-stability, strongly
minimal sets, various rank functions, primary models, and a proof of Morley's
categoricity theorem. Basic facts about infinitary languages and abstract
elementary
classes, computation of Hanf-Morley numbers.

PREREQUISITE: This is a graduate level course, while at the beginning
the pace will be slow, the pace will speed up in the second half. In the
past many students where undergraduates, so the prerequisites are kept
to the minimum of "an undergraduate-level" course in logic. Motivated
undergraduate students are encouraged to contact the instructor.
TEXT: Rami Grossberg, A course in model theory, a book in preparation.
Most of the material (and more) appears in the following books:
1. C. C. Chang and H. J. Keisler, Model Theory, North-Holland 1990.
2. Bruno Poizat, A course in Model Theory, Springer-Verlag 2000.
3. S. Shelah, Classification Theory, North-Holland 1991.
I will not use a text, but will provide access to my notes on a weekly
basis.
EVALUATION: Will be based on weekly homework assignments (20%), a 50
minutes midterm (20%) and a 3 hours in-class comprehensive final written
examination (60%).
COURSE WEBPAGE: www.math.cmu.edu/~rami/mt1.09.desc.html

80-610 Logic and Computation
Instructor: Steve Awodey
TR 1:30 - 3
SH 125
12 Units
Description: An introduction to formal 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. Further topics may also include
definability, nonstandard models of arithmetic, higher-order,
intuitionistic, and modal logic.
Textbook: Logic and Structure, van Dalen.
Prerequisite: 80-210, 80-211, 80-212, 15-251

80-315/80-615 Modal Logic
Instructor:  Horacio Arlo-Costa
TR 03:00-04:20PM
HH B103
9,12 units
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
Scott-Montague models of the so-called 'classical' modalities. Some advanced
topics are covered as well (like general frames incompleteness, and semantics
for intentional and probabilistic operators).

80-513/813 Seminar on Philosophy of Mathematics
Instructor: Wilfried Sieg
W 2:00am-4:20pm
BH 150
9-12 Units
Description: Hilbertıs various consistency programs are being investigated.
Weıll trace their roots in 19th century mathematics (in particular in
Dedekindıs work), analyze the finitist program of the 1920s in detail,
and examine the philosophical horizons for contemporary proof theoretic
investigations.
TEXTBOOK OR REFERENCES: The Architecture of Modern Mathematics - Essays
in History and Philosophy; Jose Ferreiros and Jeremy Gray (eds.)
Oxford University Press, 2006
Mostly, we'll read papers by Hilbert, Bernays and Weyl; supplemented by
(unpublished) lectures of Hilbert's.

80-814 Categorical Logic
Instructor: Steve Awodey
M 3:30 - 6
BH 150
12 Units
Description: This seminar focuses on applications of category theory in
logic. We will cover a selection of topics from the following: Lawvere
algebraic theories; dependent type theory; Kripke and sheaf semantics
for intuitionistic, first-order and modal logic; topos theory.
Lectures, homework, and occasional student presentations.  Note: this
course will begin with a 2 week refresher of basic category theory, so
that students not having had 80-413/713 -- and CS students after
immigration -- can participate by reviewing on their own.
Course notes provided.
Prerequisite: Category Theory 80-413/713 or equivalent

15-819 M: Data, Code, Decisions
Instructor: André Platzer
12 Units
TR 1:30-2:50
GHC 4301
Description: Debugging programs can be a tedious task, since bugs can
hide everywhere: in the data, the code, or in the decisions of how to
combine them to form objects. Even after hours of testing and debugging,
familiar and tricky questions arise: "have we tested enough, are there
still bugs, or does the program work correctly now?" A fundamental
approach to address these questions once and for all is to verify the
correct functioning of the program with respect to its specification.
One of the verification challenges for many current programming
languages (Java,C++,Python,...), is that they have objects combining
data (information) and code (behavior).
For handling data during verification we need to understand
corresponding theories and decision procedures, e.g., for (fragments of)
linear integer arithmetic, rational/real arithmetic, arrays and the
like. For code, we need to understand its effect and the impact of
decisions in control structures. The analysis becomes particularly
intricate for object-oriented programs, where the dynamic type of the
data determines which code to execute, which, in turn, determines the
transformation on the data, which may finally affect code execution at a
later point in time ... Ultimately, data and code become interdependent
in the presence of aliasing of object references.

This class will provide you with logic-based techniques for verifying
object-oriented programs, their data and code. At the same time, the
course provides insight on various decision procedures for theories
relevant in the domain of program verification. Decision procedures can
be used to decide, e.g., whether a property is true in a suitable
theory/interpretation of first-order logic. These theories and their
combination are of independent interest and have applications in many
other areas, including, e.g., hybrid systems analysis.

COURSE WEBPAGE: http://symbolaris.com/course/dcd.html