February 16: *Quintijn Puite*:Cut elimination for cyclic linear logic by means of two-sided proof nets.

14.00--15.30

Abstract:

In the first part we will introduce the calculus "(non-commutative) cyclic linear logic" (NCLL), which is a non-commutative variant of the multiplicative fragment of linear logic. We define two-sided proof structures for this calculus, and consider a contraction criterion, stating which among those proof structures correspond to proofs, i.e. are proof nets.

In the second part, we concentrate on the cut rule and its counterpart in our theory of proof nets. We will show that performing a cut reduction step is sound with respect to our contraction criterion. This gives rise to a confluent and terminating cut elimination procedure for NCLL-proof nets.

To main page

March 2: *Vincent van Oostrom*: Residual Systems.

14.00--16.00

Abstract:

We define a residual system as a triple (G,1,/), where - G is a graph, - 1 maps any object a to an arrow a->a, and - / maps any pair of coinitial arrows f:a->b and g:a->c to f/g:c->d and g/f:b->d for some d, and satisfying the axioms: f/f=1 f/1=f 1/f=1 (f/g)/(h/g)=(f/h)/(g/h) Examples are: 1) (Boolean,0,-) the booleans (one object, two arrows 0 and 1) with cut-off subtraction 2) (Development,emptystep,/) developments in orthogonal term rewriting (or lambda- calculus) with residuals (cf. Prop.12.1.12 of [1]) 3) (Parallelcrossing,emptyrelation,/) parallel crossings of strands represented as certain relations R on states (total orders on strands). with R/S = ((R union S)+)-S A residual system (G,1,/) generates a residual system (P,1,/,.) with composition . on composable paths in G, additionally satisfying: 1.1=1 f/(g.h)=(f/g)/h (f.g)/h=(f/h).(g/(h/f)) 1) Boolean generates the natural numbers with zero, cutoff-substraction and addition 2) Development generates reductions with the empty reduction, projection and concatenation 3) Parallelcrossing generates braids with the empty braid, a residual operation and concatenation [1] The lambda-calculus, its syntax and semantics, H.Barendregt, 1985To main page

March 16: *Henk Barendregt* (University of Nijmegen): Informal and Formal Mathematics.

14.00--15.00

Abstract: Ordinary mathematics is informal and precise.

Formal mathematics looks exaggeratedly detailed.

We will explain the purpose of a
new style of mathematics that is about to emerge.

To main page

March 16: *Arnold Beckmann* (University of Münster): The use of well-foundedness principles in weak arithmetics.

14.00--16.00

Abstract: Well-foundedness principles play an important role
in the study of provability strength for a lot of mathematical
theories like (fragments of) arithmetic or set theory.

We will summerize what is known about well-founded principles in weak
arithmetic like Buss's bounded arithmetic.

To main page

April 12: *Volodya Shavrukov*: Branches of the $E$-tree and jump pseudo-hierarchies.

13.00--15.00

Abstract: Gödel's Incompleteness Theorem also holds in the
restricted case of $\Sigma_1$ sentences
of arithmetic.

Accordingly, there are models of PA modelling
$\Sigma_1$ sentences that do not hold in the real world.

The $E$-tree is defined as the partially ordered
set of proper prime filters in the lattice of
$\Sigma_1$ sentences modulo provability in PA.

It provides an appropriate framework for studying the
relative order in which $\Sigma_1$ sentences acquire
witnesses in a model of arithmetic.

The $E$-tree exhibits unexpected connections with
degrees of unsolvability and ordinal recursion theory.
We characterize the order types of $E$-branches
in terms of coloured jump pseudo-hierarchies.

These are linearly ordered structures supporting a
hierarchy-like system of sets where each level is separated
from higher ones by at least one Turing jump.

The order types of jump pseudo-hierarchies themselves are
determined by those increasing sequences of admissible
ordinals that form countable initial segments of admissibility
spectra.

To main page

April 27: *Rosalie Iemhoff* (University of Amsterdam): Provability logic for constructive theories.

14.00--15.00

Abstract: The provability logic of a theory consists of the propositional schemes that the theory can prove about its provability predicate.
The provability predicate expresses the property of being provable in the theory.

For classical theories provability logic is well-investigated, but for
constructive theories much less is known.

In this talk we will discuss what is known about the provability logic of
Heyting Arithmetic. We will see that for three of
its main fragments there exists an axiomatization, although it is still open
whether the whole logic has a decent axiomatization or not.

Many principles of the provability logic can be formulated in
a more transparent way in preservativity logic, which is an extension
of provability logic. Preservativity
logic is the constructive analogue of interpretability logic.
We will introduce the notion of preservativity
and formulate the principles of the provability
logic of Heyting Arithmetic in this setting.

Finally, we will explain
why in this case the notion of preservativity seems more adequate
to handle questions in provability logic.

To main page

May 18: *Gerard Renardel de Lavalette* (Universiteit Groningen): Changing modalities

Abstract: Modal structures were invented by Fagin and Vardi in 1985 as an alternative for
Kripke models. Due to a flaw in the definition, working with them was rather
cumbersome.

In this talk I will present an improved definition, and use it for
the semantics of dynamic modal logic.

To main page

May 18: *Andreas Weiermann* (Universität Münster): Analytic combinatorics and proof theory.

Abstract: Using methods from analytic
combinatorics we obtain Friedman style independence results for
first order Peano arithmetic and its fragments.

We get an optimal classification for the slowly
well quasi orderedness of the class of finite trees in
terms of Otter's tree constant $2.95576...$
and we obtain a classification for the slowly
well orderedness of $\varepsilon_0$ using
a result of Yamashita.

We further obtain classification results
for hydra games, Goodstein sequences and
we present a refinement of the Paris Harrington
result.

To main page

May 18: *Michael Möllerfeld* (Universität Münster): Proof and Recursion Theory of the
mu-calculus.

Abstract: The mu-calculus is a system of positive inductive definitions,
which is widespread in computer science.
It is a generalization of ID_1, the theory of non-iterated
positive inductive definitions.
Given a language L, the language of the mu-calculus L_{mu}
arises by adding set-variables and a fixed-point constructor, called mu.

Bob Lubarsky determined the descriptive strength of the mu-calculus
in terms of strong recursively regular ordinals, called
gap-reflecting ordinals.
Although the mu-calculus is a very natural extension of ID_1,
it has not yet been proof-theoretically studied.
It turns out that the mu-calculus is fairly strong,
namely it is proof-theoretically equivalent to
$\Pi^1_2$-comprehension with set-induction.
Our results are obtained by a reduction involving systems
of non-monotone inductive definitions and systems of
set-theory defined in terms of reflection, gap-reflection and
stability.

As a recursion theoretic byproduct one gets a
fine structure analysis of classes of
non-monontone inductive definitions extending the results of
Richter and Aczel. Moreover, answering a question
raised by Lubarsky, one can characterize the sizes
of gap-reflecting ordinals in terms of chains of
stable ordinals.

To main page

May 19: *Pieter Hofstra*: Realizability and Ordered Partial Combinatory Algebras.

Abstract:

To main page

May 19: *Christoph Duchhardt*(Universität Münster): Quickly Analyzing Kripke Platek Set Theory.

Abstract:

To main page

May 19: *Jaap van Oosten*: Analyzing Modified Realizability.

Abstract: We analyze standard HRO-modified realizability for HA in terms of the Friedman translation and a notion of internal forcing. We show that a straighforward attempt to axiomatize this realizability runs into an obstacle.

To main page

June 1: *Jan-Willem Klop*: Sequentiality in the Lambda Calculus.

Abstract:This talk is about joint work with Henk Barendregt,
Inge Bethke, Roel de Vrijer.

We present a proof of Berry's Sequentiality Theorem (BST)
for the lambda calculus, based on the technique of origin
tracking in the framework of infinitary lambda calculus.

We also discuss as an application of BST the
undefinability of functions like parallel or, the
Berry-Kleene function, Malcev's function. As we
recently noticed, the nondefinability of Surjective Pairing
is also an immediate corollary of BST.

A stronger version of BST is mentioned that yields some
more nondefinability results than BST.

Our talk will be in principle self-contained, requiring
only familiarity with basic lambda calculus.

To main page

June 1: *Ronald de Wolf*: Quantum Computing.

Abstract: Current computers are based on classical physics, both in theory
(Turing machines) and in practice (PCs). However, modern quantum
physics differs in crucial aspects from classical physics, and
computers making use of quantum mechanical effects can do various
things that classical computers can't.

In this talk I will survey
the young field of quantum computing: what is a quantum computer,
what can you do with it (quickly factoring large integers, searching
large databases,...), and when will they actually be built?

To main page

November 9 : *Ieke Moerdijk*: Linear Set Theory.

Abstract: A model of set theory can be viewed as an algebraic
structure, with "union" and "singleton" as operations.

This viewpoint is developed in [JM], where it is shown how one can obtain
(forcing) models of ZF and of constructive variations of ZF, by constructing
such algebraic structures by "generators and relations" in categories
of sheaves.

Linearization of such algebraic structures gives rise to families of
Hopf algebras, and the algebraic properties of the models of set theory
yield universal cocycles in Hochschild cohomology on the linearized
structures. For example, the k-vector space on the hereditarily finite
sets carries a k+k-parametrized family of Hopf algebra structures ([M]), one
of which is the Connes-Kreimer Hopf algebra ([CK]).

[CK] A. Connes, D. Kreimer, Hopf Algebras, Renormalization and
Noncommutative Geometry, hep-th/9808042.

[JM] A. Joyal, I. Moerdijk, Algebraic Set Theory, Cambridge University
Press, 1995.

[M] I. Moerdijk, On the Connes-Kreimer construction of Hopf
algebras, math-ph/9907010.

To main page

November 16 : *Bas Luttik*: On the Expressiveness of the Choice Quantifier.

Abstract: The process specification language muCRL of Groote and Ponse (1990) combines many-sorted algebraic specification of abstract data types
with process algebraic mechanisms to specify behaviour. In particular,
it includes choice quantifiers to specify input over a data domain.

Semantically, choice quantification corresponds to taking the process
algebraic sum of the (possibly infinite) set of all instantiations of a
process expression with a data value for some variable.

I will discuss the expressiveness of choice quantifiers in the
context of finite pCRL (muCRL without parallelism and recursion).

It turns out that, with respect to the data, finite pCRL is as
expressive as (classical) first-order predicate logic. In particular,
choice quantification can be exploited to simulate both universal and
existential quantification of first-order predicate logic.

To main page

November 23 : *Bas Spitters*: Intuitionistic Measure Theory.

Abstract:Constructivism comes in several flavours. Brouwer's intuitionism and Bishop's
constructivism are two of them. We will describe them very briefly.

Intuitionistic measure theory is well-developed, but is sometimes a little
different from its classical counterpart. For instance, not all open sets are
measurable. On the other hand, every almost everywhere defined function is
measurable. This last theorem is of course related to the well-known
intuitionistic theorem that every function is continuous.

We will give some more applications of intuitionistic axioms.

Finally, we will show how certain theorems that can be proved
intuitionistically and classically, can be proved without extra axioms in
Bishop's constructivism. We use a logical trick due to Ishihara.

To main page

November 30 : *Jaco van de Pol*: Equational Binary Decision Diagrams.

Abstract:

Binary Decision Diagrams (BDDs) are a well-known data type
to represent boolean functions, and to decide satisfiability,
tautology of and equivalence between propositional formulae.

We extend BDDs with equations between individual variables,
calling the resulting objects EQ-BDDs. A straightforward notion of
reduced ordered EQ-BDDs (EQ-OBDD) is defined, and it is proved that each
EQ-BDD is logically equivalent to an EQ-OBDD. Moreover, on EQ-OBDDs
satisfiability and tautology checking can be done in constant time.
We introduce an algorithm, which for any propositional formula with
equations finds an EQ-OBDD that is equivalent to it.

Next we discuss the addition of function symbols to the formalism,
reaching quantifier free first order logic. Several procedures to
eliminate function symbols and equality exist, based on
Ackermann's reduction and the finite model property. However,
these approaches only work for so-called uninterpreted function
symbols, and they don't work in the presence of a background theory
that defines the function symbols.

We implemented a system which combines the EQ-BDD algorithm
with term rewriting, to solve boolean combinations of equations
over some equational specification. Although the theory for this
extension is underdeveloped, experiments show that such a system
is very useful.

To main page

December 7 : *Benno van den Berg*: Weak W-Types.

Abstract:

Originally, "W-type" is the name of a certain construction
for producing types in Martin-Löf Type Theory. In an article by Moerdijk and
Palmgren a categorical analogon of this construction was introduced. As
a result, we can study W-types categorically and it makes sense to say that
a category "has W-types".

In my Master thesis, I connect this topic with the theory of exact completions.
Forming an exact completion is an operation that can be performed on certain
suitable categories to obtain a so-called exact category in a universal way. In
the theory of exact completions, results are typically of the form: if a
suitable category satisfies condition so-and-so, then its exact completion satisfies
condition such-and-such, where such-an-such is stronger (more demanding)
than so-and-so. One of the aims of my thesis is to find a useful candidate
for so-and-so, if we replace such-and-such by the condition of having
W-types. I call this condition "having weak W-types".

In my talk I will give a precise formulation of the results obtained, sketch
the notion of a weak W-type and give an application of this notion in the
theory of realizability topoi.

To main page

January 11, 2002: *Aart Middeldorp*: Transforming Context-Sensitive Rewrite Systems.

Abstract:

Context-sensitive rewriting is a term rewriting strategy proposed by
Lucas to model lazy evaluation in functional programming. In the first
part of this talk we study techniques to analyze the termination
behavior of context-sensitive rewrite systems. We present two new
transformation techniques for proving termination of context-sensitive
rewriting. Our first method is simple, sound, and more powerful than
previously suggested transformations. However, it is not complete,
i.e., there are terminating context-sensitive rewrite systems that
are transformed into non-terminating term rewrite systems. The second
method that we present is both sound and complete.

Recently, Lucas showed that innermost termination of context-sensitive
rewriting is closely related to termination of rewriting with strategy
annotations as used in OBJ like languages. In the second part of the
talk we show the somewhat surprising result that none of the existing
transformations for termination is sound for innermost termination.
We conclude by presenting a simple transformation that is both sound
and complete for innermost termination.

The talk is based on joint work with Juergen Giesl.

To main page

February 1, 2002: *Troy Lee*: Is Multiplication Harder than Addition? - Arithmetical Definability over Finite Structures.

Abstract:

We show that two definability results of Julia Robinson,
namely that multiplication and the successor relation can first-order
define addition, and that the divisibility relation and successor can
first-order define multiplication, also hold over finite structures (where
ordering is used instead of successor).

The first result is obtained by
showing that the BIT predicate can be defined with TIMES and ordering,
thus FO(<,BIT)=FO(<,TIMES). This result has independent interest as an
alternative characterization of FO(<,BIT)=DLOGTIME AC^0. With a
definition of BIT, the ``carry-look-ahead'' construction can then be used
to define PLUS.

We also show that there is no first-order sentence with
TIMES but without ordering which can define PLUS. A corollary is then
that TIMES cannot first-order define ordering.

Our results, together with
recent results on the Crane Beach conjecture show that there is a language
definable in FO(<,TIMES) but not in FO(<,PLUS). In other words, there is
no first-order sentence with < and PLUS which can express TIMES.

To main page

February 15, 2002 : *Keith Devlin*: How did Mathematical Ability evolve?

Abstract:

Mathematics, as we generally understand it, is at most 5,000 years old (Numbers are at most 10,000 years old). That is too short a period for any major changes in the human brain. So, when we do mathematics, we must be using mental capacities that evolved long before mathematics came along. What are those abilities and what survival advantages led to their finding their way into the human gene pool? And if everyone has these abilities - as an evolutionary account will imply - then why do so many people find mathematics impossibly hard?

The lecture is based on the speaker's recent book *The Math Gene: How Mathematical Thinking Evolved and Why Numbers Are Like Gossip*, Basic Books 2000.

To main page

March 15, 2002: *Lev Beklemishev*: On fragments of arithmetic related to $\Delta_1$-induction.

Abstract:

We present a survey of the results
around the problem by J.Paris, whether
induction for decidable relations implies
the corresponding least element principle.
We show that this problem has negative answer
at least in a certain weaker "relativized" sense.
Relationship with the query complexity and
theories with iterated open induction
will be indicated.

To main page

April 5, 2002: *Pieter Hofstra*: Relative Completions.

Abstract:

In category theory, one encounters various kinds of completions; these
may be seen as constructions that freely add structure (e.g. (co)products,
quotients, etc.) to a category. Two important examples of such universal
constructions are the regular completion and the exact completion of a category.

We will first exhibit these constructions, and then show why they are important
for the study of realizability toposes. The applications of these constructions
to realizability, however, are easily seen to depend on the axiom of choice, and
we present a generalization that works in a constructive setting.

To main page

April 19, 2002: *Yde Venema*: Canonicity, correspondence and duality.

Abstract:

Algebraic lattice expansions, that is, lattices endowed with additional
operations, play an important role in various branches of nonclassical
logic. For instance, varieties of Boolean Algebras with Operators form
the algebraic counterpart of modal logics.

Canonicity questions concern the identification of those properties
that are preserved under taking the so-called canonical extension of a
given algebraic lattice expansion, or, as a variation, under taking its
MacNeille completion. In many cases the canonical extension can be
obtained as the double dual of the original algebra, the duality
involved here being built on well known dualities such as Stone's or
Priestley's. Interesting correspondence questions in this context relate
the (equational) properties of the algebraic lattice expansion to
(first-order) properties of the dual structure and these again to
(equational) properties of the double dual algebra.

In the talk I will first define the above notions and explain their
relevance. I will then briefly survey some recent developments in the
field. In the final part of the talk I will concentrate on a recent
result involving the canonicity and automatic correspondence of a
wide class of equations involving distributive lattices with operations
that preserve or reverse meets and joins.

To main page

April 19, 2002: *Benedikt Löwe*: Transfinite Iterative Constructions: Revision Sequences, Infinite Time Turing Machines and others.

Abstract: In several areas of mathematical logic, research has been directed to
iterative constructions that will run into transfinite processes. We shall
be looking at Revision Sequences in the sense of Gupta and Belnap and
Infinite Time Turing Machines as defined by Hamkins and Kidder and
investigated by Hamkins, Lewis and Welch.

The talk will survey complexity results in the different areas and discuss
modifications and other areas of application of transfinite revision
processes.

To main page

April 11, 2003: *Georg Moser*:Relating derivation lengths with the slow-growing hierarchy directly.

Abstract: In this article we introduce the notion of a generalized system of fundamental sequences and we define its associated slow growing hierarchy.

We claim that these concepts provide a bridge connecting (ordinal) proof theory and term rewriting theory. More precisely these concepts are genuinely related to the classification of the complexity---the derivation length--- of rewrite systems for which termination is proved by a standard termination ordering.

To substantiate this claim, we re-obtain multiple recursive bounds on the the derivation length for rewrite systems terminating under lexicographic path ordering. The novelty of our proof being that is clarifies precisely the proof-theoretic concepts exploited in the original proof by the second author. In particular it reveals the role played by the slow-growing hierarchy.

To main page

May 30,2003:*Harry Buhrman*:Simultaneous Message Passing with Quantum Bits.

Abstract: We study the communication complexity variant "Simultaneous Message
Passing" introduced by Yao in 1979. In this model there are three
players Alice, Bob and a referee. Both Alice and Bob have an input
string of n bits, say x and y. Alice and Bob are only allowed to send
messages to the referee who has to compute some Boolean function
f(x,y). The goal is to minimize the number of bits transmitted.

In the randomized version of this model where Alice and Bob posses
private random coins it was shown by Ambainis (96) that for the
EQUALITY function O(\srqt(n)) bits suffice. Newman and Szegedy (96)
showed
that the EQUALITY function needs $\Omega(\srqt(n))$ bits. Their
result was improved by Babai and Kimmel (97) who showed that for any
Boolean function the randomized and the deterministic complexity can
be at most quatratically far apart.

We consider the quantum version of this model where Alice and Bob can
send qubits to the referee. We show that in the quantum world Alice and
Bob can compute the EQUALITY function with high probability by
sending only O(log(n)) qubits to the referee.

In this talk we will review the basic "quantum computing" tools and no
prior knowledge of these is necessary.

To main page

May 30,2003:*Federico de Marchi*:Dualising Universal Algebra.

Abstract:Universal algebra studies models of equational theories defined
by means of a signature and some equations. Categorically, this study is
made possible by the correspondence between models of a theory and
algebras for the free monad on a functor naturally arising from it. This
connection generalises to a wide family of categories, and models such
structures as multisorted theories, categories with structure, term
rewriting systems.

In this formulation, a central role is played by initial algebras, as they
form the free monad mentioned above. The limit of this approach consists
in the fact that initial algebras naturally carry some finitary flavour,
whereas in the computer science practice one often seeks infinite terms,
which arise dually as final coalgebras.

The talk will present the classical theory in suitable generality, and
then focus on some of its possible dualisations, involving coalgebras.

To main page

October 17,2003 *Dimitri Hendriks*: Adbmal.

Joint work with Vincent van Oostrom.Formalisation in
Coq

Abstract:We make the notion of scope in the *lambda*-calculus explicit.
To that end, the syntax of the *lambda*-calculus
is extended with an end-of-scope operator *adbmal*,
matching the usual opening of a scope due to *lambda*.
Accordingly, *beta*-reduction is extended to the
set of scoped *lambda*-terms
by performing *minimal* scope extrusion
before performing replication as usual.
We show confluence of the resulting scoped *beta*-reduction.
Confluence of *beta*-reduction for the ordinary
*lambda*-calculus is obtained as a corollary,
by extruding scopes *maximally* before
forgetting them altogether.
Only in this final forgetful step,
*alpha*-equivalence is needed.
All our proofs have been verified in Coq.

To main page

October 30,2003 *Gilles Dowek*

Abstract: Joint work with Ying Jiang.

We give a new proof of a theorem of Mints that the positive fragment
of minimal intuitionistic logic is decidable. The idea of the proof is
to replace the eigenvariable condition by an appropriate scoping
mechanism. The algorithm given by this proof seems to be more
practical than that given by the original proof. A naive
implementation is given at the end of the paper. Another contribution
is to show that this result extends to a large class of theories,
including simple type theory (higher-order logic) and second order
propositional logic. We obtain this way a new proof of the
decidability of inhabitation for positive types in system F.

To main page

November 14,2003 *Sonja Smets*

Abstract:
**
Part I: From Quantum Physics to Operational Quantum Logic.
**

We offer an introduction to "operational quantum logic" (OQL), i.e. the Geneva approach to the logical foundations of physics that originated with the work of C. Piron and J.M. Jauch. Our main point is to explain Piron's statement that "the mathematical language of lattices is appropriate for the formulation of the postulates of general quantum physics".

Firstly, we build up the OQL-language by starting from the basic notions of "yes/no questions" and "physical properties" and ending with the notion of a "property lattice". We focus on the motivation for introducing the OQL-language, i.e. the attempt to describe a physical system in terms of its "elements of reality", referring to the 1935 EPR-paper. Particular attention will be paid to the notions of measurability and operationality. We stress that in this language, the possible realisations or states of a physical system do not play a privileged role any longer. This point will be illustrated by going into the details of the so-called "state-property" dual description of a physical system.

Secondly, we discuss the origin of the 3 basic OQL-axioms needed to describe physical system. We will add the axiom of "weak modularity" specific for quantum systems and give a possible physical interpretation. We end with the link to standard quantum mechanics by briefly going over C. Piron's representation theorem. This theorem states that a property lattice which is complete, atomic, orthocomplemented and weak modular, which satisfies the covering law and some additional properties (i.e. the lattice should be irreducible and of a sufficient dimension) can be represented in the form of the lattice of closed linear subspaces of a generalized Hilbert space (see Piron 1976).

C. Piron, Foundations of Quantum Physics, W.A. Benjamin Inc., Massachusetts
1976.
**
Part II: On the Logicality of Quantum Systems.
**

We will refer back to the first part of this talk containing a short introduction to "Operational Quantum Logic" (OQL), i.e. the Geneva approach to the logical foundations of physics.

Firstly, we focus on the differences between the logical descriptions of classical and quantum physical systems. In particular we will look at the specific state-property dual description of a classical physical system and of a quantum physical system. We will show how the compatibility of properties entails the distributive identity and how the incompatibility of properties entails the weak modular identity.

Secondly, we pay attention to the "implication"-problem in quantum logic. First we focus on the classical or intuitionistic cases, and observe that one introduces an implication connective as satisfying: "c ∧ a <= b iff c <= a → b". We will refer back to Skolem's theorem stating that any lattice with a binary connective satisfying this equation is necessarily distributive. Since this particular equation entails one form of the deduction theorem, we see that in the non-distributive weak modular case both this equation and consequently the deduction theorem fail (see for instance Dunn & Hardegree 2001). Quantum logicians have looked for ways out of this problem, we will present some of their proposals and pay particular attention to the so-called Sasaki Hook. We end with another proposal for a way out of the implication problem, presented in Coecke & Smets (nd). In particular the above equation should be replaced with another duality, called "the Sasaki duality", such that any ortholattice with a binary connective that satisfies it, is necessarily weak modular. We will pay specific attention to this Sasaki duality and show how it entails the motivation for a dynamic extension of OQL with labelled dynamic implications. Such dynamic implications hand us a new perspective on the quantum deduction theorem problem.

B. Coecke & S. Smets (nd): "The Sasaki Hook is not a [static] Implicative Connective but Induces a Backward [in Time] Dynamic One that Assigns Causes", International Journal of Theoretical Physics, to appear (quant-ph/0111076)

J.M. Dunn & G.H. Hardegree, Algebraic Methods in Philosophical Logic, Oxford
University Press Inc, NY 2001.

To main page

November 28,2003:*Philipp Gerhardy*:Refined complexity analysis of cut elimination.

Abstract:We give a refined analysis of cut elimination and
investigate in detail the role of (1) nested quantifiers
(vs. propositional connectives), (2) alternating quantifiers
(vs. quantifier blocks) and (3) contractions in the complexity of
cut elimination, i.e. the depth of the cut free proof in terms of
the depth of the original proof. We show that the non-elementary
complexity of cut elimination depends on a combination of both
nested, alternating quantifiers in cut formulas and contractions on
ancestors of such cut formulas, while in the absence of either cut
elimination is elementary. Finally, we briefly show that with the
refined analysis the upper bound and Statman's lower bound on cut
elimination coincide.

To main page

November 28,2003:*Clemens Kupke*:Completeness for Coalgebraic Modal Logic via Stone Duality.

Abstract:Coalgebras have been studied as a general approach to dynamic systems.
Modal logic seems to be a natural choice for a specification language for
coalgebras. Given an endofuntor T the problem is how to define a suitable
modal logic for T-coalgebras. Following an approach by Pattinson we first
define for an arbitrary endofunctor T:Set ---> Set a modal logic and
briefly discuss (sufficient) conditions for that logic to be sound,
complete and expressive. We then translate this approach to the case in
which we are given a functor T:Stone ---> Stone where Stone denotes the
category of Stone spaces. We now obtain a better understanding of the
above mentioned results of Pattinson: First we show that any coalgebraic
modal logic gives rise to a functor L:BA --> BA, such that the category of
L-algebras provides us an algebraic semantics for the logic. It then turns
out that Pattinson's above mentioned conditions for soundness,
completeness and expressiveness of the logic are in fact equivalent to L
being the Stone dual of the functor T.

To main page

December 12,2003:*Philip Welch*:Infinite games of perfect information and Quasi-inductive definitions.

Abstract:The connection between Gale-Stewart Games of perfect information played on
integers, with open (F_sigma) payoff sets and monotone inductive operators
is well documented through results of Gale & Stewart (respectively
Solovay, using analytic operators). We consider the problem of deciding
whether /arithmetical quasi-inductive operators/ have a similar
characterisation. Such operators have emerged in diverse areas of
philosophical logic and theoretical computer science.

To main page

January 16,2004:*Arthur Apter*:Some Results Concerning Strong Compactness and Supercompactness.

Abstract:The existence of strongly compact and supercompact cardinals is
a so-called large cardinal axiom. Large cardinal axioms are statements
about the richness of the set-theoretic universe that cannot be proved in
the usual (Zermelo-Fraenkel) axiomatization of set theory. In my talk, I
will discuss the nature of different universes of set theory in which
strongly compact and supercompact cardinals can exist, surveying known
results, and mentioning future directions for research.

To main page

January 16,2004:*Sergei Artemov*:

Abstract:New term operations discovered in the Logic of Proofs have been used to
build an extension of the typed lambda-calculus and typed combinatory
logic by new principles enabling a system to internalize its own
derivations as new terms. We will also discuss semantics and possible
applications of the resulting Reflexive Combinatory Logic.

To main page

February 13,2004:*Klaas Pieter Hart*:Embeddability of the measure algebra

Abstract:It is a theorem of Parovicenko that every Boolean algebra of
cardinality $\aleph_1$ (or less) can be embedded into the
quotient algebra $P(\omega)/fin$ and so, under CH, the latter
algebra is universal for Boolean algebras of cardinality $c$ (or less).
The question whether the CH assumption can be removed for various
individual algebras attracted lots of attention.
In this talk we show that the measure algebra need not be embeddable
into $P(\omega)/fin$ and discuss the assumption under which this occurs.

To main page

March 2,2004:*Nicola Gambino*:Wellfounded Trees, Fixpoints and Free Monads

Abstract:
Types of wellfounded trees, or W-types, are one of the most important
components of modern type theories. For example, W-types allow us to
represent many inductively defined sets in type theory.
In this talk, I will study some on the consequences of the assumption
of W-types in a type theory. To do so, I will investigate the categorical
notion of W-type recently introduced by Moerdijk and Palmgren. The main
result of the talk shows that W-types allow us to define initial algebras
for a wide class of endofunctors on locally cartesian closed categories.
As a corollary, we derive some results concerning fixpoints and free monads.
This is joint work with Martin Hyland.

To main page

March 12,2004:*Claire Kouwenhoven*:The algebraic set theory of the effective topos

Abstract:
Following the book "Algebraic set theory" from Andre Joyal and Ieke Moerdijk, we
give a characterization of the initial ZF-algebra, for toposes equipped with a
class of maps which gives rise to a model of IZF. We show in particular that,
for the effective topos, this model is isomorphic to the one proposed by Charles
McCarty in his Ph.D. thesis "Realizability and recursive mathematics".

To main page

March 22,2004:*VILEM NOVAK*:Mathematical Principles of Fuzzy Logic

Abstract:
This talk is a brief overview of fundamental concepts of the mathematical
fuzzy logic. The key idea behind fuzzy logic is the idea of grades
standing behind our reasoning when dealing with various aspects of the
vagueness phenomenon.

Mathematical fuzzy logic is not a unique theory but a group of formal
theories based on various kinds of structures of truth values. The
starting point is the structure of residuated lattice. Its extensions
provide various kinds of fuzzy logics. In the talk, we will briefly
characterize the fundamental structures of truth values. Then, we will
focus on three essential formal systems:

1. Basic fuzzy propositional and predicate logic (BL-logic).

2. Fuzzy propositional and predicate logic with evaluated syntax (based on
Lukasiewicz MV-algebra of truth values).

3. Higher order fuzzy logics (fuzzy type theory).

All fuzzy logics enjoy the completeness property. Because of the
completeness, fuzzy logic is suitable for various kinds of applications.
We will only metion formalisation of the sorites paradox which plays a
crucial role in a ll discussions on the vagueness phenomenon.

To main page

April 16,2004:*Nick Bezhanishvili*:The logic of the Rieger-Nishimura ladder

Abstract:
This talk will be about the intermediate logic L(N) of
the Rieger-Nishimura ladder N. I will give an overview of results
regarding finite axiomatization, the hereditary finite model property,
and decidability. I will also present a criterion of local
tabularity of extensions of L(N).

This is joint work with Guram Bezhanishvili.

To main page

May 14,2004:*Andreas Weiermann*:Classifying the phase transition for Ackermannian Paris Harrington
functions

Abstract:
It is well known that the Paris Harrington Ramsey function (for graphs) is
Ackermannian. Assume that this Ramsey function is paramatrized with
respect to a number theoretic function $f$ so that the largeness condition
is replaced by a corresponding $f$-largeness condition. Using lower bounds
for the standard Ramsey function (which depend crucially on Erdös's
famous probabilistic method)
we show that the resulting Ramsey function is still Ackermannian when $f$
has the form $f(i)=\frac{\log(i)}{A^{-1}(i)}$ where $A^{-1}$ denotes the
inverse of the Ackermann function. This result is sharp since for any
weakly increasing primitive recursive function $g$ the resulting Ramsey
function is primitive recursive if $f$ has the form
$f(i)=\frac{\log(i)}{g^{-1}(i)}$.

To main page

To main page