All talks will take place in HG00.062
10-11 Invited talk - Bart Jacobs
11-12 Benno van den Berg, Nick Vaporis
13-14 Francien Dechesne, Sonja
Invited talk - Jouko
Marcello Bonsangue, Jacob Vosmaer,
9-10 Invited talk - Herman
McKinna, Sam Sanders, Wouter Stekelenburg
talk - Bas Terwijn
14.30 -15 Tonny Hurkens
15-16 Klaas Landsman
van den Berg - Sheaf models in Algebraic Set Theory
Abstract: The aim of algebraic set
[JM95] is to provide a uniform categorical semantics for set theories
kinds (classical or constructive, predicative or impredicative,
well-founded or non-well-founded, etc.). In this talk we show how sheaf
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
derived rules for (extensions of) CZF.
(The contents of this talk are based on unpublished work in collaboration
with Ieke Moerdijk [BM09b]: this is
to be the third installment in a series of papers on algebraic set
announced in [BM09a].)
B. van den Berg and I. Moerdijk -- A
approach to algebraic set theory. To
appear in the
proceedings of the Logic Colloquium 2006.
[BM09b] B. van
den Berg and I. Moerdijk
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
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
information carried by a complex system composed of several parts. Our
formalism is based on an extension of epistemic logic with operators
``group knowledge". As models we introduce correlation models, as a
generalization of the ``interpreted systems'' semantics. We use this
investigate the relationship between the information carried by each of
parts of a complex system and the information carried by the whole
particular we distinguish between the ``distributed information'',
by simply pooling together all the information that can be separately
in any of the parts, and ``correlated information", obtainable only by
doing joint observations of the parts (and pooling together the
formalism throws a new light on the difference between classical and
information and gives rise to a
characterization of the notion of ``quantum entanglement''.
numbers are more finite than others
We discuss the inherent
problems and limitations
of classical non-standard mathematics and propose a much-needed
the spirit of Karl Hrbacek's
theory (see ). Instead of the dichotomy of finite and infinite
'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
Karel Hrbacek, Stratified
analysis?, The strength
of nonstandard analysis,
Springer Wien- NewYork,
Vienna, 2007, pp. 47-63.
expressivity of modal logics in the context of protocol analysis.
work with Yanjing Wang,
CWI.) In computer science, various logical languages are defined to
properties of systems. One way to pinpoint the essential differences
those logics is to compare their expressivity in terms of
and expressive power. In this paper, we study those two concepts by
the latter notion as the former lifted to classes of models. We show
general results on lifting an invariance relation on models to one on
of models, such that when the former corresponds to the distinguishing
a logic, the latter
corresponds to its expressive
power, given certain compactness requirements. In particular, we
notions of class bisimulation
to capture the
expressive power of modal logics. We demonstrate the application of our
by revisiting modal definability with our new insights.
- 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.
Bonsangue - Algebras for
(joint work with Jan Rutten,
Alexandra Silva and Filippo
Several dynamical systems, like deterministic automata and labelled
transition systems, can be described as coalgebras
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
Stekelenburg - Realizability and
Building a realizability model for the implicational fragment, which
satisfies only those statements that are constructively provable: a how
Leal - Coalgebraic Logic
Coalgebras generalize transition systems. They are given with respect
to a functor T which specifies the possible one step behaviours of
A fundamental question in this are is how to obtain a logic,
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
logic and then speculate about extensions to categories different
Tonny Hurkens - Constructive
and normal proofs from classical and 3-valued truth tables
Each line of the truth table of a connective gives rise to an
rule (if the line ends with the truth value 1) or an elimination rule.
For traditional connectives, the generated rules are constructively
The usual introduction and elimination rules can be defined as
or special cases of the generated ones.
The line 1, 0, 0 for formulas P, Q, and P -> Q leads to Modus
the line 0, 0, 0 for formulas P, Q, and P \/ Q leads to case
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
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
but in Gentzen style the root is below, whereas in Fitch style it is at
In Gentzen style, each formula represents the conclusion of a
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
A deduction is normal if the conclusion of an introduction step is not
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
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
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.
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 theoremAbstract:
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
Jacob Vosmaer - Stone duality and modal logicAbstract:
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 TheoremsAbstract:
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
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 interpretationAbstract:
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
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.