2023 Program
Week 1
 Fundamentals of Metalogic, John Slaney
 Computability and Incompleteness, Michael Norrish
 Defining and Reasoning About Programming Languages, Fabian Muehlboeck
 Propositions and Types, Proofs and Programs Ranald Clouston
Week 2
 Logics of Vagueness and Indeterminacy Nick Smith
 Gödel’s Theorem Without Tears Dominik Kirst
 Proof Theory of Temporal Logic Bahareh Afshari
 Foundations for TypeDriven Probabilistic Modelling Ohad Kammar
 Complexity Theory of Interactive Proof Systems Thomas Haines
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.
Prerequisites
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 settheoretic 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 threeyear 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 nonclassical logics, automated deduction and all sorts of logicbased AI. He was formerly the leader of the Logic and Computation group at the ANU, and of the NICTA program of the same name.
Computability and Incompleteness
(Michael Norrish)
Keywords
Computability; recursive Functions and Turing machines; diagonalisation; Peano arithmetic and Gödel numbering; undecidability of firstorder logic; incompleteness of Peano arithmetic.
Abstract
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 firstorder 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).
Prerequisites
Foundations of firstorder logic
Background reading
G. Boolos and R. Jeffrey, Computability and Logic.
Lecturer
Michael Norrish is an Associate Professor at the Australian National University. Before joining the ANU, he worked for 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 theoremproving, and the application of this technology to areas of theoretical computer science, particularly the semantics of programming languages.
Defining and Reasoning About Programming Languages
(Fabian Muehlboeck)
Keywords
Abstract
This course is about fundamental techniques to define (abstract) programming languages and their semantics. In particular, we will explore the smallstep operational semantics of lambda calculus and some of its extensions, and typesystems for the same. We will also prove some standard properties, in particular type safety.
Prerequisites
Knowledge about propositional logic, structural induction
Bio
Fabian Muehlboeck is a Lecturer at the School of Computing of the Australian National University. He obtained his PhD from Cornell University, an MS from Northeastern University (as a Fulbright exchange student), and a BSc from TU Wien. Before joining ANU, Fabian was a Postdoc at the Institute of Science and Technology Austria (ISTA). His research focuses on programming language design, in particular for industrial objectoriented languages.
Propositions and Types, Proofs and Programs
(Ranald Clouston)
Keywords
Intuitionistic logic; Natural deduction; CurryHoward isomorphism; Type theory; Lambda calculus
Abstract
Intuitionism is an approach to logic that began with some renegade ideas in the philosophy of mathematics, but has since been enthusiastically adopted by computer scientists. We begin with an introduction to intuitionistic propositional logic and show that we can reason with it in a structured way via ‘natural deduction’. We briefly discuss the relationship between natural deduction and sequent calculus. We then unveil the CurryHoward isomorphism, also known as propositionsastypes, which makes a surprising connection between logic and the simply typed lambda calculus, a functional programming language. We discuss some of the major features of this programming language / proof system, such as subject reduction, strong normalisation, and the subformula property. We see how the CurryHoward isomorphism can be pushed further into more powerful logics and programming language features, such as arithmetic, polymorphism, and dependent types.
Prerequisites
Michael Norrish and Jim de Groot’s courses in week 1
Background reading
 Phillip Wadler, ‘Propositions as Types’ https://dl.acm.org/doi/10.1145/2699407;
 JeanYves Girard, ‘Proofs and Types’ https://www.paultaylor.eu/stable/Proofs+Types
Lecturer
Ranald Clouston attended the ANU Summer School as a student back in 2003 while studying at Victoria University of Wellington in New Zealand. Since then he has completed his PhD at the University of Cambridge and worked at Aarhus University and Australian National University, his current home. He researches in the areas of type theory and proof theory, which are to some extent the same thing, with occasional splashes of category theory.
Logics of Vagueness and Indeterminacy
(Nick Smith)
Keywords
Abstract
We’ll explore logics that have been introduced to model vagueness in natural language, and other sources of indeterminacy or ‘unsettledness’ such as nonterminating computations and the view that the future is ‘open’ (in some sense stronger than that we merely don’t yet know what will happen). We’ll look at logics with truthvalue gaps, manyvalued logics – including threevalued and fuzzy logics – and supervaluationist and subvaluationist logics.
Prerequisites
An introductory course on classical logic at firstyear university level, or equivalent knowledge of classical logic gained by other means.
Bio
Nick Smith (there are quite a few in philosophy so for publication purposes he goes by Nicholas J.J. Smith) studied philosophy and logic as an undergraduate at the University of Sydney and as a graduate student at Princeton University where he was awarded a PhD in 2001. He worked in the philosophy department at Victoria University of Wellington from 2001 to 2004 before returning to the University of Sydney in 2005, where he is now Professor of Philosophy. He is the author of Vagueness and Degrees of Truth (Oxford University Press 2008) and Logic: The Laws of Truth (Princeton University Press 2012).
Gödel’s Theorem Without Tears
(Dominik Kirst)
Abstract
In this course, we will revisit Gödel’s first incompleteness theorem from the perspective of synthetic computability theory. This perspective exploits that in a constructive foundation one can freely assume that every function is computable, which nearly trivialises formally working out the computational essence underlying the Turing/Kleene/Post argument for incompleteness via undecidability. We first explore various synthetic incompleteness proofs of ascending strength for a very abstract concept of formal systems and then describe an instantiation to the concrete case of firstorder Robinson arithmetic. To illustrate all that these proofs are feasible even for mechanisation with a proof assistant, the lectures are interleaved with a tour through an accompanying Coq development.
Prerequisites
John Slaney’s course of the first week will probably be more than enough
Background reading
The title is a confluence of Fred Richman’s “Church’s thesis without tears” as well as Peter Smith’s “Gödel without (too many) tears” and the course will be based on a paper of the same title I wrote together with Benjamin Peters. Additional reading could be:
Bauer, Andrej. “First steps in synthetic computability theory.” Electronic Notes in Theoretical Computer Science 155 (2006): 531.
Beklemishev, Lev D. “Gödel incompleteness theorems and the limits of their applicability. I.” Russian Mathematical Surveys 65.5 (2010): 857.
Proof Theory of Temporal Logic
(Bahareh Afshari)
Abstract
Temporal logic describes a range of modal logics in which modal and ‘fixed point’ operators are interpreted as temporal relations. As such they are of significance in the theory of computation wherein specification and verification of statebased system is a central theme. Understanding and manipulating proofs for these logics can facilitate in establishing computational properties such as decidability and interpolation.
Formal proofs come in many styles each equipped with their own toolkit. In this course we will look at some of the standard proof systems for temporal logic and develop an appreciation for the pros and cons of the different formalisms. Main temporal logics covered in the course are LTL, CTL, PDL and Modal muCalculus. In the second half of the course further advanced topics will be discussed including (but not limited to) infinitary and cyclic proofs.
Recommended prior knowledge

basic knowledge of propositional and predicate logic

familiarity with modal logic
Reference book
 S. Demri, V. Goranko, and M. Lange. Temporal Logics in Computer Science: FiniteState Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.
Foundations for TypeDriven Probabilistic Modelling
(Ohad Kammar)
Abstract
The last few years have seen several breakthroughs in the semantic foundations of probabilistic and statistical modelling. In this course, we will use types to introduce, use, and organise abstractions for probabilistic modelling. We will do so first for discrete probability, and then more generally with the recentlydeveloped quasiBorel spaces. The course is accompanied by exercises, allowing you to develop a working knowledge and handson experience during the summer school and after it.
Details and further reading
https://denotational.co.uk/tdpmanulss2023/
Interactive Proof Systems
(Thomas Haines)
Keywords
Computational Complexity, Arithmetisation, Proof theory
Abstract
The aim of this course will be to explain the famous result IP = PSPACE. That is, any problem which can be solved in a polynomial bounded amount of space has an efficient interactive proof. To this end we will first recap the complexity classes P and NP before introducing interactive proofs systems. We will show that both Graph Isomorphism and NonIsomorphism are in IP before proceeding to our main result.
Prerequisties
Some similarity with computability and complexity
Background reading
Computational Complexity  A Conceptual Perspective, Oded Goldreich