Logic Colloquium 2007 (Wrocław, Poland, July 14-19, 2007):
Tentative Schedule
Color Coding:
Joint LICS/LC Long
Talks:
Martin Hyland
(Cambridge):
Combinatorics of Proofs (chair: Andy Pitts)
Abstract: Ideally interpretations of proofs should
exhibit some essential combinatorial features in an interesting and
appealing way. As a case study, one can consider the notion of innocent
strategy which is the basis for a game semantical interpretation of
proofs and programmes. Some combinatorial content of this notion is
sketched in the joint LICS paper accompanying this talk, whose abstract
reads as follows.
We show how to
construct the category of games and
innocent strategies from a more primitive category of games. On that
category we define a comonad and monad with the former distributing
over the latter. Innocent strategies are the maps in the induced
two-sided Kleisli category. Thus the problematic composition of
innocent strategies reflects the use of the distributive law. The
composition of simple strategies, and the combinatorics of pointers
used to give the comonad and monad are themselves described in
categorical terms. The notions of view and of legal play arise
naturally in the explanation of the distributivity. The
category-theoretic perspective provides a clear discipline for the
necessary combinatorics.
There are other
instances of a kind of categorical
combinatorics of proofs, but in this talk I shall restrict myself to
the one instance.
Colin Stirling (Edinburgh): Higher-Order
Matching, Games and Automata (chair: Luke Ong)
Abstract: We describe a particular
case where methods such as model-checking as used in verification
are transferred to simply typed lambda calculus. Higher-order
matching is the problem given t=u where t, u are terms of
simply typed lambda-calculus and u is closed, is there a substitution S
such that tS and u have the same normal form with respect to beta
eta-equality: can t be pattern matched to u? In the talk we
consider the question: can we characterize the set of all
solution terms to a matching problem? We provide an
automata-theoretic account that is relative to resource: given a
matching problem and a finite set of variables and
constants, the (possibly infinite) set of terms that are built
from those components and that solve the problem is regular. The
characterization uses standard bottom-up tree automata. However, the
technical proof uses a game-theoretic characterization of
matching.
Joint LICS/LC Short Talks:
Cristiano
Calcagno (Imperial College):
Can Logic Tame Systems Programs? (chair: Luke Ong)
Abstract: We report on our experience on designing
and implementing tools for automatic reasoning about safety of systems
programs using separation logic. We highlight some of the fundamental
obstacles that need to be overcome, such as the complexity of data
structures and scalability of the methods, on the path to realistic
systems programs.
Martín Escardó (Birmingham):
Infinite Sets that Admit Exhaustive Search I (Part II will be given as
a LICS talk at 5 p.m.) (chair: Luke Ong)
Abstract: Perhaps surprisingly, there are infinite
sets that admit mechanical exhaustive search in finite time. We
investigate three related questions: (1) What kinds of infinite sets
admit exhaustive search? (2) How do we systematically build such sets?
(3) How fast can exhaustive search over infinite sets be performed?
We give answers to
them in the realm of Kleene-Kreisel higher-type computation: (1)
involves the topological notion of compactness, (2) amounts to the
usual closure properties of compact sets, including the Tychonoff
theorem, (3) provides some fast algorithms and a conjecture.
These two talks
include my contributed LICS paper, but go beyond in two respects: a
general introduction to the role of topology in computation is given,
and a few new results are included, such as an Arzela-Ascoli type
characterization of exhaustible sets.
Rosalie Iemhoff (Utrecht): Skolemization in
Constructive Theories (chair: Andy Pitts)
Abstract: It has long been known that Skolemization
is sound but not complete for
intuitionistic logic. We will show that by slightly extending the
expressive power of
the logic one can define a
translation that removes strong quantifiers from predicate formulas and
that is
related but not equal to
Skolemization. Since the extended logic is constructive, the
translation can be considered as an
alternative to Skolemization
for constructive settings. The result easily implies an analogue of
Herbrand's theorem.
We will apply the method to
various constructive theories and compare it to other Skolemization
methods and
related translations like the
Dialectica Interpretation.
Alex Simpson (Edinburgh): Non-well-founded Proofs
(chair: Andy Pitts)
Abstract: I will discuss various situations, arising
in computer science, mathematics and logic, in which one is naturally
led to consider associated proof systems involving interesting forms of
non-well-founded proof.
Tutorial
speakers:
Steve Jackson
(North Texas): Cardinal
Arithmetic in L(R) (chair: Alessandro Andretta)
Abstract: In this series of talks we will survey the
cardinal structure of the model L(R) assuming the axiom of determinacy.
We describe the close relationship between the cardinal structure and
partition properties of the odd projective ordinals. We will present
some recent simplifications to the presentation of this theory, as well
as a result connecting the cardinal structure of L(R) to that of the
background universe V. We will attempt to make the talks as
selfcontained as possible.
Bakh Khoussainov (Auckland): Automatic
Structures (chair: Steffen Lempp)
Abstract: We study automatic structures. These are
infinite structures that have automata presentations in a precise
sense. By automata we mean any of the following: finite automata, tree
automata, Büchi automata and Rabin automata.
Automatic
structures possess a number of interesting algorithmic, algebraic and
model-theoretic properties. For example, the first order theory of
every automatic structure s decidable; automatic structures are closed
under the first order interpretations; also, there are
characterizations theorems for automatic well-founded partially ordered
sets, Boolean algebras, trees, and finitely generated groups. Most of
these theorems have algorithmic implications. For instance, the
isomorphism problem for automatic Boolean algebras is decidable.
The first lecture
covers basic definitions and presents many examples. We explain the
decidability theorem that describes extensions of the FO logic in which
each automatic structure has a decidable theory. The second lecture
surveys techniques for proving whether or not a given structure can be
presented by automata. We also talk about logical characterizations of
automatic structures. The last lecture concentrates on complexities of
automatic structures in terms of well-known concepts of logic and model
theory such as heights of well-founded relations, Scott ranks of
structures, and Cantor-Bendixson ranks of trees.
Most of the
results are joint with Liu, Minnes, Nies, Nerode, Rubin,
Semukhin, and Stephan.
Kobi Peterzil (Haifa): The Infinitesimal
Subgroup of a Definably Compact Group (chair: Ludomir Newelski)
Abstract:
Consider the compact Linear
group G=SO(3,R).
When G is viewed in any nonstandard real closed field, the set G^{00}
of
all matrices in G which are infinitesimally close to the identity
forms a
normal subgroup. Endow the quotient G/G^{00}
with a
"logic topology",
whose closed sets are those whose preimages in G are type-definable. It
is easy to see that G/G^{00}, with this
logic topology, is isomorphic to SO(3,R),
with the
Euclidean topology.
Several years ago,
A. Pillay conjectured that a
similar phenomenon
should be
true for every "definably compact" group in an arbitrary o-minimal
structure, even if the group itself was not defined
over the real numbers. Roughly speaking, Pillay conjectured that every
definably
compact group G in a sufficiently saturated o-minimal structure has
a canonical
type-definable normal subgroup G^{00}
such that the group
G/G^{00},
when endowed with the logic topology as above, is isomorphic to a
compact real Lie group.
Moreover, the real dimension of this Lie group equals the o-minimal
dimension of G.
My goal in these
talks is to show, with the help of
examples, how the
interaction between different notions, such as o-minimality,
Lie groups, compactness, measure theory, and Shelah's Independence
property,
yields a solution to the conjecture.
For
background on o-minimality, see
van den Dries's book [2] below. For
Pillay's
conjecture, see [6]. For
key-steps in the solution to the conjecture, see [1,5,3,4].
1. A. Berarducci, M. Otero, Y.
Peterzil, and A. Pillay, A descending
chain
condition for groups in -minimal structures, APAL 134 (2005), 303-313
2. L. v.d. Dries, Tame topology and
o-minimal structures, Cambridge U.
Press, New York, 1998
3. M. Edmundo and M. Otero,
Definably compact abelian groups, J.
Math. Logic 4 (2004), 163-180.
4. E. Hrushovski, Y. Peterzil and A.
Pillay, Groups, measure and the
NIP,
J. AMS.
5. Y. Peterzil and A. Pillay,
Generic sets in definably compact groups,
Fund. Math. 193 (2007), 153-170
6. A. Pillay, Type-definability,
compact Lie groups, and -minimality,
J. Math. Logic 4 (2004), 147-162
Invited Speakers:
Albert
Atserias (Barcelona): Structured Finite Model Theory (chair: Jurek Marcinkowski)
Abstract: Many of the classical results of model
theory, most notably some of the direct consequences of the Compactness
Theorem, fail badly in restriction to finite structures. A classical
example is the Łoś-Tarski preservation-under-substructures Theorem,
which is known to fail in the finite. Motivated by certain
application-areas in computer science and combinatorics, it has been
argued that it might be profitable to consider some further
restrictions beyond finiteness. What classical theorems of model theory
hold on classes of finite trees? or finite planar graphs? or finite
structures of bounded treewidth? or, more generally, minor-closed
classes of finite graphs? The goal of our talk is to give an overview
of the recent results in this area. Interestingly, many of these
results have at its heart an application of Gaifman's Locality Theorem,
which seems to play in this area a role comparable to the one
played by the Compactness Theorem in classical model theory.
Matthias Baaz (Vienna): Towards a Proof Theory of
Analogical Reasoning (chair: Pavel Pudlák)
Abstract: In this lecture we compare three types of
analogies based on generalizations and their instantiations:
- Generalization w.r.t. to invariant parts of proofs (e.g., graphs
of
rule applications etc.).
- Generalization w.r.t. to an underlying meaning. (Here proofs and
calculations are considered as trees of formal expressions. We analyze
the well-known calculation of Euler demonstrating that the 5th Fermat
number is compound.)
- Generalization w.r.t. to the premises of a proof. (This type of
analogies is especially important for juridical reasoning.)
We
show that proof transformations of this kind are essential for the
development of a proof theory of analogical reasoning.
Vasco Brattka (Cape Town): Computable Analysis
and Effective
Descriptive Set
Theory (chair: Steffen Lempp)
Abstract:
Computable analysis can be
considered as an extension of computability theory to
infinite objects such as real numbers, continuous functions and
closed subsets that are studied in analysis. In a similar
way as discrete degrees of non-computability can be
classified in the arithmetical hierarchy, the
corresponding hierarchy for such classifications in analysis is the
Borel
hierarchy. Thus, it is natural to expect a fruitful
interaction between effective descriptive set theory and computable
analysis. In this talk we present an extension of the
Representation Theorem of computable analysis to effectively
Borel measurable maps. This theorem allows to introduce
a conservative extension of the notion of effective
Borel measurability to admissibly represented topological
spaces as they are used in computable analysis. A resulting
notion of reducibility for functions is described and techniques of
completeness proofs from computability theory can be
imported into this branch of effective descriptive
set theory. We apply these techniques to characterise
the degree of non-computability of topological operations
such as the closure, the interior, the boundary and
the derived set operation with respect to hyperspace
representations for computable metric spaces.
[1] Vasco
Brattka.
Effective Borel measurability and reducibility
of functions. Mathematical Logic Quarterly,
51(1):19-44, 2005
[2] Vasco Brattka and Guido Gherardi.
Borel
complexity of topological
operations on computable metric spaces. In
S.B. Cooper, B. Löwe, and A. Sorbi (eds.), Computation
and Logic in the Real World, vol. 4497, LNCS,
Springer, Berlin, 2007
Zoé Chatzidakis (Paris
7): Model Theory of Difference Fields, and Some Applications (chair:
Ludomir Newelski)
Abstract: A difference field is a field with a
distinguished autormosphism. I will first give a survey of the model
theory of the existentially closed difference fields, and then of some
application(s) to diophantine geometry. The main tool for applications
is the dichotomy theorem, and I will spend some time explaining what
are its consequences in the particular context of difference fields,
and how they can be used.
Gabriel Debs (Paris 6): Coding Compact Spaces of
Borel Functions (chair: Sławomir Solecki)
Abstract: Let B(X) denote the space of all Borel
functions on some Polish space X, equipped with the pointwise
convergence topology (i.e. the topology induced by the product topology
on R^{X}). When X is
uncountable the space B(X) is clearly non metrizable. But it follows
from the early work of Rosenthal and Bourgain-Fremlin-Talagrand that
the compact subspaces of B(X)
possess many metric-like properties : For example most of the standard
topological notions admit sequential formulations. Notice that such a
compact space K needs not to be metrizable even if it is separable.
However in this latter case, one can equip K with some natural
“descriptive structures” that we shall describe in more detail in this
talk. One consequence of the main result that we shall present here is
that all these structures are actually “equivalent” in some sense. This
will also provide a positive answer to a question asked by Argyros,
Dodos and Kanellopoulos concerning the notion of analytic Rosenthal compacta that
they introduced recently. Though many of the statements we shall
consider are totally classical, the proofs make a crucial use of
Effective Descriptive Set Theory, namely of some fundamental results of
Moschovakis on inductive definability.
Fernando Ferreira (Lisbon): On a New Functional
Interpretation (chair: Ulrich Kohlenbach)
Abstract: Gödel's functional "Dialectica"
interpretation of 1958 was published with the explicit aim of being a
contribution to Hilbert's program. As things go, it introduced a new
technical tool in Proof Theory: one that presents a trade-off between
quantifier complexity and finite-type computable functionals.
Gödel's particular interpretation reduces HA (Heyting arithmetic)
to a quantifier-free calculus T of finite-type functionals, thereby
reducing the consistency of the former to the consistency of the
latter. It is seldom observed explicitly that Gödel's
interpretation can also be used to prove certain conservation results.
For instance, the adjunction of certain principles (axiom of choice AC,
independence of premises IP, Markov's principle MP) does not change the
provably Π^{0}_{2}-sentences
of HA.
We describe a new
(2005) functional interpretation
of HA. This functional interpretation (due to the author and Paulo
Oliva) uses the same functionals as Gödel's but changes the
assignment of formulas. Contrary to Gödel's assignment, our
assignment does not preserve set-theoretic truth. The new
interpretation yields new conservation results. Some false
set-theoretic principles like the refutation of extensionality or
Brouwer's FAN theorem, as well as some semi-intuitionistic principles
like LLPO (less limited principle of omniscience) or weak König's
lemma (WKL), can be adjoined to HA without changing the provably
Π^{0}_{2}-sentences.
More memorably, within intuitionistic logic, the
above principles are not able to prove further terminating computations.
As an
illustration, we show that the provably total
functions of the classically inconsistent second-order intuitionistic theory WKL_{0}
+ LLPO + IP + MP + AC^{N} + FAN
are the primitive recursive functions, where AC^{N} is
the countable axiom of choice. By the negative translation of
Gödel-Gentzen, we get, as an easy corollary, Harvey Friedman's
well-known conservation result of (classical) WKL_{0}
over RCA_{0}.
Finally, we would
like to draw attention to an
ubiquitous principle in mathematical logic: the bounded collection
scheme. It appears in bounded theories of arithmetic, in admissible set
theory (as Δ_{0}-collection), and in analysis (if we view
Brouwer's
FAN principle as a form of collection) and proof mining (Kohlenbach's
uniform boundedness principles). We believe that the new interpretation
provides a fresh and integrated look at bounded collection.
Andrzej Grzegorczyk (Warsaw): Philosophical
Content of Formal
Achievements (chair: Zofia Adamowicz)
Abstract: Two theses will be proposed:
The first general Thesis: A
Perception of Philosophical Content depends on the Taste of the Scholar. In
Science about reality it is Truth.
This means a good description
of real objects (events).
In Science about
potentialities (formal /
imaginary Science), the value is an Invention of Consistent Construction
and may be called: joke and/or beauty.
The second Thesis: In formal
science, called here imaginaries,
we can make the following similar distinction
in the taste of scholars:
- Maths: Mathematicians
were always proud that they can calculate
functions. They, e.g., calculate by
recursion: f(0)=a, f(n+1)= F(f,n)…
Calculation is the
fundamental joke (or beauty) of the construction.
- Logic: Logicians are
more philosophers, and were always proud that they can define relations.
They define using logical connectives and quantifiers.
Definition is the
fundamental joke (or beauty).
Some arguments, an example, and a propaganda for these distinctions
will be given.
Bjørn Kjos-Hanssen (Cornell): Brownian Motion
and Kolmogorov
Complexity (chair: Steffen Lempp)
Abstract: Probabilistic
potential theory contains results of the following form: A randomly
chosen small set of
reals is
almost surely disjoint from a given small set of reals. Here the
size of a set
can be for example its Hausdorff dimension.
Using
computability theory and Kolmogorov complexity, we obtain some results
of this kind, for certain randomly chosen
sets associated with Brownian motion.
We then investigate to what extent these results can be reproduced
using only potential theory.
Piotr Kowalski (Wroclaw): Definability in
Differential Fields (chair: Ludomir Newelski)
Abstract: A differential field is a field equipped
with a derivation. In the positive characteristic case one often needs
to "improve" the notion of derivation by introducing Hasse-Schmidt
derivations. I will briefly discuss the first-order theory of
(differentially closed) differential fields. Then, I will focus on two
special kinds of definable sets there. Sets of the first kind played a
crucial role in the Hrushovski's proof of the Mordell-Lang conjecture
[2]. Sets of the second kind appear in the statement of a theorem of Ax
[1] and its generalizations.
[1] James
Ax, On Schanuel's conjectures, Ann. of Math. (2) 93 (1971), 252-268.
[2] Ehud
Hrushovski, Mordell-Lang conjecture for function fields, Journal AMS 9
(1996), 667-690.
Paul Larson (Miami University): Large Cardinals
and Forcing-Absoluteness (chair: Joel Hamkins)
Abstract:
Absoluteness theorems of Levy and
Shoenfield state that the truth
values of Σ_{1} and Σ^{1}_{2}
sentences cannot be changed by set
forcing. In the presence of large cardinals, forcing-absoluteness
extends to much larger classes of statements. Jumping to the end of a
long story, we will talk about some of the strongest forcing
absoluteness results, including extensions of Woodin`s Σ^{2}_{1}
absoluteness theorem.
Tony Martin (UCLA): Sets and the Concept of Set
(chair: Pen Maddy)
Abstract: Those who doubt that the subject matter of
mathematics is a realm of abstract objects often do so because of a
general disbelief in the existence of abstract objects. I will propose
a very different basis for doubts about the status of mathematical
objects. Many people think that various statements of set theory, e.g.,
the Continuum Hypothesis, are neither true nor false. I am not one of
one of these people, but I do think we cannot at present be certain
that the CH has a truth-value. I will argue that if it is not certain
that the CH has a truth-value then it is also uncertain whether there
is any system of objects that satisfies our concept of a universe of
sets. It is common to say that the CH has no truth-value and to blame
this on the existence of many systems of objects that satisfy the set
concept. Part of my job will be to discredit this position. Another
part will be to give an account of what set theoretic truth and falsity
could amount to if there is no universe of sets.
Special
Sessions:
Philosophical
and
Applied Logic at the JPL (JPL, organized by Penelope Maddy):
Sunday,
2:00 p.m.:
Aldo
Antonelli (Irvine): From Philosophical Logic to Computer Science - and
Back
Abstract: Over the past 25 years or so, computer
scientists have looked at philosophical logic in search of tools for
the formal modeling of a number of interactive computational processes,
whereas philosophical logician have drawn new inspiration from a set of
problems specific to theoretical computer science and artificial
intelligence. This talk provides a (perforce idiosyncratic) survey of
the interactions between the two fields, pointing out interdisciplinary
connections and fruitful cross-fertilizations.
Sunday,
2:45 p.m.:
Horacio
Arlò
Costa (Carnegie-Mellon): Philosophical Logic Meets Formal Epistemology
(CANCELED)
Abstract: Formal epistemology is a branch of
epistemology that uses formal methods to articulate and solve
traditional epistemic problems. The talk surveys some recent
interactions between philosophical logic and formal epistemology. We
focus on epistemic problems related to the representation of attitudes
and their change, both for single and multiple agents. The
consideration of these problems has motivated, for example, new work in
areas like belief revision, epistemic and dynamic logic or formalisms
to represent uncertainty.
More expressive and sophisticated formalisms have been developed (first
and second order extensions of well known formalisms as well as new
multi-modal and multi-agent approaches). Finally the consideration of
some paradoxes concerning the relation of probability and qualitative
belief, as well as problems related to judgment aggregation, have
motivated researchers to rethink the very foundations of the Kripkean
semantic program in modal logic. We survey some of these new
developments as well as the philosophical problems that motivated them.
Monday,
4:30 p.m.:
Greg
Restall
(Melbourne): Proof Theory and Meaning: Three Case Studies
Abstract: Many of us are attracted to the idea that
inference rules play a role in determining meanings. In this talk I
will illustrate options for infererentialist approaches to meaning by
looking at three case case studies discussed in the recent literature:
(1) classical logic, (2) modalities, and (3) inductive and coinductive
types.
Monday,
5:15 p.m.:
Albert
Visser
(Utrecht): Interpretations in Philosophical Logic
Abstract: In my talk, I will discuss the use of
interpretations as a tool for comparing theories. The talk consists
of two parts. In the first half I will discuss some general
issues.
- I will sketch the various
notions of interpretation and the various notions of sameness of
theories definable in terms of interpretations.
- I will compare comparison of
theories based on interpretations with other notions of comparison,
like conservativity.
- I will comment on the question:
what does it tell us when we have an interpretation of one theory in
another?
In the second
half, I will illustrate a use of interpretations to study the
Predicative Frege Hierarchy obtained by iterating Predicative
Comprehension plus Frege Function. (See for a description John
Burgess' book Fixing Frege.) Roughly, the result is that, modulo mutual
interpretability, we get Robinson's Arithmetic Q plus all iterated
consistency statements for Q, so Q+con(Q)+con(Q+con(Q))+.... The second
level of this hierarchy, i.e., Q+con(Q), is mutually interpretable with
Elementary Arithmetic. It is open whether there is a natural hierarchy
of faster and faster functions corresponding to the iterated
consistencies.
Model
Theory (MT,
organized
by Françoise Delon and Ludomir Newelski):
Sunday,
2:00 p.m.:
Amador
Martin-Pizarro
(HU Berlin): Some Thoughts on Bad Objects
Abstract:
The Algebraicity Conjecture states
that a simple 2ω-categorical
group can be seen as an algebraic group over an algebraically closed
field. This long-standing open conjecture
belong to a wider conjecture, called "Principe du Nirvana", whose
various
specific instances have been refuted in the last decades. A specific
programme in order to characterize such simple groups was described,
which
originally imposed the non-existence of certain objects called bad
fields
(describing an undesired configuration characterizing the Borel
subgroups). We will discuss the relevance of bad fields and foster
diverse
links with other areas of algebraic geometry.
Sunday,
2:45 p.m.:
Vera
Djordjevic (Uppsala): Independence in Structures and Finite
Satisfiability
Abstract: An outline of ideas and methods
concerning proving the finite
submodel property by probabilistic means will be given. It appears like
some notion
of "sufficient independence"
between definable relations is
needed for a probabilistic argument to work out. We consider a notion,
the n-embedding of
types property, which has
some relationship with the
n-amalgamation property considered elsewhere. The main result about the
finite submodel
property applies to countably
categorical simple structures
with trivial forking, finite SU-rank and with the n-embedding of types
property for
every n.
Monday,
4:30 p.m.:
Marcus
Tressl (Regensburg): Super Real Closed Rings
Abstract:
A super real closed ring is a
commutative ring A with unit together
with functions F_{A}: A^{n} → A
for all n in N and every continuous function F: R^{n} → R,
satisfying the composition rules
(F∘(...,G,...))_{A} = F_{A}∘(...,G_{A},...).
For example, every ring C(X) of continuous real-valued functions
is a super real closed ring, where F_{C(X)}
is composition with
F; also super real fields
in the sense of Dales-Woodin at prime z-ideals are naturally
equipped with a super real closed ring structure.
I will overview
the algebraic properties
of super real closed rings, give an application to o-minimal
structures expanding the real field
and discuss the relation to C^{∞}-rings
(in the sense of Moerdijk-Reyes).
Monday,
5:15 p.m.:
Ziv
Shami (Tel Aviv): Countable Imaginary Simple Unidimensional Theories
Abstract: We show that these theories are
supersimple, provided that forking is witnessed by pseudo-low formulas
(a formula is pseudo-low if forking by it is a type-definable
relation). In particular, any low or 1-based countable imaginary simple
unidimensional theory is supersimple.
Proof
Complexity and
Nonclassical Logics (PC, organized by Pavel
Pudlák):
Wednesday,
2:00
p.m.:
Alasdair Urquhart
(Toronto): Complexity Problems for Substructural Logics
Abstract: Substructural logics such as relevance
logics and linear logics are the most complex nonclassical
propositional calculuses investigated to date. They include
undecidable systems, as well as logics that are decidable, but provably
intractable. This talk surveys some of the work in the area, and
also lists some open questions.
Wednesday, 2:30 p.m.: Emil
Jeřábek (Prague): Proof Systems for Modal Logics
Abstract: We discuss some issues in proof complexity
of calculi for propositional modal and intermediate logics. We consider
the usual Frege ("Hilbert style") proof systems, as well as their
variants (extended Frege, substitution Frege) inspired by the classical
case. We are interested in polynomial simulations, lower bounds,
feasible disjunction properties, feasible partial conservativity
results, and similar questions.
Wednesday, 3:00 p.m.: George Metcalfe (Vanderbilt): Substructural Fuzzy
Logics
Abstract: In this talk I will discuss a family of
substructural logics defined by algebras based on the real unit
interval [0,1]; well known examples being Lukasiewicz logic and
Gödel-Dummett logic. Gentzen systems can often be obtained for
these logics simply by extending sequent calculi for substructural
logics like Linear Logic to the level of hypersequents. Moreover, the
elimination of a special "density rule'' from proofs in such calculi
can be used to show completeness results for both Gentzen and Hilbert
systems for the logics. Indeed, in certain cases, conditions that
guarantee cut-elimination for the calculi also guarantee
density-elimination, providing a syntactic characterization of the
logics from this family.
Logic
and Analysis
(L&A, organized by Itaï Ben Yaacov and Ulrich
Kohlenbach):
Wednesday,
2:00
p.m.: Julien
Melleray (Urbana): Geometry of the Urysohn Space: A Model-theoretic
Approach
Abstract: The Urysohn space was built by Pavel
Urysohn in 1924. Over the past 15 years or so, there has been growing
interest in this space and its geometry. In the talk I'll try to
explain how one can use model-theoretic methods (via the framework of
model theory of metric structures) to tackle some problems involving
the Urysohn space and its geometry. I'll discuss in particular the
homogeneity properties of the space, and questions about conjugacy of
isometries.
Wednesday,
2:45
p.m.: Philipp
Gerhardy (Pittsburgh/Oslo): Local Stability of Ergodic Averages
Abstract: 'Proof mining' is the subfield
of mathematical logic that is
concerned
with the extraction of additional information from proofs - even
ineffective proofs! - in mathematics and computer science. The main
focus is on developing general (and feasible) methods to unwind the
computational content of proofs and to apply these methods to real
existing proofs. We present an application of proof mining in the field
of ergodic theory. The Mean Ergodic Theorem states that a for a
nonexpansive operator T on a Hilbert space H and for any f in H, the
sequence of ergodic averages A_{n} f ≔ ^{1}/_{n+1} ∑_{i≤0} T^{i} f
converges to a limit. While a full rate of convergence is not
possible, we present explicit rates for the classically equivalent
statement that for any number-theoretic function K, the averages A_{m}
f are stable within ε in some interval [n,K(n)]. These
computable bounds have been obtained by applying methods of proof
mining to a standard textbook proof of the Mean Ergodic Theorem.
Thursday, 11:30 a.m.: Peter
Hertling
(München): Computability and Non-Computability Results for the
Topological Entropy of Shift Spaces
Abstract: The topological entropy, a numerical
quantity assigned to a continuous function from a compact space to
itself, is invariant under topological conjugacy and serves as a tool
for classifying dynamical systems. Therefore, computing the topological
entropy is an important problem in dynamical systems theory. We discuss
several recent positive and negative results concerning the
computability of the topological entropy, mostly of shift dynamical
systems.
Thursday, 12:15 p.m.: Andreas Weiermann (Ghent): Analytic Combinatorics
of the Transfinite
Abstract: Roughly speaking, Analytic Combinatorics
(AC) is the art of counting using Cauchy's integral formula. Typically
(following Flajolet et al.) AC is used for investigations on the
average case analysis of algorithms. In this talk we will show how to
apply AC to systems of ordinal notations (for relatively small
ordinals). We explain surprising connections to the theory of
partitions as studied, for example, by Hardy and Ramanujan.
The resulting
information is used for proving logical limit laws (joint work with
Alan R. Woods) and for classifying phase transition thresholds for
Gödel incompleteness.
Set
Theory (ST,
organized
by Ilijas Farah and Joel Hamkins):
Wednesday, 2:00
p.m.: Matteo
Viale (Vienna): The Constructible Universe for the
Anti-foundation Axiom System ZFA
Abstract: Aczel [1], and independently Forti and
Honsel [2], introduced a strengthening
of the axiom of foundation asserting the existence of a unique
transitive collapse for every binary relation which is a set. The first
order axiomatization of set theory with foundation replaced by this
axiom is currently named in the literature ZFA. Forti and Honsel [3]
also
show that if M and N are transitive models of ZFA such that
M∩WF = N∩WF, then M=N (where WF is the definable class of
well-founded sets). We
exploit this idea to show that there are natural Gödel operations
which
are absolute for the theory ZFA such that the smallest transitive class
which is closed under these Gödel operation is the "constructible"
universe of the theory ZFA. The results that we present appeared in [4].
[1]
Peter Aczel, "Non well-founded set theories", CSLI lecture notes 14,
CSLI publications, 1988, Stanford
[2] Marco Forti, Furio Honsel,
"Set Theory with free construction principles", Annali Scuola Normale
Superiore di Pisa, Classe di Scienze, volume 10, 1983, pp. 493-522
[3] Marco Forti, Furio
Honsel, "Axiom of Choice and free construction principles I", Bull.
Soc. Math. Belg.,volume 36(B), 1984, pp. 69-79
[4] Matteo Viale, "The
cumulative hierachy and the constructible universe of ZFA", Math. Log.
Quart., volume 50(1), 2004, pp. 99-103
Wednesday,
2:30 p.m.: Gunter Fuchs (Münster): Maximality Principles for
Closed Forcings
Abstract: I am going to talk about the modifications
of the maximality principles,
which were originally introduced by Joel Hamkins, that result from
restricting them to subclasses
of <κ-closed forcings.
The subclasses I consider are the entire class of <κ-closed
forcings, the
<κ-directed closed forcings
and the collapses to κ. So for example, the maximality principle for
<κ-closed forcings
says that any statement that can be forced to be true by a <κ-closed
poset in such a way that it remains true in any further generic
extension by
<κ-closed forcing, is already true. The talk will center around the
following aspects: Consistency of the
principles, the compatibility with
large cardinal properties of κ, the relationships between the different
versions of the principle,
outright consequences, the possibilities
of combining them in the sense that they hold at many regular κ at the
same time, and the
limitations of the extent to which
they may be combined.
Wednesday, 3:00 p.m.: Lionel Nguyen Van Thé (Calgary): The
Urysohn sphere is oscillation stable (joint with Jordi López
Abad, Paris 7, and Norbert Sauer,
Calgary)
Abstract: In 1994, Odell et Schlumprecht built a
uniformly continuous map from the unit sphere of the Hilbert space into
the unit interval and which does not stabilize on any isometric copy of
the sphere. This result allowed to show that the Hilbert space has a
property known as 'distortion'. The purpose of the present talk is to
show that this situation is different when working with another
remarkable metric space sharing many common features with the Hilbert
sphere: the Urysohn sphere.
Thursday,
11:30 a.m.: Victoria Gitman (City
University of New York): Scott's Problem For Proper Scott Sets
Abstract: Given a model of Peano Arithmetic (PA),
define its "standard system" to be the collection of subsets of
the natural numbers that arise as intersections of the definable sets
of the model with its standard part. In 1962, Scott observed that
standard systems satisfy certain basic computable theoretic and set
theoretic properties. A collection of subsets of the natural numbers
having these properties came to be known as a "Scott set". As a partial
converse, Scott showed that countable Scott sets are exactly the
"countable" standard systems and in 1982, Knight and Nadel extended his
result to standard systems of size ω_{1}.
The question of
whether Scott sets are exactly the standard systems of models of PA
came to be known as "Scott's problem". I will introduce the history of
Scott's Problem and talk about my results for standard systems of size
ω_{2}, which were obtained using forcing
constructions with
models of PA together with the Proper Forcing Axiom. In particular, I
will define the notion of a proper Scott set and show under PFA that
every proper arithmetically closed Scott is the standard system of a
model of PA. I will also focus on the set theoretic questions (and
answers) involving the existence of proper Scott sets.
Thursday,
12:00
noon:
Márton
Elekes (Hungarian Academy of Sciences): Partitioning κ-fold Covers into
κ Many Subcovers
Abstract: Motivated by a question of
A. Hajnal we investigate the following set of problems. Let X be a
set, κ a cardinal number, and H
a family that covers
each x in X at least κ times. Under what assumptions can we
decompose H into κ many
subcovers? Equivalently,
under what assumptions can we colour H
by κ many
colours so that for each x in X and each colour c there exists
H in H of colour c containing
x?
The
assumptions we make can be, e.g., that H
consists of open, closed,
compact, convex sets, or polytopes in R^{n},
or intervals in a
linearly ordered set, or we can make various restrictions on the
cardinality of X, H, or
elements of H.
Besides numerous
positive and
negative results, many questions turn out
to be independent of the axioms of set theory.
The
speaker's research was partially supported by OTKA grants no. 49786,
61600, F43620 and
the Öveges Project of NKTH and KPI.
This
is a joint work with T. Mátrai and L. Soukup.
Thursday, 12:30
p.m.:
Asger
Törnquist (Toronto): Classifying Measure Preserving Actions Up to
Conjugacy and Orbit Equivalence
Abstract: Extending a well-known theorem by Foreman
and Weiss we show: If H is an infinite subgroup of a discrete countable
group G, then the measure preserving actions of H that can be extended
to G cannot be classified by countable structures. As a consequence,
the measure preserving actions of a countable group with the relative
property (T) cannot be classified up to orbit equivalence by countable
structures.
Program
Committee:
Alessandro Andretta
(Torino)
Françoise Delon (Paris 7)
Ulrich Kohlenbach (Darmstadt)
Steffen Lempp, Chair (Madison)
Penelope Maddy (Irvine)
Jerzy Marcinkowski (Wrocław)
Ludomir Newelski (Wrocław)
Andrew Pitts (Cambridge)
Pavel Pudlák (Czech Academy of Sciences)
Sławomir Solecki (Urbana)
Frank Stephan (National University of Singapore)
Göran Sundholm (Leiden)
Prepared by Steffen Lempp
(@math.wisc.edu">lemppmath.wisc.edu)