Math Logic Seminars
Schedule for Spring 2009
Visit
http://logic.cmu.edu/seminar/seminar.html for seminar details.
MONDAY, January 12, 2009
Philipp Gerhardy, Department of Mathematics, The University of Oslo, Blindern
Proof mining in topological dynamics
Time:4:40 P.M.
Location: BH 232Q
TUESDAY, January 27, 2009
James Cummings, Carnegie Mellon University.
Recent advances in polychromatic Ramsey theory
Time:12:00 P.M.
Location: BH 150
TUESDAY, February 3, 2009
Spencer Unger, Carnegie Mellon University.
The tree property
Time:12:30 P.M.
Location: BH 150
TUESDAY, February 10, 2009
Spencer Unger, Carnegie Mellon University.
The tree property II
Time:12:00 P.M.
Location: BH 150
TUESDAY, February 17, 2009
Spencer Unger, Carnegie Mellon University.
The tree property III
Time:12:00 P.M.
Location: BH 150
Abstract: This will be the third in a series of three talks surveying a result due to Mitchell, that Con(ZFC + there is a weakly compact cardinal) implies Con(ZFC + omega_2 has the tree property). (Note: This series of talks is designed as a sort of lead up to Itay Neeman's workshop at the end of the month.)
TUESDAY, February 24, 2009
Spencer Unger, Carnegie Mellon University.
The tree property IV
Time:12:00 P.M.
Location: BH 150
Abstract:This will be the fourth and last in a series of talks surveying a result due to Mitchell, that Con(ZFC + there is a weakly compact cardinal) implies Con(ZFC + omega_2 has the tree property). (Note: This series of talks is designed as a sort of lead up to Itay Neeman's workshop at the end of the month.)
TUESDAY, March 17, 2009
Peter Lumsdaine, Department of Mathematical Sciences, Carnegie Mellon University
TITLE: Sheaves and forcing
ABSTRACT: Forcing can be presented in many ways: as generic extensions, as Boolean-valued models, purely syntactically... I shall describe the category-theoretic approach, looking at forcing extensions as categories of sheaves. In particular, I will aim to give a concrete dictionary between this perspective and more familiar set-theoretic presentations.
Time: 12:00 P.M.
Location: BH 150
TUESDAY, March 24, 2009
Amine Chaieb, Department of Mathematical Sciences, Carnegie Mellon University
TITLE: Formal power series in Isabelle/HOL
ABSTRACT:We show how to use (axiomatic) type classes to formalize formal power series (FPS) over arbitrary domains. We prove that if the basic domain is an integral domain, then so is the FPS construction. We also formalize multiplicative inverses and division, arbitrary nth roots, composition of FPS and the compositional inverses. We present simple proofs and formalizations from Generatingfunctionology by Wilf and formalize some elementary FPS like the exponential, logarithmic, binomial, and some trigonometric series and some of their simple applications. From this formalization we immediately obtain (for free) the field of formal Laurent series and with minimal efforts a formalization of polynomials. All formalizations referred to above are univariate.
Time: 12:00 P.M.
Location: BH 150
FRIDAY March 27, 2009
Harvey Friedman, Ohio State.
TITLE: Boolean relation theory
ABSTRACT: Boolean Relation Theory (BRT) has its origins in the basic
Complementation Theorem and Thin Set Theorem. The former asserts that
for all strictly dominating f:N^k into N, there exists infinite A
contained in N, such that fA = N\A, and the latter asserts that for all
f:N^k into N, there exists infinite A contained in N, such that fA is
not N. Here fA abbreviates f[A^k], and is viewed as the forward image of
f on A.
More generally, BRT investigates statements of the form "for several
multivariate functions a certain kind, there are several sets of a
certain kind, such that a given Boolean equation (or inequation) holds
among these sets and the forward images of the functions on these sets".
The truth value of the statement depends on the choice of functions,
sets, number of functions, number of sets, and the Boolean equation
(inequation).
BRT leads quickly to statements that are provable only by going well
beyond the usual ZFC axioms for mathematics. Our forthcoming book
focuses on a BRT statement involving two functions and three sets, on N.
We survey the results in our forthcoming book coming out in the ASL
Lecture Notes in Logic.
Time: 11:30 P.M.
Location: BH A53
TUESDAY, March 31, 2009
Ernest Schimmerling, Carnegie Mellon
University.
TITLE: Inner model theory I
ABSTRACT: Jensen proved that the combinatorial principle "square" holds
in L. I will outline the proof of this theorem, as well as that of
Jensen's "covering lemma" for L, which also involves "fine structure".
This will lead into a discussion of large cardinals and mice. I expect
this will take two lectures. Ultimately, inner model theory combines
fine structure and iteration trees, but that is beyond the scope of
these lectures. Instead, the third lecture will be on forcing with
Woodin's extender algebra because the proofs are reminiscent of how
iteration trees are used in inner model theory, and because the extender
algebra is used in applications of inner model theory to descriptive set
theory.
Time: 12:00 P.M.
Location: BH 150
TUESDAY, April 7, 2009
Ernest Schimmerling, Carnegie Mellon
University.
TITLE: Inner model theory II
ABSTRACT: Jensen proved that the combinatorial principle "square" holds
in L. I will outline the proof of this theorem, as well as that of
Jensen's "covering lemma" for L, which also involves "fine structure".
This will lead into a discussion of large cardinals and mice. I expect
this will take two lectures. Ultimately, inner model theory combines
fine structure and iteration trees, but that is beyond the scope of
these lectures. Instead, the third lecture will be on forcing with
Woodin's extender algebra because the proofs are reminiscent of how
iteration trees are used in inner model theory, and because the extender
algebra is used in applications of inner model theory to descriptive set
theory.
Time: 12:00 P.M.
Location: BH 150
TUESDAY, April 21, 2009
Ernest Schimmerling, Carnegie Mellon
University.
TITLE: Inner model theory III
ABSTRACT: Jensen proved that the combinatorial principle "square" holds
in L. I will outline the proof of this theorem, as well as that of
Jensen's "covering lemma" for L, which also involves "fine structure".
This will lead into a discussion of large cardinals and mice. I expect
this will take two lectures. Ultimately, inner model theory combines
fine structure and iteration trees, but that is beyond the scope of
these lectures. Instead, the third lecture will be on forcing with
Woodin's extender algebra because the proofs are reminiscent of how
iteration trees are used in inner model theory, and because the extender
algebra is used in applications of inner model theory to descriptive set
theory.
Time: 12:00 P.M.
Location: BH 150
-
