Computational Logic Seminar
Speaker: Elena Nogina The City University of New York
Title: Reflection Principles Involving Provability and Explicit Proofs
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.
Wednesday, November 6, 2013 6:30 pm GC 4214.03
Speaker: Kerry Ojakian Bronx Community College
Title: Tanaka’s embedding theorem
Thursday, November 7, 2013 7:00 am CUNY Graduate Center, Room 6417
Speaker: Dustin Mulcahey
Title: Path Induction and the Path-Loop Space Fibration
As we continue our foray into the book, we begin to view types as spaces (or, “equivalently”, as omega groupoids). My goal for this section is to focus on the path induction rule and argue that it corresponds to the path-loop fibration.
More specifically, we can make an analogy between the path space over a space X and the type of all equivalences over a type A. The path space of X is homotopy equivalent to X, and I argue that path induction says “essentially the same thing” about the type of all equivalences over A. I aim to make this analogy as formal as possible, and then delve further into the material in chapter 2.
I would also like to go over some exercises. I’ve done a few, but if anyone wants to come up to the board and show off, then they are welcome!
Friday, November 8, 2013 10:00 am
Speaker: Miha Habič The CUNY Graduate Center
Title: Grounded Martin’s axiom
I will present a weakening of Martin’s axiom which asserts the existence of partial generics only for ccc posets contained in a ccc ground model. This principle, named the grounded Martin’s axiom, emerges naturally in the analysis of the Solovay-Tennenbaum proof of the consistency of MA. While the grounded MA has some of the combinatorial consequences of MA, it will be shown to be more flexible (being consistent with a singular continuum, for example) and more robust under forcing (being preserved in a strong way under both adding a Cohen or a random real).
Friday, November 8, 2013 12:30 pm GC6417
Speaker: Chris Miller Ohio State University
Title: A class of strange expansions of dense linear orders by open sets
There are expansions of dense linear orders by open sets (of arbitrary arities) such that all of the following hold:
1) Every definable set is a boolean combination of existentially definable sets.
2) Some definable sets are not existentially definable.
3) Some projections of closed bounded definable sets are somewhere both dense and codense.
4) There is a unique maximal reduct having the property that every unary definable set either has interior or is nowhere dense. It properly expands the underlying order, yet is still rather trivial.
At least some of these structures come up naturally in model theory. For example, if G is a generic predicate for the real field, then the expansion of (G,<) by the G-traces of all semialgebraic open sets is such a structure, which moreover is interdefinable with the structure induced on G in (R,+,x,G).
Friday, November 8, 2013 2:00 pm GC 6417
Speaker: Gunter Fuchs The City University of New York
Title: Prikry-type sequences, iterations and critical sequences
I will present some old, some new and some classic results on the kinds of sequences which are added by some forcings which are related to Prikry forcing, in some sense. After finding combinatorial properties characterizing these sequences, I will show how to iterate the universe in such a way that the critical sequence of that iteration will satisfy that combinatorial property with respect to the target model, rendering it generic. This connection enables us to analyze precisely the collection of generic sequences which are present in one specific forcing extension. Time permitting, I will also explore connections to Boolean ultrapowers.