Return to Answer

added 116 characters in body

Source Link

edited Aug 4 at 20:02

118.2k
40
447
741

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.

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 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.

Source Link

created Aug 4 at 19:56

118.2k
40
447
741

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.