Typo about ranks in section on replacement

[pglutz]

Typo location: There is a typo in the section about the strength of replacement. Permalink to file and line number: https://github.com/OpenLogicProject/OpenLogic/blob/14154c9e90bfb8848f74c567b688c421961618e8/content/set-theory/replacement/strength.tex#L19

Description of typo: The text currently reads "rank(omega + omega) = V_{omega + omega}." However, the rank function was defined to always output an ordinal. The line also references corollary ordsetrankalpha (permalink: https://github.com/pglutz/OpenLogic/blob/e275e3706bf1421a8747bd2ee09b048f619cdbec/content/set-theory/spine/rank.tex#L85) which states that for any ordinal alpha, rank(alpha) = alpha.

Proposed fix: So I believe the line should probably read "rank(omega + omega) = omega + omega." However, the next line contains the phrase "this set" which is apparently referring to V{omega + omega}, which will no longer make sense if this change is made. The best option might be to move the sentence about the rank of omega + omega closer to the end of the paragraph, which I think improves the flow of the paragraph anyway (the first part of the paragraph argues that V{omega + omega} is a model of Z, the second half argues that omega + omega is not in V_{omega + omega} so it is more natural to bring up the rank of omega + omega in the second half).

[rzach]

@timbutton can you have a look?

[timbutton]

Hi Richard, Sure, no problem -- but I don't know how to interact with github! Any tips? Tim

On Sat, 13 Jun 2020 at 14:42, Richard Zach notifications@github.com wrote:

@timbutton https://github.com/timbutton can you have a look?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/OpenLogicProject/OpenLogic/issues/237#issuecomment-643625650, or unsubscribe https://github.com/notifications/unsubscribe-auth/AM5CQB4RR3S7WUTPKWOATSTRWN65LANCNFSM4N42E3WA .

[rzach]

Here's a very basic intro: https://github.com/rzach/git4phi I believe you have push permissions, you can clone the project, make the change, then push. Or, you first fork the project, make the changes in your fork, then send a pull request to incorporate the changes into the main repository. (If you don't yet know what all these words mean, the intro above explains them.) However, for this question specifically, you could just tell me that this is the way you want it fixed and I'll fix it. Or just cut-and-paste the way you want the paragraph to read in here.

[timbutton]

Hiya

OK looks like the easiest thing for now is just to make the first few lines of the paragraph as follows:

Unless we go beyond $\Z$, we cannot prove the existence of any von Neumann ordinal greater than or equal to $\omega + \omega$. Here is a sketch of why. Working in~$\ZF$, consider the set $V{\omega+\omega}$. This set acts as the domain for a \emph{model} for $\Z$. Indeed, where $\phi$ is any axiom of $\Z$, let $\phi^{V{\omega+\omega}}$ be the formula which results by restricting all of $\phi$'s quantifiers to $V{\omega+\omega}$ (that is, replace $\exists x$'' with$(\exists x \in V{\omega+\omega})$'', and replace $\forall x$'' with$(\forall x \in V{\omega+\omega})$''). It can be shown that, for every axiom $\phi$ of $\Z$, we have that $\ZF \vdash \phi^{V{\omega+\omega}}$. But $\omega+\omega$ is not \emph{in} $V_{\omega+\omega}$, by \olref[spine][rank]{ordsetrankalpha}. So $\Z$ is consistent with the non-existence of $\omega+\omega$.

Cheers! Tim

On Wed, 17 Jun 2020 at 15:36, Richard Zach notifications@github.com wrote:

Here's a very basic intro: https://github.com/rzach/git4phi I believe you have push permissions, you can clone the project, make the change, then push. Or, you first fork the project, make the changes in your fork, then send a pull request to incorporate the changes into the main repository. (If you don't yet know what all these words mean, the intro above explains them.) However, for this question specifically, you could just tell me that this is the way you want it fixed and I'll fix it. Or just cut-and-paste the way you want the paragraph to read in here.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/OpenLogicProject/OpenLogic/issues/237#issuecomment-645413626, or unsubscribe https://github.com/notifications/unsubscribe-auth/AM5CQB3RN2TNCZDIGTBWV6DRXDIFFANCNFSM4N42E3WA .