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.
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).