Logo Utrecht University

TULIPS – The Utrecht Logic in Progress Series

Upcoming Talks


Loeb constructively meets μ

A famous result of Solovay identifies the classical modal Loeb system (GL) as the provability logic of Peano Arithmetic. Under this perspective, Goedel’s Second Incompleteness Theorem and Loeb’s Theorem correspond to explicit definability of
fixpoints of modalized formulas in GL. Van Benthem has observed that this definability of fixpoints entails that adding standard fixpoint operators of positive formulas does not increase the expressive power of GL. Visser has analyzed this observation syntactically and extended it to a proof that GL is a retract of the modal μ-calculus in a suitably defined category of interpretations. A fully polished theory of such embeddings and translations involving the fixpoint operator and similar binders is yet to be developed; our current efforts focus on utilizing the theory of higher-order rewrite systems (HRS).

Furthermore, we face some interesting problems when studying intuitionistic analogs of such results. First, while the fixpoint theorem for modalized formulas works in intuitionistic GL, the propositional reasoning underlying derivations of van Benthem and Visser is essentially classical. Deep results about the intuitionistic propositional calculus (IPC)  established by Pitts and Ruitenburg can be used to overcome this limitation.

Second, over IPC (and sometimes even classically) it is for several reasons natural to look at a more general syntactic setup replacing the box with Lewis arrow, which arithmetically is standardly interpreted in terms of preservativity (although it does admit many other interpretations). As it turns out, there are two major incompatible ways of computing explicit fixpoints for formulas whose principal connective is the strict implication, each requiring a different base logic. Our approach here can be described as the first study of reverse mathematics of explicit fixpoints.

Time: 16.00 – 18.00

Location: 103, Drift 25

Unifying Two Views of Conditionals

In this talk, my goal is to draw together two traditions that often share similar motives, but reach different views about the logic of conditionals. Lewis and Stalnaker developed a semantics for conditionals based on selection functions, sometimes called the `variably-strict’ conditional. Routley and Meyer developed a semantics for conditionals based on a ternary relation, sometimes called an `enthymematic-relevant’ conditional. These traditions agree that the material and strict conditional are inadequate-and for similar reasons-but traditionally, these camps also disagree on some important details.

My approach will blend together the idea that antecedent selections play a role in evaluating all conditionals together with the idea that the logic of conditionals is enthymematic. Much of the work is accomplished by shifting attention from the selection function at individual points of models to a `type-raised’ selection function that `holds at whole propositions’. A conditional proposition [If A, B] can then be seen as the proposition that grounds the maximally extensive type-raised selection function on proposition [A] that embeds into proposition [B]. This perspective allows us to capture all different kinds of conditionals—both counterfactuals and implications—by imposing frame conditions on type-raised selection functions.

Time: 16.00 – 18.00

Location: 103, Drift 25


Time: 16.00 – 18.00

Location: 205, ICU Spinoza