2026 Program

Week 1

Week 2


Fundamentals of Metalogic
(John Slaney)

Keywords

Completeness theorems, Model theory, proof theory.

Abstract

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 Interactive Theorem-Proving with Isabelle
(Liam O’Connor)

Abstract

This course will introduce the use of interactive proof assistants both for mathematics and for work in software verification. We will introduce the basics of interactive theorem proving using the proof assistant Isabelle/HOL. Starting from elementary logical formulae, we will prove many theorems “live” in lectures, and apply what we have learned to proof exercises and challenges. Proof assistants can be both very fun and very addictive in equal measure. It is my hope to share that fun with you :)

Topic list (tentative):

  1. Propositional and first-order logic, natural deduction proofs. Types, definitions, unfolding.
  2. Structural induction, inductive definitions, induction tactics.
  3. Simplifier, rewriting, function definitions, other definitions.
  4. Structured proofs in Isar, calculational proofs. More automatic methods, sledgehammer.

Remaining topics to be covered if there is time:

  • General recursion and termination measures
  • Type classes and locales
  • Program verification with SIMPL or AutoCorres
  • Designing tactics with Eisbach

Student Participation

Please install Isabelle from here before the first lecture.

Isabelle comes as a bundle with everything needed for the three main platforms (Windows, Linux, Mac), including Isabelle/jEdit which can be launched easily from the bundle. If students have trouble installing it, contact Liam O’Connor, liam.oconnor@anu.edu.au.

Prerequisites

Some familiarity with simple first order and propositional logic is assumed. Some functional programming experience (in particular, some familiarity with lambda calculus or a language like Haskell) is also recommended.

Recommended further reading

Concrete Semantics, Tobias Nipkow and Gerwin Klein

Lecturer Liam O’Connor is a Senior Lecturer at the Australian National University and an Honorary Fellow at the University of Edinburgh, where he worked until 2024. He obtained his PhD from UNSW in 2019, the dissertation for which received the John Makepeace Bennett award. He has broad interests in theoretical computer science, especially in semantics, models and specifications, as well as in the application of these theoretical techniques to practical problems in programming languages, systems and software engineering.

Topic TBA
(Ranald Clouston)

Topic TBA
(Peter Höfner)

Topic TBA
(Amal Ahmed)

Infinite Ramsey Theory and Logic
(Natasha Dobrinen)

Abstract

Natasha Dobrinen is a professor in the Mathematics Department at the University of Notre Dame. She is a set theorist whose work involves combinatorics, topology, and computability theory. Her development of new techniques to solve a longstanding open problem on Ramsey theory of the triangle-free Henson graph gave impetus to the current flourishing of the field of Big Ramsey Degrees and led to an invited address at the 2022 ICM. She is currently president of the Association for Symbolic Logic, a Coordinating Editor for the Annals of Pure and Applied Logic, and an Editor for the Notre Dame Journal of Formal Logic and the mathematics journal Order. Born and raised in San Francisco, she earned a bachelors from UC Berkeley in 1996 and a PhD from the University of Minnesota in 2001. She held postdocs at Penn State and at the KGRC in Vienna, and has spent cumulatively around a decade in various places in Europe.

Prerequisites

Countable ordinals, transfinite induction on countable ordinals, Axiom of Choice (to be delivered in Ranald Clouston’s week one lectures).

Lecturer

Ramsey’s Theorem was originally proved to solve a problem of formal logic, and in fact, he proved the infinite version first and then deduced the finite version from it. Ramsey’s Theorem for pairs states that given any coloring of pairs of natural numbers into finitely many colors, there is an infinite set of natural numbers in which all pairs have the same color.

The aims of this course are to (1) Prove Ramsey’s Theorem, (2) Extend Ramsey’s Theorem to other countable linear orders such as the integers and the rationals, (3) Introduce Ramsey theory where infinite subsets of the natural numbers are colored. Topic (2) covers what is called ``big Ramsey degrees” and will include connections with some Ramsey theorems on trees and a question regarding the strength of the Axiom of Choice. Topic (3) will include how the Axiom of Choice creates a barrier to direct analogues of Ramsey’s Theorem for colorings of infinite sets, and the work-around using Borel sets. I will include some informal discussions of the method of forcing, and if time permits, we will give a proof of the Galvin-Prikry Theorem using combinatorial forcing.

Algorithmic Information Theory
(Rod Downey)

Abstract

Given a binary string σ how much information does it contain? How much can it be compressed? For infinite sequences, why do we think that 0101010101 . . . does not look random whereas others do, although both have the same probability of occurring, namely 0? How should we formalize such questions?

There is a deep and interesting of algorithmic information theory or algorithmic randomness where a notion of absolute randomness is abandoned and replaced by one which uses the theores of computation and of computational complexity to calibrate or quantify randomness. This leads to notions of randomness of individual strings and reals.

Questions include: What kinds of computational power does having access to random sources give us? What complexity is needed to construct an algorithmicially random source? Can I use a notion of randomness for individual objects to prove classical theorems in mathematics or computer science?

This course will deal with the basics of this theory. Some background reading might include delving into [LV93, Nie09, DH10, Dow08, DH19] or articles from my homepage.

References

[DH10] Rodney Downey and Denis Hirschfeldt. Algorithmic randomness and complexity. Theory and Applications of Computability. Springer, New York, 2010. [DH19] R. Downey and D. Hirschfeldt. Computability and randomness. Notices of the American Mathematical Society, 66(7):1001–1012, 2019. [Dow08] R. Downey. Five lectures on algorithmic randomness. In C. Chong, Q. Feng, T. Slaman, W. Woodin, and Y. Yang, editors, Computational Prospects of Infinity, Part I: Tutorials, pages 3–82. World Scientific, 2008. [LV93] Ming Li and Paul Vitanyi. An introduction to Kolmogorov Complexity and its Applications. Texts and Monographs in Computer Science. Springer-Verlag, 1993. [Nie09] André Nies. Computability and Randomness, volume 51 of Oxford Logic Guides. Oxford University Press, Oxford, 2009.

Lecturer

Professor Rod Downey is a very well-known mathematician and theoretical computer scientist. He works in classical and applied computability theory and in complexity theory (mainly parameterized complexity), reverse mathematics and algorithmic information theory. Professor Downey is not only “world famous in New Zealand” (as a local saying goes in this country), but one of New Zealand’s best known mathematicians. He has won numerous awards for his work in logic and his work in theoretical computer science. These include the inaugural MacLaurin Fellowship, the Hamilton Prize of the RSNZ, NZ Association of Scientists Research Medal, the NZMS Research Award, and the Vice Chancellor’s Award for Research. He was elected a fellow of both the RSNZ and the NZMS. He is an editor of numerous journals, and chaired the prizes committee of the Association for Symbolic Logic. He gave an invited lecture at the International Congress of Mathematicians (2006), and has given invited addresses an numerous conferences including the International Congress of Logic Methodology and Philosophy of Science, and the IEEE Conference on Computational Complexity. He is also an accomplished surfer and Scottish Country dancer.

(Bio from Cris Calude, EATCS Bulletin)

Proofs as Part of Programming
(K. Rustan M. Leino)

Abstract

These lectures show how specifications and proofs can be a natural part of programming. The main goal is to teach how to write and verify programs in a practical setting. Using the Dafny programming language, we will start with the basics of pre- and postconditions and invariants. As programs become more involved, we will need abstraction and proofs. I will show various styles of proofs. Going beyond executable programs, we will also see how the same proof setting extends to the formalization of models of systems.

Lecturer

K. Rustan M. Leino is known for his work on programming languages and programming methods and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award.

Leino is a research engineer at Harmonic. Previously, he has been Senior Principal Applied Scientist at Amazon Web Services, co-instructor at MIT, Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher at DEC/Compaq Systems Research Center (SRC). He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft.

Leino hosts the Verification Corner channel on youtube. He is a multi-instrumentalist, he instructed group cardio and strength classes for many years, and he likes to cook.

Proof Theory of Modal and Non-Classical Logics: the Method of Labelled Sequent Calculi
(Sara Negri)

Keywords

Proof theory; labelled sequent calculi; modal logic; intuitionistic logic; non-classical logics; Kripke and neighbourhood semantics; cut elimination; proof search, correspondence theory.

Abstract

The course introduces the proof-theoretic method of labelled sequent calculi, a uniform framework for developing analytic proof systems for modal and non-classical logics. We begin by examining the relationship between semantics and proof theory, showing how Kripke semantics can be internalized into sequent calculi by means of labels representing possible worlds and accessibility relations.

We then construct labelled calculi for the basic modal logic K and explain how semantic frame conditions can be systematically transformed into inference rules, yielding cut-free systems with strong structural properties. This methodology extends naturally to intuitionistic, intermediate, and other non-classical logics, providing a modular approach to proof search, countermodel construction, and completeness proofs.

Finally, we discuss recent developments that go beyond geometric frame conditions, including applications to epistemic, provability, and non-normal modal logics. Throughout the course, we emphasize how labelled calculi provide a common proof-theoretic language for studying analyticity, correspondence, decidability, and automated reasoning across a broad range of logical systems.

Pre-requisites

Foundations of propositional and first-order logic. Prior knowledge of modal logic or proof theory is helpful but not required.

Lecturer

Sara Negri is Professor of Mathematical Logic at the University of Genoa and is internationally recognised for her contributions to proof theory, particularly in modal and non-classical logics. She is the author of the two monographs “Structural Proof Theory” and “Proof Analysis: A Contribution to Hilbert’s Last Problem” (both with Jan von Plato).

Before her current appointment, she served from 2015 as Professor of Theoretical Philosophy at the University of Helsinki and held research positions at the Academy of Finland and the Helsinki Collegium for Advanced Studies. Her visiting and postdoctoral appointments include the University of Amsterdam, Imperial College London, the Mittag-Leffler Institute in Stockholm, the University of Munich, the Hausdorff Research Institute for Mathematics in Bonn, the Scuola Normale Superiore in Pisa, and the University of Verona. She is a member of the Academia Europaea.

bars magnifying-glass xmark