MLNL'09 - Schedule and abstracts

Abstract: The aim of algebraic set theory [JM95] is to provide a uniform categorical semantics for set theories of different kinds (classical or constructive, predicative or impredicative, well-founded or non-well-founded, etc.). In this talk we show how sheaf models for constructive set theories like IZF or Peter Aczel's CZF fit into the framework of algebraic set theory and how this semantics can be used to obtain derived rules for (extensions of) CZF. (The contents of this talk are based on unpublished work in collaboration with Ieke Moerdijk [BM09b]: this is supposed to be the third installment in a series of papers on algebraic set theory announced in [BM09a].)

[BM09a] B. van den Berg and I. Moerdijk -- A unified approach to algebraic set theory. To appear in the proceedings of the Logic Colloquium 2006.

[BM09b] B. van den Berg and I. Moerdijk -- Aspects of predicative algebraic set theory III: sheaf models. Under construction.

[JM95]} A. Joyal and I. Moerdijk -- Algebraic set theory. London Mathematical Society Lecture Note Series 220, Cambridge University Press, 1995.

Sonja Smets - Correlated Information: A Logic for Multi-Partite Quantum Systems

Abstract: I will present recent joint work with A. Baltag on a logical analysis of both classical and quantum correlations. In this work we propose a new logical system to reason about the information carried by a complex system composed of several parts. Our formalism is based on an extension of epistemic logic with operators for ``group knowledge". As models we introduce correlation models, as a generalization of the ``interpreted systems'' semantics. We use this setting to investigate the relationship between the information carried by each of the parts of a complex system and the information carried by the whole system. In particular we distinguish between the ``distributed information'', obtainable by simply pooling together all the information that can be separately observed in any of the parts, and ``correlated information", obtainable only by doing joint observations of the parts (and pooling together the results). Our formalism throws a new light on the difference between classical and quantum information and gives rise to a informational-logical characterization of the notion of ``quantum entanglement''.

Sam Sanders - Some numbers are more finite than others

Abstract: We discuss the inherent problems and limitations of classical non-standard mathematics and propose a much-needed refinement in the spirit of Karl Hrbacek's stratified set theory (see [1]). Instead of the dichotomy of finite and infinite numbers, a 'stratified' nonstandard theory of mathematics incorporates many degrees of infinity. We show the close relation between the classical and strati?ed approach of nonstandard mathematics and discuss current results and possible future research.

[1] Karel Hrbacek, Stratified analysis?, The strength of nonstandard analysis, Springer Wien- NewYork, Vienna, 2007, pp. 47-63.

Francien Dechesne – Comparing expressivity of modal logics in the context of protocol analysis.

Abstract: (Joint work with Yanjing Wang, CWI.) In computer science, various logical languages are defined to analyze properties of systems. One way to pinpoint the essential differences between those logics is to compare their expressivity in terms of distinguishing power and expressive power. In this paper, we study those two concepts by regarding the latter notion as the former lifted to classes of models. We show some general results on lifting an invariance relation on models to one on classes of models, such that when the former corresponds to the distinguishing power of a logic, the latter corresponds to its expressive power, given certain compactness requirements. In particular, we introduce notions of class bisimulation to capture the expressive power of modal logics. We demonstrate the application of our results by revisiting modal definability with our new insights.

James McKinna - Proof Search in Dependently-Typed Programming

Certified programming in the Curry-Howard-deBruijn paradigm naturally
supports, and is supported by, an interactive, incremental, approach to
typechecking and type inhabitation.

In this talk I will try to delineate some sub-classes of proof search
problem which arise in this setting, the kinds of programmer-supplied
evidence which allow their solution, and some of the challenges to
making this style of programming practicable.

Marcello Bonsangue - Algebras for Coalgebras

Abstract: (joint work with Jan Rutten, Alexandra Silva and Filippo Bonchi) Several dynamical systems, like deterministic automata and labelled transition systems, can be described as coalgebras of suitable Set endofunctors. In this talk we show that finite coalgebras of finitary functors can be characterized up to bisimulation by a specification language that generalizes Kleene’s regular expressions for finite automata. We give a sound and complete axiomatization of bisimulation for this specification language. We demonstrate the usefulness of our framework by providing finite equational systems for (non)deterministic finite automata, and labelled transition systems.

Wouter Stekelenburg - Realizability and Completeness

Abstract: Building a realizability model for the implicational fragment, which satisfies only those statements that are constructively provable: a how to guide.

Raul Leal - Coalgebraic Logic

Abstract Coalgebras generalize transition systems. They are given with respect
to a functor T which specifies the possible one step behaviours of
the system.

A fundamental question in this are is how to obtain a logic, for
arbitrary functor T, for T coalgebras. This question has been widely
study in the case of set endofunctors using extensions of classical
logic. However, there is no much work on categories different from
Set neither on non classical coalgebraic logic.

In this talk we present two of the main proposals for coalgebraic
logic and then speculate about extensions to categories different
from Set.

Tonny Hurkens - Constructive and normal proofs from classical and 3-valued truth tables

Abstract: Each line of the truth table of a connective gives rise to an introduction
rule (if the line ends with the truth value 1) or an elimination rule.
For traditional connectives, the generated rules are constructively correct.
The usual introduction and elimination rules can be defined as combinations
or special cases of the generated ones.
The line 1, 0, 0 for formulas P, Q, and P -> Q leads to Modus Ponens,
the line 0, 0, 0 for formulas P, Q, and P \/ Q leads to case distinction.
Both lines also occur in the truth table of conjunction.
This can be represented in a 3-valued logic as the line 1/2, 0, 0.
it leads to the second elimination rule for conjunction: P /\ Q implies Q.

The structure of a proof is not always obvious.
I claim that the simple deduction from A /\ (B /\ C) via B /\ C to C is a tree,
but in Gentzen style the root is below, whereas in Fitch style it is at the top.
In Gentzen style, each formula represents the conclusion of a subdeduction;
In Fitch style, each formula represents an assumption of a subdeduction;
in a deductive Beth tableau, one has to mark which role a formula plays.
(One could also do this in a natural deduction: instead of repeating the
conclusion of a case distinction, one could indicate the cancelled assumption.)

A deduction is normal if the conclusion of an introduction step is not used as
main formula of an elimination step.
There is a normal natural deduction from A /\ (B /\ C) to B /\ C whose
combination with the normal deduction from B /\ C to C is not normal.

Tableaus are normal since the main formula of an elimination step has to an assumption.
One can check whether a deduction in Gentzen or Fitch style is normal by
marking each conclusion of an introduction step and marking the conclusion of
a case distinction if in one or both cases the conclusion is marked.

This can be explained in terms of a 3-valued logic in which the marked formulas P*
have a weaker interpretation (truth value > 0) than unmarked formulas P (truth value = 1).
One can add an explicit repetition rule (P implies P*).
Then for example Modus Ponens can be reformulated as: P -> Q and P* imply Q.
In order to introduce (P -> Q)*, one has to deduce Q* from P.
So one can easily deduce (A -> A)* (without leaving an assumption), whereas A -> A
has truth value 1/2 if A has truth value 1/2.

Bart Jacobs - Quantum Logic in Dagger Categories with Kernels
We introduce dagger kernel categories as an elementary setting
for quantum logic: their kernel subobject posets turn out to
be orthomodular lattices, with suitable direct en inverse
images between them. Examples arise from relations, partial
injections, Hilbert spaces, Boolean algebras, orthomodular
lattices and Foulis semigroups.

Bas Terwijn - Constructive logic and computational lattices.

Abstract: The Medvedev lattice is a structure from computability
theory that is interesting for various reasons. It was
originally introduced for its connections with constructive
logic, but it is also interesting in other respects, for
example in connection with computation on the reals, the
study of Pi-0-1 classes, algorithmic randomness, or as a
generalization of the Turing degrees.
In this talk we discuss the connections with constructive
logic, in particular the question what logics can be
obtained by factors of the Medvedev lattice. This gives
rise to questions of a purely structural nature about the
intervals in the lattice. We will also discuss a closely
related lattice, the Muchnik lattice, and characterize
its finite intervals.

Nick Vaporis - A generalisation of Ghilardi's theorem
Abstract: In the setting of intuitionistic propositional logic,
Ghilardi's theorem establishes the equivalence of the extension
property and projectivity. The refined version we present
characterises the extension property up to n in terms of the T_n--
projective formulas, where T_n is the intermediate logic of finite
n--ary trees.

Jacob Vosmaer - Stone duality and modal logic
Abstract: Modal logic is an enrichment of classical propositional logic which is obtained by adding predicates expressing modalities to the language of propositional logic. Possible interpretations of modalities are `possibly P', `it is known that P', `it is provable that P', where P is a proposition. We will discuss two different semantics for modal logic: Kripke semantics (which are geometric or spatial in nature) and algebraic semantics. We will show that these a priori very different semantic views of modal logic are in fact two sides of the same coin, the coin being Stone duality between Boolean algebras and compact, Hausdorff, zero-dimensional topological spaces. With all this groundwork laid out, we may conclude the presentation with one of the author's own contributions to this field, concerning the duality between compact Hausdorff topological modal algebras and finitely branching Kripke frames.

Klaas Landsman - The Conway-Kochen-Specker Theorems
Abstract: The Kochen-Specker Theorem of 1967 was initially just meant
to strengthen a result by von Neumann from 1932 on the nonexistence of
a hidden variable interpretation of quantum mechanics. Over the last
four decades, the theorem has gained in importance. For example, in
1998 Butterfield and Isham initiated the cross-fertilization between
topos theory and quantum mechanics on the basis of Kochen-Specker, and
in
2006 and 2008 Conway and Kochen used it as a lemma in (allegedly)
proving the existence of Free Will. With Chris Heunen and Bas
Spitters, the speaker
recently gave a logical reinterpretation of the theorem, showing that
it implies that a theory describing the state space of a quantum system
cannot have any model. All this leads to the conclusion that quantum
logic admits neither a naive Boolean truth interpretation (as shown
already by Kochen and Specker), nor a natural Kripkean possible-
worlds semantics. The aim of this talk is to review this entire
development, which confirms the bizarre and incomprehensible nature of
our most precise and fundamental physical theory to date.

Jouko Vaananen - Second order logic, set theory and foundations of mathematics

Herman Geuvers - A review of the Curry-Howard-De Bruijn formulas-as-types interpretation
Abstract: In the 60s of the 20th century, Howard (going back to early ideas of
Curry) and De Bruijn independently developed the idea of interpreting
a formula as the type of its proofs. Their motivations were quite
different, coming from proof theory (Howard giving another treatment
of Kleene's realizability interpretation) and from proof checking (De
Bruijn developing the Automath system for the verification of
mathematical proofs using a computer).

Apart from these, the formulas-as-types interpretation has become
important in the foundations of mathematics, due to the work of
Martin-L"of, whodeveloped intuitionistic type theory as a foundation
for mathematics, based on the Brouwer-Heyting-Kolmogorov
interpretation of proofs.

Combining these three views, we arrive at the fundamental concept of
"program extraction", where a program (algorithm) is extracted from a
(constructive) proof and thereby we obtain "program correctness by
construction".

In the talk, we will review the logical ideas underlying the
formulas-as-types interpretation and their practical application in
proof checking and program extraction.

Two interesting more recent topics that we will discuss are the
extension of the Curry-Howard interpretation to classical logic and
the application to proofs in analysis.