2023 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.

Computability and Incompleteness
(Michael Norrish)

Keywords

Computability; recursive Functions and Turing machines; diagonalisation; Peano arithmetic and Gödel numbering; undecidability of first-order 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 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 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 theorem-proving, 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 small-step operational semantics of lambda calculus and some of its extensions, and type-systems 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 object-oriented languages.

Propositions and Types, Proofs and Programs
(Ranald Clouston)

Keywords

Intuitionistic logic; Natural deduction; Curry-Howard 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 Curry-Howard isomorphism, also known as propositions-as-types, 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 sub-formula property. We see how the Curry-Howard isomorphism can be pushed further into more powerful logics and programming language features, such as arithmetic, polymorphism, and dependent types.

Pre-requisites

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;
  • Jean-Yves 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 non-terminating 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 truth-value gaps, many-valued logics – including three-valued and fuzzy logics – and supervaluationist and subvaluationist logics.

Prerequisites

An introductory course on classical logic at first-year 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 first-order 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): 5-31.

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 state-based 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 mu-Calculus. 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: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.

Foundations for Type-Driven 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 recently-developed quasi-Borel spaces. The course is accompanied by exercises, allowing you to develop a working knowledge and hands-on experience during the summer school and after it.

Details and further reading

https://denotational.co.uk/tdpm-anu-lss-2023/

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 Non-Isomorphism are in IP before proceeding to our main result.

Pre-requisties

Some similarity with computability and complexity

Background reading

Computational Complexity - A Conceptual Perspective, Oded Goldreich

bars search times arrow-up