BLC 2009 - Abstracts
This talk is about the phase transition for Friedman's long finite sequences.
An upper- and lower bound will be presented that are not far apart.
Many logics and programming languages can be equipped with game
semantics, whereby programs of type A (or proofs of proposition A)
are represented by strategies over the game representation of A. In
the case of proof semantics, the strategies in question are
total. These games models are often admit definability results --- for
a given system, we might provide some constraints on strategies such
that each strategy satisfying said constraints is the denotation of
some program (or proof.) In this work we consider a relatively
constraint-free games model (in which you can embed many other games
models.) We develop a proof system for this model that is "fully
complete" in a strong sense: proofs of a formula are in 1-1
correspondence with strategies over the game representation of that
formula. Thus we can use the logic to represent strategies
syntactically, and thus use it to model proofs in Multiplicative
Linear Logic, imperative objects, and so on. The logic is
polarised and contains many standard connectives (tensors, with, par,
exponentials...) although the proof rules themselves are nonstandard
- a key notion is that of a /sequoid/ operator, identifying the
location of the next move (or /focus/) of the formula.
In this talk I will discuss the connection between program testing and
Martin-Löf's meaning explanations for his intuitionistic type theory.
First I give a short overview of the historical development of the ideas
behind the meaning explanations. Then I explain the connection with
program testing. Finally, I will mention the possibility of pursuing the
testing point of view for impredicative logical systems as well.
Yuguo He (Cambridge) Parameterized Complexity Classes under Logical Reductions
The W-hierarchy is very important in parameterized complexity theory
since it captures our intuition of intractability. The parameterized
complexity classes of the W-hierarchy are usually defined as the
problems reducible to certain natural complete problems by means of
fixed-parameter tractable (fpt) reductions. We investigate whether the
classes can be characterised by means of weaker, logical reductions.We
show that each class W[t] has complete problems under slicewise
bounded-variable first order reductions, which are a natural weakening
of fpt-reductions. We also investigate the consequence of relaxing
some of the restrictions on such kind of logical reductions. Our
results show that slicewise first-order reductions are too strong,
whereas slicewise quantifier-free reductions are too weak.
Richard Kaye (Birmingham) Generic Initial Segments in Models of Arithmetic (invited talk)
Models of Peano arithmetic are structures resembling the natural numbers
with their arithmetic structure of order, addition and multiplication,
and satisfying the induction axiom scheme expressed in first-order
logic. They interesting structure in their own right, but of course
have also been used to study provability in number theory and
combinatorics. Initial segments (also called "cuts") of such models are
possibly the most important aspect of the structural properties of the
model, and their study also has consequences for provability etc. They
are important too because theories of analysis are conveniently
interpreted in the expanded structure (M,I) consisting of a model of
arithmetic M with an identified initial segment I.
This talk will focus on a particularly nice construction of initial
segments related to a Banach-Mazur game in arithmetically saturated
models of Peano arithmetic. The intuition is that if an initial segment
I of a model M is constructed in as general way as possible, with as
little information being added, then the first order theory of the pair
(M,I) should be determined in a comparatively straightforward way from
the theory of M together with the closure properties of I. The initial
segments constructed in this way are called generic and the construction
takes place relative to some appropriate closure conditions chosen in
advance: one can consider a generic initial segment closed under the
primitive recursive functions, or an elementary generic initial
segment.
In particular I shall report on recent work by the author and Tin Lok
Wong on generic initial segments. In particular we will explain the
notion of genericity and its relation to the Banach-Mazur game. The main
theorem concerns a description of truth in the structure (M, I), where I
is a generic cut of a model M of PA. This work relates to open questions
raised by Roman Kossak on free cuts.
Margarita Korovina (Manchester) A Logical Approach to Effective Reasoning About Dynamical
and Hybrid Systems (invited talk)
Verification of dynamical and hybrid systems is a well recognised
problem. In many cases, a representation of a hybrid system is based
on continuous constraints and reasoning about hybrid systems is based
on solving of such constraints. Up to recently, only a limited type
of dynamics has been considered namely polynomial dynamics, which is
insufficient for many applications. In this talk we discuss several
approaches to enrich classes of continuous dynamics and methods for
solving corresponding continuous constraints.
Julien Melleray (Lyon) Logic and Analysis: Automorphism Groups of Metric Structures (invited talk)
Automorphism groups of countable first-order structures are natural
combinatorial objects, and it is well-known that properties of the
automorphism group (as a topological group or as an abstract group)
have some consequences on the theory of the structure, and vice versa.
In the talk I will try to explain how, using continuous first order
logic, one can extend the framework above to Polish spaces and groups;
examples of such groups include the isometry group of a separable
Hilbert space, the homeomorphism group of the real line, the
measure-preserving bijections of the unit interval, etc. Then I will
explain some recent related results, based on the Baire category
theorem, that enable one to provide new examples of Polish groups
whose topology is completely encoded in their algebraic structure
(this last part is joint work with I. Ben Yaacov and A. Berenstein).
Paulo Oliva (Queen Mary, London) Selection Functions, Bar Recursion and Nash Equilibrium (invited talk)
The usual existential and universal quantifiers over a set X can be thought of
as type 2 operations, which take a predicate p : X -> Bool as input and return
a Bool as output. If instead of Bool we allow an arbitrary set R, several other
operations can also be thought of as "generalised quantifiers", e.g.
limit : (Nat -> Y) -> Y,
for a compact metric spaces Y, and
supremum : ([0,1] -> Real) -> Real
integral : ([0,1] -> Real) -> Real.
A generalised quantifier phi : (X -> R) -> R is called attainable if it has a
selection function
e : (X -> R) -> X
i.e. if there exists a function e : (X -> R) -> X producing the point where the
quantifier "attains its p-value" for any "predicate" p : X -> R
phi(p) = p(e(p)).
In the case of the existential quantifier, for instance, this is Hilbert's
epsilon term. In the case of integration, the mean value theorem says that
integration over C[0,1] has a selection function, i.e. for any p in C[0,1]
there exists an x in [0,1] such that
integral(p) = p(x).
Hence, there must exist a function e : ([0,1] -> R) -> [0,1] such that
integral(p) = p(e(p)).
This talk aims to motivate the concept of selection functions and some associated
constructions through simple concrete examples from Nash equilibrium (backward
induction), fixed point theory (Bekic's lemma), algorithms (backtracking) and
proof theory (bar recursion). Talk based on joint work with Martin Escardo.
Two views commonly taken of the relationship between logic and computers,
especially by logicians, are that computers are essentially logic
machines, and that logic played an important role in the invention of the
stored-program computer. This talk will use historical evidence to
question both of these assumptions, arguing that the connection between
logic and computers was only firmly established after 1950, when the first
computers were already in operation. This in turn raises the question of
why the link between logic and computing should feel so natural, and an
answer to this will be suggested that reaches back to the origins of
symbolic algebra and logic in the nineteenth century.
Stephen Read (St Andrews) Medieval Logic: Obligations and Insolubles (invited talk)
The recovery of Aristotle's logical writings such as the Analytics in the Latin West in the 12th century (the
so-called logica nova) provided the spur to the development of
the medievals' original ideas about logic (the logica modernorum), covering consequences, properties (such as supposition
theory), insolubles (logical paradoxes) and obligations. Coming to
understand the strange genre of logical disputation in the Obligationes-treatises, where an Opponent places a Respondent under a
series of logical obligations, has occupied the past fifty
years. Obligations terminology spreads out into other treatises, in
particular, those on insolubles. Much original work was done on both
theories in the early 14th century,
particularly in Oxford. The talk will set the background to
understanding these contributions, and focus on an interchange between
Thomas Bradwardine and Richard Kilvington in the 1320s, in Bradwardine's
Insolubilia and Kilvington's Sophismata.
Reverse Mathematics is a program in foundations of mathematics
initiated by Friedman and developed extensively by Simpson. Its
aim is to determine which minimal axioms prove theorems of ordinary mathe-
matics. Nonstandard methods have played an important role in this program.
We are interested in Reverse Mathematics where equality is replaced
by the nonstandard relation $\sim$, i.e. equality up to infnitesimals. We obtain
a `copy' of Reverse Mathematics for WKL0 in a weak system of nonstandard
arithmetic. Surprisingly, the same system is also a `copy' of Constructive Re-
verse Mathematics.
References:
[1] Harvey Friedman, Some systems of second order arithmetic and their use, Proceedings of the
International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1, Canad. Math.
Congress, Montreal, Que., 1975, pp. 235 - 242.
[2] Harvey Friedman, Systems of second order arithmetic with restricted induction, I & II (Abstracts),
Journal of Symbolic Logic 41 (1976), 557 - 559.
[3] H. Jerome Keisler, Nonstandard arithmetic and reverse mathematics, Bull. Symbolic Logic 12
(2006), no. 1, 100 - 125.
[4] H. Jerome Keisler, Nonstandard arithmetic and reverse mathematics, Bull. Symbolic Logic 12 (2006),
no. 1, 100 - 125. MR2209331 (2006m:03092)
[5] Stephen G. Simpson, Subsystems of second order arithmetic, Perspectives in Mathematical
Logic, Springer-Verlag, Berlin, 1999.
[6] Kazuyuki Tanaka, The self-embedding theorem of WKL0 and a non-standard method, Ann.
Pure Appl. Logic 84 (1997), no. 1, 41 - 49.
Every complete metric spaces possesses the unique solution property:
if a continuous real-valued function has approximate roots and in a
uniform manner at most one root, then it actually has a root. The
unique solution moreover becomes a continuous function in the
parameters by a natural generalisation of the uniqueness
hypothesis. This metatheorem can be traced back to the Russian school
of recursive mathematics; has since proved productive in constructive
and computable analysis; and stood right at the beginnings of proof
mining. For short, uniqueness helps to find the solution above any
"pure existence proof" tied together with the use of classical logic,
as there are the frequent arguments based on the Bolzano-Weierstrasz
principle.
Its technical usefulness aside, why does the metatheorem work at
all? Continuity is an issue; another one is (avoiding) choice.
Neither gives a definitive answer, but the latter has shown the right
direction. Working with completions defined without sequences has in
fact revealed that completeness is even equivalent to the unique
solution property. If not new, this is a characterisation of
completeness for metric spaces custom-made for short proofs of the
numerous basic theorems to which uniqueness is inherent. The Banach
fixed point theorem and its applications (implicit functions,
Picard-Lindeloef, etc.) are simple but characteristic examples.
Alexander Summers (Imperial College, London) Natural Delimited Control : A Curry-Howard Correspondence
with Gentzen-Style Classical Logic (invited talk)
The Curry-Howard Isomorphism historically connects the Lambda Calculus
with the Gentzen's natural deduction for intuitionistic logic. Since
the 90's the idea of creating a similar connection between classical
logics and languages with non-functional programming features has been
considered.
We present the nu-lambda-mu calculus: an extension of Parigot's
lambda-mu calculus achieving a direct correspondence with Gentzen's
classical natural deduction. We equip the resulting calculus with a
naturally non-confluent reduction relation, motivated by an intuitive
semantics.
The reduction behaviour of the calculus is highly expressive, and able
to encode those of popular alternatives in the literature. From a
logical perspective, we can encode Urban's non-confluent cut
elimination for classical sequent calculus. From a programming
perspective, a delimited control operator arises naturally, which can
be used to encode jumps, exceptions, loops etc.
Thomas Studer (Bern) On the Proof Theory of Common Knowledge
We survey recent results on the proof theory for the
logic of common knowledge. In the first part of the talk
we discuss the problems of syntactic cut-elimination and
of 'nice' deductive systems for common knowledge.
The second part is devoted to a co-inductive system for
common knowledge which is interesting in the context of
evidence based epistemic logics.
Neil Thapen (Prague) Search Problems in Bounded Arithmetic (invited talk)
The bounded arithmetic hierarchy is a sequence of weak fragments of
Peano arithmetic, defined by restricting the induction scheme to
formulas from the polynomial time hierarchy. The set of NP search
problems provably total in one of these theories gives a measure of
the strength of the theory, playing an analagous role to the sets of
provably recursive functions of stronger theories of arithmetic.
We describe some recent work characterizing these problems in terms of
a combinatorial principle about games; this is shown by translating
first-order proofs in such a theory into large, uniform propositional
proofs in a proof system where the soundness of the rules can be
witnessed by a feasible strategy for reducing one game to another. We
also show that this can be restated as a principle about local
improvements of labellings of a large graph, and that this new
principle can be extended naturally to characterize the provable NP
search problems of "second-order" bounded arithmetic theories
corresponding to PSPACE and EXP.
Stan Wainer (Leeds) Proof Theoretic Bounding Functions (invited talk)
This talk will be about the function a+2x and the role it, and its various
(strong) generalizations, play in bounding the size and complexity of
functions provably computable in a spectrum of theories between
IΔ0(exp), PA and Π11-CA0. The close connections with
independence results (e.g. Friedman's miniaturised version of Kruskal's
Theorem) will be surveyed.
Andreas Weiermann (Gent, Belgium) Some Recent Results on Well Partial Orderings and their
Maximal Order Types (invited talk)
A well partial order (wpo) is a well-founded partial order which does not admit
infinite antichains.
Famous examples for wpo's are provided, for example, by Higman's
Lemma and Kruskal's tree theorem.
An important result in the area by de Jongh and Parikh states that every wpo
can be extended to a linear order (on the same domain) which among all such
linear extensions has a maximal possible order type. It turns out from
results of de Jongh, Parikh, Schmidt and Friedman that such
maximal order types are mathematical invariants which prove
very useful for classifying the
proof-theoretic strength of wpo'ness assertions.
For example, a classic result by Friedman states that Kruskal's tree theorem
is not provable in predicative analysis.
In our talk we present a new, short and
very aesthetic formula which allows to describe a
plethora of (old and new) results on maximal order types
in a uniform way and we indicate related proof-theoretic applications.
(Joint work with Michael Rathjen.)
Our long term research aim consists in classifying the strength of Friedman-Kriz style tree theorems
which are based on a so called gap condition.
Anton Setzer
Last modified: Fri Aug 28 20:32:02 BST 2009