Recently while thinking about the interpretation of the internal language of a topos, it occurred to me to wonder what would happen if we restricted to the fragment of typed first-order logic which doesn't involve "passing to different test objects". So, in the list below, the "accepted" list is where the test object remains unchanged in the interpretation; the "marginal" list is where from the original test object $U$ we pass to $V$ for each morphism $V \to U$; and the "excluded" list is where an epimorphic cover of the original test object is involved.
Accepted
$\top$, $\land$, $\exists!$
Marginal
$\bot$, $\lnot$, $\rightarrow$, $\forall$
Excluded
$\lor$, $\exists$
I wonder if either the "accepted" fragment, or the "accepted + marginal" fragment, of intuitionistic first-order logic has been studied.
(A similar question could also have arisen in the study of forcing, where similarly in "accepted" $p \in \mathbb{P}$ remains constant; in "marginal" we pass to arbitrary $q \le p$; and in "excluded" the interpretation involves "dense below $p$". Which is hardly surprising, given that classical forcing can be expressed in terms of the $\lnot\lnot$-sheaves on $\mathbb{P}$.)