@ZuhairAl-Johar you are correct, I misread the definitions, I'll edit my answer when I get home

The problem of $L_{∞,ω}$ was asked by Mostowski, Lopez-Escobar solved it by first finding that the Hanf number of $L_{κ,ω}$ is less or equal to $\beth_{(2^{κ})^+}$, then assume $φ∈L_{κ^+,ω}$ express well-ordering (we can assume it is a single sentence, if we require a theory $T⊆L_{λ,ω}$ we can just take $κ=\max(|T|,λ)$ and let $φ$ be the conjunction of $T$) then they construct a (quite complicated) sentence $ψ∈L_{κ^+,ω}$ such that ordinals $(α,∈;...)$ does not satisfy $ψ$ if $α>\beth_{2^{2^{2^{κ}}}}$ but there exists $α≥\beth_{(2^{κ^+})^+}$ that satisfy this sentece

When you looked at finite sets you added an infinite set, but in the case of Ordinals you added an ordinal, and in the case of sets you added a set, so of course they would be different, (and indeed all of those 3 cases we have a property that is absolute downward)

Quantification over symbols translates into sets of formulaes (as Alex said, in model theory we use types and in logic we use infinitary logic). Generally infinitary formulaes can't be translated to second order logic (although some cases have it easy, see this interesting case)

For another possible reference, following Jech's book "the axiom of choice" in chapter 9 problem 3 and 4 they construct models of ZFCA with infinitely many atoms but every set contains only finitely many atoms in its transitive closure by generalizing permutation models whose permutations are permutations over a proper class, in such models the Hartogs number of the class of atoms is $\aleph_0$

@EmilJeřábek good catch, I'll admit I'm usually loose with my use of LEM, so I tend to not notice "useless contradictions"

@EmilJeřábek I fixed up the wording to be more clear

Interesting, the proof I know for the joint consistency theorem is to show the conservative variation using Craig’s interpolation (see my answer) and from there the standard variation is immediate, I guess that the difference comes to preference of using models or being purely syntactic

Usually the "common formulation" of the joint consistency theorem is proven using the Conservative Extension formulation, I will soon write an answer that proves the variation without assuming the Robinson’s joint consistency theorem

Furthermore, in $ZF+AD$ every regular $\kappa<\aleph_{\omega_1}$ is Jonsson

It is consistent that every regular cardinal bellow $\Theta$ is measurable (specifically, $L(\mathbb R)$ will satisfy this). IIRC, there is a similar result about supercomapcts

@PeterLeFanuLumsdaine You are correct, I had a small brainfart

@PeterLeFanuLumsdaine doesn't this fall under "already definable over positive logic"?