ABSTRACT. When Avicenna (11th century Persia) wanted to set up modal logic rigorously, he had available to him a rich but confused body of material from Aristotle and the Aristotelian commentators. Avicenna rearranged and sifted this material into two related formal systems, which we can call Mod and Temp. Mod is a fragment of monadic predicate modal logic; apart from a couple of mishaps on the edges it is a robust system up to modern standards. Temp is equally robust but more mysterious. Mathematically it can be correctly described as an S5 Kripke semantics for Mod, with fixed universe and an existence predicate; Avicenna several times uses Temp to give what in this sense are 'semantic proofs' of inferences in Mod. But Avicenna himself couldn't have described Temp that way, and though everything is formally correct, we have little idea how he justified its use to himself.

ABSTRACT. Late in his career Avicenna (11th c. Persia) made a fresh approach to propositional logic, basing it on his temporal logic. This has to be seen as work in progress - there are awkwardnesses and some outright mistakes. But overall it comes remarkably close to Boole (19th c.).

ABSTRACT. A.N. Prior (1914-69) was the founder of modern temporal logic. In the 1950s and 1960s he showed that tense-logic can be used in order to keep track of the past and of the future possibilities in a way which makes it possible to reason systematically on temporal matters.

From the early 1930s Prior had been an active member of the Presbyterian community in New Zealand. He became a specialist in the debates regarding the logical tension between the doctrine of divine foreknowledge and the doctrine of human freedom. He demonstrated how this logical problem can be formalized and analysed in terms of his tense-logic. He found great inspiration in the works of Aristotle, Diodorus, Thomas Aquinas, William of Ockham, C.S. Peirce, Jan Łukasiewicz, Saul Kripke and several others. He argued that in the discussion concerning divine foreknowledge and human freedom there are just a few reasonable positions. – In general Prior demonstrated that temporal logic can be used to analyze the notion of time itself as well as fundamental existential problems, such as the problem of determinism versus freedom of choice.

ABSTRACT. A shorthand notebook of Gödel's from late 1935 shows that he read Gentzen's original, unpublished consistency proof for arithmetic. By 1941, many such notebooks were filled with various formulations of the result, one with explicit use of choice sequences, and a generalization based on an induction principle for functionals of finite type over Baire space. Gödel's main aim was to extend Gentzen's result into a consistency proof for analysis. In the lecture, an overview of these so far unknown results about consistency proofs for arithmetic will be presented.

ABSTRACT. The notion of sheaf models (which can be traced back to the works of Beth and Kripke) is an important tool for the metamathematical analysis of higher-order logic. The problem of generalising such an interpretation for universes of dependent type theory is complex, and it was precisely for this reason that the notion of stack was introduced in the context of algebraic geometry. I will present a way to adapt such a notion for models of univalent type theory, i.e. type theory extended with the univalence axiom and propositional truncation. Some applications are that such type theory is compatible with Brouwer’s fan theorem, and that countable choice is independent.

ABSTRACT. A basic tenet of Martin--L\"of type theory is that types are inductively generated by their elements. This idea finds clearest expression in the W-types and the more general tree types; categorically, these admit characterisation as initial algebras for certain polynomial endofunctors of the category of types over a given context. The calculus of polynomial endofunctors is interesting in its own right, with application in combinatorics, algebraic topology and computer science; a key organising principle is that polynomial functors between the slices of a locally cartesian closed category form into a bicategory whose composition is given by substitution of multivariate polynomials.

The notion of bicategory also crops up in a very deep observation of Walters: namely, that the theory of categories enriched over a monoidal category admits generalisation to a theory of categories enriched over a bicategory. This is closely bound up with what is sometimes called indexed or variable category theory, that is, category theory relative to a base category that acts as a surrogate for the category of sets. In this talk, we consider the natural question: what are categories enriched over the bicategory of polynomials? The answer turns out to be quite interesting: they encode notions of Lawvere theory and PROP appropriate to the indexed setting.

ABSTRACT. Some of the different proposals for how to make precise Gentzen’s way of justifying the introduction and elimination rules of natural deduction are briefly surveyed. A crucial question is whether the justification is applicable only to inferences occurring in intuitionistic logic or can be extended also to inferences occurring in classical logic. I shall argue that it is extendible to classical inference rules but that for some logical constants the introduction rules must vary depending on whether the constant is read classically or intuitionistically – when the constant is read classically the rule must be weaker than when it is read intuitionistically.

Respecting this condition, it is possible to allow classical and intuitionistic logical constants in one and the same system, a system that we may call the ecumenical system. In this system the usual elimination rules for some logical constants do not hold when the constant is read classically. Modus ponens is an example – it is not valid generally when implication is read classically, but remains valid when also all of the constants of the subformulas of the implication are read classically.