The Logic and Computation Group is composed of faculty and graduate students from the Computer and Information Science, Mathematics, and Philosophy departments, and participates in the Institute for Research in the Cognitive Sciences. The Logic and Computation group runs a weekly seminar. The seminar is open to the public and all are welcome.
The seminar meets regularly during the school year on Mondays at 3:30 p.m. in room DRL 4C8 on the fourth (top) floor of the David Rittenhouse Laboratory (DRL), on the Southeast corner of 33-rd and Walnut Streets at the University of Pennsylvania. Directions may be found here. Please note this is a new meeting time and a change from the previous meeting time of 4:30. The meeting room remains the same. Any changes to this venue or schedule will be specifically noted.
We prove a uniformly computable version of de Finetti's theorem. The classical result states that an exchangeable sequence of real random variables is a mixture of independent and identically distributed (i.i.d.) sequences of random variables. Moreover, there is a measure-valued random variable, called the directing random measure, conditioned on which the random sequence is i.i.d. The distribution of the directing random measure is essentially unique and is called the de Finetti measure. We show that computable exchangeable sequences of real random variables have computable de Finetti measures. In the process, we show that a distribution on [0,1]^omega is computable if and only if its moments are uniformly computable, which suffices to prove the theorem in the case of (almost surely) continuous directing random measures. In the general case, we give a proof inspired by a randomized algorithm which succeeds with probability one. We also apply the computable de Finetti theorem to show how exchangeable stochastic processes in probabilistic functional programming languages can be rewritten as procedures that do not use mutation. This is joint work with Daniel Roy.
Type-amalgamation properties of a theory are about when certain kinds of finite directed systems of types are consistent, and when such systems have an essentially unique solution. A fundamental property of stable and simple theories is that triples of complete types p(x,y), q(y,z), and r(x,z) over a model which satisfy natural coherence and independence conditions can always be amalgamated -- this is called 3-existence over models. Similarly, the n-existence property is about amalgamating systems of types indexed by proper subsets of {1, ..., n}.
Hrushovski recently gave an interesting characterization of which stable theories have the 4-existence property which has to do with the definability of certain kinds of groupoids in the theory. In ongoing work with Alexei Kolesnikov, we are trying to generalize these results to characterize the n-existence property using higher-dimensional groupoids, and I will try to give an idea of our methods.
I will talk about the project of editing (with Wilfried Sieg and Michael Hallett) Hilbert's unpublished lecture notes on foundations of mathematics, and discuss the implications of Hilbert for the present-day philosophy of mathematics.
I will talk about the project of editing (with Wilfried Sieg and Michael Hallett) Hilbert's unpublished lecture notes on foundations of mathematics, and discuss the implications of Hilbert for the present-day philosophy of mathematics.
Ultrametric spaces are some of the nicest topological spaces there are. In this series of talks we will discuss ultrametric spaces whose distance function takes values in an arbitrary complete lattice Gamma. We will show that the category of Gamma-ultrametric spaces and non-expanding maps is equivalent to a full subcategory of separated presheaves on Gamma^{op}. We will further show that under this equivalence the sheaves correspond to the spherically complete Gamma-ultrametric spaces. After we have established this equivalence we will use it to show that theorems originally proved for Gamma-ultrametric spaces can be proved for sheaves. This talk is based on part of my research during this last year.
Ultrametric spaces are some of the nicest topological spaces there are. In this series of talks we will discuss ultrametric spaces whose distance function takes values in an arbitrary complete lattice Gamma. We will show that the category of Gamma-ultrametric spaces and non-expanding maps is equivalent to a full subcategory of separated presheaves on Gamma^{op}. We will further show that under this equivalence the sheaves correspond to the spherically complete Gamma-ultrametric spaces. After we have established this equivalence we will use it to show that theorems originally proved for Gamma-ultrametric spaces can be proved for sheaves. This talk is based on part of my research during this last year.
One of the features which distinguishes first order logic from higher order logics is the absoluteness of the satisfaction relation. Specifically if we have two standard models of set theory V_0 and V_1 with V_0 subset V_1 then for any first order theory T and model M (both in V_0) V_0 thinks (M models T) if and only if V_1 thinks (M models T). Unfortunately as we move from first order to second order (and higher) we lose absoluteness. Given a second order T and a model M such that V_0 thinks (M models T) we have no reason to believe that V_1 will also think (M models T). However, in a wide class of theories T which occur in practice (such as topological spaces, complete lattices, ect.) for all models M where V_0 thinks (M models T), even if V_1 doesn't think (M models T) there is a "canonical" extension M' of M such that V_1 thinks (M' models T). In this context we call M' the "relativization" of M (with respect to T).
In this (series of) talk(s) we will formally introduce this notion of relativization and we will show there is a higher order theory of Grothendieck Toposes such that (assuming the axiom of choice) every model always has relativizations (with respect to the theory). This talk is based on part of my research during this last year.
One of the features which distinguishes first order logic from higher order logics is the absoluteness of the satisfaction relation. Specifically if we have two standard models of set theory V_0 and V_1 with V_0 subset V_1 then for any first order theory T and model M (both in V_0) V_0 thinks (M models T) if and only if V_1 thinks (M models T). Unfortunately as we move from first order to second order (and higher) we lose absoluteness. Given a second order T and a model M such that V_0 thinks (M models T) we have no reason to believe that V_1 will also think (M models T). However, in a wide class of theories T which occur in practice (such as topological spaces, complete lattices, ect.) for all models M where V_0 thinks (M models T), even if V_1 doesn't think (M models T) there is a "canonical" extension M' of M such that V_1 thinks (M' models T). In this context we call M' the "relativization" of M (with respect to T).
In this (series of) talk(s) we will formally introduce this notion of relativization and we will show there is a higher order theory of Grothendieck Toposes such that (assuming the axiom of choice) every model always has relativizations (with respect to the theory). This talk is based on part of my research during this last year.
One of the features which distinguishes first order logic from higher order logics is the absoluteness of the satisfaction relation. Specifically if we have two standard models of set theory V_0 and V_1 with V_0 subset V_1 then for any first order theory T and model M (both in V_0) V_0 thinks (M models T) if and only if V_1 thinks (M models T). Unfortunately as we move from first order to second order (and higher) we lose absoluteness. Given a second order T and a model M such that V_0 thinks (M models T) we have no reason to believe that V_1 will also think (M models T). However, in a wide class of theories T which occur in practice (such as topological spaces, complete lattices, ect.) for all models M where V_0 thinks (M models T), even if V_1 doesn't think (M models T) there is a "canonical" extension M' of M such that V_1 thinks (M' models T). In this context we call M' the "relativization" of M (with respect to T).
In this (series of) talk(s) we will formally introduce this notion of relativization and we will show there is a higher order theory of Grothendieck Toposes such that (assuming the axiom of choice) every model always has relativizations (with respect to the theory). This talk is based on part of my research during this last year.
The most fundamental results of monadic second-order decidability, beyond the decidability of just pure monadic second-order logic, deal with the decidability of the monadic second-order theories of one and two successors and the decidability of the second-order theory of linear order (Buchi, Rabin). Having moved from sets to multisets, we refine the underlying logic as linear logic. In contrast to the classical results, we prove the undecidability of just pure monadic linear logic, even if we use nothing but Horn formulas built up from unary predicates, in which no function symbols are present.
As for affine logic (linear logic plus weakening), we prove the undecidability of the Horn fragment of affine logic, which involves only one binary predicate ("linear order") and a fixed finite number of unary predicates, and which contains no function symbols at all. We also show the undecidability of the Horn fragment of monadic affine logic of one constant symbol ("zero") and one unary function symbol ("successor"), and a fixed finite number of unary predicates.
Along these lines, we obtain the undecidability of the optimistic protocol completion even for the class of communication protocols with two participants such that either of them is a finite automaton provided with one register capable of storing one atomic message, all the predicates used are at most unary, and no compound messages are used.