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. Any changes to this venue or schedule will be specifically noted.
Although logic and proof theory have been successfully used as a framework for the specification of computation systems, there is still an important gap between the systems that logic can capture and the systems used in practice. This thesis attempts to reduce this gap by exploiting, in the context of the computation-as-proof-search paradigm, two non-canonical aspects of sequent calculus, namely the polarity assignment in focused proofs and the linear logic exponentials. We exploit these aspects in three different domains of computer science: tabled deduction, logical frameworks, and algorithmic specifications. This thesis provides a proof theoretic explanation for tabled deduction by exploiting the fact that in intuitionistic logic atoms can be assigned arbitrary polarity. A table is a partially ordered set of formulas and is incorporated into a proof via multicut derivations. Here, we consider two cases: the first case is when tables contain only finite successes and the second case is when tables may also contain finite failures. We propose a focused proof system for each one of these cases and show that, in some subsets of logic, the only proofs and open derivations available in these systems are those that do not attempt to reprove tabled formulas. We illustrate these results with some examples, such as simulation, winning strategies, and let polymorphism type-checking.
We show that linear logic can be used as a general framework for encoding proof systems for minimal, intuitionistic, and classical logics. First, we demonstrate that with a single linear logic theory, one can faithfully account for natural deduction (normal and non-normal), sequent calculus (with and without cut), natural deduction with general elimination rules, free deduction and tableaux proof systems by using logical equivalences and different polarity assignments to meta-level literals. Then we exploit the fact that linear logic exponentials are not canonical and propose linear logic theories that faithfully encode different proof systems; for example, a multi-conclusion system for intuitionistic logic and several focusing proof systems.
The last contribution of this thesis investigates what type of algorithms can be expressed by using linear logic’s non-canonical exponentials. In particular, we use different exponentials to “locate” multisets of data, and then we show that focused proof search can be precisely linked to a simple algorithmic specification language that contains while-loops, conditionals, and insertion into and deletion from multisets. Finally, we illustrate this result with several graph algorithms, such as Dijkstra’s algorithm for finding the shortest distances in a positively weighted graph and an algorithm for checking if a graph is bipartite.
We study FO(MTC), first-order logic with monadic transitive closure, a logical formalism in between FO and MSO on trees. We characterize the expressive power of FO(MTC) in terms of nested tree-walking automata. Using the latter, we show that FO(MTC) is strictly less expressive than MSO, solving an open problem. We also present a temporal logic on trees that is expressively complete for FO(MTC), in the form of an extension of the XML document navigation language XPath with two operators: the Kleene star for taking the transitive closure of path expressions, and a subtree relativisation operator, allowing one to restrict attention to a specific subtree while evaluating a subexpression. We show that the expressive power of this XPath dialect equals that of FO(MTC) for Boolean, unary and binary queries. We also investigate the complexity of the automata model as well as the XPath dialect. We show that query evaluation be done in polynomial time (combined complexity), but that emptiness (or, satisfiability) is 2ExpTime-complete. Based on joint work with Luc Segoufin (JACM 2010).
We consider the category-theoretic structure of abstract elementary classes (AECs), and consider their relationship to accessible categories, the latter being category theorists' proposed context in which to analyze classes of models (elementary or otherwise). We translate a few notions and techniques related to accessible categories into the realm of AECs, and draw two surprising conclusions. Building on work described in the previous talk, we discover that the connection with accessible categories yields a partial Galois stability spectrum result for weakly tame AECs. Moreover, using nothing more than the Yoneda embedding, we obtain a peculiar structure theorem for categorical AECs, where the models may be replaced by sets equipped with actions of the monoid of endomorphisms of the categorical structure. These results--clear at the level of category theory, but unforeseeable from other angles--illustrate the potent role that this perspective may yet play in model theory.
For all the success of first order model theory, there are a host of mathematical objects which, defying first order axiomatization, lie outside of its scope: Banach spaces and Artinian rings, for example. The abstract elementary class (AEC) provides a unifying context in which to analyze the model theory of such classes of objects and, more generally, of non-first order logics. Obtained by taking the notion of elementary class, abandoning syntax, and retaining only the purely diagrammatic, category-theoretic properties of elementary embedding, they require a new notion of type -- Galois type -- which must necessarily be characterized in non-syntactic terms. Given this change, and given that we cannot fall back upon compactness of the underlying logic, classical methods and results rarely generalize to this framework.
We present a near-exception to this: we exhibit a way of topologizing sets of Galois types (analogous to the syntactic topologies familiar from classical model theory), thereby providing a foothold for the definition of Cantor-Bendixson rank for Galois types and, ultimately, a family of Morley-like ranks. As an application, we use the latter to prove a generalization of a Galois stability result due to Baldwin, Kueker and Van Dieren.
One of the most remarkable results in finite model theory is that for any first order formula phi the limit as n -> infinity of ({M models phi: |M| =n} / {M:|M| = n}) is either 0 or 1. In other words, any formula is realized asymptotically almost surely or asymptotically almost never. This is called the 0-1 law for first order logic.
Since its discovery there have been several other 0-1 laws proved for collections of finite structures which satisfied some condition, such as being a graph, or a triangle free graph, or a partial order.
Given any first order theory T we can look at the collection of finite subsets of models of T and we can ask if those finite subsets have a 0-1 law (i.e., does any formula asymptotically almost surely hold or asymptotically almost never hold). In the case that there is a 0-1 law the resulting theory is not necessarily the same as T. This gives us a map 01Law from complete theories to (possibly incomplete) theories. We can then ask "How computable can the output, 01Law(T), be when the input, T, is a computable complete theory?"
In this talk we will prove that provided T is computable and 01Law(T) is complete then 01Law(T) must be computable from the halting problem. We will also show that every set computable from the halting problem is, in a strong sense, reducible to a theory of the form 01Law(T) for a computable T.
If we have time we will also discuss other properties of the 01Law operator, such as showing that for any countable ordinal alpha there is a theory such that 01Law can be iterated alpha many times with each iteration being a complete theory.
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Constructive reverse mathematics is reverse mathematics carried out in Bishop-style constructive mathematics (BISH)---that is, using intuitionistic logic and, where necessary, constructive ZF set theory. There are two primary foci of constructive reverse mathematics:
first, investigating which constructive principles are necessary to prove a given constructive theorem;
secondly, investigating what non-constructive principles are necessary additions to BISH in order to prove a given non-constructive theorem.
I will present work on constructive reverse mathematics, carried out with Josef Berger and Hannes Diener. The main theme of the talk is the connection between the antithesis of Specker's theorem, various continuity properties, versions of the fan theorem, and Ishihara's principle.
The mid-Nineties of the last century saw a revival of interest in topological semantics for modal logic first introduced by A. Tarski and his student J.C.C. McKinsey in 1941. Spurred by the recent development of a variety of dynamic logical systems which were based on a mixture of topological view of space and a modal view of time, a small industry emerged working on simplifying Tarski and MacKinsey's classic completeness results. The ultimate goal was a set of techniques that would enable us to largely mechanize the construction, axiomatization, determination of computational complexity, and other important aspects of the logical systems based on the topo-semantics. One was after a topological kin of Bisimulation, Correspondence Theory, Completeness via Sahlqvist Formulae, Tiling and related reduction techniques in complexity evaluation, and other sophisticated but user friendly techniques of the relational approach to modal logic.
Although the work has produced a steady stream of results, papers and even some Ph.D. thesis on the topic, the progress has not been as smooth as initially envisaged. The field has yet to acquire an accessible set of techniques that is not only easily taught but also easily transferable to related formal question. Our goal in this talk is to look closely at a variety of results in the topo-semantics over the last decade and extrapolate a set of techniques that go beyond a specific application to a specific logical systems. The main aim of the work is to find a method that would enable one to establish complete axiomatizations of interesting topological spaces, such as
1. Euclidean Metric Spaces: Q, Q^2, Q^3,... R, R^2, R^3,...
2. Fractal Spaces noninteger valued dimensions: Cantor Space, Koch Snowflake, Sierpinski Carpet, Menger Sponge, ...
3. Finite and infinite tree topologies: T_2, the infinite binary tree, and T_2+, the infinite binary tree with limits.
It turns out that the concept best suited for analyzing such a varied and rich collection of spaces is that of a self-similar fractal structure. As we will see in the talk, the needed fractals are built in a series of self-similar stages which enable one to understand techniques used in various semantic constructions in topological semantics for modal logic without much of a heavy technical investment in understanding the theories of fractals. A simple set of tools of the fractal approach seem curiously well crafted for the task of understanding topological spatial structures and reasoning.
Our work is inspired by two theorems of Sierpinski proved sometimes in the 1920s. He proved that two fractals, Sierpinski Carpet and Menger Sponge, are topologically universal. The former fractal embeds all planar Jordan curves; the latter embeds the unrestricted class of Jordan curves. As we will see, the two constructions are universal in an additional logical sense, and related constructions contain a substantial amount of topological structure. We will mostly work with the basic modal logic, which in topological setting is S4. We will show some of the fractal completeness constructions for this logic, most notably the completeness of S4 with respect to the real line, plane, and cube. This proof has seen several simplifications over the past decade. Our proof consolidates all the simplifications and introduces a streamlined principled proof of the result. We will further suggest some ways for dealing with extended modal topo-languages using the fractal techniques introduced. This work is based on a joint project with Tamar Lando (UC Berkeley). We will leave the audience with a list of recent results in the field as well as a list of open problems with varying degrees of "openness".
Some of the recent work in the area of topological semantics for modal logic includes:
M. Aiello, J. van Benthem, G. Bezhanishvili, ``Reasoning about space: the modal way'', Journal of Logic and Computation, 13, 889-920 (2003).
S. Artemov, J. Davoren and A. Nerode,``Modal logics and topological semantics for hybrid systems'', Technical Report MSI 97-05, Cornell University (1997).
G. Bezhanishvili, M, Gehrke, "A new proof of completeness of S4 with respect to real line," APAL, 133,no 1-3, p. 287-302 (2005).
B. Konev, R. Kontchakov, D. Tishovsky, F. Wolter and M. Zakharyaschev, ``On dynamic topological and metric logics'', Studia Logica (2006).
P. Kremer and G. Mints, ``Dynamic topological logic'', Bulletin of Symbolic Logic 3, 371-372 (1997).
G.Mints and T. Zhang, ``A proof of topological completeness for S4 in (0,1) '', (2006).