What are these generalizations of the principles of omniscience called?

Question

I will give some principles that are slightly stronger versions of the principles of omniscience. Despite being about the natural numbers, they imply their analytic versions! Under countable choice (or even just $\text {AC}_{\mathbb N, 2}$) they are equivalent to the original principles. My question is if there is a prior reference for these principles.

Here they are. For formulas $\phi$ and $\psi(n)$ such that $\forall n. (\phi \lor \psi(n))$ ($\forall n$ means $\forall n \in \mathbb N$), the stronger principles are:

• LPO: $\phi \lor \forall n. \psi(n)$
• WLPO: $(\lnot \lnot \phi) \lor \forall n. \psi(n)$
• LLPO: Also assume that $\forall n. (\chi \lor \gamma(n))$. Then $(\lnot (\phi \land \chi)) \implies ((\forall n. \psi(n)) \lor (\forall n. \gamma(n)))$
• Markov's principle: $(\lnot \forall n. \psi(n)) \implies \phi$
• Note that $(\lnot \phi) \implies \forall n. \psi(n)$ is just a theorem.

We recover the original principles when $\psi(n)$ is decidable by setting $\phi$ as $\exists n. \lnot \psi(n)$.

As an example of how they imply the analytic principles, consider the LPO. We get the analytic LPO by setting $\phi$ as $x - y > 0 \lor x - y < 0$ and $\psi(n)$ as $x - y \in (-\frac 1 {2^n}, \frac 1 {2^n})$. (This works because $\bigcap_{n \in \mathbb N} (-\frac 1 {2^n}, \frac 1 {2^n}) = \{0\}$.) The other principles are similar.

These seem like a pretty natural generalization. Basically, instead of requiring exclusive or, we permit any disjunction (which with countable choice we can convert back into an exclusive or). Is there a prior reference for them?

Answer 1

The first is called Constant Domain in The Drinker Paradox and its Dual by Warren, Diener & McKubre-Jordens (2018). More specifically, they use a general quantifier and a variant without variable, as you have it, is reflected upon on the bottom of page 4. The name for the one in the list there is elaborated on in the Kripke model discussion a few pages later.