Can $GPK^{+}_{\infty}$ + $AC_{WF}$ prove "$ZFC$ proves that the class of ordinals is not weakly compact for definable classes?

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 odel-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 odel-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$?