2023 Program
Week 1
- Fundamentals of Metalogic by John Slaney
- Computability and Incompleteness by Michael Norrish
- Modal Logic by Jim de Groot
- Propositions and Types, Proofs and Programs by Ranald Clouston
Week 2
- Logics of Vagueness and Indeterminacy by Nick Smith
- Gödel’s Theorem Without Tears by Dominik Kirst
- Proof Theory of Temporal Logic by Bahareh Afshari
- Foundations for Type-Driven Probabilistic Modelling by Ohad Kammar
- Complexity Theory of Interactive Proof Systems by 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.
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.
Slides
Modal Logic
(Jim de Groot)
Keywords
Normal modal logic, possible-world semantics, bisimulations, Hennessy-Milner theorem, Van Benthem characterisation theorem.
Abstract
Modal logic lies in between propositional logic and first order logic. It is widely used in mathematics, philosophy and computer science. On the one hand it can be used to reason about more complex statements concerning necessity, knowledge and obligation, while on the other hand it is simple enough to still be decidable.
The goal of this course is to explore modal logic, and to characterise the precise relation between modal logic and first-order logic. We do so by taking a semantic point of view, interpreting formulae in so-called possible world semantics. We then introduce bisimulations, which can be used to identify worlds in which precisely the same formulae are true. Ultimately we prove the Van Benthem characterisation theorem, which (intuitively) states that modal logic is the bisimulation-invariant fragment of first-order logic.
Pre-requisites
Mathematical maturity and some familiarity with propositional and first-order logic.
Background reading
I’ll use parts of Modal Logic by Blackburn, de Rijke and Venema. Precise references to the book are given in the slides.
Lecturer
My name is Jim and I’ll be telling you about modal logic in the summer school. I was born and raised in Amsterdam, and studied mathematics there. I obtained my PhD in mathematical logic here at the ANU, and I’m now working here as a postdoc. In my spare time I like to go hiking and camping in the beautiful national parks surrounding Canberra.
Slides
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
- Jean-Yves Girard, Proofs and 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.
Slides
- Part 1: Intuitionistic Logic
- Part 2: Natural Deduction
- Part 3: Lambda Calculus
- Part 4: Curry-Howard
- Part 5: Extensions
- NoLargestNumber.lean
Logics of Vagueness and Indeterminacy
(Nick Smith)
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.
Lecturer
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).
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.
Slides
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/
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.
Slides
Complexity Theory of 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
Oded Goldreich, Computational Complexity – A Conceptual Perspective
Slides