Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorYimingXu
   • CommentTimeApr 30th 2021
   • (edited Apr 30th 2021)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThis question comes to me because I am interested in organising ETCS in a formal language. I found this material called FOLDS https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf and it is claimed that topos axioms can be stated in FOLDS as in the style of the axioms on page 19. However, when we have both an initial object 0 and a terminal object 1, the sort of arrows from 1 to 0 is empty, but it does not seem to me that FOLDS allows empty sort. On page 20 of the above link, it is written: When X is a sort, and x:X, that is, x=〈2,X,a〉 for some a, x is called a variable of sort X And later it is written that we can use the natural numbers to serve as the "a". Therefore, once we have a sort, we can form infinitely many variables. If we require every sort to be non-empty then we have soundness issue here: it can be easily proved that there does not exist any arrow 0 -> 1, otherwise we will have $0\cong 1$. So is it my misunderstand? How do we treat empty sort in FOLDS?

   This question comes to me because I am interested in organising ETCS in a formal language. I found this material called FOLDS https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf and it is claimed that topos axioms can be stated in FOLDS as in the style of the axioms on page 19. However, when we have both an initial object 0 and a terminal object 1, the sort of arrows from 1 to 0 is empty, but it does not seem to me that FOLDS allows empty sort.

   On page 20 of the above link, it is written:

   When X is a sort, and x:X, that is, x=〈2,X,a〉 for some a, x is called a variable of sort X

   And later it is written that we can use the natural numbers to serve as the “a”. Therefore, once we have a sort, we can form infinitely many variables.

   If we require every sort to be non-empty then we have soundness issue here: it can be easily proved that there does not exist any arrow 0 -> 1, otherwise we will have $0\cong 1$.

   So is it my misunderstand? How do we treat empty sort in FOLDS?

2. • CommentRowNumber2.
   • CommentAuthorOscar_Cunningham
   • CommentTimeApr 30th 2021
   • PermaLink
   Author: Oscar_Cunningham
   Format: MarkdownItexThe 'variables' are just part of the language. In order to be able to say something like $\neg\exists x:1\to 0$ you need to have a symbol '$x$', but this doesn't mean there exists an $x$ of that type in the interpretation.

   The ’variables’ are just part of the language. In order to be able to say something like $\neg\exists x:1\to 0$ you need to have a symbol ’$x$’, but this doesn’t mean there exists an $x$ of that type in the interpretation.

3. • CommentRowNumber3.
   • CommentAuthorYimingXu
   • CommentTimeApr 30th 2021
   • (edited Apr 30th 2021)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThanks for replying! I am confused though: Am I correct that $\exists x: 1 \to 0$ is not even a formula so we cannot add a $\not$ before it? If I am correct with this, how can I express that there does not exist any arrow 0 ->1 as a formula in this logic? (If such a statement cannot be formulated in formula, I wonder if the claim that topos theory can be formulated in this system is wrong.)

   Thanks for replying!

   I am confused though: Am I correct that $\exists x: 1 \to 0$ is not even a formula so we cannot add a $\not$ before it? If I am correct with this, how can I express that there does not exist any arrow 0 ->1 as a formula in this logic? (If such a statement cannot be formulated in formula, I wonder if the claim that topos theory can be formulated in this system is wrong.)

4. • CommentRowNumber4.
   • CommentAuthorOscar_Cunningham
   • CommentTimeApr 30th 2021
   • PermaLink
   Author: Oscar_Cunningham
   Format: MarkdownItexTo be more precise the formula would be '$\neg\exists x:1\to 0.\mathbf{t}$', where $\mathbf{t}$ is simply the 'true' formula.

   To be more precise the formula would be ’$\neg\exists x:1\to 0.\mathbf{t}$’, where $\mathbf{t}$ is simply the ’true’ formula.

5. • CommentRowNumber5.
   • CommentAuthorYimingXu
   • CommentTimeApr 30th 2021
   • (edited Apr 30th 2021)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThis is what comes up to my mind which I failed convincing myself that it works: if we express existence as this. Then the fact that "for every object $X$ which is not isomorphic to zero, there exists an arrow $1 \to X$" will be expressed as $\forall X. \not X \cong 0 \implies \exists f: 1 \to X. t$. However, if we want to instantiate this formula for an object $X_0$ which is non-zero, and we want a variable $f_0: 1\to X_0$ to be used in our next step of proof, then as the bounded variable $f$ does not appear in the body of the formula, we do not have an $f_0$ to work with after we eliminate the $\exists$.

   This is what comes up to my mind which I failed convincing myself that it works: if we express existence as this. Then the fact that “for every object $X$ which is not isomorphic to zero, there exists an arrow $1 \to X$” will be expressed as $\forall X. \not X \cong 0 \implies \exists f: 1 \to X. t$. However, if we want to instantiate this formula for an object $X_0$ which is non-zero, and we want a variable $f_0: 1\to X_0$ to be used in our next step of proof, then as the bounded variable $f$ does not appear in the body of the formula, we do not have an $f_0$ to work with after we eliminate the $\exists$.

6. • CommentRowNumber6.
   • CommentAuthorYimingXu
   • CommentTimeApr 30th 2021
   • (edited Apr 30th 2021)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexAnd the problem is not solved if we ensure that $f$ appears in the formula: if we express the existence of $x: 1 \to X$ as $\exists x. x = x$, then we get a variable $x: 1 \to X$ to use after applying the deductive rules to eliminate the quantifier. But then under the same style, we should write 'there does not exist $x$ such that $x: 1 \to 0$" as $\not\exists x:1 \to 0. x = x$. By the rules of equality of FOLDS (on page 36), we have $x = x$, where $x$ is of any sort, including the sort $1\to 0$, which is legal to form. Hence we get a contradiction. how can we make "writing out a term $x: 1\to 0$' forbidden? Otherwise we get into this contradiction. I am so confused...

   And the problem is not solved if we ensure that $f$ appears in the formula: if we express the existence of $x: 1 \to X$ as $\exists x. x = x$, then we get a variable $x: 1 \to X$ to use after applying the deductive rules to eliminate the quantifier. But then under the same style, we should write ’there does not exist $x$ such that $x: 1 \to 0$” as $\not\exists x:1 \to 0. x = x$. By the rules of equality of FOLDS (on page 36), we have $x = x$, where $x$ is of any sort, including the sort $1\to 0$, which is legal to form. Hence we get a contradiction. how can we make “writing out a term $x: 1\to 0$’ forbidden? Otherwise we get into this contradiction. I am so confused…

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeApr 30th 2021
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe variable doesn't need to appear in the body of the formula in order for $\exists$-elimination to give you a free variable to work with.

   The variable doesn’t need to appear in the body of the formula in order for $\exists$-elimination to give you a free variable to work with.

8. • CommentRowNumber8.
   • CommentAuthorYimingXu
   • CommentTimeMay 1st 2021
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexI see. The thing I did not pay enough attention before is the context. the structural rules only works given a context.And the fact that "we do not have a variable $x:1\to 0$" in a context prevent us from writing out the formula $x:1\to 0 = x : 1\to 0$. I was dealing with the rules too naively. Thanks for correcting me if this comment of mine is still wrong/not the point.

   I see. The thing I did not pay enough attention before is the context. the structural rules only works given a context.And the fact that “we do not have a variable $x:1\to 0$” in a context prevent us from writing out the formula $x:1\to 0 = x : 1\to 0$. I was dealing with the rules too naively. Thanks for correcting me if this comment of mine is still wrong/not the point.