We introduce a realizability semantics based on interactive learning for full second-order Heyting arithmetic with excluded middle and Skolem axioms over Σ10-formulas. Realizers are written in a classical version of Girard's System $\mathsf{F}$ and can be viewed as programs that learn by interacting with the environment. We show that the realizers of any Π20-formula represent terminating learning processes whose outcomes are numerical witnesses for the existential quantifier of the formula.

Previous work has demonstrated that categories are useful and expressive models for databases. In the current paper we build on that model, showing that certain queries and constraints correspond to lifting problems, as found in modern approaches to algebraic topology. In our formulation, each SPARQL graph pattern query corresponds to a category-theoretic lifting problem, whereby the set of solutions to the query is precisely the set of lifts. We interpret constraints within the same formalism, and then investigate some basic properties of queries and constraints. In particular, to any database π, we can associate a certain derived database Qry(π) of queries on π. As an application, we explain how giving users access to certain parts of Qry(π), rather than direct access to π, improves the ability to manage the impact of schema evolution.

For any partial combinatory algebra (PCA for short) $\mathcal{A}$, the class of $\mathcal{A}$-representable partial functions from $\mathbb{N}$ to $\mathcal{A}$ quotiented by the filter of cofinite sets of $\mathbb{N}$ is a PCA such that the representable partial functions are exactly the limiting partial functions of $\mathcal{A}$-representable partial functions (Akama 2004). The n-times iteration of this construction results in a PCA that represents any n-iterated limiting partial recursive function, and the inductive limit of the PCAs over all n is a PCA that represents any arithmetical partial function. Kleene's realizability interpretation over the former PCA interprets the logical principles of double negation elimination for Σ0n-formulae, and over the latter PCA, it interprets Peano's arithmetic (PA for short). A hierarchy of logical systems between Heyting's arithmetic (HA for short) and PA is used to discuss the prenex normal form theorem, relativised independence-of-premise schemes, and the statement ‘PA is an unbounded extension of HA’.

In this paper we characterise the categories of Lawvere theories and equational theories that correspond to the categories of analytic and polynomial monads on Set, and hence also to the categories of the symmetric and rigid operads in Set. We show that the category of analytic monads is equivalent to the category of regular-linear theories. The category of polynomial monads is equivalent to the category of rigid theories, that is, regular-linear theories satisfying an additional global condition. This solves a problem posed by A. Carboni and P. T. Johnstone. The Lawvere theories corresponding to these monads are identified via some factorisation systems. We also show that the categories of analytic monads and finitary endofunctors on Set are monadic over the category of analytic functors. The corresponding monad for analytic monads distributes over the monad for finitary endofunctors and hence the category of (finitary) monads on Set is monadic over the category of analytic functors. This extends a result of M. Barr.

We show that the problem of whether a finite set of regular-linear axioms defines a rigid theory is undecidable.

Seely's paper Locally cartesian closed categories and type theory (Seely 1984) contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Bénabou–Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development, we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result, we prove that if we remove Π-types, the resulting categories with families with only Σ and extensional identity types are biequivalent to left exact categories.