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.

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

]]>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…

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

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

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

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

]]>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?

]]>