Hi, all.

I am trying to understand the proof of proposition 7.6 in Shulman’s paper https://arxiv.org/pdf/1808.05204.pdf . I am interested in understanding it for applying it within SEAR to obtain interesting constructions (or ETCS, I say SEAR here because it comes with a collection axiom). One point that confuses me is that I am not yet familiar to the notion of stacks. As the claim is that the proof of 7.6 can be carried our within SEAR for each particular case, I think it would be ideal if I can see how the proof of 7.6 expands on particular examples to obtain a proof within SEAR. (Note: I do not think I am confused by how to apply the principle of replacement, I am confused by how its proof works for these particular examples. Say, from the context we can obtain from collection, how can we derive the existence of the context we want by manipulation within these examples without directly appeal to the replacement schema.)

For the simplest example I can think of, consider we want to build the well-ordered set N without explicitly defining the order “$lt$”. I think we may obtain an isomorphic copy of the well-ordered set N using replacement.

Let U be N, u be a natural number n in N, we can prove for each n there exists a set A and a relation R on A, such that R is a well order on A. That is, the context $\Theta$ is $[A,R:A\looparrowright A]$, and it can be proved that consider the formula $\phi$ such that $\phi(N,n,A,R:A\looparrowright A)$ is true iff $A$ has cardinality $n$ and $R$ is a well-order on $A$, then there would be a context over a cover $p:V \to N$ which descents to a context over $N$, and the resultant context should consist of a set $\tilde{A}$ and a relation on $\tilde{A}$, where $\tilde{A}$ has a map to $N$, call it $q$. I think then $q^{-1}(n)$ will be the well-ordered set contains $n$ elements, and the whole $\tilde{A}$ is the disjoint union of $A_0,\cdots,A_n,\cdots$. where $A_n$ is the well-ordered set containing $n$ elements. Then we can collect the maximal elements in each such set and obtain a copy of $N$ with the order $\lt$.

This example above is due to myself and I am not sure if I have got it correct, but the following example from Mike Shulman must be correct. It is a bit complicated and let me expand the story in details below.

For an ordinal $\alpha$, there is a notion of the $\alpha$-th Beth number, denoted as $\beth_\alpha$. This **number** itself is a **set**, so you may think of associate each ordinal with a set.

If $\alpha \lt \omega$, means that $\alpha$ is a finite ordinal, that is, a natural number, then the $\alpha$-th Beth number is the power set That is, , $P^\alpha(\mathbb N\beth_0 =\mathbb N\beth_1= PN$, $\beth_2 = PPN$ and $\beth_3 =PPPN$, etc.

Now consider the notion of the $\omega$-th Beth number, $\beth_\omega$ is defined to be the minimal set such that for every natural number $n$, the set $\beth_n$ injects to it. We are going construct $\beth_\omega$, and its construction relies on schema of replacement.

Regarding how to apply the replacement schema (credit to Mike Shulman):

The way to use replacement of contexts here is something like the following. For simplicity consider the natural numbers N. For x in N, consider the context consisting of a set X, a function p : X -> N, a relation R from X to X, and a function z : N -> X. Depending on x and on this context, consider the statement that the image of p is {y | y <= x}, that z is an isomorphism onto the fiber p^{-1}(0), and that R is the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x. One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic. Therefore, by replacement of contexts, there is a universal such context over N, which in particular has a function p : X -> N x N. Pulling this back along the diagonal map of N, we obtain an N-indexed family of sets that is the sequence of iterated powersets starting with N, and thus its total space is beth_omega.

Recall the statement of replacement of contexts (from Shulman’s paper):

for any formula $\phi(U, u :\in U, \Theta)$, for any $U$, if for every $u :\in U$ there is an extension $\Theta$ of $(U, u)$ such that $\phi(U, u, \Theta)$, and moreover this extension $\Theta$ is unique up to a unique isomorphism of contexts $\Phi_\Theta$, then there is an extension $\Theta_0$ of $(U ^* U,\Delta U )$ in $Set/U$ such that $\phi(U, u , u ^ * \Theta_0 )$ for all $u :\in U$.

Here the $\phi$ is the “statement” in ” consider the statement that the image of p”. This statement is on the following parameters: 1. The fixed natural number $x$, as in “For x in N, consider…”. 2. the function $p:X\to N$, 3. the relation $R:X\looparrowright X$, which is “the union of “membership” relations witnessing that p^{-1}(y+1) is the powerset of p^{-1}(y) for all y<x”. (Union of relations are given by consider a relation from $X$ to $Y$ as a subset of the power set ${\cal P} (X\times Y)$). 4. the funcion $z:N\to X$, which injects $N$ to $X$.

Intuitively, this relation says that $X$ is a set which is fibred over $N$ via the projection map $p:X\to N$, such that the fibre of $0$ is $N$, and for each number $m\lt n$ the fiber of its successor $m+1$ is the power set of the fiber of $m$. (*) Therefore, $\beth_n$ is the fiber of $n$.

Call the predicate by $Upow(n,p:X\to N,R:X\looparrowright,z:{N}\to X)$, we apply replacement of contexts on $Upow$. Here $U$ is $N$, $u\in U$, is $n\in N$, $\Theta$ is the list $[X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]$. As suggested by

One can prove by induction on x that two contexts satisfying this statement are uniquely isomorphic.

By induction on $n\in N$, we prove there exists a context $[X,p:X\to { N},R:X\looparrowright X, z:{ N} \to X]$ up to unique isomorphism such that $Upow(n,p:X\to N,R:X\looparrowright X,z:{ N}\to X)$. Therefore we can apply replacement. It gives a context $\Theta_0:=[X_0(\to N),p_0:X_0\to { N}\times { N}, R_0:X_0\looparrowright X_0,z_0:{\Bbb N}\times {N}\to X_0]$ where the maps $p_0,z_0$ and the relation $z_0$ are in the slice category. In particular, the fibre of the map $p_0:X_0\to { N}\times { N}$ on the point $(n,n)$ is the greatest fiber, i.e., the fiber of $n$ as in (*) above, of a context satisfying $Upow(n,p:X\to N,R:X\looparrowright,z:{ N}\to X)$. Therefore, pulling back along the diagonal map just means take out all these sets $\beth_1,...,\beth_n,\beth_{n+1},...$ (infinitely many). All these sets are contained as a subset of $X_0$, so we can take union of them.

Could someone please explain the proof of 7.6 in Shulman’s paper, in terms of some examples such as the two above, to illustrate how the proofs work? It does not have to be convoluted. I am most confused by the step which uses “Set is a stack of its regular topology”.

]]>I was recently looking for references on the horizontal categorification of the notion of a monad, maybe called something like a 'monadoid'. I was surprised that I couldn't find anything on nlab or elsewhere about this, given that monads are so well-documented and it it clear to see what the right definition of a monadoid should be. (Monads are internal monoids in some endofunctor category End(C), equivalently they're End(C) enriched categories with one object, and then you can immediately generalize this and define monadoids to be End(C)-enriched categories.) I've quickly put together a document listing the right definitions for monadoids and some related concepts like their algebras (algebroids?) and the counterpart of the Kleisi category. I've also written down some simple examples and how they might be interpreted as computational side effects with a twist. So my question is twofold:

1) Has anyone seen anything like this before? Is there already a reference somewhere on nlab for what I've been calling monadoids?

2) If not, would nlab be a good place to upload these definitions/make an nlab entry for them?

I would be a first-time contributor here on nlab, so am hesitant to just make a page without checking first that the concept is relevant and has not already been documented!

Thanks! ]]>

Hi, all.

I would like to understand hoe does SEAR Axiom 5 works, that is Axiom of collection in SEAR.There is a section on “Application of Collection” and a sentence “(more detail to be added here…)”. My question is basically “what is intended to be there” in short.

According to my current understanding the example in this incomplete section, which aims to construct the ghost of $\{P^n(N)\mid n\in N\}$ should work as follows: we have a predicate taking a natural number $n$ and a set $Pn$, such predicate holds if $Pn \cong P^n(N)$ (here $\cong$ means bijection, cannot use equality here because the nlab page claims that there is no equality between sets.). And by axiom 5, we have a set $B$, a function $p:B\to N$. and a $B$-indexed family of sets $M:B\looparrowright Y$ such that for any $b\in B$, $M_b \cong P^{p(b)}( N)$ and for any $n\in N$, there exists a member of$b$ which is mapped to $n$. (because $P^n(N)$ exists for every $n$).

Does this sound correct?

If so, then it seems to me that the application of Axiom 5 only gives $Y$ contains $\coprod_{n\in N}P^n(N)$. As the nlab page claims that the collection axioms plays a similar role as replacement. How can I demonstrate that the thing I have obtained here is useful enough to be an analogue of the set $\{P^n( N)\mid n\in N\}$ as in ZF?

Other examples on SEAR Axiom 5 would also be nice! Thank you!

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

]]>It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

I think the statement of strong induction to prove is as the following.

For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

]]>I am reading the following document about Lawvere’s ETCS:

http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf

My question is about Theorem 6 in this document. The aim is to prove an equivalence relation is an equalizer. On page 29, the author says:

Finally we can assert our theorem (I think the $a_0q = a_1g$ in the link is a typo.) $a_0q = a_1q$ iff $a_0 \equiv a_1$.

And finished the proof.

That is, the author proves for every element $\langle a_0,a_1\rangle$ from the terminal object $1$, we have the split via the map which we want to prove to be an equalizer. But to prove the equalizer result, we need that we still have the factorization when $1$ is replaced by any arbitrary object. I know that $1$ is the generator in ETCS, and have trouble working out the proof that the existence of factorization for $1$ implies the existence of factorization for any $T$. I tried taking the elements of $T$, and unable to construct a factorization from $T$ from the factorization for its elements.

Any help, please? Thank you!

Note: If someone is reading the link above, then please note that the composition is written as: if $f: A \to B,g: B\to C$, then the author will write $fg$ to denote the composition of $f$ of $g$, rather than $g \circ f$.

]]>http://cstheory.stackexchange.com/questions/18716/good-reference-about-approximate-methods-for-solving-logic-problems

I also have found several papers about it. E.g. undecidability of modalo logics can be overcome by limiting depth of nesting of modal operators. While this is not mathematically pure solution, it is very good approximation to the human reasoning that is not quite capable of self-reflection.

Are there chances that heuristic methods - e.g. genetic algorithms or neural networks can overome undecidability problem - e.g. by discovering theorems and proofs that can not be discovered by algorithmic methods?

I see big prospects for categorical logic to become the universal logic that unifies all sorts of reasoning types (human agent modelling, creativity modelling, mathematical reasoninig, legal reasoning are all types of reasoning that requires different different methods but the application borders are smooth and therefore unification is necessary) but the application will be impossible if there is no methods for handling undecidable cases. Therefore one should be able to overcome undecidability. ]]>

Intuitively, in physical real systems, entropy is scale dependent in the sense that at small and big scales entropy seems to be maximum and arriving to a minimum at a certain characteristic scale. Do this fact some any fundament in categorical definitions ? ]]>

Ok-since there is an adjunction between the theories of a logic and the models of those theories,maybe there is a need to somehow meld probability theory and logic using category theory/categorical logic?Since machine learning as far as I read of artificial intelligence is much easier in probability theory,and also it would be much easier to generate random numbers based on the learned distribution,probabilities would give the creativity part of true intelligence,and logic would be used to structure what the AI agent learned.

As I see it,the end goal of this idea is an algorithm based on the syntax-semantics adjuntion that would learn (semantics->;syntax) and then generate (syntax->semantics) hypotheses about the subject,then test it out and learn based on reinforcement methods.Basically the end goal would be a general algorithm for the scientific method,which sounds crazy,but i've been thinking about this for a few years and just need to let this out in the open,since I don't yet have the appropriate knowledge or skills to work this idea out whether it's semi-feasible or not.

Also,if I'm thinking staright,then maybe we could use the curry-howard isomorphism and metaprogramming to write an AI agent that would improve itself,but this is bordering on sci-fi and this is why I'm writing this-to know wether or not I'm yet another crackpot. ]]>