I want to ask a perhaps basic question about derivability rules of existential quantifier in coherent (or geometric, it doesn't matter) logic which confuses me recently. It seems to me we do not have enough rules in the standard literature. The following are axioms and rules related to existential quantifier in coherent logic:
- We have the double rule of the following form, where we require the variable $y$ does not appear in $\psi$:
- And we have the Frobenius axiom $\phi \wedge (\exists y)\psi \vdash_{\vec x} (\exists y)(\phi \wedge \psi)$.
For example, these are the only rules and axioms associated to existential quantifier that can be found in both Theories, Sites, and Toposes and in Sketch of an elephant (their formulations are essentially the same). However, this seems strange because we have no introduction rule for existential quantifier. In particular, it seems we cannot prove a sequent where the existential quantification appears on the right hand side in a sequent, unless our theory somehow already takes it as an axiom.
Let me take an explicit example. Let our signature contains the usual function symbols of Peano arithmetic, but without multiplication for simplicity. Explicitly, we have three function symbols $0,S,+$ of arity 0, 1, and 2, respectively. $0$ is also called a constant. We consider the following simple coherent axiomatisation, which is essentially an inductive definition of addition using successor:
- $\top \vdash_{x} x + 0 = x$;
- $\top \vdash_{x,y} x + Sy = S(x + y) $;
Call this theory $\mathbb{T}$. Now, it is obvious to see that the sequent $\top \vdash SS0 = S0 + S0$ is derivable from $\mathbb{T}$. However, the sequent
$\top \vdash \exists x(SS0 = x + x)$
is obviously not derivable in our theory $\mathbb{T}$, simply because there are no rules or axioms, except for the Frobenius axioms, in our theory $\mathbb{T}$ that can prove an existential quantification appearing on the right of a sequent; but the Frobenius axiom already supposes an existential quantification, hence it really does not help.
If I am not mistaken about the above fact --- if the sequent is indeed derivable, then I apologise for my possibly stupid question --- there are two possibilities. One is that we really do not want the sequent $\top \vdash \exists (SS0 = x + x)$ to be derivable, even though the sequent $\top \vdash SS0 = S0 + S0$ is derivable. This might be due to some weird properties that intuitively holds, but does not hold in a general coherent category. Another possibility is that we really do not have a full characterisation of derivability rules in coherent logic (and regular and geometric logic). What we should add is the usual introduction rules of existential quantification: if $\psi$ contains a closed term of sort $A$ and the sequent $\phi \vdash_{\vec x} \psi$ is derivable, then the sequent $\phi \vdash_{\vec x} \exists y\psi[y/t]$ should also be derivable, provided that $y$ is a variable of sort $A$ that does not appear in $\psi$.
This is a great question. I think a proof of $\top \vdash \exists x (SS0 = x + x)$ is as follows.
The trick is to start with the identity $\exists x (SS0 = x + x) \vdash \exists x (SS0 = x + x)$. Then you can change the variable name in the formula on the left, to get the equivalent $\exists y (SS0 = y+y) \vdash \exists x (SS0 = x + x)$. Using the double rule that you mention, this is equivalent to $SS0 = y + y \vdash_y \exists x (SS0 = x + x)$.
In this formula, you can now substitute $y = S0$, to get $SS0 = S0 + S0 \vdash \exists x (SS0 = x+x)$. You already mentioned that $\top \vdash SS0 = S0 + S0$ holds, so by applying the cut rule, this shows $\top \vdash \exists x (SS0 = x+x)$.
Hi, thanks for your answer! Yes, that should be how you derive it. The double rule here is somehow unusual than other proof systems which I'm more familiar with. But this definitely clears up my confusion. Thanks again!
Hi, bit late to the party again, and Jens has already shown how we can syntactically prove your sequent using the rules of geometric logic, but I just wanted to add that the double rule you've mentioned encodes that existential quantification on 
Now existential quantification preserves terminal/top elements (that is the formula in context 
All of these remarks may seem trivial, and potentially they are, but I find it beneficial having multiple viewpoints of the same concept.
Hi, thanks for writing this! Yes, I believe this adjunction perspective is really important for categorical logic. I think my previous confusion about this is how far this formal adjunction characterisation can go, since I think this is not the usual way where the axiomatisation of existential quantification proceeds in logical textbooks.
Actually, this adjunction property made me to realise the following, possibly also trivial, fact. For a category $\mathcal C$ with finite limits, it is well-known that all morphisms having images (not necessarily regular images, i.e. images are not necessarily preserved by pullbacks) is equivalent to every pullback functor $f^* : \mathrm{Sub}(y) \to \mathrm{Sub}(x)$ having left adjoint. Now since in logic, we actually do not express all existential quantification over arbitrary morphism --- only projections, it is actually enough to require all pullback functor of projections $\pi^* : \mathrm{Sub}(y) \to \mathrm{Sub}(x \times y)$ having a left adjoint for all morphisms to have a left adjoint. Essentially, the left adjoint of an arbitrary morphism $f: x \to y$ can be expressed as the following: for any subobject $S$ of $x$, we have
$\exists_f (S) \cong \exists_{\pi_y}(\pi_x^* S \wedge \Gamma_f) $
where $\pi_x,\pi_y$ are projections from $x \times y$ to $x$ and $y$, respectively; $\Gamma_f$ is the graph of $f$, which is the equaliser of $f \circ \pi_x, \pi_y : x \times y \to y$. The proof of this fact is elementary. If we view it in the internal logic of $\mathcal C$, this simply states that
$\exists_f(S) = \exists_x(S \wedge f(x) = y)$
This explains that the adjunction characterisation of existential quantification is exactly responsible for a category of finite limits to have images.
If it's elementary, I certainly hadn't realised the full depth of that connection! Bravo!
