September 30: Edwin Mares: Semantics for Quantified Substructural Logic
16.00--17.00
Abstract:
Previous attempts to produce a semantics for quantified relevant logic have met with mixed success. The intended logics turned out to be incomplete over Routley and Meyer´s constant domain semantics. And Fine´s increasing domain semantics, although ingenious, is extremely complicated and inflexible. The present model theory is much simpler and more flexible. It uses general frames, which have an algebra of propositions in addition to the usual set of worlds. It seems straightforward to adapt this semantics to many logics the propositional fragment of which have a worlds semantics. If time permits, the modification of this semantics to treat other substructural logics, such as BCK and Linear Logic, will be discussed.
To main page

October 14: Nikolay Vereshchagin: Game semantics for intuitionistic propositional calculus IPC
16.00--17.30
Abstract:
The first game semantics of IPC is due to P. Lorentzen, who assigned to every propositional formula a certain game between two players, Proponent and Opponent, such that Proponent has a winning startegy in the game iff the formula is derivable in IPC.
Recently, Ilya Mezhirov (a student at Moscow University) significantly simplified and improved Lorentzen games. For Mezhirov's games the completeness and soundness proofs are rather easy.
Another semantics was proposed by G. Japaridze. The variables of a propositional formula are interpreted as games of quite general type between two players and connectives as certain operations over games of that type. A formula is called `computable' if for all games substituted for variables the Proponent has a winning strategy. Every derivable (in IPC) formula is `computable' but the converse is unknown.
To main page

October 14: Jaap van Oosten: A general form of relative recursion
16.00--17.00
Abstract:
We generalize the notion of "recursive in" to arbitrary partial combinatory algebras (pcas). For every pca A and partial function f:A-->A a new pca A[f] is constructed in which the function f is representable by an element. A universal property of this construction is formulated in terms of J.Longley's 2-category of pcas and decidable applicative morphisms. Applications will be given. A surprising corollary is, that in Longley's category, every total pca is isomorphic to a nontotal one. See here for the paper.
To main page

December 2: Jamie Gabbay: One-and-a-Halfth order logic
16.00--17.00
Abstract:
Abstract: One-and-a-halfth order logic is a first-order logic with explicit variables ranging over formulae (*formula variables*). There is no quantification over these variables but they can be substituted for, allowing us to reason weakly about classes of first-order formulae. Substitution for formula variables does not avoid capture by quantified variables, giving the logic something of the flavour of cylindric algebra, though it is given by a sequent presentation (with cut-elimination) which I shall discuss.
Some of the proofs are quite beautiful and, time permitting, I will sketch them.
I will briefly describe how one-and-a-halfth order logic emerges from a novel algebraic specification of first-order logic which we are developing at Eindhoven, and I will describe precise relationships with cylindric algebras and with first-order logic.
Slides will be on my web page before the talk.
To main page

December 9: Greg Restall: Proofnets for S5: sequents and natural deduction for modal logic
16.00--17.00
Abstract:
In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery (to take account of the modal vocabulary) is directly motivated in terms of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising.
To main page

January 6: Bas Spitters: Observational Integration Theory
16.00--17.00
Abstract:
In this talk I will present a constructive theory of integration. The theory is constructive in the sense of Bishop, or Brouwer. However we avoid the axiom of countable, or dependent, choice. Thus our results can be interpreted in any topos.

To be more precise we outline how to develop most of Bishop's theorems on integration theory that do not mention points explicitly. Coquand's constructive version of the Stone representation theorem is an important tool in this process. It is also used to give a new proof of Bishop's spectral theorem.

This talk illustrates the general theme of developing mathematics observationally, connection ideas by Kolmogorov, von Neumann and Segal on the one hand and point-free (aka formal) topology on the other. I think this provides a nice illustration how ideas from logic (proof theory) can be used to obtain mathematical results.

Finally, I will show (by constructing a model) that in this context the reals can not be proved to be uncountable and show how we live with this fact.
To main page

January 6: Milad Niqui: Exact Real Numbers in Coinductive Type Theory
16.00--17.00
Abstract:
In this talk I will discuss a type theoretic formalisation of normalisation algorithm of Edalat and Potts for lazy exact real arithmetic. I will present general form of the algorithm as the specification of a map between coinductive types of streams and that of expression trees. I will distinguish two methods of formalising the algorithm in constructive type theory: semantic and syntactic approach. Finally I show how a further categorical/type theoretic notion of coinduction--recursion is needed to be able to formalise the general form of the algorithm.
To main page

February 24: Asger Tornquist: Construction of non-conjugate actions
16.00--17.00
Abstract:
It is a classical result that all conjugacy classes in the group of all measure preserving transformations on [0,1] are meagre, and that the generic transformation is ergodic. Foreman and Weiss showed that the conjugacy relation for ergodic transformations does not allow classification by countable structures, and more recently, Foreman, Weiss and Rudolph showed that it is a complete analytic relation. In this talk, I will present a modest attempt at extending some of these results to actions of any countable group. We will show that every countable group has "E_0 many" ergodic measure preserving a.e. free actions on [0,1], thus showing that the conjugacy relation is never concretely classifiable. In particular, it follows that any countable group has continuum many such actions.
To main page

March 3: Robert Lubarsky: Notions of reals in Constructive ZF
16.00--17.00
Abstract:
As so often happens when changing the logic from classical to intuitionistic, many classical results about the reals are no longer valid for the intuitionistic reals. This talk will discuss how the Dedekind reals can be different from the Cauchy reals, how a Cauchy real may fail to have a modulus of convergence, and other related results.
To main page

April 21: Saeed Salehi: Modal Logic of Cut-Free Provability in Weak Arithmetics
15.00--16.00
Abstract:
Normal propositional modal logics are usually formalized by some set of modal axioms containing the axiom

(K)   ¤(A → B) → (¤A → ¤B)
plus the rule of necessitation
(RN)   A / ¤A
over the classical propositional calculus. The Gödel-Löb logic, which is known to be the provability logic of sufficiently strong arithmetical theories such as Peano's arithmetic or primitive recursive arithmetic, is then obtained by adding Löb's axiom
(L)   ¤(¤A → A) → ¤A
to K. When the modal operator ¤ is interpreted as cut-free provability in weak arithmetics (where the exponentiation function is not total) then the axiom (K) does not hold. For considering these provability logics (with weaker provability predicates over weaker theories) one is inclined to study non-normal modal logics.
In this talk, we review the theory of minimal modal logic E which is axiomatized by the single rule of inference
(RE)   (A ↔ B) / (¤A ↔ ¤B)
over classical propositional calculus. Then we will see that the normal modal logic K is obtained from E by adding the axioms
(M)   ¤(A & B) → ¤A & ¤B  
and
(C)   ¤A & ¤B → ¤(A & B)  
and the necessitation rule (RN).
While (M) and (RN) are still valid for cut-free provability of weak arithmetics, we observe that (C) is not: for getting a cut-free proof of A&B out of a cut-free proof p of A and a cut-free proof q of B, we should merge p and q together and perform some arithmetical operations which could be too costly to be handled in our weak arithmetic. Loosely speaking, the axiom (K) is a kind of formalized cut rule, which should not hold is those arithmetics that cannot prove the equivalence of cut-free provability with the usual Hilbert-style provability. We note that the cost of cut-elimination is of (super-)exponential in proof theory.
We also introduce another axiom (S) valid for Herbrand provability in IΔ0, and derive Gödel's Second Incompleteness Theorem for Herbrand Consistency of IΔ0; that is the unprovability of the Herbrand Consistency of IΔ0 in itself.
To main page

April 21: Roland Hinnion: Positive Set Theories
16.00--17.00
Abstract:
Positive set theories can be seen as solutions to the set theoretical paradoxes, via a weakening of the (dangerous) strength of the classical negation ; this in contrast to the other paths (like ZF or NF). Several versions have been studied , among which some are closely related to fields and subjects disseminated as well in space as in time (non-exhaustive list): partial sets, paradoxical sets, approximable sets, naïve sets in non-classical logics , partial information , contradictory information.

A characteristic of these theories is that (generally) they are easy to modelize as long as one does not expect the models to satisfy identity criteria ,but much harder to modelize when such expectations are present. In particular are there still several open problems wrt this, namely in the case of the partial sets (equivalently: naïve sets in paracomplete logics); while the 2 main other "branches" (the "classical" and the "paradoxical" ones) present very rich modelisation possibilities (as well term models as topological models,satisfying identity criteria).

The talk will give an overview of the present situation, for the 3 "branches" (classical, partial, paradoxical) , taking in account:
- the importance of the kind of formal language that is involved,
- the type of identity criteria that can be used (extensionality / intensionality)
- the modelisation possibilities (term models / topological models) .
The talk will be self-contained and an adequate bibliography will be available.
To main page

May 12: Marek Kwiatkowski: Ordinal arithmetic via infinitary term rewriting
15.00--16.00
Abstract:
The talk has three parts. First, we introduce the audience to the framework of term rewriting, a Turing-complete model of computation underlying the design of functional programming languages. Then infinitary term rewriting, a relatively recent extension of this model, is presented. Finally we give an infinitary term rewriting system encapsulating ordinal arithmetic on a stretch of countable ordinals with the use of fundamental sequences. Rewriting-related properties of this system and its expressive power are discussed.
To main page

May 12: Joost Joosten: Computational complexity and short proofs of consistency statements
16.00--17.00
Abstract:
In this talk I shall discuss connections between various fields of logic. First, I shall make some comments on links between computational complexity and arithmetics. Next I shall dwell on the relation between propositional logic and computational complexity.
This shall culminate in a beautiful theorem by Pudlák and Krajicek relating optimal propositional proof systems to poly-time axiomatized theories that prove in a short way all finite consistency statements of all poly-time axiomatized theories. I shall sketch a proof of this theorem and talk about new results that I obtained in this direction.
Although this abstract uses many difficult words, I think I can present parts of the talk on a pretty elementary level. I even wrote a popular mathematical text (in Dutch) on the above mentioned theorem of Pudlák and Krajicek which can be found in this report list or here in pdf format.
To main page

To main page