Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorYimingXu
    • CommentTimeApr 30th 2021
    • (edited Apr 30th 2021)

    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 010\cong 1.

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

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

    • CommentRowNumber3.
    • CommentAuthorYimingXu
    • CommentTimeApr 30th 2021
    • (edited Apr 30th 2021)

    Thanks for replying!

    I am confused though: Am I correct that x:10\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.)

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

    • CommentRowNumber5.
    • CommentAuthorYimingXu
    • CommentTimeApr 30th 2021
    • (edited Apr 30th 2021)

    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 XX which is not isomorphic to zero, there exists an arrow 1X1 \to X” will be expressed as X.¬X0f:1X.t\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 0X_0 which is non-zero, and we want a variable f 0:1X 0f_0: 1\to X_0 to be used in our next step of proof, then as the bounded variable ff does not appear in the body of the formula, we do not have an f 0f_0 to work with after we eliminate the \exists.

    • CommentRowNumber6.
    • CommentAuthorYimingXu
    • CommentTimeApr 30th 2021
    • (edited Apr 30th 2021)

    And the problem is not solved if we ensure that ff appears in the formula: if we express the existence of x:1Xx: 1 \to X as x.x=x\exists x. x = x, then we get a variable x:1Xx: 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 xx such that x:10x: 1 \to 0” as ¬x:10.x=x\not\exists x:1 \to 0. x = x. By the rules of equality of FOLDS (on page 36), we have x=xx = x, where xx is of any sort, including the sort 101\to 0, which is legal to form. Hence we get a contradiction. how can we make “writing out a term x:10x: 1\to 0’ forbidden? Otherwise we get into this contradiction. I am so confused…

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeApr 30th 2021

    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.

    • CommentRowNumber8.
    • CommentAuthorYimingXu
    • CommentTimeMay 1st 2021

    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:10x:1\to 0” in a context prevent us from writing out the formula x:10=x:10x: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.