MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

# Everett Piper

 353 Reputation 331 views

## Registered User

 Name Everett Piper Member for 3 years Seen 9 hours ago Website Location Boulder, CO Age 30
I am a math instructor at the University of Colorado at Boulder. My interests have evolved from proof theory and philosophical concerns about knowledge to the upper reaches of set theory and the large cardinal hierarchy. I also occasionally dabble in combinatorics of the finite sort.
 May8 comment Forcing mildly over a worldly cardinal.As far as the other axioms of ZFC go, you might try to violate them by requiring some kind of definability constraint on $V_\theta$. What I have in mind here is something like: assume $\theta$ is worldly and every set (in $V_\theta$) is definable from parameters in some set $X$ (given ahead of time). Then could there be a forcing extension where, say, pairing fails in the sense that there are sets $a$ and $b$ where $\{a,b\}$ is not definable (from parameters in $X$)? I don't know if this situation could ever arise, but it seems like it could in contexts like $V=L$ or there is an $I_0$ cardinal May8 comment Forcing mildly over a worldly cardinal.Second, the desired forcing would have to kill some particular axiom of ZFC. Joel suggests altering the truth-value of some particular instance of replacement, but couldn't we attack an instance of collection (I'm not sure if this even makes sense) or even introduce a set into $V_\theta$ that has no choice function, thereby violating choice instead? This seems to require that one look at a symmetric inner model $M$ and inspect its version of $V_\theta$ (though I'm guessing this isn't what you had in mind, Erin). May8 comment Forcing mildly over a worldly cardinal.I have some thoughts on this, though I don't know if any of them are really that good. First, it is a theorem that set-forcing over a ground model of ZFC will only yield models of ZFC, so starting with $V_\theta$ itself won't work. However, in Joel's response, it appears that we could have started with $V_\theta$ and killed the worldliness of $\theta$. However, the requirement that $\theta$ be singular makes the forcing appear to be a class forcing from the point-of-view of $V_\theta$. If this is the case, then one can't eliminate the hypothesis that $\theta$ be singular here. Is this correct? Apr14 awarded ● Organizer Apr14 revised When does $ZFC \vdash\ ‘ ZFC \vdash \varphi\ ’$ imply $ZFC \vdash \varphi$?added the proof theory tag Apr14 comment When does $ZFC \vdash\ ‘ ZFC \vdash \varphi\ ’$ imply $ZFC \vdash \varphi$?On a slightly different note, you may want to hunt down the following two articles: (I) Kent, C. F. The relation of $A$ to $Prov(A)$ in the Lindenbaum sentence algebra. J. Symbolic Logic 38 (1973), 295–298; (II) Macintyre, A.; Simmons, H. Gödel's diagonalization technique and related properties of theories. Colloq. Math. 28 (1973), 165–180. Apr14 comment When does $ZFC \vdash\ ‘ ZFC \vdash \varphi\ ’$ imply $ZFC \vdash \varphi$?particular instance of the reflection principle $Pr_\tau(\phi)\rightarrow\phi$ and then concatenate $\phi$. The penultimate line of this proof is justified since we merely appended an axiom of T to the original T-proof of $Pr_\tau(\phi)$ and the last line follows from a single application of modus ponens. So it's actually straight-forward to produce a number witnessing a T-proof of $\phi$ given a number witnessing T-proof of $Pr_\tau(\phi)$. Apr14 comment When does $ZFC \vdash\ ‘ ZFC \vdash \varphi\ ’$ imply $ZFC \vdash \varphi$?There is a more-or-less standard way to formalize $\Sigma_1^0$ soundness for ZFC: Given a formula $\tau$ enumerating the axioms of ZFC, construct the proof-predicate $Pr_\tau(x)$. Now construct the theory T. T has all axioms of ZFC and a schema of all sentences of the form $Pr_\tau(\varphi)\rightarrow \varphi$ where $\varphi$ is any formula in the language of ZFC. Sometimes T includes as an axiom "< is a well-ordering of $\omega$."Working in T, any proof of $Pr_\tau(\phi)$ can be transformed into a proof of $\phi$ in a simple way: copy the T-proof of $Pr_\tau(\phi)$, concatenate the Mar7 comment Reflection principles Erin, I'm curious about the specific reflection principle you're interested in. It seems you are interested primarily in set theory so it may very well be the case that you are interested in a set-theoretic reflection principle as opposed to a proof-theoretic principle. Proof-theoretic principles are typically formalized versions of the intuition that a particular proof-system or set of axioms is sound. Set-theoretic reflection principles seem to express the intuition that certain kinds of structure in V keep repeating or reflecting arbitrarily high up in the cumulative hierarchy. Mar7 comment Reflection principles principles. For example, there really is no "good" formalization of "is provable" in the sense that there are lots of non-standard proof predicates that can be constructed and there is no mathematical distinction between the non-standard and standard proof predicates. There is also ambiguity in the sentence(s) formalizing that S is a consistent theory (or has a model, or has an omega-model, etc.). There is an excellent article (and also a book) by Torkel Franzen. Smorynski's article in the Handbook of Mathematical Logic is also a good place to start. I can provide lots more info/literature if Mar7 comment Reflection principles It might be worthwhile to note the reflection principle mentioned by Jaykov is actually a schema; there is such a conditional for every sentence $\phi$ in the formal language being used. Further, the intuitive reading for each individual member of the scheme is something like "If S proves $\Phi$ then $\Phi$ is true (or $\Phi$ holds, or whatever variation you prefer)". For arbitrary $\Phi$ this is known as the Uniform Reflection Principle for S. Feferman (Turing, Beklemishev, Smorynski and others) have shown that there are all kinds of subtleties involving these proof-theoretic reflection Feb21 comment Set forcing and ultrapowersOn my latest reading I have become confused. I have a sense that there is/was no distinction between an elementary embedding $j:V\prec V[G]$ and an elementary embedding $j:V[G]\prec V$ where $G$ is a $V$-generic subset of a set $\mathbb{P}$. I guess I'm still trying to understand the nuance here. But thank you for pointing out the historical relevance of your remarks. Feb21 comment Set forcing and ultrapowersJoel, I believe I was really asking about ultrapowers by class forcing when I originally posed my question. But if you're thinking of some wider class of transitive models I'm certainly curious. I've read your paper (thanks for the correction regarding Prof. Kirmayer, by the way) several times and this traverse through I had a new thought (which always seems to happen). Feb20 revised Set forcing and ultrapowersTried to justify why I think the corollary implies a fact about ultrapowers Feb20 asked Set forcing and ultrapowers Feb1 comment Can a model of set theory be realized as a Cohen-subset forcing extension in two different ways, with different grounds and different cardinals?Are you only interested in the case where you specifically force to get just a Cohen subset, i.e. only $Add(\kappa,1)$, or could you allow forcings which generically adjoin a Cohen subset as a by-product of adjoining some other generic object? Jan12 asked Elementary Embeddings and Relative Constructibility