Blog Archives

Topic Archive: proof theory

Computational Logic SeminarTuesday, February 14, 20172:00 pmGraduate Center, rm. 4422

Melvin Fitting

Cut Elimination

Lehman College - CUNY Graduate Center

Gentzen proved a famous cut elimination theorem using constructive methods. It is also possible to prove it non-constructively, with a conceptually simpler argument, but a constructive proof is important for a number of reasons. I will present the constructive argument for cut elimination, for classical propositional logic, formulated using tableaus. This is purely expository; there is nothing new. But it is a proof that every logician, or logician-to-be, should know, and I will cover the basics using a detailed set of slides which will be made available afterward, on my web site.

Computational Logic SeminarTuesday, May 3, 20162:00 pmGraduate Center, rm. 4422

Lev Beklemishev

Some abstract versions of Goedel’s Second Incompleteness Theorem based on non-classical logics

Steklov Mathematical Institute of Russian Academy of Sciences in Moscow

We study abstract versions of Goedel’s second incompleteness theorem and formulate generalizations of Loeb’s derivability conditions that work for logics weaker than the classical one. We isolate the role of the contraction and weakening rules in Goedel’s theorem and give a (toy) example of a system based on modal logic without contraction invalidating Goedel’s argument. On the other hand, Goedel’s theorem is established for a version of Peano arithmetic without contraction. (Joint work with Daniyar Shamkanov)

Model theory seminarFriday, March 21, 201412:30 pmGC 6417

Henry Towsner

The consistency of Peano Arithmetic

University of Pennsylvania

In 1936, only a few years after the incompleteness theorems were proved, Gentzen proved the consistency of Peano arithmetic by using transfinite induction up to the ordinal epsilon_0. I will give a short proof of the result, based on on the simplification introduced by Schutte, and discuss some of the consequences.

CUNY Logic WorkshopFriday, February 21, 20142:00 pmGC 6417

Michael Benedikt

The proof/plan correspondence in databases

Oxford University

We consider answering queries over datasources (for logicians: finite relational structures) that are connected to one another by integrity constraints (logical relationships). A relation in a datasource may have multiple means of access with different required arguments, and the means of access within and across relations may differ radically in cost. We present a method for generating the lowest cost query plan, where a plan is a reformulation of the query referencing only the allowable access methods, equivalent to the original query on all datasources satisfying the integrity constraints. A solution to this problem can be applied in many database contexts, including answering queries using views, optimizing queries using constraints, and querying on top of web services or web forms. It could also be applied to give a more logic-based foundation for traditional database query planning.

Proof-driven query reformulation generates plans by applying interpolation procedures to a “proof that the query can be answered,” an approach that goes back at least to Craig’s proof of the Beth Definability theorem via interpolation. A few additional ingredients are needed to apply interpolation to database problems, including:

— variations of Beth Definability that allow us to target plans (explicit definitions) of specific forms

— an extension of interpolation that considers the “access patterns” within quantification

— specialized proof procedures for classes of integrity constraints of interest to databases

— cost-based search procedures for concurrently exploring the collection of proofs and plans

The resulting query planning system blends automated deduction, query optimization, and heuristic search.

This is joint work with Balder ten Cate, Julien Leblay and Efi Tsamoura.

Computational Logic SeminarTuesday, November 5, 20132:00 pmGraduate Center, rm. 3209

Elena Nogina

Reflection Principles Involving Provability and Explicit Proofs

The City University of New York

Reflection principles are classical objects in proof theory and the areas studying Gödel’s Incompleteness. Reflection principles based on provability predicates were introduced in the 1930s by Rosser and Turing, and later were explored by Feferman, Kreisel & Levi, Schmerl, Artemov, Beklemishev and others.

We study reflection principles of Peano Arithmetic involving both Proof and Provability predicates. We find a classification of these principles and establish their linear ordering with respect to their metamathematical strength.

CUNY Logic WorkshopFriday, December 13, 20132:00 pmGC 6417

Sam Sanders

Higher-order Reverse Mathematics: Where existence meets computation via infinitesimals.

Department of Mathematics, Ghent University

Classically, the existence of an object tells us very little about how to construct said object.
We consider a nonstandard version of Ulrich Kohlenbach’s higher-order Reverse Mathematics
in which there is a very elegant and direct correspondence between, on one hand, the existence
of a functional computing an object and, on the other hand, the classical existence of this object
with the same standard and nonstandard properties. We discuss how these results -potentially-
contribute to the programs of finitistic and predicativist mathematics.

Sam Sanders
Department of Mathematics, Ghent University
Sam Sanders finished his PhD in 2010 at Ghent University, under the supervision of Andreas Weiermann and Chris Impens, and now holds a postdoctoral position there. He studies analysis and the foundations of mathematics, doing work in reverse mathematics using nonstandard analysis, proof theory, and computability theory.
Sergei Artemov
The CUNY Graduate Center
Professor Artemov holds a Distinguished Professor position at the Graduate Center of the City University of New York, in the Computer Science, Mathematics and Philosophy programs. He is also Professor of Mathematics at Moscow State University, the founder and the Head of the research laboratory Logical Problems in Computer Science. He conducts research in the areas of logic in computer science, mathematical logic and proof theory, knowledge representation and artificial intelligence, automated deduction and verification and optimal control and hybrid systems.