Skip navigation
The Australian National University

Course descriptions

Fundamentals of metalogic

Content: Completeness theorems, Model theory and proof theory.

Course description: This course provides an introduction to the metatheory of elementary logic. Following a "refresher" on the basics of notation and the use of classical logic as a representation language, we concentrate on the twin notions of models and proof. An axiomatic system of first order logic is introduced and proved complete for the standard semantics, and then we give a very brief overview of the basic concepts of proof theory and of formal set theory. The material in this course is presupposed by other courses in the Summer School, which is why it is presented first.

Pre-requisites: it is assumed that students are at least familiar with logical notation for connectives and quantifiers, and can manipulate truth tables, some kind of proof system or semantic tableaux or the like. Normally they will have done a first logic course at tertiary level. Some basic mathematical competence is also presupposed, to be comfortable with the notion of a formal language, follow proofs by induction, be OK with basic set-theoretic notation and the like.

Lecturer: John Slaney is the founder and convenor of the Logic Summer school. He originated in England, ever so long ago, and discovered Australia in 1977. Undeterred by the fact that it had apparently been discovered before, he gradually moved here, joining the Automated Reasoning Project in 1988 on a three-year contract because he could not think of anywhere better to be a logician. He is still here and still can't. His research interests pretty much cover the waterfront, including non-classical logics, automated deduction and all sorts of logic-based AI. He was formerly the leader of the Logic and Computation group at the ANU, and of the NICTA program of the same name.

Introduction to modal logic

Content: Kripke models, Hilbert calculi, Frame correspondences, Tableaux-based decisions procedures and Propositional linear temporal logic

Course description: We cover the syntax, Kripke semantics, correspondence theory and tableaux-style proof theory of propositional modal and temporal logics. These logics have important applications in a diverse range of fields incuding Artificial Intelligence, Theoretical Computer Science and Hybrid Systems.

Pre-requisites: You should have a good grounding in classical propositional and first-order logic, including material covered in the "Fundamentals of Metalogic" course. Some very basic notions from graph theory would also be useful, but are not essential.

Lecturer: Rajeev Gore is currently a a professor in the ANU, and leader of the Logic and Computation research group. He was an Australian Research Council Queen Elizabeth II Fellow at the ANU from 1997-2001, a Research Fellow and later Senior Fellow at the ANU from 1994-2011, and a Research Associate at the University of Manchester from 1992-1993. He obtained his PhD in Modal Theorem Proving from the University of Cambridge in 1992.

Overview of automated reasoning

Content: Automated propositional theorem proving; automated first-order theorem proving; Interactive theorem proving

Course description: In many applications, we expect computers to reason logically. We might naively expect this to be what computers are good at, but in fact they find it extremely difficult. In this overview course, we look at various methods to automate logical reasoning, which are needed to support a variety of application domains.

Automated reasoning procedures are parametrized by the logic they are capable of reasoning with. We distinguish between propositional logic and first-order logic. Development and application of propositional logic procedures, also called SAT solvers, received considerable attention in the last ten years, e.g., for solving constraint satisfaction problems, applications in hardware design, verification, and planning and scheduling. Regarding automated deduction in first-order logic, we discuss applications, standard deductive procedures such as resolution, and basic concepts, such as unification. We also examine the dual problem of theorem proving, viz., generating models of a given theory, which has applications to finding counterexamples for non-theorems, and we provide an overview of some recent trends (instance-based methods, satisfiability modulo theories). Finally, we describe in some depth so-called quantifier elimination methods for theorem proving in decidable fragments of arithmetics over the reals and the integers.

Pre-requisites: Elementary logic, as provided by the "Fundamentals of Metalogic" course of this Summer School.

Lecturer: Peter Baumgartner is a researcher in the Canberra Laboratory of Data61 (part of CSIRO). In NICTA, the precursor of Data61, he was a Principal Researcher in Software Systems and formerly the lab manager of the "Managing Complexity" theme. Previous employments were at the Max Planck Institute for Computer Science and the University of Koblenz, both in Germany. His research interest is automated deduction, particularly for first-order logic, and its applications. He holds a PhD and a Habilitation degree in Computer Science.

Computability and incompleteness

Contents: Computability; recursive Functions and Turing machines; diagonalisation; Peano arithmetic and Gödel numbering; undecidability of first-order logic; incompleteness of Peano arithmetic.

Course Description: We begin with two formal accounts of the intuitive notion of computability: recursive functions and Turing machines. They turn out to be the same, hence Church's Thesis: functions that can be computed by any means are precisely the partial recursive functions. Then we revisit the old Cretan who says that all Cretans always lie, and other forms of diagonalisation argument such as Halting Problem. Next we look at an axiomatic theory of arithmetic, known as Peano Arithmetic (PA), and show how we can represent all recursive functions in PA. This will lead to Goedel numbering: a neat trick enabling us to effectively encode notions like "theorem", "proof" and "provability in PA" within PA itself. We spend a while discussing Diagonalisation Lemma and Derivability Conditions. Finally, in one fell swoop we prove undecidability of first-order logic (Church's Theorem), undefinability of truth (Tarski's Theorem), incompleteness of PA given consistency of PA (First Goedel's Theorem) and unprovability of consistency of PA given consistency of PA (Second Goedel's Theorem).

Pre-requisites: Foundations of first-order logic

Background reading: G. Boolos and R. Jeffrey, Computability and Logic.

Lecturer: Michael Norrish is a Pricipal Researcher in the Canberra Laboratory of Data61 (CSIRO). He is originally from Wellington, New Zealand, and is very happy to be back in the southern hemisphere, after an extended stint in Cambridge, England. It was there that he did his PhD, and then spent three years as a research fellow at St. Catharine's College. His research interests include interactive theorem-proving, and the application of this technology to areas of theoretical computer science, particularly the semantics of programming languages.

Finite Model Theory

Contents: Finite model theory, inexpressibility proofs, descriptive complexity.

Course Description: Finite model theory studies the expressive power of logics on finite models. In this course we will first look into the differences between finite model theory and classical model theory. Then we will discuss expressibility of different logics over finite models, such as fixed point logics, logics with restricted number of variables, logics with counting, and techniques to prove inexpressibility results over finite models, i.e., Ehrenfeucht-Fraisse games. After that, we will go on to study descriptive complexity and discuss the applications of finite model theory in relational databases.

Prerequisites: Basic complexity theory and first order logic

Lecturer: Qing Wang is a Fellow and Senior Lecturer at the Australian National University's Research School of Computer Science. She completed her Ph.D. in Computer Science at Christian-Albrechts-University Kiel (Germany) in 2010. Before that, she received her Masters in Information Systems from Massey University (New Zealand) and Bachelor of Engineering from South China University of Technology (China). Her research interests are in database theory and application in relation to logic and formal methods.

Axiomatic Object Theory

Contents: Axioms and logical objects (truth values, classes); situations, possible and impossible worlds; concepts, counterparts and compossibility; forms, fictions and Fregean senses; Frege numbers, mathematical individuals and mathematical relations.

Course description: In this course, we present a Hilbert-style axiomatic (deductive) system ("object theory") and derive a body of theorems that have philosophical significance. The axioms are motivated and presented in the first lecture, and once they are in place, we define a variety of abstract objects and systematize them by deriving the their governing principles as theorems. For example, we define possible worlds and then derive that a proposition is necessarily true if and only if it is true at all possible worlds. Similar results are obtained for other abstract objects: truth-values, logical classes, situations, impossible worlds, concepts (including complete individual concepts), forms, fictions, Fregean senses, Fregean (natural) numbers, and theoretical mathematical individuals and relations generally. The course will prepare the intermediate student to read a variety of technical works in philosophy and, for those who request it, a reading list can be disseminated in advance. The lecturer will also help advanced students study a more technical work (

Lecturer: Edward N. Zalta is a Senior Research Scholar at the Center for the Study of Language and Information (CSLI). His research specialties include Metaphysics and Epistemology, Philosophy of Mathematics, Philosophical Logic/Philosophy of Logic, and Computational Metaphysics. He has published two books (1983, 1988) and papers in a wide variety of journals (including The Journal of Philosophy, Mind, Australasian Journal of Philosophy, Noûs, and the Journal of Philosophical Logic). For a list of publications, see here and for a full c.v., see here. Zalta is also the Principal Editor of the Stanford Encyclopedia of Philosophy.

An Introduction to Proof Theory

Contents: Basic sequent calculus, cut elimination; substructural logics; hypersequents.

Course description: This course provides an introduction to the methods of proof theory for sequent systems. We begin by introducing sequent systems for classical and intuitionistic logic and sketch a proof of one of the most important results in basic proof theory, the Cut Elimination Theorem, and explore some of its consequences. After this, we motivate dropping the structural rules of the basic sequent system to obtain substructural logics (relevant logic, linear logic, Lambek calculus), indicating what effects these modifications have on the proof of Cut Elimination as well as the distinctions they allow us to draw with respect to the logical connectives. We then motivate some generalisations of sequents to accommodate modal logics, in particular display logic, labelled sequents, and tree hypersequents. We will compare and contrast how these represent modal inference. Following this, we use hypersequents to explore the modal logic S5, as well as two-dimensional extension. We will close by showing how to define sequent and hypersequent systems for a range of substructural logics in a systematic and algorithmic way.

Prerequisites: It is assumed that students are familiar basic logical notation and concepts, as covered in “Fundamentals of Metalogic”. No prior background in proof theory is required. Prior exposure to Kripke models, as covered in “Introduction to modal logic” would be useful before the modal proof theory lectures, but is not required.

Lecturers: Shawn Standefer is a postdoctoral research fellow working with Greg Restall at The University of Melbourne on a handful of topics related to philosophical proof theory. He got his PhD from the University of Pittsburgh in 2013, with a dissertation on truth and paradox. After a couple of years teaching in the US, he moved to Australia for his postdoc. He’s enjoying being a part of the Australian logic community and is currently the organiser for the Melbourne Logic Seminar.

Agata Ciabattoni is a professor for nonclassical logics in computer science at the Faculty of Informatics of the Vienna University of Technology. In 2011 she has been awarded a START prize (the Austrian equivalent of the ERC starting grant) for her project Non classical proofs: Theory, Applications and Tools. She is working on theoretical aspects of nonclassical logics (proof theory and semantics), tools for their investigation, and applications.

More courses TBA

Updated:  8 November 2016 / Responsible Officer:  JavaScript must be enabled to display this email address. / Page Contact:  JavaScript must be enabled to display this email address. / Powered by: Snorkel 1.4