This work is based on a joint paper with Guillaume Geoffroy. We discuss the problem of the Axiom of Choice in realizability and we present a technique for realizing fragments of Zorn’s lemma (which is one of the many versions of the Axiom of Choice).

In this talk I would like to present recent results about the admissible rules in some intuitionistic modal logics. The admissible rules are those rules under which the set of theorems of the logic is closed. Thereby giving insight in the structure of all possible inferences in a logic. We will consider intuitionistic modal logics containing the completeness axiom. We provide proof systems describing their admissible rules.

We introduce a concrete domain model for the quantum lambda calculus and lambda-rho extended with a fixpoint operator. A distinctive feature of lambda-rho is that it relies on density matrices for describing both quantum information and probabilistic distributions over computation states. It has been shown that there is a conservative translation from lambda-rho to the quantum lambda calculus of Selinger and Valiron. In contrast to existing models for quantum lambda calculi featuring recursion with intuitionistic arrows, our model is finite-dimensional and does not need more than cones of positive matrices and affine arrows.

It is a well known fact that the intuitionistic logic enjoys the disjunction property (DP), i.e., if A \vee B is provable then either A is provable or B is provable. Buss and Mints and later Buss and Pudlak studied the computational complexity of the disjunction property in intuitionistic logic and proved that it is "feasible". A proof system (for instance a Gentzen-style, natural deduction, or Hilbert-style system) P for a logic is said to have feasible DP if there is a polynomial time algorithm that given a proof of the formula A \vee B in P, it outputs either a proof of A or a proof of B in P. Later, Ferrari et.al. studied the same problem and provided a framework to prove the feasibility of DP for proof systems for intuitionistic logic and some intermediate and intuitionistic modal logics.

In this talk, we present a uniform method to prove feasible DP for various intuitionistic modal logics. More specifically, we prove that if the rules in a sequent calculus for an intuitionistic modal logic have a special form, then the sequent calculus enjoys feasible DP. Our method is essentially an adaptation of the method used by Hrubes in his lower bound proof for the intuitionistic Frege system. As a consequence, we uniformly prove that the sequent calculi for intuitionistic logic, the intuitionistic version of several modal logics including K, T, K4, S4, S5, their Fisher-Servi versions, propositional lax logic, and many others have feasible DP. Our method also provides a way to prove negative results: we show that any intermediate modal logic without DP does not have a calculus of the given form. This talk is based on a joint work with Amir Tabatabi.

We study the logical strength of some well-known combinatorial consequences of Ramsey’s theorem for pairs and two colours of the form ‘for every infinite set X there exists an infinite set Y such that P(X,Y)’, where P(X,Y) is some property expressible in the language of first-order arithmetic. We work over a weak base theory assuming mathematical induction only for computable properties. Such modest assumptions allow for a finer analysis of the principles in question but at the same time cause the notion of an infinite subset of the natural numbers to split into two inequivalent versions.

This leads us to consider two variants of our principles, ‘normal’ and ‘long’, depending on ‘how infinite’ we require the witnessing set Y to be. We show that the normal versions, based on a weaker notion of infinity, are partially conservative over the base theory and in particular they do not prove totality of any nonelementary computable function. As for the long versions, we show that they tend to behave in one of two ways: they either imply mathematical induction for computably enumerable properties or are equivalent to their normal counterparts.

Unification, matching, and generalization problems play an important role in various areas of mathematics, computer science, and artificial intelligence. Unification and matching are central computational mechanisms in automated reasoning, rewriting, and declarative programming. Generalization is closely related to detecting similarities between different objects and to learning general structures from concrete instances. Anti-unification is a logic-based method for computing generalizations, with a wide range of applications.

We work with languages where imprecise information is represented by proximity relations. They are fuzzy counterparts of tolerance (reflexive, symmetric, but not necessarily transitive) relations and generalize similarity relations (fuzzy equivalences). We propose unification, matching and anti-unification algorithms in such languages whose signatures tolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizes on the one hand, proximity-based symbolic techniques to full fuzzy signatures, and on the other hand, similarity-based techniques over a full fuzzy signature by extending similarity to proximity.

Provability games are a kind of logical games played over a formula to check its validity. We present a type of provability game called Mazhirov's game, originally introduced by I. Mezhirov for intuitionistic propositional logic and Grzegorczyk modal logic. We extend this approach to characterise validity in other logics. In the present paper, we first introduce a game for classical propositional logic and then show how it can be extended to the modal logic of function frames. In the talk, we also want to discuss some limitations and prospects of using Mezhirov's games.

Connectivity is one of several properties that cannot be expressed in first-order logic (FO). We introduce a new logic, called FO+Conn, that has atomic operators Conn_k that can express connectivity in undirected graphs when up to k vertices (that we can quantify) have been deleted. We study the expressive power of the new logic and the complexity of its model-checking problem.

In this talk, I will introduce my current book project, "Women in the History of Logic", and raise and discuss three important methodological questions:

1. What gets to count as "logic" when writing such a history?

2. Who gets to count as a "logician" when writing such a history?

3. Why does it matter who our logical foremothers are?

I will focus on the final question, by showing how understanding the role of women in the history of logic is not (merely) a matter of properly attributing logical developments to the right people, but that by working to understand how these women were involved in the field, and how they have come to be excluded from our understanding of the history of logic, we can understand how it is that women are still being excluded from the current state of logic, and also what we can do about it.

In this abstract, to compare rewriting induction (RI, for short) with cyclic proof systems, under certain assumptions, we show a transformation from cut-free cyclic proofs into RI proofs. More precisely, we first transform an inductive definition set of first-order predicate logic into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent holds if and only if its corresponding equation is an inductive theorem of the TRS. Then, we show a transformation of a cut- and quantifier-free cyclic proof of a quantifier-free sequent into an RI proof for the equation that corresponds to the sequent.