This is the homepage of the "Logic Seminar" here at BRICS. We meet (currently every week) on Thursday at 11:15, this semester in the seminar room at B4.
The seminar maintains a mailing list called logic-seminar. Mails send to logic-seminar@brics.dk are directly redirected to all the members of this list. If you want to be on this list (or off), contact one of the persons in charge of the seminar (see bottom of the page).
History so far / Current and next seminars:
"Induction for decidable $\Delta_1$ relations"
An open problem formulated by J. Paris is whether $\Delta_1$ induction schema implies $\Sigma_1$-collection over elementary arithmetic. We obtain a reduction of this question to a purely recursion-theoretic one, related to bounded-query oracle computations. We also prove that $\Delta_1$-induction schema is independent from the set of all true $\Pi_2$-sentences, which strengthens a well-known theorem of Parsons.
In the late 70s S. Feferman introduced a
mathematically strong system
S for classical mathematics
(and in particular analysis) and showed that S is conservative
over Peano arithmetic PA (related systems were also
investigated by G. Takeuti). S is formulated in the language of
arithmetic in all finite types (with induction restricted to
arithmetical formulas) and based on a non-constructive
µ-operator. The conservation proof uses Gödel's functional
interpretation relative to µ.
In this talk we survey some of our work which was stimulated by
Feferman's paper: systems in the language of finite types allow a
rather direct formalization of important analytical concepts and
functional interpretation, because of its good behaviour with
respect to the logical deduction rules (`modularity'), is a very
useful tool to extract constructive data out of given proofs. For
these data to be of mathematical relevance it is important to keep
their numerical complexity low (in particular well below general
alpha(<epsilon_0)-recursion). This led to the study of
systems of finite type which still allow to formalize substantial
parts of analysis, but which also guarantee the extractability of
primitive recursive, elementary recursive and even polynomial data.
The extraction process is based on a monotone functional interpretation,
a new method to exhibit the computational content of fragments of
arithmetical comprehension and the use of non-standard axioms.
In this talk we
Last time, we went as far as it's reasonably possible to go by
starting from the bottom and going up.
This time, I'll talk about some of the other ways of trying to define
the boundary. I'll definitely talk about indescribable cardinals
(which allows me to bring in the alarming notion of transfinitely higher
order logic), and measurable cardinals, the most important of all
large cardinals. I might also mention partition (Erdos, Ramsey) cardinals
and compact cardinals.
Measurable cardinals are interesting for a variety of reasons. One
reason is that it took twenty-five years to find out that they were
actually large. Another is that their existence, or non-existence, has
an impact on what look like normal mathematical
statements---specifically, Lebesgue measurability of sets of real
numbers. The existence of a measurable cardinal also implies some
slightly startling things about sets of integers in the constructible
universe. (I'll explain what that is.)
Ever since Cantor discovered that some infinities are bigger than
others, set theorists have been trying to discover (or decide) where
the boundaries of the set-theoretic universe lie.
In these talks, I'll take you on a trip round the various boundary
posts, which are increasingly large cardinals with increasingly silly
names. (Almost no set-theoretic formulae will appear; this is
concepts only!)
In the first part of the trip, we start from home, and head towards
what looks like the farthest point. But every time we reach a boundary
post, somebody says it's not the real boundary .. and somebody else
suggests we're hallucinating the whole experience anyway.
The boundary posts we meet on this part are the inaccessible,
hyperinaccessible, Mahlo and hyper-Mahlo cardinals.
Heyting algebras are the algebraic counterpart of intuitionistic
propositional logic (IPL), in the same way as Boolean algebras model
classical propositional logic. In recent years research on Heyting
algebras has been revitalised by Andy Pitts'
uniform interpolation theorem, which in its syntactic form
states that IPL has not only interpolation property, but there exist
both least and greatest interpolants. In algebraic terms, every
morphism between (finitely presented) Heyting algebras has both
adjoints.
In this talk I will briefly survey recent research, including my own:
Every finitely presented Heyting algebra is co-Heyting: there exists
an operation `supplement' satisfying equations dual to those of
implication (this extends a theorem of S. Ghilardi). We give some
insight in the structure of finitely presented Heyting algebras, and
show the existence of a duality, simpler than Priestley
duality.
Most of the material presented in this talk is contained in my recent
preprint on finitely presented Heyting algebras
(heyting.ps.gz).
Intuitively, the fan theorem states that every finitely branching tree
all whose branches are finite is itself finite. It is important in
constructive mathematics, since considerable fragments of analysis can
be reconstructed using it.
We will explore different formulations of the fan theorem with the aim
of finding one which can easily be represented in a particular formal
system.
Fix a class C of finite structures (e.g., graphs, permutations, trees). C has a *convergenge law* with respect to a logic L if every sentence in L has an asymptotic probability in randomly chosen structures from C. If, in addition, the asymptotic probability is always 0 or 1, C has a *0-1 law* with respect to L. The mathematical methods used to show convergence and 0-1 laws are closely related to methods used in average case analysis of algorithms. We will survey some of the research directions in this area. We will also discuss applications to approximability of functions in the complexity classes MAX P and #P.