2024 Program
Week 1
- Fundamentals of Metalogic by John Slaney
- Computability and Incompleteness by Michael Norrish
- Formalizing and Reasoning About Programming Languages by Fabian Muehlboeck
- Propositions and Types, Proofs and Programs by Ranald Clouston
Week 2
- Interpolation through the Lens of Proof Theory by Iris van der Giessen
- Verification via Temporal Logic: an Introduction by Mark Reynolds
- Qualitative Calculi via Relation Algebras by Tomasz Kowalski
- Automatic Structures and their Logical theory by Sophie Pinchinat
- Applying Logic in Software and Inefficient Computation by Thomas Sewell
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.
Formalizing and Reasoning About Programming Languages
(Fabian Muehlboeck)
Abstract
Formal programming language semantics allow us to reason about programs and their properties. Here, we explore the common technique of small-step structural operation semantics. We start with basic lambda calculus, contrast it with its simply-typed version, and discuss proofs of type-safety and possibly normalization. We then explore a few standard extensions, such as tagged sums, pairs, and records, and ultimately introduce basic parametric polymorphism.
Pre-requisites
Knowledge about propositional logic, structural induction
Lecturer
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 see how the Curry-Howard isomorphism can be pushed further into more powerful logics and programming language features, such as dependent types.
Pre-requisites
John Slaney and Fabian Muehlboeck’s week 1 courses
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.
Interpolation through the Lens of Proof Theory
(Iris van der Giessen)
Abstract
Craig interpolation is a fundamental concept in mathematical logic and computer science. Craig interpolants are formulas in a specified vocabulary that, intuitively speaking, explain why one formula entails the other. The existence of Craig interpolants is a useful property serving in many applications in database theory, knowledge representation, proof complexity, and more. For example, interpolants are used to enlarge knowledge bases by learning new concepts and the feasible extraction of interpolants from proofs relates to the NP vs co-NP problem. The goal of the course is to introduce theory and practice of interpolation through the lens of proof theory. Proof-theoretic techniques allow to explicitly construct interpolants which is useful in computations. We will discuss methods based on different systems such as sequent calculi and refutation systems. We will touch upon different version of Craig interpolation, such as Lyndon interpolation and uniform interpolation. We illustrate the applications of such methods in different fields including knowledge representation, formalized proofs, and proof complexity.
Verification via Temporal Logic: an Introduction
(Mark Reynolds)
Abstract
In this series of five lectures we have a look at how temporal logic has been used in formal verification of the behaviour of systems. We introduce some simple propositional temporal logics, linear time LTL and branching time CTL, and consider algorithms for determining satisfiability and model checking. If time permits we will have a quick look at some extensions.
Qualitative Calculi via Relation Algebras
(Tomasz Kowalski)
Abstract
Intuitive human reasoning makes heavy use of binary relations: the chair is behind the table, the cat is on the mat, summer school happens during December, Canberra is southwest of Sydney. Binary relations can be composed: if the cat is on the mat and the mat is in the room, then the cat is in the room. And converted: Sydney is northeast of Canberra. Obviously, unions, intersections, and complements of binary relations are also binary relations.
The idea of a qualitative calculus for some domain is to take typical binary relations over that domain, close them under unions, intersections, complements, composition and converse and see what happens. What happens typically is a relation algebra in the sense of Tarski. But sometimes it is more natural to tweak the operations a little, and then it may be a non-associative relation algebra in the sense of Maddux, or something even more general.
The course will focus on algebraic foundations of qualitative calculi. We will cover: (a) Non-associative relation algebras and their qualitative representations, (b) advantages of qualitative representations over classical Tarskian representations, (c) games for representability, (d) computability and complexity questions, (e) examples, open questions, and other loose ends.
Automatic Structures and their Logical theory
(Sophie Pinchinat)
Abstract
Model checking operational models of dynamic systems against logical statements is understood as a powerful formal method to conduct accurate analysis of their functional properties. Most results in the literature concern finite models and rather focus on the trade-off between the expressiveness of statements and complexity issues to make this method effective in practice. This finiteness assumption on input models to model checkers requires mathematical prowess to reach a finite abstraction of the actual behavior of the system before its analysis. Needless to say that the resulting abstraction may misrepresent important features that matter in the verification process. Therefore, in most cases the abstraction mechanism often relies on the very nature of the property to be analyzed, and need being revisited and proved correct each time a new statement is considered.
It is therefore of utter importance to seek approaches allowing a relaxation of this finiteness assumption, while maintaining effective methods, or at least decidability of the model checking problem.
This course demonstrates the power of automata theory to handle infinite-state system model checking against statement expressed in first-order logic, a well-understood setting based on Automatic Structures, but also much more recent results that allow for verifying properties beyond first-order-definable ones.
If time left, we illustrate an application of this remarkable setting to reason about epistemic information dynamics.
Recommended prior knowledge
Basic knowledge of propositional and first-order logic familiarity with formal language theory and finite-state automata
Relevant literature
Sasha Rubin: Automatic structures. Handbook of Automata Theory (II.) 2021: 1031-1070
Gaëtan Douéneau-Tabot, Sophie Pinchinat, François Schwarzentruber: Chain-Monadic Second Order Logic over Regular Automatic Trees and Epistemic Planning Synthesis. Advances in Modal Logic 2018: 237-256
Applying Logic in Software and Inefficient Computation
(Thomas Sewell)
Keywords
theorem proving, computation, reflection
Abstract
The summer school offers the opportunity to study various formal logics, logics whose deduction mechanisms are explicitly encoded as operations in a formal structure. These structures nearly always have program-like characteristics. This course will look at tools which encode those structures in software, specifically various theorem provers. We will look at the overall design and implementation of such tools and give an introductory tutorial/workshop on using one. We will discuss proof by reflection, a mechanism by which a formal logic (e.g. one in a theorem prover) can recurse to another as part of a proof. Finally, we will look at a common frustration situation, where a reasonable approach to a proving some statement results in a valid proof but an inefficient computation. We will look over some cases where this situation arises, some being interesting anecdotes from past projects, and others being useful examples for teaching prover features.
Pre-requisites
Standard mathematical logic. Knowledge of a formal logic, e.g. from any of the first week courses. For those who have seen or used a theorem prover before, more advanced exercises may be provided.
Bio
Thomas is a lecturer in Computer Science at the University of NSW. He has a long history in applied formal methods, working on verified software projects such as the seL4 microkernel and the CakeML compiler.