This Week in Logic at CUNY:
– – – – Monday, Nov 14, 2011 – – – –
– – – – Tuesday, Nov 15, 2011 – – – –
Computational Logic Seminar
November 15, Time 2:00 – 4:00 PM, Room 3309
Author: Sergei Artemov (Graduate Center)
Title: Provability vs. computational semantics for intuitionistic logic
Abstract: The intended semantics of first-order intuitionistic logic was the Brouwer-Heyting-Kolmogorov (BHK) semantics (1934) that explains intuitionistic validity using notions of proof and computable function (construction). BHK ideas inspired Kleene’s realizability (1945), which led to the class of computational interpretations based on the notion of a computable function. A good example of computational BHK semantics is given by Martin-Lof type theory. Since, in a formal mathematical setting, a computational program does not yield a proof of its correctness, a purely
computational semantics cannot provide an adequate account of BHK proofs. On the other hand, formal proof of a sigma-formula yields a corresponding computational program, hence a proof-based semantics could, in principle, represent BHK in its entirety. In this talk we will discuss when exactly computational semantics deviates from BHK and show that the provability BHK developed in the framework of the logic of proofs (1995-2011) is free of these deficiencies.
– – – – Wednesday, Nov 16, 2011 – – – –
– – – – Thursday, Nov 17, 2011 – – – –
– – – – Friday, Nov 18, 2011 – – – –
Logic Workshop and Set Theory Seminar
Friday, November 18, 2011 10:00 am GC 6417
Professor Peter Koepke (Rheinische Friedrich-Wilhelms-Universität Bonn) Violating the Singular Cardinals Hypothesis without Large Cardinals
Abstract. After Easton had proved that the behavior of the exponential function 2κ at regular cardinals κ is independent of the axioms of set theory except for some simple classical laws, attention turned to the situation at singular cardinals. The Singular Cardinals Hypothesis SCH implies that the Generalized Continuum Hypothesis GCH 2κ = κ+ holds at a singular cardinal κ if GCH holds below κ. The SCH has triggered many developments in large cardinals, forcing and inner model theory. Gitik and Mitchell have determined the consistency strength of the negation of SCH in Zermelo Fraenkel set theory with the axiom of choice in terms of measurable cardinals of high Mitchell orders.
Over several years, Arthur Apter and I have pursued a program of determining such consistency strengths in Zermelo Fraenkel set theory without the axiom of choice. Often the consistency strengths become much lower than in the choiceful setting. In my talk I want to present joint work with Moti Gitik that the following is relatively consistent with Zermelo Fraenkel set theory: GCH holds below the first
uncountable limit cardinal ℵω and there is a surjection from its power set P(ℵω) onto some arbitrarily high cardinal λ. The proof uses forcing and symmetric submodels to adjoin λ subsets of ℵω that have a lot of pairwise agreement so that the GCH below ℵω is preserved.
The result lead to the conjecture that without the axiom of choice and without assuming large cardinal strength an – appropriately modified – exponential function can take rather arbitrary values at all infinite cardinals.
Note the special time! This talk begins at 10 am, and is joint between the CUNY Logic Workshop and the Set Theory Seminar. There will be a second Logic Workshop talk today at 2 pm.
Model Theory Seminar
Friday, November 18, 2011 12:30 pm GC 6417
Mr. Manuel Alves (Ph.D. Program in Mathematics, Graduate Center of CUNY) Zilber’s trichotomy
Friday, November 18, 2011 2:00 pm GC 6417
Dr. Sam Sanders (Ghent University)
Reuniting the antipodes: bringing together Nonstandard Analysis and Constructive Analysis
Abstract. Constructive Analysis was introduced by Erret Bishop to identify the `computational meaning’ of mathematics. In the spirit of intuitionistic mathematics, notions like `algorithm,’ `explicit computation,’ and `finite procedure’ are central. The exact meaning of these vague terms was left open, to ensure the compatibility of Constructive Analysis with several traditions in mathematics. Constructive Reverse Mathematics (CRM) is a spin-off of Harvey Friedman’s famous Reverse Mathematics program, based on Constructive Analysis. Bishop famously derided Nonstandard Analysis for its lack of computational meaning. In this talk, we introduce `Ω-invariance’: a simple and elegant definition of `finite procedure’ in (classical) Nonstandard Analysis. Using an intuitive interpretation, we obtain many results from CRM, thus showing that Ω-invariance is quite close to Bishop’s notion of `finite procedure.’
This is the second Logic Workshop talk of the day. The first, by Peter Koepke, begins at 10:00 am.
Next Week in Logic at CUNY:
– – – – Monday, Nov 21, 2011 – – – –
– – – – Tuesday, Nov 22, 2011 – – – –
– – – – Wednesday, Nov 23, 2011 – – – –
– – – – Thursday, Nov 24, 2011 – – – –
*** CUNY Holiday ***
– – – – Friday, Nov 25, 2011 – – – –
*** CUNY Holiday ***
– – – – Other Logic News – – – –
– – – – Web Site – – – –
The majority of this information, including an interactive calendar of future events, can be found at our website: