- 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
- Logics of Vagueness and Indeterminacy Nick Smith
- Gödel’s Theorem Without Tears Dominik Kirst
- Proof Theory of Temporal Logic Bahareh Afshari
- Foundations for Type-Driven Probabilistic Modelling Ohad Kammar
- Complexity Theory of Interactive Proof Systems Thomas Haines
Fundamentals of Metalogic
Completeness theorems, Model theory, proof theory.
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.
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.
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
Computability; recursive Functions and Turing machines; diagonalisation; Peano arithmetic and Gödel numbering; undecidability of first-order logic; incompleteness of Peano arithmetic.
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).
Foundations of first-order logic
G. Boolos and R. Jeffrey, Computability and Logic.
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
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.
Knowledge about propositional logic, structural induction
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
Intuitionistic logic; Natural deduction; Curry-Howard isomorphism; Type theory; Lambda calculus
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.
Michael Norrish and Jim de Groot’s courses in week 1
- 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
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
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.
An introductory course on classical logic at first-year university level, or equivalent knowledge of classical logic gained by other means.
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
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.
John Slaney’s course of the first week will probably be more than enough
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
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
- 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
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
Interactive Proof Systems
Computational Complexity, Arithmetisation, Proof theory
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.
Some similarity with computability and complexity
Computational Complexity - A Conceptual Perspective, Oded Goldreich