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

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

For two sets of natural numbers $A,B$, the arrows between them are the computable functions $A \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,\cdots,n_k\}$, and suppose WLOG that $n_1,...,n_k$ is ordered from the lowest to the largest, then the function can be captured by $nlist ([f(n_1),\cdots,f(n_k)])$.

Therefore, exponential on the functions whose domain is finite is given by: $B^A$, for $A,B\subseteq N$, with finite $A = \{n_1,\cdots,n_k\}$, $B^A = \{nlist(f(n_1),...,f(n_k))\mid$ $f$ is a function $A\to B$ $\}$.

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

1.Find the order of $a$ in $A$, where the order is just the usual ordering on natural number.

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

Then given a function $g:A\times C \to B$, we can obtain a function $C\to B^A$ as follows:

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

Given an element $c\in C$, we form the set $\{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\}$, then the element in $B^A$ will be given by $nlist([f(c,a_1),...,f(c,a_k)])$. This defined a function $C\to B^A$.

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

]]>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\}$, 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.

]]>Thank you for trying to help! Sorry, I was too sketchy there. For this sentence, I meant to exclude all functions $N\to \{0,1}A \to B$ where $A,B\subseteq N$ and $A$ is infinite. I want $N$ 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 $N$. So I do not have hope to get it work then. Next time I ask about a construction I will be more precise.

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

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

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

ZFC can prove BZC consistent, since $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.

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

Take the subcategory of **Sets** whose set of object is $| 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\to N$.

We know that there is a bijection $N\times N \to N$, call this function $npair$. Inductively, this bijection gives a bijection from list of natural numbers to $N$, call this function $nlist$.

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

If $l\in N$ is a natural number that encodes a list, then $nel(n,l)\in N$ is the $n$-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.

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

]]>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_{\omega+\omega}$ is a model of BZC, hence gives a topos of sets that is a model of ETCS, regardless of countable models.

]]>A cardinal number $\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?

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

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