FALL 2003
Tuesday, 2pm – 4pm, room 4421
December 2 talk
Yegor Bryukhov. Type Theory for a practicing mathematician.
Abstract: continue
December 2 talk
Yegor Bryukhov. Type Theory for a practicing mathematician.
Abstract: In this talk we will follow R.Constable’s paper “Naive Computational Type Theory” which in turn “follows” the book of Paul Halmos “Naive Set Theory”. This paper gives some new perspectives in Type Theory, including a new meaning of openness of Type Theory. We’ll start from the fundamentals: “what is type”, “propositions as types”, and then go to type-theoretic analogues of a set, subset, pair, union, intersection, function, relation, etc. We will consider two meanings of this popular statement “Type Theory is open-ended”, one is old and the other one is new. They are related but the new one is much deeper. It shows that the Type Theory is VERY different from the Set Theory. Time permitting we’ll discuss dependent intersection (a relatively new result by Alexei Kopylov) and records.
November 25 talk
Walter Dean (GC and Rutgers). From Church’s Thesis to Extended Church’s Thesis.
Abstract: In 1936, Church officially announced the statement which we now refer to as Church’s Thesis as follows: We now define the notion … of an effectively calculable function of positive integers by identifying it with the notion of a recursive function of positive integers (or a $\lambda$-definable function of positive integers). This definition is thought to be justified by the considerations which follow, so far as positive justification can ever be obtained for the selection of a formal definition to correspond to an intuitive notion.
In contrast, Lewis and Papadimitriou’s popular _Elements of the theory of computation_ presents Church’s Thesis as follows: [W]e take the Turing machine to be a precise formal equivalent of the intuitive notion of “algorithm”: nothing will be considered an algorithm if it cannot be rendered as a Turing machine. The principle that Turing machines are formal versions of algorithms and that no computational procedure will be considered an algorithm unless it can be presented as a Turing machine is known as Church’s Thesis …
This talk will consider the relationship between three statements about computability. The first is intended to represent the view of Church (which was also shared by Kleene and Turing), the third that of L&P (which is shared by several other modern commentators) while the second reflects a important intermediary: * CT0: A function f: N -> N is effectively calculable iff it is (general) recursive. * CT: A function f: N -> N is algorithmically computable iff it is (general) recursive. * ECT: Any informally described and intuitively effective algorithm can be *analyzed* as a properly interpreted instance of a class of a formal models of computation (e.g. as a particular Turing machine or recursive function) in a manner which faithfully represents its essential procedural properties.
Time permitting, I will also argue for the following claims:
1) No version of CT or (more significantly) ECT was explicitly proposed by any of Church, Turing, Kleene or Post.
2) CT and ECT are clearly distinct proposal but are often mistakenly conflated. Correctly conceived, ECT functions as a strong argument in favor of CT versions of which are presented by Kleene (1955) and Rogers (1967).
3) Independent of the question of the truth of CT (i.e. of the existence of computable but non-recursive functions), there are both mathematical and conceptual grounds to reject any precise instance of ECT which could have been proposed before 1950.
4) Several modern versions of ECT have been proposed by (among others) Sieg & Byrne [1996], Gurevich [1999], [2003] and Moschovakis [1997], [2001]. I will not argue against them directly here, but will rather point out that they presuppose a view which I will call *algorithmic realism*. Roughly stated, this view claims that individual algorithms should be viewed as determinate, free-standing abstract objects akin to those of classical mathematics. On the basis of my argument for 3), I will offer some preliminary reasons why this view ought to regarded with suspicion.
November 18 talk
Florian Lengyel. Cartesian closed categories and lambda calculus II.
Abstract: Following the exposition in Lambek and Scott’s “Introduction to higher order categorical logic,” with its emphasis on categories as certain kinds of deductive systems, we introduce enough category theory to understand the equivalence between the category of typed lambda calculi and the category of cartesian closed categories and weak natural number objects. The talk is in two parts. The first part introduces basic categorical notions, such as categories, functors, limits, adjoints, equivalences and cartesian closed categories. We give examples of these notions from mathematics and computer science.
The second part develops more specific machinery for the equivalence: free cartesian categories generated by graphs, polynomial categories, weak natural numbers objects in cartesian closed categories, typed lambda calculi, the internal language of a cartesian closed category with a weak natural numbers object, and the category of typed lambda calculi. We define the cartesian closed category generated by a typed lambda calculus, and give the equivalence of categories.
November 11 talk
Florian Lengyel. Cartesian closed categories and lambda calculus I.
Abstract: Following the exposition in Lambek and Scott’s “Introduction to higher order categorical logic,” with its emphasis on categories as certain kinds of deductive systems, we introduce enough category theory to understand the equivalence between the category of typed lambda calculi and the category of cartesian closed categories and weak natural number objects. The talk is in two parts. The first part introduces basic categorical notions, such as categories, functors, limits, adjoints, equivalences and cartesian closed categories. We give examples of these notions from mathematics and computer science.
The second part develops more specific machinery for the equivalence: free cartesian categories generated by graphs, polynomial categories, weak natural numbers objects in cartesian closed categories, typed lambda calculi, the internal language of a cartesian closed category with a weak natural numbers object, and the category of typed lambda calculi. We define the cartesian closed category generated by a typed lambda calculus, and give the equivalence of categories.
November 4 talk
No formal talk.
October 28 talk
Eduardo Bonelli, Stevens-Tech. On Natural Deduction for the Logic of Proofs.
Abstract: Recent work has studied a reformulation of proof systems in natural deduction style for modal logic via so called judgemental reconstruction [DP01a] following the methodology of Martin-Löf [ML83]. In this work we introduce hypothetical judgements with explicit evidence and provide an explanation of such judgements by means of inference rules. This yields a concise natural deduction presentation for the Logic of Proofs. This is work in progress and is part of a more general effort to explore the computational contents of LP.
[DP01a] Rowan Davies and Frank Pfenning. A Judgemental Reconstruction of Modal Logic. Mathematical Structures in Computer Science, 11:511-540,2001 [ML83] Per Martin Lof. On the Meaning of the Logical Constants and the Justifications of the Logical Laws. Lectures given at the meeting Teoria della Dimostrazione e Filosofia della Logica, in Siena, 6-9 April 1983, by the Scuola di Specializzazione in Logica Matematica of the Universit? degli Studi di Siena.October 21 talk
Hidenori Kurokawa. On Basic Intuitionistic Logic of Proofs.
Abstract: At this talk a progress on a Logic of Proofs for intuitionistic arithmetic HA will be reported. Problem 4 from Artemov’s list https://www.cs.gc.cuny.edu/~sartemov/ asks to check a completeness of the Basic Intuitionistic Logic of Proofs = intuitionistic logic + x:F–›F + x:F V ¬ x:F (no functional symbols present) with respect to HA. A natural way of proving that combines methods from Artemov and Strassen papers of 1993-94 on the classical Basic Logic of Proofs and de Jongh – Smorynski work on completeness of intuitionistic logic with respect to HA. We will talk about the papers mentioned above and report a progress on BILP. In particular, we describe Kripke style models for BILP and establish a completeness result.
October 14 talk
Bryan Renne. On game semantics for the Logic of Proofs.
Abstract:
I will present a game semantics for LP in the spirit of the propositional Abelard/Eloise games played on syntactic parse trees of a given formula. After showing the semantics is sound and complete with respect to the Hilbert-style theory LP, I’ll constructively prove the realization theorem, which states that a formula is true iff Eloise has a strategy to win any game played on that formula. Hence, in LP, terms are encoded strategies for the games played on the formulas these terms prove.
October 7 talk
No seminar this Tuesday (October 7), since CUNY works by Monday schedule.
September 30 talk
Eric Pacuit will finish his talk on Kripke style semantics for the Logic of Proofs. In particular, he will show how we might extend Fitting semantics to LPS5, which is LP plus the realized Euclidean axiom.
Then, time permitting, Bryan Renne will begin give an overview of the paper by Robert Constable “Types in Logic, Mathematics and Programming”. In Sam Buss ed. Handbook of Proof Theory, Elsevier Science, 1997.
September 23 talk
Eric Pacuit will speak on Kripke style semantics for the Logic of Proofs.
In two recent reports by Fitting, a Kripke semantics for Artemov’s logic of proofs has been developed. The main idea is to extend a standard Kripke model with an evidence function. Given a state of the world w, and a proof polynomial t this function returns a set of formulas that are interpreted as the formulas that t provides evidence for at state w. We will first give an overview of this semantics and discuss soundness and semantics. We will then (time permitting) show how we might extend this semantics to LPS5, which is LP plus the realized Euclidean axiom.
September 16 talk
Bryan Renne
Title: “LP tableaux revisited”
I will be discussing the LP tableau system I introduced last semester, only it is now expressed in terms of Mkrtychev models (M-models) instead of as a syntactic transformation between an already-existing Gentzen proof system for LP. I will prove soundness and completeness results of the system with respect to M-models, which is very nice as it takes the general form of such results in tableaux (although there is a “small” twist).
September 8 talk
Professor Melvin Fitting, CUNY
Title: Realization of S4 in the Logic of Proofs: a model theoretic proof.
Abstract (written by S.A.):
An alternative proof of the realization theorem of S4 by proof polynomials will be given. The method used is the maximal consistent set construction. The author noticed that the collection of the maximal consistent sets over LP has the natural S4-model Kripke structure, which could provide a good hint of where to look for a Kripke semantics for LP. The paper clarifies an old question about the role of the operation “+” union on proof polynomials. It is shown that there is some realization of S4 into the “+”-free fragment of LP, though for “natural” realizations one still needs “+”. The paper also seems to provide a solution to Problem 14 from my list of problems in https://www.cs.gc.cuny.edu/~sartemov/ concerning a proof of the realization theorem which does not depend on cut-elimination in S4.