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, 1985

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.

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