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

n-Forum: Define operations so the collection of sets of natural numbers become a model of ETCS?

Bottom of Page

1 to 14 of 14

  1.  
    • CommentRowNumber1.
    • CommentAuthorYimingXu
    • CommentTimeMay 11th 2021
    • (edited May 11th 2021)

    We know Finset is a topos, but is not a model of ETCS since it does not have a natural number object.

    Is there any smart way of defining product/coproduct/exponential on the subcategory of Sets whose collection of object is collection of all sets of natural numbers (and therefore includes itself, so it is like joining a NNO to the category of finite sets), so it becomes a model of ETCS?

    If it is not possible, I simply want a smaller model of ETCS which is not the category Sets.

    If such a model does not exists, is there any proof that relevant to the fact that there is no subtopos of Sets which is a model of ETCS?

  2. Such a thing would have to not be definable in ETCS itself, or else ETCS would prove itself consistent. But if ETCS is consistent then it has a countable model, so you can define some notion of homomorphism between natural numbers to turn them into a model.

    • CommentRowNumber3.
    • CommentAuthorHurkyl
    • CommentTimeMay 11th 2021
    • (edited May 11th 2021)

    A cardinal number α\mathbb N\alpha is a strong limit cardinal iff the category of sets with cardinality less than alpha is a topos.

    I believe any such example is a model of ETCS?

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 11th 2021

    It’s consistent that there is no inner model for a set theory, I believe: https://en.m.wikipedia.org/wiki/Minimal_model_(set_theory).

    And I think V ω+ωV_{\omega+\omega} is a model of BZC, hence gives a topos of sets that is a model of ETCS, regardless of countable models.

    • CommentRowNumber5.
    • CommentAuthorYimingXu
    • CommentTimeMay 11th 2021
    • (edited May 11th 2021)

    Thanks to all the three of you who gives me response!

    –A cardinal number α is a strong limit cardinal iff the category of sets with cardinality less than alpha is a topos. /I think Vω+ω is a model of BZC, hence gives a topos of sets that is a model of ETCS.

    Thanks for pointing out this so I know that it is not impossible.

    –Such a thing would have to not be definable in ETCS itself, or else ETCS would prove itself consistent (inconsistent?)./ Such a thing would have to not be definable in ETCS itself, or else ETCS would prove itself consistent.

    I guess you are possibly talking about Godel’s second completness theorem? I think the point that I am not trying find an inner model of ZF or ETCS, but a model of ETCS inside “material set theory”, might be subtle here.

    –But if ETCS is consistent then it has a countable model, so you can define some notion of homomorphism between natural numbers to turn them into a model.

    Interesting, what does this follow from? But then some natural number should serve as the natural number object. I cannot imagine how the construction would be.

    • CommentRowNumber6.
    • CommentAuthorYimingXu
    • CommentTimeMay 11th 2021
    • (edited May 11th 2021)

    I think maybe we have hope for a model with cardinality |P(N)||P( N)|? I feel the following might works, but very artificial.

    Take the subcategory of Sets whose set of object is |P(N)|| P( N)|. Arrows are all the arrows between these sets in Sets but exclude all the functions from any infinite set, except for the successor function N→NN\to N.

    We know that there is a bijection N×N→NN\times N \to N, call this function npairnpair. Inductively, this bijection gives a bijection from list of natural numbers to N N, call this function nlistnlist.

    If p∈Np\in N is a natural number that encodes a pair, that is, p=npair(a,b)p = npair(a,b) for some a,b∈Na,b\in N, then nfst(p)=a,nsnd(p)=bnfst(p) =a,nsnd(p) = b.

    If l∈Nl\in N is a natural number that encodes a list, then nel(n,l)∈Nnel(n,l)\in N is the nn-th element of this list.

    Then we can encode pairs of natural numbers as natural numbers, so the usual construction of product/pullback in Sets can be turned into a set of natural numbers. Also exponentials, which are sets of functions, can be encoded as a natural number.

    It is not obvious to me if capturing pairs and functions by natural numbers and excluding these functions with infinite domain makes some axioms unsatisfied already.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 11th 2021

    ZFC can prove BZC consistent, since V ω+ωV_{\omega+\omega} is a model of the latter, and is a set of the former. Since ETCS is about the same as BZC, since means that ZFC can prove that ETCS has a model. But if your background material set theory is BZC, then you cannot prove there is a model of ETCS, else BZC would be able to prove a model of itself exists, and this is not allowed by Gödel incompleteness.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2021

    But if ETCS is consistent then it has a countable model, so you can define some notion of homomorphism between natural numbers to turn them into a model.

    Interesting, what does this follow from?

    The downward Lowenheim-Skolem theorem.

    • CommentRowNumber9.
    • CommentAuthorYimingXu
    • CommentTimeMay 12th 2021
    • (edited May 12th 2021)

    Thank you! But what if we do not want to work in the background of any form of material set theory?

    if we do not want to axiomatise set theory and just define natural numbers as in (simple) type theory (i.e. without DTT) only and get a model of ETCS, would the construction outline above sound plausible?

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 12th 2021

    No it’s not yet plausible, because you haven’t giving a very convincing argument that you have a topos, sorry. The sentence “Also exponentials…” is a long way from proving your category is cartesian closed.

    Arrows are all the arrows between these sets in Sets but exclude all the functions from any infinite set,

    I don’t know what this means, so, even worse, it’s not clear what your category is. It’s not clear you have a natural number object, either.

    • CommentRowNumber11.
    • CommentAuthorYimingXu
    • CommentTimeMay 12th 2021

    Thank you for trying to help! Sorry, I was too sketchy there. For this sentence, I meant to exclude all functions A→BA \to B where A,B⊆NA,B\subseteq N and AA is infinite. I want NN to be the natural number object so just keep the successor map.

    Anyway, I have discovered problem that it will not work since it does not satisfy the axiom of choice. For the axiom of choice I certainly need maps from NN. So I do not have hope to get it work then. Next time I ask about a construction I will be more precise.

    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 12th 2021

    No problem with not having the axiom of choice, I’d be interested if you could still get a topos, subobject classifier and all. It probably couldn’t be {0,1}\{0,1\}, since you are removing all functions . But maybe I just don’t understand what your category is, or how it is meant to be a model of ETCS.

    • CommentRowNumber13.
    • CommentAuthorYimingXu
    • CommentTimeMay 13th 2021
    • (edited May 13th 2021)

    I am not removing all functions, but the ones whose domain is infinite, because a function from a finite set of natural number can be turned into a list, which can then be turn into a natural number. I realise that it is very wrong this morning. I am currently trying to prove a topos structure on the category consists of:

    The set of objects is P(N)N\to \{0,1}P(N).

    For two sets of natural numbers A,BA,B, the arrows between them are the computable functions A→BA \to B. Computable function has codes, which is a natural number encoding this function, so we have hope of having exponential. (I cannot say much about it before grabbing some knowledge about computable functions.)

    Product is, for A SUBSET N, B SUBSET N, {npair a b| a IN A /\ b IN B}

    Coproduct is, for A SUBSET N, B SUBSET N, {npair 0 a| a IN A} UNION {npair 1 b| b IN B}

    pushout and pullback are that in the category of Sets​​, but encoded as sets of natural numbers. That is, for two functions f: A -> B, g: A -> C, where A and B are set of natural numbers, the pullback is {npair a b| a IN A /\ b IN B /\ f(a) = g(b)}. Pushout is {npair 0 a| a IN A} UNION {npair 1 b| b IN B} and elements npair 0 a and npair 1 b are identified if they come from the image of the same element in A.

    I would post here if I can make progress on this construction.

    Here is my previous thought for Cartesian closure, which I believe it works if only take the object to be finite sets of natural numbers, it clarifies what was in my mind before, but may be useless later:

    For a function whose domain is finite, say, its domain is {n 1,⋯,n k}\{n_1,\cdots,n_k\}, and suppose WLOG that n 1,...,n kn_1,...,n_k is ordered from the lowest to the largest, then the function can be captured by nlist([f(n 1),⋯,f(n k)])nlist ([f(n_1),\cdots,f(n_k)]).

    Therefore, exponential on the functions whose domain is finite is given by: B AB^A, for A,B⊆NA,B\subseteq N, with finite A={n 1,⋯,n k}A = \{n_1,\cdots,n_k\}, B A={nlist(f(n 1),...,f(n k))∣B^A = \{nlist(f(n_1),...,f(n_k))\mid ff is a function A→BA\to B }\}.

    For the evaluation map, this is a map A×B A→BA\times B^A \to B. Given a natural number a∈Aa\in A and an element f∈B Af\in B^A, which is a natural number encoding a function, ev(a,f)ev(a,f) is given by (Note that it is not literally evaluating the pair (a,f), but the natural number npair(a,f)npair(a,f), same as below):

    1.Find the order of aa in AA, where the order is just the usual ordering on natural number.

    2.If aa is the rr-th member of AA, then ev(a,f)ev(a,f) is nel(r,f)nel(r,f), which is the rr-th element of the list that ff is encoded, which is supposed to be f(a)f(a).

    Then given a function g:A×C→Bg:A\times C \to B, we can obtain a function C→B AC\to B^A as follows:

    Recall A×C={npair(a,c)|a∈A,c∈C}A\times C = \{npair (a,c)| a \in A, c \in C\}

    Given an element c∈Cc\in C, we form the set {a∈A∣∃m∈A×C,nfst(m)=alandnsnd(n)=c}\{a\in A\mid \exists m \in A\times C, nfst(m) = a \land nsnd(n) = c\}, we order this set with the usual ordering on natural numbers, and obtain a set {a 1,...,a k}\{a_1,...,a_k\}, then the element in B AB^A will be given by nlist([f(c,a 1),...,f(c,a k)])nlist([f(c,a_1),...,f(c,a_k)]). This defined a function C→B AC\to B^A.

    For the commutativity condition: Given m∈A×Cm\in A\times C, which is npair(a,c)npair (a,c) for some a∈Aa\in A and c∈Cc\in C, g∈A×C→Bg\in A\times C\to B, we want ev(a,g¯)=g(a,c)ev(a,\overline{g}) = g(a,c), and this is by definition.

    • CommentRowNumber14.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 13th 2021

    You may be rediscovering the effective topos, but I can’t say for sure.

1 to 14 of 14

  1.