|
|
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 http://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 http://www.cs.gc.cuny.edu/~sartemov/
concerning a proof of the realization theorem which does not depend
on cut-elimination in S4.
|
