Events 2015-2016

Logic Colloquium

August 28, 2015, 4:10 PM (60 Evans Hall)

Antonio Montalban
Associate Professor of Mathematics, UC Berkeley

Analytic Equivalence Relations with 1-many Classes

We will survey the new results connecting Vaught’s conjecture and computability theory. We will look at some of these result from the more general viewpoint of analytic equivalence relations.

There are two types of results we will concentrate on. On the one hand are the ones about equivalence relations satisfying hyperarithmetic-is-recursive, which provide a purely computability theoretic equivalent to Vaught’s conjecture. On the other hand are the ones about equivalence relations on the natural numbers that are “intermediate,” which I hope will eventually provide another equivalent statement.

Slides

Logic Colloquium

September 11, 2015, 4:10 PM (60 Evans Hall)

Thomas Icard
Assistant Professor of Philosophy and Symbolic Systems, Stanford University

A Survey on Topological Semantics for Provability Logics

This will be a survey of ideas and results on topological interpretations of provability logics, especially polymodal provability logics. Esakia first proved completeness for the basic Gödel-Löb logic of provability with respect to scattered spaces. Abashidze and Blass (independently) proved completeness w.r.t. a particular scattered space defined on the ordinal omega^omega. I will discuss older work of my own that extended the Abashidze-Blass result to a polymodal provability logic, which is complete with respect to a polytopological space on epsilon_0. I will then discuss more recent developments, including work by Beklemishev, Fernandez, Joosten, Gabelaia, Aguilera, and others, generalizing and improving upon much of this.

Slides

Logic Colloquium

September 25, 2015, 4:10 PM (60 Evans Hall)

Dana Scott
University Professor, Emeritus, Carnegie Mellon University; Visiting Scholar, UC Berkeley

Can Modalities Save Naive Set Theory?

The late “Grisha” Mints once asked the speaker whether a naive set theory could be consistent in modal logic. Specifically he asked whether restricting the comprehension scheme to necessary properties was safe. Scott was working on a set theory in the Lewis system S4 of modal logic and Mints was happy to position his question in the same modal system. Obviously a very, very weak modality can avoid paradoxes, but such results are not especially interesting. At that time (2009) Scott could not answer the consistency question, and neither could Mints. Last November Scott noted that CMU Philosophy was hosting a seminar on a naive set theory by Harvey Lederman. Scott wrote him for his paper and said, “By the way, there is this question of Grisha Mints, and I wonder if you have an opinion?” Lederman sent back a sketch of a proof of the inconsistency of a strengthened version of comprehension. That proof at first did not quite work out, but was repaired in correspondence. Lederman mentioned the questions to two of his colleagues, and in March of 2015 Tiankai Liu suggested a possible model of a weaker comprehension scheme, which after a small correction gave a consistency proof. A few days later, Peter Fritz came up with essentially the same model. A paper has now been submitted for publication jointly by Fritz, Lederman, Liu, and Scott.

Slides

Paper

Logic Colloquium

October 09, 2015, 4:10 PM (60 Evans Hall)

Takayuki Kihara
JSPS Postdoctoral Fellow, Department of Mathematics, UC Berkeley

Recursion Theoretic Methods in Descriptive Set Theory and Infinite Dimensional Topology

The notion of degree spectrum of a structure in computable model theory is defined as the collection of all Turing degrees of presentations of the structure. We introduce the degree spectrum of a represented space as the class of collections of all Turing degrees of presentations of points in the space. The notion of point degree spectrum creates a connection among various areas of mathematics including computability theory, descriptive set theory, infinite dimensional topology and Banach space theory.

Through this new connection, for instance, we construct a family of continuum many infinite dimensional Cantor manifolds with property C in the sense of H aver/Addis-Gresham whose Borel structures at an arbitrary finite rank are mutually non-isomorphic. This provides new examples of Banach algebras of real valued Baire class two functions on metrizable compacta, and strengthen various theorems in infinite dimensional topology such as Pol’s solution to Alexandrov’s old problem.

To prove our main theorem, an invariant which we call degree co-spectrum, a collection of Turing ideals realized as lower Turing cones of points of a Polish space, plays a key role. The key idea is measuring the quantity of all possible Scott ideals (omega-models of WKL) realized within the degree co-spectrum (on a cone) of a given space. This is joint work with Arno Pauly (University of Cambridge, UK).

Slides

Logic Colloquium

October 23, 2015, 4:10 PM (60 Evans Hall)

Larry Moss
Professor of Mathematics, Indiana University, Bloomington

Natural Logic

Much of modern logic originates in work on the foundations of mathematics. My talk reports on work in logic that has a different goal, the study of inference in language. This study leads to what I will call “natural logic”, the enterprise of studying logical inference in languages that look more like natural language than standard logical systems. An early paper in this field is George Lakoff’s 1970 paper “Linguistics and Natural Logic.”

By now there is a growing body of work which presents logical systems that differ from first-order logic in various ways. Most of the systems are complete and decidable. Some are modern versions of syllogistic logic, but with additional features not present in syllogistic logics. And then there are flavors of logic which look rather far from either traditional or modern logic.

The talk will be programmatic and far-ranging rather than detailed. I hope to touch on computer implementations of natural logics, teaching materials on this topic, and interactions of logic and cognitive science. And keeping with most other talks in the Logic Colloquium, I’ll show that the whole subject of natural logic is full of questions with mathematical interest.

Slides

Logic Colloquium

November 06, 2015, 4:10 PM (60 Evans Hall)

Silvain Rideau
Morrey Visiting Assistant Professor, Department of Mathematics, UC Berkeley

Transferring imaginaries

Since it was first formulated by Poizat thirty years ago, the question of eliminating imaginaries, has become an important, if not necessary, step in understanding the model theory of given algebraic structures; it consists in classifying all the definable equivalence relations in a structure. An ever growing collection of such results is now available but this question remains open in many otherwise well understood structures.

Some of the recent elimination of imaginaries results are actually reductions to previously known elimination of imaginaries results. The goal of this talk will be to consider these reductions from an abstract standpoint and provide various settings in which one might derive elimination of imaginaires in a theory from elimination of imaginaries in some other theory.

Slides

Logic Colloquium

November 20, 2015, 4:10 PM (60 Evans Hall)

Edward Zalta
Senior Research Scholar, Center for the Study of Language and Information, Stanford University

Reflections on Foundations for Mathematical Structuralism

In a paper recently published in Mind (“Foundations for Mathematical Structuralism”), Nodelman and I offer a rigorous formulation of mathematical structuralism. A mathematics-free theory of structures and structural objects is presented in a background formalism and then the whole is applied to the analysis of mathematics. While the principal structuralist intuitions about structures and the elements of structures are preserved, distinctions formalized in the theory undermine a variety of arguments that have been put forward concerning the nature of structural elements. Arguments from Russell, Dedekind, Benacerraf, Shapiro, Linnebo, Awodey, Keranen, and others, are considered. For those interested in reading the paper in advance, a preprint is available at: http://mally.stanford.edu/Papers/structuralism.pdf

Logic Colloquium

December 04, 2015, 4:10 PM (60 Evans Hall)

Natarajan Shankar
Computer Scientist, SRI International

PVS and the Pragmatics of Formal Proof

A formal system establishes a trinity between language, meaning, and inference. Many domains of thought can be captured using formal systems so that sound conclusions can be drawn through correct inferences. Philosophers have long speculated about machines that can distinguish sound arguments from flawed ones, and with modern computing, we can realize this dream to a significant extent. A research program to mechanize formal proof inevitably confronts a range of foundational and pragmatic choices. Should the foundations be classical or constructive, and should they be based on set theory, type theory, or category theory? What definitional principles should the language admit? How can formalizations be constructed from reusable modules? Should proofs be represented in a Hilbert calculus, natural deduction, or sequent calculus? Which inference steps in the proof calculus can and should be effectively mechanized in order to close the gap between informal arguments and their formal counterparts?

SRI’s Prototype Verification System (PVS) is an interactive proof assistant aimed at capturing the pragmatic features of mathematical expression and argumentation. The PVS language augments a simply typed higher-order logic with subtypes, dependent types, and algebraic datatypes. The PVS interactive proof checker integrates a number of decision procedures into the sequent calculus proof system. We examine the implications of these choices for the original goal of constructing mathematically sound arguments.

Slides

Logic Colloquium

January 22, 2016, 4:10 PM (60 Evans Hall)

John R. Steel
Professor of Mathematics, UC Berkeley

Ordinality Definability in Models of the Axiom of Determinacy

Let HOD be the class of all hereditarily ordinal definable sets, and let M be a model of the Axiom of Determinacy. The inner model HOD^M consisting of all sets that are hereditarily ordinal definable in the sense of M is of great interest, for a variety of reasons. In the first part of the talk, we shall give a general introduction that explains some of these reasons.

We shall then describe a general Comparison Lemma for “hod mice” (structures that approximate HOD^M). Modulo still-open conjectures on the existence of iteration strategies, this lemma yields models M of the Axiom of Determinacy such that HOD^M can be analyzed fine structurally (for example, satisfies the GCH), and yet satisfies very strong large cardinal hypotheses (for example, that there are superstrong cardinals).

Model Theory Seminar

January 29, 2016, 4:10 PM (60 Evans Hall)

Pierre Simon
CNRS, Université Claude Bernard - Lyon 1

Decomposition of dependent structures

A structure is a set equipped with a family of predicates and functions on it, for example a group or a field. A structure is said to be dependent if it is not as complicated as a random graph (in some precise sense). The fields of complex numbers, real numbers and p-adic numbers are examples of dependent structures. If a dependent structure contains no definable order, then it is stable: a much stronger property that is now very well understood. Stability can be thought of as an abstraction of algebraic geometry. At the other extreme, are dependent structures which are very much controlled by linear orders. We call such structures distal. Distality is meant to serve as a general model for semi-algebraic (or analytic) geometry. In this talk, I will explain those notions and state a recent theorem saying that any dependent structure can be locally decomposed into a stable-like and a distal-like part.

Logic Colloquium

February 05, 2016, 4:10 PM (60 Evans Hall)

Vijay D’Silva
Google Research

Interpolant Construction and Applications

In the last decade, algorithms for the construction of interpolants from proofs have found numerous practical applications such as the analysis of circuits, generation of Floyd/Hoare proofs of program correctness, and parallelization of constraint solvers. The first part of this talk will trace how interpolation has spread from mathematical logic to commercial software via computational complexity theory and computer aided verification. The second part will delve into details of the algorithms for construction of interpolants in logics and theories. In the propositional case, the space of interpolant constructions has a semi-lattice structure that determines the logical strength and size of the interpolants obtained. In the case of first-order theories, this structure is still being unravelled. The talk will conclude with a review of open theoretical and empirical problems concerning interpolant construction.

Slides

Logic Colloquium

February 19, 2016, 4:10 PM (60 Evans Hall)

Christoph Benzmüller
Stanford University and Freie Universität Berlin

A Success Story of Higher-Order Theorem Proving in Computational Metaphysics

I will report on the discovery and verification of the inconsistency in Gödel’s ontological argument with reasoning tools for higher-order logic. Despite the popularity of the argument since the appearance of Gödel’s manuscript in the early 70’s, the inconsistency of the axioms used in the argument remained unnoticed until 2013, when it was detected automatically by the higher-order theorem prover LEO-II.

Understanding and verifying the refutation generated by LEO-II turned out to be a time-consuming task. Its completion required the reconstruction of the refutation in the Isabelle/HOL proof assistant. This effort also led to a more efficient way of automating higher-order modal logic S5 with a universal accessibility relation within the logic embedding technique we utilize in our work.

The development of an improved syntactical hiding for the logic embedding technique allows the refutation to be presented in a human-friendly way, suitable for non-experts in the technicalities of higher-order theorem proving. This should bring us a step closer to wider adoption of logic-based artificial intelligence tools by philosophers.

If time permits, I will also point to alternative, ongoing applications of the logic embeddings technique, such as the encoding of Zalta’s theory of abstract objects or the mechanization of Scott’s free logic.

Slides

Logic Colloquium

March 04, 2016, 4:10 PM (60 Evans Hall)

Katrin Tent
Professor of Mathematics and Mathematical Logic, Universität Münster

Describing finite groups by short sentences

We say that a class of finite structures for a finite first-order signature is r-compressible for an unbounded function r : N → N+ if each structure G in the class has a first-order description of size at most O(r(|G|)). We show that the class of finite simple groups is log-compressible, and the class of all finite groups is log3-compressible. The result relies on the classification of finite simple groups, the bi-interpretability of the twisted Ree groups with finite difference fields, the existence of profinite presentations with few relators for finite groups, and group cohomology.

Logic Colloquium

March 18, 2016, 4:10 PM (60 Evans Hall)

Guram Bezhanishvili
Professor of Mathematical Sciences, New Mexico State University

The algebra of topology: Tarski’s program 70 years later

In a slogan, Tarski’s program can be described as “creating an algebraic apparatus adequate for the treatment of portions of point-set topology” (McKinsey-Tarski, 1944). The “algebraic apparatus” can be developed in several ways. For example, we can look at the algebra of open sets of a topological space X or the powerset algebra of X equipped with topological closure (or interior). Both of these approaches are not only closely related, but are also widely used in logic. The first approach yields a topological representation of Heyting algebras, and hence provides topological completeness of intuitionistic logic (one of the first completeness results for intuitionistic logic, established by Tarski in the 1930s). On the other hand, the second approach provides a topological representation of closure algebras, thus yielding topological completeness of Lewis’s modal system S4. McKinsey and Tarski observed a close connection between these two approaches, which allowed them to prove that Gödel’s translation of intuitionistic logic into S4 is full and faithful. I will review this line of research of Tarski and his collaborators, discuss further advances in this direction, obtained in the second half of the twentieth century, and finish with the latest new developments.

Slides

Alfred Tarski Lectures

April 04, 2016, 4:10 PM (20 Barrows)

William W. Tait
Professor Emeritus, Department of Philosophy and CHSS, University of Chicago

On Skepticism about the Ideal

There is a historic skepticism about mathematics that hangs on the fact that the objects of mathematics, structures and their elements—numbers, functions, sets, etc., are ideal, i.e. that empirical facts, facts about the natural world, have no relevance to the truth of propositions about them.

Of course, the view that ‘existence’ simply means empirical existence, so that the term is misused as applied to ideal things can be countered only on pragmatic grounds, that we use the term in other contexts and that it is very useful there. The rejection of ideal existence becomes meaningful only if one has a transcendental ground on which to stand and judge applications of the term. I believe that the ground, at least implicitly, has been a wrong thesis about how language works, namely the view that genuine reference to objects presupposes a non-linguistic interaction with them. And that is what I want to talk about. My argument draws on a reading of Wittgenstein’s Philosophical Investigations, a reading which is more positive than a more common one according to which he, himself, was a skeptic.

Alfred Tarski Lectures

April 06, 2016, 4:10 PM (20 Barrows)

William W. Tait
Professor Emeritus, Department of Philosophy and CHSS, University of Chicago

Cut-Elimination for Subsystems of Classical Second-Order Number Theory: The Predicative Case

I will present the classical results of Gentzen and Schuette for first-order and ramified second-order number theory.

Alfred Tarski Lectures

April 08, 2016, 4:10 PM (20 Barrows)

William W. Tait
Professor Emeritus, Department of Philosophy and CHSS, University of Chicago

Cut-Elimination for Subsystems of Classical Second-Order Number Theory: Cut-Elimination for Π11 − CA with the ω-Rule—and Beyond(?)

I will present a simplification of the proof of cut-eliminability of Gaisi Takeuti and Mariko Yasugi for this system. In particular, I will avoid the use of Takeuti’s ordinal diagrams. (I do use the finite part of the Veblen hierarchy, though.) Given time and sufficient conviction, I may speak about the possibility of extending the result to Π21 − CA and beyond.

Logic Colloquium

April 22, 2016, 4:10 PM (60 Evans Hall)

Kai Wehmeier
Professor of Logic and Philosophy of Science, UC Irvine

The Role of Variables in Predicate Logic: Frege vs. Tarski

Standard presentations of predicate logic, following Tarski, segment a quantified statement such as x(P(x) ∧ R(x, a)) into the constituents x and P(x) ∧ R(x, a). At least on the face of it, Frege held a different view about the logical form of quantification; for him the same sentence decomposes into the constituents xxx and P( ) ∧ R( , a). In order to adjudicate between these views, I will develop some of the details of Fregean predicate logic, with special emphasis on the compositionality of its semantics. I will then compare Tarskian and Fregean treatments of variables and draw some philosophical conclusions from this comparison. In particular, I will address the extensionality of predicate logic and Kit Fine’s so-called antinomy of the variable.

Logic Colloquium

May 06, 2016, 4:10 PM (60 Evans Hall)

Omer Ben Neria
Hedrick Assistant Adjunct Professor of Mathematics, UCLA

The distance between HOD and V

The pursuit of better understanding of the universe of set theory V motivated an extensive study of definable inner models M whose goal is to serve as good approximations to V.
A common property of these inner models is that they are contained in HOD, the universe of hereditarily ordinal definable sets. Motivated by the question of how “close” HOD is to V, we consider various related forcing methods and survey known and new results. This is a joint work with Spencer Unger.

Special Logic Seminar

May 10, 2016, 4:10 PM (234 Moses Hall)

Johan van Benthem
Amsterdam and Stanford

Decidable Versions of First-Order Predicate Logic

There are two ways of finding decidability inside first-order logic: one is by restricting attention to language fragments, the other is by generalizing the usual semantics. In this talk, I explain a recent generalized semantics by Aldo Antonelli, which leads to a decidable version of predicate logic that induces an effective translation into the Guarded Fragment. I will discuss this proposal and the resulting program.

Also, I make a comparison with existing decidable first-order semantics via general assignment models and via games, and with the move in modal logic from relational semantics to neighborhood semantics. Finally, I discuss the resulting landscape of weak decidable first-order logics, and its links with decidable fragments of the first-order language. This suggests many open problems that I will flag throughout.

Ref. H. Andréka, J. van Benthem & I. Németi, 2016, ‘On a New Semantics for First‐Order Predicate Logic’, Journal of Philosophical Logic, to appear.