2
$\begingroup$

Working in a set theoretical background, when we express various categorical coherence conditions by expanding all definitions involved back down to a set-theoretical level, what we end up with are statements with multiple universal quantifiers outside of them. For example, consider the following $2$-d diagram:

To express that this diagram commutes at the set theoretical level, we would write

$$\forall\Sigma\in{\bf Ob}_{\mathbb{S}ig}\forall M\in{\bf Ob}_{{\sf Mod}(\Sigma)}\forall e'\in{\sf Sen}'(\Phi(\Sigma))\Big(M\models_\Sigma\alpha_\Sigma(e')\iff\beta_\Sigma(M)\models'_{\Phi(\Sigma)}e'\Big).$$

But to express that this diagram commutes at the $2$-d categorical level, we just say the diagram commutes or write $$(\models'\star1_{\Phi^{op}})\circ\beta=\alpha^\dagger\circ\models.$$

This statement contains exactly the same information as the one above it, but without any quantification by virtue of wrapping all the pieces together and expressing their interplay 'at a higher level'.

Is this process a version of quantifier elimination? More generally, what does quantifier elimination look like from the perspective of higher category theory?

We can get 'there exists' quantifiers mixed in with the 'for all's if we choose the correct codomain category, and these also vanish when we express things higher dimensionally. Any pointers are appreciated, and if this question is trivial from a logical perspective I apologize in advance :^).

Improve this question
$\endgroup$
1
  • 6
    $\begingroup$ I don't think this has anything to do with quantifier elimination as the phrase is usually used; it seems closer to the observation (initially of Skolem, later elaborated on by Godel in the context of functional interpretations if I have my history right) that we can hide quantifiers by using higher-type objects. But I'm not familiar enough with category theory to be certain. $\endgroup$
    – Noah Schweber
    Commented Aug 4 at 19:34

2 Answers 2

Reset to default
7
$\begingroup$

As far as I can tell, the quantifiers are just hidden in the definition of equality. Your example is too complicated for a humble $1$-category theorist like myself so I am going to replace it with a simpler example, namely: when does the diagram

$$X \rightrightarrows Y$$

commute? This means we have two morphisms $f, g : X \to Y$ which are equal, $f = g$. But in, for example, $\text{Set}$, what does this mean? It means $\forall x : f(x) = g(x)$. So we have hidden one universal quantifier in the definition of what it means for two functions to be equal. Similarly we could hide multiple universal quantifiers in the definition of what it means for two functors or natural transformations to be equal.

This doesn't have anything to do with quantifier elimination, which is about replacing a statement with a quantifier with an equivalent statement, in the same language, without a quantifier; in quantifier elimination the quantifier has not been hidden by notation, it actually disappears. For example, consider the statement that a square matrix $M$ over a field has nontrivial kernel; this can be stated with a quantifier as $\exists v : v \neq 0, Mv = 0$, but thanks to the existence of the determinant it can also be restated without a quantifier as $\det(M) = 0$. There is no hiding being done here, this is a genuinely non-trivially equivalent statement that doesn't have a quantifier in it. As I understand it, this is a special case of quantifier elimination for the theory of algebraically closed fields, or Chevalley's theorem.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you Qiaochiu, this clarifies things for me. $\endgroup$
    – Alec Rhea
    Commented Aug 4 at 20:03
  • 3
    $\begingroup$ @AlecRhea The use of function equality to express quantification can be pushed to define quantification as just an abbreviation for certain equations between functions. $\forall x\,\psi(x)$ abbreviates $(\lambda x\,\psi(x))=(\lambda x\,\top)$. $\endgroup$
    – Andreas Blass
    Commented Aug 6 at 16:07
3
$\begingroup$

The situation you are describing is not quantifier elimination but rather an application of function extensionality, the principle stating that, for any functions $f, g$ with domain $A$, $$(\forall x \in A.\, f(x) = g(x)) \Leftrightarrow f = g.$$ Since you are also using $\Leftrightarrow$ in one place where $=$ might be expected, let me just point out that there is also the principle of propositional extensionality which states $(P \Leftrightarrow Q) \Leftrightarrow P = Q$.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .