Workshop on Philosophical Topics in Mathematics and Proof Theory 

The event will take place on Tuesday 24 June 2025 at Janskerkhof (Utrecht University), following the PhD defense of Robin Martinot.

Speakers

Albert Visser (Utrecht University)
Amir Tabatabai (University of Groningen)
Heinrich Wansing (Ruhr University Bochum)
Andrew Arana (Université de Lorraine)
Marianna Girlando (University of Amsterdam)
Colin Caret (Utrecht University)
Robin Martinot (Ruhr University Bochum)

Program June 24

9.15-9.30 Walk-in and welcome [Morning location: Janskerkhof 2-3, room 110]

9.30-10.15 Heinrich Wansing - Another view on Abelian logic
10.15-10.45 Robin Martinot - Meaningful proof systems and bilateralism

10.45-11.15 Coffee break

11.15-12.00 Albert Visser - When are two Theories the same?
12.00-12.45 Andrew Arana - Syntactic purity in the setting of equational proofs

12.45-14.45 Lunch break

14.45-15.30 Amir Tabatabai - Philosophy Meets Computational Complexity [Afternoon location: Stijlkamer, room 0.06, Janskerkhof 13]
15.30-16.15 Marianna Girlando - From semantics to syntax: working with labelled proof systems

16.15-16.45 Coffee break

16.45-17.30 Colin Caret - All About Contraction

18:30 Workshop dinner (Sarban)

Abstracts

When are two Theories the same?

Albert Visser

In this talk, I will explain how notions of sameness of theories can be extracted from categories of theories and interpretations. Every notion of sameness of interpretations leads to a notion of sameness of theories.

Three well-known notions of this kind are  definitional equivalence (aka synonymy), bi-interpretability and mutual interpretability. A closely related notion that does not fall under the paradigm is recursive Boolean isomorphism. 

Different notions do different jobs. For example, mutual interpretability tells us about the strength of a theory and bi-interpretability preserves almost all good properties of theories like finite axiomatizability, kappa-categoricity and sequentiality.

I will discuss some examples of such notions of sameness and some examples that separate such notions of sameness. Moreover, I present some general insights.

Philosophy Meets Computational Complexity

Amir Tabatabai

Constructivism provides a philosophical and synthetic foundation for what classical mathematicians call computable mathematics. In a similar spirit, one may ask whether there exists a philosophical and synthetic standpoint that captures the feasibly computable world, that is, the world where only polynomial-time computation is permitted.

In this talk, we argue that absolute predicativism, a viewpoint rejecting all self-referential definitions, including that of the set of natural numbers, precisely characterizes this feasible realm. From a technical perspective, this new foundation may shed light on the nature of feasible computation and longstanding open problems in computational complexity such as the P versus NP problem. Philosophically, however, it reveals the unexpected foundational role of feasible computation and suggests that computational explosions and vicious circles are two sides of the same coin.

Another view on Abelian logic

Heinrich Wansing

In this paper, we introduce two new semantic presentations of Abelian logic, the non-trivial negation inconsistent logic of Abelian lattice-ordered groups, which was independently developed by Ettore Casari, and by Robert Meyer and John Slaney. The first semantics is a ternary frame Kripke semantics, and the second is based on ideas from Edwin Mares’ work. Thereby emerges a condition for the falsity of Abelian implication to be supported, which we analyse further in the separate context of the first-degree entailment logic. This is joint work with Satoru Niki.

Syntactic purity in the setting of equational proofs

Andrew Arana

Roughly, a proof is said to be pure if it draws only on what is “close” or “intrinsic” to what is being proved. We might try to measure this distance between theorem and proof formally, as Robin does in her thesis, or even syntactically. We can see an attempt to do this in Gentzen’s work via the subformula property, but this approach is limited because the subformula property does not necessarily hold when there are non-logical axioms. In this talk, based on joint work with Mitsu Okada, we sketch an approach to syntactic purity based on the theory of term rewriting in the context of equational logic. In this setting we can identify a notion of syntactic purity and can characterize a process of proof purification, even if full syntactic purity is not necessarily available.

All About Contraction

Colin Caret

Logical solutions to paradox rejects basic principles of classical logic. Many of them reject classical principles of negation. Curry's paradox is a thorn in the side of these strategies, as it does not essentially involve negation. One family of formal solutions to Curry's paradox reject classical principles for the conditional, such as the principle of contraction. Following an idea of Nolan, we would like to have some independent motivation for embracing one of these formal solution to the paradox. In this talk, I will explore the possibility that aboutness theory explains the failure of contraction. Aboutness theory stems from the work of Lewis, Yablo, Fine and others on the semantic nature of the subject matters of propositions. How does the subject matter of a conditional relate to that of its parts? I will argue that the answer to this question can motivate failure of contraction independently of any considerations about solving the paradox.

From semantics to syntax: working with labelled proof systems

Marianna Girlando

Labelled calculi are a family of proof systems for modal logic that extend the syntax of Gentzen-style sequent calculi with labels—syntactic annotations that encode semantic information from Kripke models. These calculi enjoy strong proof-theoretic properties, such as cut-admissibility, and support countermodel construction from failed proof search trees. Their modularity makes them adaptable to a wide range of modal logics, with structural rules reflecting frame conditions.

In this talk, I will introduce labelled calculi for modal logics in the S5 cube, outline their main properties, and demonstrate how the framework generalizes to other modal systems. These include intuitionistic modal logics, interpreted via bi-relational Kripke models, and conditional logics, which will be presented through neighborhood semantics.

Meaningful proof systems and bilateralism
Robin Martinot

In this talk we reflect on the notion of a ‘meaningful’ proof system, by which we mean a proof system that has a philosophically optimal relation to a semantics. We can distinguish several properties that affect this, such as syntactic purity (and its counterpart, semantic pollution); categoricity of proof systems; and suitability of a proof system for proof-theoretic semantics. We discuss some work in progress on these properties, focusing mostly on semantic pollution, in the setting of Abelian logic. This logic can have interesting descriptions involving bilateral versions of proof systems and models (see e.g. recent work by Wansing & Niki). Bilateral formal systems take a notion of denial as primitive next to the usual notion of assertion. This results in an enrichment of the language of a proof system, and so provides a suitable case study for semantic pollution, which has been unexplored in these systems so far.

Attendance is free for anyone who is interested.

Organized by Robin Martinot & Rosalie Iemhoff