C7X

@MoreAnonymous It is known that deciding truth of an arithmetical sentence is not a problem that can be solved recursively, but the goal of Goedel-encoding is to get encodings where operations on the strings are simple (often times e.g. primitive recursive).

Thank you! (I suppose personally I thought it was more of a "sledgehammer" approach to the problem to take the quantifiers one at a time, and as per the last line of your answer, Hamkins's method seems to work just as well.)

In the answer, should the first occurrence of $\varphi^{+*^{V_\alpha}}$ be replaced with $\varphi^{+*V_\alpha}$? The notation in the question is $\varphi^{*B}$ in contrast to $\varphi^{*^B}$

As far as I have read, I see an "internalizing parameter string" $\exists x_i(x_i=v_i)$. If the parameters are not stored in free variables, are the $v_i$ extra constant symbols in the language?

Sorry for my late response. I have updated my answer earlier although before seeing your last message, and I can continue working on the problem tomorrow.

@ZuhairAl-Johar Now I think I see, thanks! Now that you mention it, it shouldn't be difficult to extend the theorem in my post to allow for a bounded quantifier to the left of the one that gets bounded to $W$, in your example the quantifier $\forall x\in A$ would now be covered by the theorem. If it works I can edit my answer to add the extension soon. But I am still not sure how to bound two or more quantifiers to $W$

@ZuhairAl-Johar "Is that correct?" - That is correct. In your most recent comment I am reading "before that" as meaning "rightwards of that". "then Hamkins proof already proves that" - the main way I understand this is that it would happen if the expansion of the language by $\mathcal P$ is unnecessary, and everything can be kept in $\mathscr L_\in$ by simply replacing $\forall x\subseteq k\ldots$ with $\exists K(\forall y(y\subseteq k\iff y\in K)\land\ldots)$, etc. Is this also your line of reasoning? (Soon it may be a good idea to move to chat from this thread.)

(cont'd) Hamkins's proof is a good starting point, and it seems to bound the quantifiers "all at once" rather than inductively adding them. It may work to simply use the fact that $\mathcal P$ never shows up in the block of bounded quantifiers, so the subformula of $\varphi$ in which all the $\mathcal P$'s appear is still absolute to $V_\kappa$ by $(V_\alpha,\in,\mathcal P\upharpoonright V_\alpha)\prec(V_\kappa,\in,\mathcal P\upharpoonright V_\kappa)$, but I am less comfortable working with arguments that "bound all the quantifiers at once" as I am not sure if a mistake would slip in.

@ZuhairAl-Johar You are correct, anterior-closedness of the bounded quantifiers is violated. This happens since the "$W$ does not occur" clause was removed, breaching the order of the bounding and making the $\varphi^{``W}$ considered diverge from how the order of bounding works in Reflection*. (cont'd)

Re. 3rd comment: If I have done it correctly, the point of introducing the class symbol should be to show there is a model $V_\kappa$ in which every formula, including ones in the language which uses quantifiers like $\forall x\subseteq k$, will anterior-reflect, as long as only one quantifier gets bounded to $W$. This model existence shows it is consistent with ZFC, but $\mathcal P$ need not be a function symbol in any model where anterior-reflection with 1 bounded quantifier is considered.

@ZuhairAl-Johar Re. 1st comment: You're right, when reading I must have thought that anterior closure meant that the block of quantifiers that get newly bounded to $W$ has to be anterior-closed.

@user76284 Let EST have axioms of extensionality, empty set, pairing, union, ∀x,y∃z(z=x×y), Δ₀-separation, and induction along ω. Then EST+Vopenka's principle recovers replacement and powerset. researchgate.net/publication/…

Hello, I saw a claim online that Arai's 2019 preprint "A simplified analysis of first-order reflection" (arxiv.org/abs/1907.07611) contains errors. The claim is on this blog post bit.ly/3c87nnK, since it's written in Japanese I have used Google Translate, hopefully there are no errors in translation. As I understand it their claim is since ψ^(1,0,...,0)_K_n(2) = K_n, the map to the ordinal notation is non-injective so Lemma 3.8 fails. Does this impact the rest of the analysis?

@RE60K @RE60K The support of a function $e$ is the set $\{x\in dom(e)\mid e(x)\neq 0\}$. Probably will depend on the context of the paper, but if for each vertex $v$ there's an associated function $e$ I'd guess $e$ maps each vertex to the number of edges connecting $v$ to the vertex. Then the support of $e$ (function $e$ chosen when working with vertex $v$) would be the set of vertices connected to $v$

Sorry I didn't realize that in the comment thread, I was considering transitive models so that we had some nice propeties (such as absoluteness of Δ₀ formulae)

> Suppose we don't have the empty set, then A,B are ordinals!

Are we working in a model where the empty set doesn't exist?

I thought that $\alpha\cap\beta$ was also an ordinal, since it consists just of the transitive proper sets consisting of members of $\alpha$ that also just consist of members from $\beta$, i.e. transitive subsets of $\alpha\cap\beta$

Hello!

I'm rather new to SE, is it a good idea to move to chat?

Sorry for the slow updates, I see how to implement your proof now in a system without foundation. I'll edit it to talk about separation and your proof

My construction was an attempt to create a sort of "transitive closure" of the Quine atom $q$ - if $TS(x)$ denotes the set of transitive subsets of $x$, it was $X=TS(q)\cup TS(TS(q))\cup TS(TS(TS(q)))\cup\ldots$. I believed $ord(X)$ was true and $X$ and $\omega\cdot 2$ were $\subseteq$-incomparable, but now I'm starting to doubt $ord(X)$.

Additionally, since $TS(x)=\{y\in\mathcal P(x)\mid trs(y)\}$, this construction may require powerset so it's not very friendly to a weak theory like is needed

Does that proof by contradiction work if we don't assume foundation?

Also my construction used the Quine atom, so I was working in a no-foundation environment. But now I'm rethinking the claim "I have constructed two ordinals incomparable by $\subseteq$", I might have been wrong in saying my construction was an ordinal after all

Sorry, I didn't realize that! I think we still have trochotomy of $\in$ for ordinals, I'll edit my answer.

I think this may be false, I believe I have constructed two ordinals incomparable by $\subseteq$, but I need more time to check

Also, I was under the impression that the notion of a Δ_1^0 formulae does exist in the arithmetic hierarchy, and it's a formula that's logically equivalent to both a Σ_1^0 formula and a Π_1^0 formula. I wasn't sure if the logical equivalence was semantic (the Σ_1^0 and Π_1^0 formulae are satisfied exactly when the Δ_1^0 formula is in the true model (N,<)) or syntactic (they're provably logically equivalent using some rewrite rules.)

@Binary198 I think so: Δ_0^1 sets are recursive, and some TM can decide if a given (Godel-number of a) sentence is an axiom of ZFC (including instances of schemata). If we have one first-order sentence φ formalizing "there exists an I0 cardinal", φ has a fixed Godel-number, and there can be a different machine that acceps iff (the ZFC TM halts or the input = Godel-number of φ).

Proposition 0.7 here pldml.icm.edu.pl/pldml/element/…

I've seen a relevant reference for when a theory has a model L_η with η<(least stable ordinal), I can look for it

Hi!