Events 2014-2015

Logic Colloquium

September 05, 2014, 4:10 PM (60 Evans Hall)

Paolo Mancosu
Professor of Philosophy, University of California, Berkeley

In good company? On Hume’s principle and the assignment of numbers to infinite concepts

In a recent article, I have explored the historical, mathematical, and philosophical issues related to the new theory of numerosities. The theory of numerosities provides a context in which to assign numerosities to infinite sets of natural numbers in such a way as to preserve the part-whole principle, namely if a set A is properly included in B then the numerosity of A is strictly less than the numerosity of B. Numerosities assignments differ from the standard assignment of size provided by Cantor’s cardinality assignments. In this talk I generalize some specific worries, raised by Richard Heck, emerging from the theory of numerosities to a line of thought resulting in what I call a ‘good company’ objection to Hume’s principle (HP). The talk has four main parts. The first takes a historical look at nineteenth-century attributions of equality of numbers in terms of one-one correlation and argues that there was no agreement as to how to extend such determinations to infinite sets of objects. This leads to the second part where I show that there are countably infinite many abstraction principles that are ‘good’, in the sense that they share the same virtues of HP and from which we can derive the axioms of second-order arithmetic. All the principles I present agree with HP in the assignment of numbers to finite concepts but diverge from it in the assignment of numbers to infinite concepts. The third part connects this material to a debate on Finite Hume Principle between Heck and MacBride and states the ‘good company’ objection as a generalization of Heck’s objection to the analyticity of HP based on the theory of numerosities. I then give a taxonomy of possible neo-logicist responses to the ‘good company’ objection.

Logic Colloquium

October 03, 2014, 4:10 PM (60 Evans Hall)

Sanjit Seshia
Associate Professor of Electrical Engineering and Computer Science, University of California, Berkeley

The Logic of Cars: Reasoning about Cyber-Physical Systems with Computational Logic

Cyber-physical systems (CPS) are those that tightly integrate computational processes with the physical world. Examples include medical devices and systems, automotive systems, intelligent power systems, and robots. In this talk, we explore how computational logic can be an effective way to model, design, and verify cyber-physical systems. Using today’s automobiles as a motivating application, we will explore the use of logic, especially temporal logic, in reasoning about such systems. The talk will survey some core theoretical problems along with current approaches to solve them, and sketch directions for future work.

Logic Colloquium

October 17, 2014, 4:10 PM (60 Evans Hall)

Dominic Hughes
Visiting Scholar, Department of Mathematics, Stanford University

First-order proofs without syntax

Proofs of first-order logic are traditionally syntactic, built inductively from symbolic inference rules. This talk reformulates classical first-order logic (predicate calculus) with proofs which are combinatorial rather than syntactic. A combinatorial proof is defined by graph-theoretic conditions which can be verified easily (linear time complexity).

To be accessible to a broad audience (mathematicians, computer scientists, logicians and philosophers—including undergraduates) the lecture uses many colorful pictorial examples. Niche technicalities (such as relationships with Gentzen’s sharpened Hauptsatz for LK and Herbrand’s theorem) are deferred to the end.

The work extends ‘Proofs Without Syntax’ [Annals of Mathematics, 2006], which treated the propositional case.

Logic Colloquium

October 24, 2014, 4:10 PM (60 Evans Hall)

Thomas Scanlon
Professor of Mathematics, University of California, Berkeley

Differential algebraic equations from definability

Many valued “functions” play an important role in complex analysis. In many cases of interest, these may converted to honest functions through the application of a differential operator. For example, the complex logarithm is only well defined up to the addition of an integral multiple of twice pi times the square root of negative one, but the logarithmic derivative which takes a function f(z) to the derivative of log(f(z)) is a well-defined function from (nowhere zero, differentiable, complex valued) functions to functions. Curiously, the logarithmic derivative is actually a differential rational function. That is, it is given by an expression which is a rational function of its argument and some of the derivatives of the argument. Other functions obtained by applying differential operators to eliminate the ambiguity of multivalued functions share this feature. I will describe a general context in which multivalued functions arising as inverses to certain analytic covering maps may be converted to well-defined differential algebraic functions by composing them with a well chosen differential operator.

While the theorem itself has some nice consequences in the theories of functional transcendence and differential algebra, in this lecture I will focus on two ideas from logic underlying the proof. First, the notion of elimination of imaginaries in the theories of algebraically closed and differentially closed fields will supply the requisite differential operator. Secondly, a beautiful theorem of Peterzil and Starchenko on definable complex analytic sets will be used to show that the classical analytic construction of such functions is necessarily algebraic.

Slides

Logic Colloquium

November 07, 2014, 4:10 PM (60 Evans Hall)

Balder ten Cate
Computer Scientist at LogicBlox and Associate Adjunct Professor of Computer Science, UC Santa Cruz

Craig interpolation theorems and database applications

The Craig interpolation theorem, proved by William Craig in the 1950s, states that every valid first-order implication A |= B has an interpolant C such that A |= C and C |= B and all non-logical symbols occurring in C occur both in A and in B. Moreover, such an interpolant C can be effectively constructed from a proof of the implication A |= B.

The Craig interpolation theorem is considered one of the cornerstones in our understanding of first-order model theory and proof theory.

Over the last few years, we have seen the emergence of several new applications of Craig interpolation in the area of data management. In particular, interpolation-based techniques have been proposed for querying under access restrictions and semantic query optimization.

These applications, in turn, have led to the study of new variants of Craig interpolation. I will present two such new theorems, namely an interpolation theorem for first-order formulas with relational access restrictions, and an effective interpolation theorem for the guarded-negation fragment of first-order logic.

Slides

Logic Colloquium

November 21, 2014, 4:10 PM (60 Evans Hall)

Juliet Floyd
Professor of Philosophy, Boston University

The Sheffer Box

In May 2012, with the help of Bernard Linsky, I discovered a missing box of original documents and research materials pertaining to the work of H.M. Sheffer (1882-1964), the logician known for his strokes. The box had been assembled and saved by Burton Dreben, with whom I worked on Sheffer in 1988. This talk will report on my assembly and analysis of these primary resource materials.

Sheffer is of interest for our understanding of the reception of logic in the United States: the work of Frege, Russell, Zermelo, the early Wittgenstein, and others. A student of Royce, William James, Huntington, and Russell, he made some contributions to the algebra of logic tradition, though his own “general theory of notational relativity” never reached mathematical fruition. He influenced many, including C.H. Langford, and, slightly and indirectly, Zermelo.
In addition, however, the philosophical strands of his thinking form an interesting comparison and contrast to those of his contemporaries Wittgenstein and C.I. Lewis, on whom he lectured at Harvard, and those of Emil Post, with whom Sheffer corresponded about his “general theory of notational relativity”.

Sheffer took down the only extant notes of Bertrand Russell’s 1910 lectures at Cambridge University, and these, now being edited by Bernard Linsky, are among the materials I shall discuss. Other materials in the box included correspondence with Russell in which Sheffer describes meeting with Frege, Peano, Hadamard and others in 1911; notes of Sheffer’s spring 1922 logic lectures at Harvard, taken down by Marvin Farber; Farber’s correspondence with Sheffer concerning his work with Zermelo in 1923, as well as other lecture notes of relevance to our understanding of the history and presentation of logic in the United States the 1910s and 1920s.

Slides

Handout

Logic Colloquium

December 12, 2014, 4:10 PM (60 Evans Hall)

Christos Papadimitriou
C. Lester Hogan Professor of Electrical Engineering and Computer Science, UC Berkeley

Exponential existence proofs and complexity

Many computational problems in NP have the property that a solution is guaranteed to exist for every instance, and yet these problems do not seem to belong in P. Examples are factoring, Nash equilibrium, finding a short vector in a lattice, or a prime in [n, 2n], among many others. Such problems can be categorized by the corresponding existence proof. Rather surprisingly, it turns out that, in all known cases, this existence proof contains a simple graph-theoretic argument (such as “every graph has an even number of odd nodes,” or “every directed acyclic graph has a sink” or the pigeonhole principle) albeit applied to an exponentially large graph. Several natural problems are known to be complete for the corresponding classes. I shall introduce and discuss this intriguing aspect of complexity theory, including certain recent developments.

Logic Colloquium

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

Samson Abramsky
Christopher Strachey Professor of Computing, Oxford University

Contextual Semantics: From Quantum Mechanics to Logic, Databases, Constraints and Natural Language Semantics

Quantum Mechanics presents a radically different perspective on physical reality compared with the world of classical physics. In particular, results such as the Bell and Kochen-Specker theorems highlight the essentially non-local and contextual nature of quantum mechanics. The rapidly developing field of quantum information seeks to exploit these non-classical features of quantum physics to transcend classical bounds on information processing tasks.

In this talk, we shall explore the rich mathematical structures underlying these results. The study of non-locality and contextuality can be expressed in a unified and generalised form in the language of sheaves or bundles, in terms of obstructions to global sections. There are also strong connections with logic. For example, Bell inequalities, one of the major tools of quantum information and foundations, arise systematically from logical consistency conditions.

These general mathematical characterisations of non-locality and contextuality also allow precise connections to be made with a number of seemingly unrelated topics, in classical computation, logic, and natural language semantics. By varying the semiring in which distributions are valued, the same structures and results can be recognised in databases and constraint satisfaction as in probability models arising from quantum mechanics. A rich field of contextual semantics, applicable to many of the situations where the pervasive phenomenon of contextuality arises, promises to emerge.

Slides

Logic Colloquium

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

Pierre Simon
CNRS, Université Claude Bernard - Lyon 1

Around finite VC-dimension and the (p,k)-theorem

Let N points be chosen at random in some finite domain of the plane. With high probability, for every circle, the proportion of points inside the circle is very close to the area of the circle. (Hence for example a computer can approximately reconstruct a disc given random points inside and outside of it.) This works because the family of discs satisfies a combinatorial property known as finite VC-dimension. This notion originates in machine learning theory: the property described implies that a class of finite VC-dimension is “learnable”. In the first part of my talk, I will present this and state a measure-free analog of this learnability property called the (p,k)-theorem (due to Alon-Kleitman and Matousek).

The definition of finite VC-dimension also appeared independently in model theory under the name NIP (negation of the Independence Property). A formula f(x,y) is NIP if the family of definable sets it defines has finite VC-dimension. In the second part of the talk, I will discuss some interesting consequences of the (p,k)-theorem in model theory and mention open problems.

Logic Colloquium

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

Andrew Marks
NSF Postdoctoral Fellow, Department of Mathematics, California Institute of Technology

Baire measurable paradoxical decompositions and a Baire category solution to the dynamical von Neumann-Day problem

The Banach-Tarski paradox states that the unit ball in 3 is equidecomposable with two unit balls in 3 by rigid motions. In 1930, Marczewski asked whether there is such an equidecomposition where each piece has the Baire property. Using an intricate construction, Dougherty and Foreman gave a positive answer to this question.

We generalize Dougherty and Foreman’s result to completely characterize which Borel group actions have Baire measurable paradoxical decompositions. We show that if a group acting by Borel automorphisms on a Polish space has a paradoxical decomposition, then it admits a paradoxical decomposition using pieces having the Baire property. We also obtain a Baire category solution to the dynamical von Neumann-Day problem, in the spirit of Whyte and Gaboriau-Lyons: if a is a nonamenable action of a group on a Polish space X by Borel automorphisms, then there is a free Baire measurable action of 𝔽2 on X which is Lipschitz with respect to a. The main tool we use to prove these theorems is a version of Hall’s matching theorem for Borel graphs.

This is joint work with Spencer Unger at UCLA.

Logic Colloquium

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

Valeria de Paiva
AI and NLU Sunnyvale Lab, Nuance Communications

Constructive Modal Logics: 15 years later

This talk will review the program of intuitionistic modal logic in its two original sources: modal logicians interested in Intuitionism and functional programmers/type theorists interested in (computational) modalities. I will discuss some trends of this kind of work since the first Intuitionistic Modal Logic and Applications (IMLA) in Trento in 1999 and the tendencies that we can see in this line of work today. http://www.cs.bham.ac.uk/~vdp/

Slides

Logic Colloquium

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

Keita Yokoyama
Assistant Professor, School of Information Science, Japan Advanced Institute of Science and Technology

Reverse mathematics and program termination

It is well-known that proof theory and computer science have a good connection. In this talk, I will focus on the relation between reverse mathematics and the study of program termination. In the study of reverse mathematics, Ramsey’s theorem is one of the most important topics and the strength of Ramsey’s theorem is well-investigated from both of the proof-theoretic view point and the computability theoretic view point. On the other hand, Ramsey’s theorem is often used in computer science. In the study of termination analysis, Podelski/Rybalchenko used Ramsey’s theorem for pairs to introduce a new algorithm for termination checking. Looking at the above connection with Ramsey’s theorem, we study the relation between reverse mathematics and termination analysis.

This is a joint work with Stefano Berardi and Silvia Steila.

Alfred Tarski Lectures

March 30, 2015, 4:10 PM (2 LeConte Hall)

Julia F. Knight
Charles L. Huisking Professor of Mathematics, University of Notre Dame

Computability and complexity of mathematical structures

Alfred Tarski Lectures

April 01, 2015, 4:10 PM (2 LeConte Hall)

Julia F. Knight
Charles L. Huisking Professor of Mathematics, University of Notre Dame

Comparing classes of countable structures

Alfred Tarski Lectures

April 03, 2015, 4:10 PM (2 LeConte Hall)

Julia F. Knight
Charles L. Huisking Professor of Mathematics, University of Notre Dame

Computability and complexity of uncountable structures

Logic Colloquium

April 17, 2015, 4:10 PM (60 Evans Hall)

Tadeusz Litak
FAU Erlangen-Nürnberg

Whence Cometh Incompleteness?

I will explain the background of my recent collaboration with Wes Holliday. It is well known among modal logicians that while “naturally” obtained modal logics tend to be Kripke complete, things look very differently when one looks at the class of all modal logics. In the 1970’s, S.K. Thomason found a fundamental reason why this phenomenon is unavoidable: modal consequence over Kripke frames is every bit as complex as full second-order consequence. Shortly afterward, Wim Blok proved another amazing result: even those logics that are complete tend to be surrounded by uncountably many incomplete ones, which are sound wrt precisely the same class of Kripke structures. Kripke incompleteness turned out to be much more of a norm than anybody had expected; and in a very precise sense, the problem is irreparable, at least as long as the notion of proof remains decidable.

A question then arises if some sensible generalization of Kripke semantics would make the phenomenon of incompleteness disappear. In a way, the answer was known even before Kripke frames dominated the picture: every modal logic is complete wrt Boolean Algebras with Operators (BAOs). As it turns out, this is the best general completeness result we can hope for. It is possible to find naturally motivated semantics properly contained between Kripke semantics and algebraic semantics which do not suffer from the “Thomason effect”: the induced notion of consequence can be axiomatized. However, as soon as these notions nontrivially depart from the full generality of algebraic semantics and try to capture at least some of the defining properties of Kripke frames, not only can one still find examples of incomplete logics, but the limitative result of Blok survives.

These questions were investigated in my PhD dissertation a decade ago, building on several decades of work in the modal community. By the time the dissertation was completed, there was still one possible escape route left: one of the three defining properties of (dual algebras of) Kripke frames could perhaps allow a general completeness result. More recently, Wes Holliday’s work on “possibility semantics” for modal logic rekindled the interest in that particular notion of completeness. Now we have found that even this escape route is blocked. Furthermore, the story turns out to involve an unjustly forgotten example, paper and program of Johan van Benthem.

Logic Colloquium

May 01, 2015, 4:10 PM (60 Evans Hall)

Stuart Russell
Professor of Computer Science and Smith-Zadeh Professor in Engineering, University of California, Berkeley

Unifying logic and probability: The BLOG language

Logic and probability are ancient subjects whose unification holds significant potential for the field of artificial intelligence. The BLOG (Bayesian LOGic) language provides a way to write probability models using syntactic and semantic devices from first-order logic. In modern parlance, it is a relational, open-universe probabilistic programming language that allows one to define probability distributions over the entire space of first-order model structures that can be constructed given the constant, function, and predicate symbols of the program. I will describe the language mainly through examples and cover its application to monitoring the Comprehensive Nuclear-Test-Ban Treaty.

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