Consider the topological set theory $GPK^{+}_{\infty}$ +$AC_{WF}$, where $GPK^{+}_{\infty}$ is defined as follows (this from Olivier Esser's papers, "An Interpretation of the Zermelo-Fraenkel Set Theory and the Kelly-Morse Set Theory in a Positive Theory" and "On the Consistency of a Positive Theory"):
Bounded Positive Formulas: Within the language $\mathscr L$ = ($\in$, =) of set theory, the class $BPF$ of bounded positive formulas is defined as follows (as the smallest class of formulas of $\mathscr L$ such that, or, in the alternative, the class of formulas obtained by applying a finite number of times the following rules):
(1) If $x$ and $y$ are variables, then $x$$\in$$y$ and $x$=$y$ are $BPF$ formulas.
(2) If $\varphi$ and $\psi$ are $BPF$ formulas, then so are $\varphi$$\land$$\psi$, $\varphi$$\lor$$\psi$, $\exists$$x$$\varphi$, and ($\forall$$x$$\in$$y$)$\varphi$.
Definition. If $\Sigma$ is a collection of formulas (possibly with parameters, but where the variable '$a$' does not appear), $comp({\Sigma})$ is the following scheme:
$\exists$$a$$\forall$$x$($x$$\in$$a$$\Leftrightarrow$$\alpha$), for each $\alpha$$\in$$\Sigma$.
Definition. A class is definable (with parameters) collection of sets.
Definition. A set can be defined in one of two (equivalent) ways:
(1) If $a$, $y$ are classes, then $a$ is a set iff $\exists$$y$($a$$\in$$y$), or
(2) A class {$A$|$\alpha$} is said to be a set if $\exists$$a$$\forall$$x$($x$$\in$$a$ $\Leftrightarrow$ $\alpha$); in this case one identifies $a$ and $A$.
$GPK^{+}_{\infty}$ consists of the following axioms:
(1) Extensionality. $\forall$$x$$\forall$$y$[($\forall$$z$($z$$\in$$x$$\Leftrightarrow$$z$$\in$$y$) $\Rightarrow$ $x$=$y$];
(2) Empty Set. $\exists$$x$$\forall$$y$($y$$\notin$$x$);
(3) Comprehension. $comp({BPF})$ (i.e. the universal closures of the formulas $\exists$$a$$\forall$$x$($x$$\in$$a$$\Leftrightarrow$$\varphi$), where $\varphi$ is a $BPF$;
(4) Closure. For any formula $\Gamma$($z$, $y_1$,...,$y_n$) whose free variables are among $z$,$y_1$,...,$y_n$,
$\forall$$y$,...,$\forall$$y_n$ $\exists$$x$[$\forall$$z$($\Gamma$($z$,$y_1$,...,$y_n$) $\Rightarrow$ $z$$\in$$x$) $\land$ $\forall$$y$($\forall$$z$($\Gamma$($z$,$y_1$,...,$y_n$) $\Rightarrow$ $z$$\in$$y$) $\Rightarrow$ $x$$\subset$$y$)]. [The scheme Closure says that for each class $A$={$z$|$\Gamma$($z$,$y_1$,...,$y_n$)} there is a smallest set (for the inclusion) which contains it; this set is denoted by $\bar A$ or $cl({A})$.]
(5) Infinity. There exists a limit ordinal.
Definition. $AC_{WF}$$=_{df}$ $\exists$$f$[($\forall$$x$$\in$$WF$)$\exists$$!$($x$,$y$)$\in$$f$ $\land$ ($\forall$$x$$\in$$WF$)$\forall$$y$(($x$$\neq$$\emptyset$ $\land$ ($x$,$y$)$\in$$f$) $\Rightarrow$ $y$$\in$ $x$)] [$AC_{WF}$ says that there is a set $f$ such that $f$$\cap$$WF$ is a class-function $F$ such that ($\forall$$x$$\in$$WF$)($x$$\neq$$\emptyset$ $\Rightarrow$ $F$($x$)$\in$$x$), where $WF$ is the class of well-founded sets of $GPK^{+}_{\infty}$.]
Furthermore, Esser, in "An Interpretation of the Zermelo-Fraenkel Set Theory and the Kelly-Morse Set Theory in a Positive Theory", characterizes Kelly-Morse 'set theory' (class theory, actually) as follows:
Recall that the Kelly-Morse theory is the class theory of G$\ddot o$del-Bernays to which we add the following scheme: For any formula $\varphi$ (with parameters) the collection {$x$| ($x$ is a set) $\land$ $\varphi$} is a class (in G$\ddot o$del-Bernays class theory we have only this if $\varphi$ is a formula containing no class variables).
It should also be noted that in "On the Consistency of a Positive Theory", Esser proves that $GPK^{+}_{\infty}$ + $AC_{WF}$ and $KMC$ + "On is ramifiable" are mutually interpretable , where $KMC$ is Kelly- Morse with Global Choice, and "On is ramifiable" is defined as follows:
A class of $KMC$ is sais to be On-finite iff it is a set, On-infinite if not. We mean by On is ramifiable the following sentence: "Every On-infinite tree with On-finite levels has an On-infinite branch".
A tree $T$ is a class of sets (called the nodes of the tree) together with an ordering relation $\lt_{T}$ such that for each node of the tree the class {$x$| $x$$\lt_{T}$$a$} is a well-ordered set. A branch of a tree is a well ordered subclass of the tree. The length of a branch is the ordinal of the well ordered type of the branch if it is a set, and On if it is not a set . A successor of a branch $B$ is a node $x$ of $T$ such that {$y$|$y$$\lt_{T}$$x$}$\supseteq$$B$. A node $x$ is said to be an immediate successor of $B$ iff {$y$| $y$$\lt_{T}$ $x$}=$B$. The $\alpha^{th}$ level ($\alpha$$\in$On) of a tree $T$ is the class of the $x$$\in$$T$ such that {$y$| $y$$\lt_{T}$ } is a branch of length $\alpha$. A tree ($T$,$\lt_{T}$) is said to be a binary tree iff
(i) each element of $T$ has at most two immediate successors;
(ii) every branch of limit length has at most one immediate successor.
Finally, in "On the Consistency of a Positive Theory", Esser makes the following claim:
...we can give a natural model of $KMC$ + "On is ramifiable" inside of "ZF$ + "there exists a weakly compact strongly inaccessible cardinal".
Now for the questions (these refer to the Enayat-Hamkins preprint, "$ZFC$ proves that the class of ordinals is not weakly compact for definable classes" [arXiv:1610.02729v1 [mathLO]]):
Consider the two main theorems of the Enayat-Hamkins paper:
Theorem $A$. Let $\mathcal M$ be any model of $ZFC$.
(1) The definable tree property fails in $\mathcal M$: There is an $\mathcal M$-definable Ord-tree with no $\mathcal M$-definable cofinal branch.
(2) The definable partition property fails in $\mathcal M$: There is an $\mathcal M$-definable 2-coloring $f$: $[$$X$$]^2$ $\rightarrow$ $2$ for some $\mathcal M$-definable proper class $X$ such that no $\mathcal M$-definable proper class is momochromatic for $f$.
(3) The definable compactness property fails in $\mathcal M$: There is a definable theory $\Gamma$ in the logic $\mathcal L_{Ord,\omega}$ (in the sense of $\mathcal M$) of size Ord such that every set-sized subtheory of $\Gamma$ is satisfiable in $\mathcal M$, but there is no $\mathcal M$-definable model of $\Gamma$.
Theorem B. The definable $\lozenge_{Ord}$ principle holds in a model of $ZFC$ iff $\mathcal M$ carries an $\mathcal M$-definable global well-ordering.
Instead of assuming $ZFC$ as the metatheory (as Enayat and Hamkins do), let me assume $GPK^{+}_{\infty}$ + $AC_{WF}$ as the metatheory. Can $GPK^{+}_{\infty}$ +$AC_{WF}$ prove that $ZFC$ proves Theorems $A$ and $B$ in a manner that is less "unexpected" in the sense that given an interpretation of $ZFC$ in $GPK^{+}_{\infty}$ + $AC_{WF}$, that interpretation of $ZFC$ proves Theorems $A$ and $B$ more 'naturally' in that $ZFC$ was interpreted in a positive theory?
Question 2: How are the definitions of "On is ramifiable" and "Tree" as Esser defined them related to the corresponding definitions in the Enayat-Hamkins paper?
Querstion 3: Does $ZF$ (with AC excluded) prove Theorems $A$ and $B$?
