User wouter stekelenburg - MathOverflow

Answer by Wouter Stekelenburg for Does this kind of endofunctor ever have an initial algebra?

2013-04-23T07:13:57Z

I don't know any examples with $\Omega$, but $x\mapsto 2^{2^x}$ has an initial algebra in the effective topos. The object $2^{2^x}$ is a quotient of a subobject of the natural number object for any object $x$. The category of quotients of subobjects of the natural number object is `weakly complete' (see Hyland 1988 'A small complete category'). This is complete enough to get an initial algebra in this subcategory, and I am pretty sure that it is initial in the category of all algebras in the effective topos. My paper (Stekelenburg 2010 'A note on extensional PERs') has a description of these algebras.

Categories of recursive functions

2013-04-04T13:37:08Z

I have a couple of conjectures on recursive functions, that I feel must have been proved or refuted by someone else, but I don't know where to look. In short:

1. The primitive recursive functions form a pseudoinitial small finite product category with natural number object.

2. The partial recursive functions form a pseudoinitial small regular category with natural number object.

The longer version is as follows.

In non closed Cartesian categories, the natural number objects should be defined in a more stable way: $N$ together with $0:1\to N$ and $s:N\to N$ is a natural number object if for each $f:X\to Y$ and $g:Y\to Y$ there is an $h:N\times X \to Y$ such that $h(0,x) = f(x)$ and $h(n+1,x) = g(h(n,x))$. This roughly means that the projection $N\times X\to X$ is a natural number object in the slice over $X$ for every object $X$.

A 0-cell in a 2-category is pseudoinitial if there is an up to isomorphism unique 1-cell to every other two cell. The first conjecture in full is as follows: The 2-category of small finite product category with a chosen natural number object and finite product preserving functors which preserve the choice of natural number object and all natural transformations, has a pseudoinitial 0-cell. One of these pseudoinitial 0-cells is the category whose objects are powers of $\mathbb N$ and whose morphisms are primitive recursive functions. The second conjecture says that there is a pseudoinitial object in the category of small regular categories with NNO. This time the category of recursively enumerable sets and recursive functions is such a pseudoinitial 0-cell.

The conjectures fail if non standard models of arithmetic can exclude primitive / partial recursive functions that exists in the standard model: categories of non standard recursive functions could be counterexamples.

Have you seen anything like this before? If so, am I right?

Answer by Wouter Stekelenburg for Was the early calculus inconsistent?

2013-03-20T14:16:00Z

The completeness of the real number implies that there are no infinitesimals. If $\epsilon$ is infinitesimal, then $n\epsilon<1$ for all $n\in \mathbb N$. This bounded increasing sequence has no least upper bound, although it should by completeness.

In the form of Archimedes' axiom, completeness has been a part of mathematics since ancient times. Archimedes himself used it to solve some problems of calculus. I always thought that Berkeley spotted this inconsistency and rightfully complained about it.

Answer by Wouter Stekelenburg for Adjoint of Pushout as Modal Operators in Internal Logic

2013-02-11T16:21:14Z

The pullback $\forall$ and $\exists$ are adjoint to the inverse image map of a morphism, which sends a subobject to its pullback along the morphism. I don't know what a pushout of a subobject is, though you could give that name to either $\exists$ or $\forall$. In those cases one of your modalities is simply the pullback, however.

Kripke models of modal logic are related to sheaf models of constructive logic, and the modalities themselves are functors- or even monads-up-to-logical-equivalence depending on the modal logic.

Answer by Wouter Stekelenburg for Nelson natural number objects in a topos (say)

2013-01-25T16:35:38Z

I think the answer is no, because being an natural number object is a universal property and being a model of Nelson arithmetic is not.

As long as a category is Heyting (is a regular category where the inverse image maps between subobject lattices have right adjoints) it is possible to talk about models of any first order theory inside the category. There is a problem though: often the models of a first order theory are not unique up to (unique) isomorphism in Heyting categories. So being the model of a first order theory in a Heyting category isn't often a universal property.

A natural number object is not essentially a model of Peano arithmetic, as Peano arithmetic has many non standard models. I would say that it is essentially a model of second order arithmetic, although this doesn't directly make sense in other categories than toposes.

Nelson arithmetic is weaker than Peano arithmetic, and therefore has the same non standard models, if not many more. One could say that there are usually are many non isomorphic Nelson natural number objects. But I don't think this is what you mean.

After Francois' comment, I might have a better idea of what you are looking for. I suppose you want something like a natural number object, that happens to force Nelson's arithmetic in the internal language.

The definition of natural number object makes sense in arbitrary monoidal categories, if formulated properly. In these contexts we still have all primitive recursive functions, though; they don't have the restrictions in complexity that the survey article on Nelson's arithmetic mentions. So removing structure from the ambient category is insufficient.

Linear logics are capable of controlling complexity, and I would look for an answer there. The idea is that the ambient category has an endofunctor $!$, and that recursion does not give you morphisms from the natural number object $N$, but from $!N$ instead. You can now control the debt of recursion in functions $N\to N$ by controlling which morphisms $!N\to N$ factor though a canonical morphism $!N\to N$. I have tried to find a related universal property a couple of months back, but have been unsuccessful.

Answer by Wouter Stekelenburg for Monoidal structure on a category with products and with terminal object

2012-11-01T19:57:58Z

You can find it as an example of a monoidal category in Tom Leinster's "Higher Operads, Higher Categories", which contains loads of coherence proofs for higher categories.

Answer by Wouter Stekelenburg for A continuous notion of realizability

2012-10-24T09:49:17Z

Kleene defined a continuous realizability over Baire space, i.e. $\mathbb N^{\mathbb N}$ with the product topology. In this model $\forall x\exists y\phi(x,y)$ is valid, if there is a continuous function $f$ such that $\forall x\phi(x,f(x))$ is valid. That sounds like what you are looking for. A realizability model assigns a set of realizers to each formula, and $p\models q$ is valid if there is a suitable partial function mapping realizers of $p$ to realizers $q$. In Kleene's example the realizers are members of Baire space and the functions are the partial continuous ones.

To generalize this example, you should consider the category equilogical spaces as an interesting category to develop such a continuous model theory in. In this category realizers can be points of arbitrary T_0-spaces. I am unsure how much research has been done in this area.

Realizability models can be extended to realizability toposes, if and only if they have (order) partial combinatory algebras as object of realizers. This can be gathered from Streicher and Lietz's "Impredicativity entails untypedness" in combination with Hofstra's "All realizability is Relative". In order to get all realized functions to be continuous, I would suggest looking into topological partial combinatory algebras. Some research on these has been done by Ingemarie Bethke.

I invite you to have a look at my PhD. thesis, which can be downloaded from http://www.staff.science.uu.nl/~steke104/. It contains a lot of information on realizability toposes.

Answer by Wouter Stekelenburg for Small categories and completeness

2012-10-03T19:39:19Z

Small (co)complete categories are posets by a theorem of Freyd. If $C$ has all small coproducts and its class of morphisms $C_1$ is small, then $C(x,y)^{C_1}\simeq C(\coprod_{f\in C_1} x, y)\subseteq C_1$. If $C(x,y)>1$, then $C_1$ has a subset of strictly greater cardinality: contradiction.

A poset that has suprema and infima of all of its subsets is a complete category.

Answer by Wouter Stekelenburg for What categories correspond to the typed lambda calculus with parametric types?

2012-09-22T13:13:30Z

The internal language of a locally Cartesian closed category is a dependent type theory. A category $\mathcal C$ is locally Cartesian closed, if all of its slices $\mathcal C/X$ are Cartesian closed. An arrow $f:X\to Y$ is both interpreted as a variable substitution and as a family of types indexed over $Y$ in the type theory.

Answer by Wouter Stekelenburg for On internal functions and arrows in a Topos

2012-06-25T08:09:01Z

Question 1] Morphisms $\lambda:X\times Y\to\Omega$ correspond to subobjects $L\subseteq X\times Y$. The conditions ed says that the projection $\pi_0:L\to X$ is a (regular) epimorphism, and uv says that $\pi_0$ is a monomorphism. Therefore $\pi_0$ is an isomorphism, and $l = \pi_1\circ \pi_0^{-1}:X\to Y$ is the corresponding morphism. In the other direction, for each $l:X\to Y$ there is a graph ${\rm gr}(l)\subseteq X\times Y$. The projection $\pi_0:{\rm gr}(l) \to X$ is an isomorphism, and hence satisfies ed and uv. This sets up a bijection between functional relations and morphisms in a topos.

Subquestion] these are provably equivalent in first order constructive logic.

Question 2] It should be $f_*\Omega_{\mathcal F}$, because $f_* :\mathcal F\to\mathcal E$. Now we are dealing with naturally equivalent locales, $\mathcal E(X\times Y,f_*\Omega)\simeq \mathcal F(f^*X\times f^*Y,\Omega)$. Hence the morphisms satisfying ed and uv coincide.

Answer by Wouter Stekelenburg for products in a category without reference to objects or sources and targets

2011-06-26T10:40:08Z

As Freyd and Scedrov show in "Categories, Allegories", you can think of a category as some kind of partial monoid. Such a monoid has a set of partial units that take over the role of objects in standard presentations of categories.

Answer by Wouter Stekelenburg for Bijection of proper classes

2011-06-18T08:06:37Z

Many set theories with classes have the limitation of size principle. This says all proper classes have the same cardinality. The only interesting bijections are the ones that are definable by a formula (because formulas give extra information that anonymous bijections hide). There probably are alternative foundations where the limitation of size principle does not hold or models of ZFC where the definable classes have different sizes. You might find an interesting theory of functions (and bijections) of proper classes there.

Answer by Wouter Stekelenburg for What abstract nonsense is necessary to say the word "submersion"?

2010-11-12T11:36:26Z

Given two manifolds $M$and $N$ and a differentiable map $f:M\to N$, pull back the tangent bundle of $N$. The derivative arrow $Df: TM \to f^*TN$ is a morphism of vector bundles over $M$ and a regular epimorphism iff $f$ is a submersion. So the extra structure we need is something like the tangent bundle on every object of the category.

Answer by Wouter Stekelenburg for Independence and Category Theory

2010-10-18T09:11:42Z

A category is small if its objects and morphisms form a set rather then some other kind of class. Smallness is therefore relative to the model of set theory we are working in and the whole notion was invented just to express this dependence on set theory. The limits you are talking about are unstable: they change when the model of sets in the background changes. Most mathematicians that work with categories simply avoid such pathological cases.

Answer by Wouter Stekelenburg for Name for a functor with this property?

2010-10-18T08:49:38Z

If the right adjoints are also a right inverses, than such functors are called (Grothendieck) fibrations. If the right adjoint are full and faithful, than such functors are called Street fibrations.

name my cat: regular categories where inverse images also have right adjoint

2010-10-14T13:18:10Z

I need a name for a regular category where the inverse image maps have right adjoints.

If $\mathcal C$ is a regular category, then the poset of subobjects $\mathsf{Sub}(X)$ of any object $X$ is a semilattice and the inverse image map of any arrow $f:X\to Y$ has a left adjoint $\exists_f:\mathsf{Sub}(X) \to \mathsf{Sub}(Y)$. If $\mathcal C$ is a Heyting category, then the inverse image map $f$ also has a right adjoint $\forall_f:\mathsf{Sub}(X) \to \mathsf{Sub}(Y)$. But Heyting categories also have all finite coproducts and I want a name for regular categories that just have those right adjoints.

Do you know if this category of categories already has a name? Can you suggest a name?

Update: Heyting categories or logoses need not have all finite coproducts, but posets of subobjects are lattices, where I only need semilattices.

Answer by Wouter Stekelenburg for Au revoir, law of excluded middle?

2010-05-24T10:32:22Z

In a topos, the question is not whether a sentence is true or false, but where it is true, because toposes -- at least the geometric ones you're talking about -- are generalized spaces. Usually, there are some limit points where this question cannot be decided for all sentences. The problem is then that other points can be found within any distance (more accurately: any open neighborhood) both where a sentence is true and where the same sentence is false.

Answer by Wouter Stekelenburg for What is the difference between the biconditional iff. and equality = ?

2010-05-17T07:55:43Z

If two predicates describe the same set, does that mean that they are equal or that they are logically equivalent? "$\phi = \psi$" could mean that $\phi$ and $\psi$ are literally the same formula. We write $\Leftrightarrow$ for logical equivalence to avoid ambiguity.

Answer by Wouter Stekelenburg for Why do so many textbooks have so much technical detail and so little enlightenment?

2010-01-28T12:41:04Z

Books are expensive, and a book that can be used in many different problems is more useful than one that focuses exclusively on one. That is why nice stories of the adventures of mathematics are harder to sell than dry theoretical expositions.

A story of solving a problem or proving a theorem is likely to be more entertaining and easier to follow and to remember even if the solution involves a lot of difficult mathematics. But each each story can hold just a small amount of theory, and once you know the stories, the story book becomes useless.

Dry theoretical expositions find their way into our own stories, when we consult them in order to find a solution for one of our problems. We are more likely to buy such books, because they are so much more useful to us in reality. Beyond that it is all economics: writers of mathematical texts develop a dry theoretical style, because that is what their readers demand.

Comment by Wouter Stekelenburg

2013-04-11T06:58:00Z

@Paul: A counterexample to the conjectures. I did specify the objects of my categories in the question: powers of $\mathbb N$ for the first and recursively enumerable set for the second.

Comment by Wouter Stekelenburg

2013-04-09T16:20:23Z

So the answer to my second question is no, because the free arithmetical universal is a counterexample.

Comment by Wouter Stekelenburg

2013-04-05T07:04:29Z

@Francois: I assume regular categories have finite limits. The definition of NNO is in the question, but 'parametrized' sounds like a good description.

Comment by Wouter Stekelenburg

2013-04-04T16:42:05Z

@Francois: in a regular category, a partial function $X\rightharpoonup Y$ is an isomorphism class of spans $(m:Z\to X, f:Z\to Y)$ where $m$ is monic. If a non standard model forces that $0=1$ is provable, doesn't it automatically force $0=1$?

Comment by Wouter Stekelenburg

2013-04-03T06:39:56Z

Not every topos is a Grothendieck topos, and for non Grothendieck toposes the answer is: no, such sites do not exist.

Comment by Wouter Stekelenburg

2013-03-25T09:51:45Z

To see that $\pi_0: L\to X$ is a monomorphism, consider its kernel pair $l,r:Z\to L\times L$. Now $\pi_0\circ l =\pi_0\circ r$ by definition, and $\pi_1\circ l = \pi_1\circ r$ by uv), because the morphism $(\pi_0\circ l,\pi_1\circ l,\pi_1\circ r): Z\to X\times Y\times Y$ represents the subobject $\{ (x,y,y')| \lambda(x,y)\land\lambda(x,y') \}$. Because $\pi_i\circ l = \pi_i\circ r$, $l=r$. To conclude: every parallel pair $f,g:W\to L$ such that $\pi_0\circ f= \pi_0\circ g$ factors uniquely through $l,r$. Therefore every such pair satisfies $f=g$.

Comment by Wouter Stekelenburg

2013-03-20T15:25:51Z

I guess that would hard to say in Newtons and Leibniz's work, because they never talked about real numbers. For nonstandard arithmetic and synthetic differential geometry, the answer is: yes. In those cases, completeness is subtly weakened to allow infinitesimal real numbers.

Comment by Wouter Stekelenburg

2013-03-20T15:15:25Z

But it is the kind that Berkeley would have had in mind.

Comment by Wouter Stekelenburg

2013-02-11T18:51:47Z

I said one of your modalities would be the pull back. If $\exists$ is the pushout and that $\Box$ is the right adjoint of the pushout. Then $\Box$ is the inverse image map, because the inverse image map is right adjoint to $\exists$, and adjoints are unique (... up to unique equivalence, but for subobjects, equivalence is equality).

Comment by Wouter Stekelenburg

2013-01-27T09:06:03Z

When linear logic was introduced by Girard, $!$ was a comonad. In order to get control over complexity, however, you have to let go of $!\alpha\to !!\alpha$, I think.

Comment by Wouter Stekelenburg

2012-11-01T23:17:00Z

Just formulated, but the book gives a lot of information that will allow you to prove it yourself.

Comment by Wouter Stekelenburg

2012-10-04T08:06:09Z

@Todd Trimble: since every object has an identity morphism, the set of morphisms has a greater cardinality than the set of objects. I fotgot to mention that.

Comment by Wouter Stekelenburg

2012-10-03T19:28:51Z

@Muro: all complete lattices are complete categories, so now you do.

Comment by Wouter Stekelenburg

2012-09-13T12:25:10Z

@Godelian: Cauchy completeness makes the sequence 1/n converge to 0 and this is logically equivalent to the Archimedean property. So how can there be a non Archimedean complete ordered fields?

Comment by Wouter Stekelenburg

2012-08-31T08:12:49Z

You are wrong about the effective topos. The real numbers are a quotient of a set the natural number there, but this covering set is not the image of a function $\mathbb N\to\mathbb N$.