I will discuss Wojciech Moczydlowski's work on normalization
in intuitionistic set theories. I will present a version of IZF
(Intuitionistic Zermelo-Fraenkel set theory), and a weakly normalizing
lambda calculus for its proof theory. The normalization result
corresponds to a cut-elimination result. Time permitting, we will
discuss other approaches to normalizing intuitionistic set theories.
In 2007, Terence Tao wrote on his blog an essay about soft analysis, hard
analysis and the finitization of soft analysis statements into hard
analysis statements. One of his main examples was a quasi-finitization of
the infinite pigeonhole principle IPP, arriving at the "finitary" infinite
pigeonhole principle FIPP_1. That turned out not to be the proper
formulation and so we proposed an alternative version FIPP_2. Tao himself
formulated yet another version FIPP_3 in a revised version of his essay.
We give a counterexample to FIPP_1 and discuss for both of the versions
FIPP_2 and FIPP_3 the faithfulness of their respective finitization of IPP
by stydying the equivalences IPP<->FIPP_2 and IPP<->FIPP_3 in the context
of reverse mathematics...
A well-known open problem in epistemic logic is to give a syntactic characterization of the successful formulas, which are preserved in “self-defined” submodels, and the self-refuting formulas, which are falsified in self-defined submodels. Intuitively, a successful formula always remains true when it is “learned,” while a self-refuting formula always becomes false. The most famous example of an unsuccessful (and indeed self-refuting) formula is the Moore sentence p & ~Kp, read as “p is true but you do not know p.” We show that in all modal logics with introspection (axioms 4 and 5), Moorean phenomena are the source of all unsuccessfulness. This is a distinctive feature of modal logics with introspection, for without introspection there are non-Moorean reasons for failures of success. We give full syntactic characterizations of the successful and self-refuting formulas, and we establish some semantic results about related classes of formulas, including the knowable and learnable formulas.
Some twenty years ago I wrote a thesis on Dialectica Categories, a categorical approach to Goedel's Dialectica Interpretation, which was published in 1958. Goedel's goal was to show the consistency of higher-order arithmetic and his Dialectica Interpretation has been a fundamental tool in proof theory from its inception (cf. Avigad and Feferman,1999). Recently several papers have been written about extensions and reformulations of that categorical work. In particular, in 2008 Bodil Biering defended a phd thesis on a complete reformulation, dealing with a first-order version of the interpretation. In this talk I want to describe Biering's reformulation and its rationale. Time permitting I would like to discuss other aspects of her thesis that deserve further investigation in my opinion.
The design of the programming language Haskell leans on category theory in several different areas. I will describe the way one can interpret (most) of the language design as a category, as well as how endofunctors, monads and fixpoints show up as constructions in the language itself. If time allows, I will finish with describing the work by Conor McBride on introducing formal derivatives of 'nice' endofunctors to produce a new formalism for Zipper datatypes.