BLC 2009 - Abstracts

Martijn Baartse (Gent, Belgium) Phase Transitions for Friedman's Long sequence Theorem

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.

Martin Churchill (Bath) A Logic of Sequentiality

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.

Peter Dybjer (Chalmers, Gothenburg, Sweden) Program Testing and Constructive Validity (invited talk)

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.

Mark Priestley (Westminster, London) Logic and the Invention of the Computer (invited talk)

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.

Sam Sanders (Gent, Belgium) A Copy of Several Reverse Mathematics (Abstract in pdf)

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.

Peter Schuster (Munich and Leeds) Unique Solutions (invited talk)

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