User andrej bauer - MathOverflow

Answer by Andrej Bauer for Lawvere's fixed point theorem and the Recursion Theorem

2013-05-20T07:22:07Z

There is indeed a very close connection between Lawvere's fixed-point theorem and Recursion theorem, but one has to look at it the right way. Namely, it all becomes clear once we do it in the effective topos.

Let us start by recalling Lawvere's theorem. (I use $X \to Y$ and $Y^X$ as synonyms for the set of all functions from $X$ to $Y$.)

Theorem (Lawvere): If $e : A \to B^A$ is onto then every $f : B \to B$ has a fixed point.

Proof. There is $x \in A$ such that $e(x)(y) = f(e(y)(y))$ for all $y \in A$, because $e$ is onto and $x \mapsto f(e(y)(y))$ is a map from $A$ to $B$. Then $e(x)(x) = f(e(x)(x))$ so $e(x)(x)$ is a fixed point of $f$. QED.

Now here is Recursion theorem written so that it is most similar to Lawvere's theorem. I explain below why this is the Recursion theorem.

Recursion theorem: Suppose countable choice holds and $e : \mathbb{N} \to B^{\mathbb{N}}$ is onto. Then every total relation $R \subseteq B \times B$ has a fixed point.

We say that $x \in B$ is the fixed point of $R$ if $R(x,x)$. Note that total relations can also be viewed as multivalued maps, so this is a fixed point theorem which generalizes the instance of Lawvere's fixed point theorem in which $A = \mathbb{N}$.

Proof. Because $R$ is total, for every $n \in \mathbb{N}$ there is $y \in B$ such that $R(e(n)(n), y)$. Therefore, by countable choice, there is a map $c : \mathbb{N} \to B$ such that $R(e(n)(n), c(n))$ for all $n \in \mathbb{N}$. As $e$ is onto there exists $k \in \mathbb{N}$ such that $e(k) = c$. But then $e(k)(k)$ is a fixed point of $R$ because $e(k)(k) = c(k)$. QED.

Of course, you are asking yourself what the theorem has to do with Recursion theorem from computability theory. Note that the proof is intuitionistic and uses countable choice, therefore it is valid in the effective topos. To get the connection with the classical recursion theorem, we need to understand what the object of partial computable maps looks like in the effective topos. In fact, it is just the function space $\mathbb{N} \to \mathbb{N}_\bot$ where I do not really want to get into the internal definition of $\mathbb{N} _{\bot}$, let me describe it as a numbered set instead: the underlying set of $\mathbb{N} _\bot$ is $\mathbb{N} \cup \lbrace \bot \rbrace$. A number $r$ realizes $\bot \in \mathbb{N} _\bot$ if the $r$-th Turing machine diverges on input $0$, and it realizes $n \in \mathbb{N} _\bot$ if the $r$-th Turing machine halts and outputs $n$ on input $0$.

Another way to explain the object of partial computable maps $\mathbb{N} \to \mathbb{N} _\bot$ in the effective topos is that this is the object of those partial maps whose domain is a countable subset of $\mathbb{N}$ (which of course is just the internal version of the classic theorem that partial computable maps have c.e. sets as their domains).

Anyhow, $\mathbb{N} \to \mathbb{N}_\bot$ is countable in the effective topos. This can be proved from the axioms of synthetic computability, but a shortcut is just to observe that there is an effective enumeration of partial computable maps, which realizes an enumeration $\varphi : \mathbb{N} \to (\mathbb{N} \to \mathbb{N} _\bot)$ in the effective topos.. But then, since by $\lambda$-calculus $$(\mathbb{N} \to (\mathbb{N} \to \mathbb{N} _\bot)) \cong (\mathbb{N} \times \mathbb{N} \to \mathbb{N} _\bot) \cong \mathbb{N} \to \mathbb{N} _\bot$$ we see that we may apply Recursion theorem to $\mathbb{N} \to \mathbb{N} _\bot$. So, given any $f : \mathbb{N} \to \mathbb{N}$, consider the total relation $R$ defined on $\mathbb{N} \to \mathbb{N} _\bot$ by $$R(u,v) \iff \exists k \in \mathbb{N} . u = \varphi_k \land v = \varphi_{f(k)}.$$ There is a fixed point $u$ and so by definition of $R$ there is $k$ such that $u = \varphi_k$ and $u = \varphi_{f(k)}$. And we have the usual recursion theorem as a consequence.

Let's do another one, just to convince you this is the recursion theorem. There is an enumeration $W$ of all countable subsets of $\mathbb{N}$ (yes, there are countably many countable subsets of $\mathbb{N}$ in the effective topos, and that is a way cool axiom if you like to smoke weird stuff). A typical exercise in recursion theorem asks for $n$ such that $W_n = \lbrace{ n \rbrace}$. Because the countable subsets of $\mathbb{N}$ satisfy the condition of recursion theorem, we get such a set simply by considering the total relation $R$ defined by $$R(S,T) \iff \exists m \in \mathbb{N} . S = W_m \land T = \lbrace m\rbrace.$$ Indeed, a fixed point is a countable set $S$ such that for some $m$ we have $S = W_m$ and $S = \lbrace m \rbrace$.

I could go on, but I am in fact preparing a paper about this which should appear on arXiv in a couple of days. See also my materials on synthetic computability (older material has suboptimal proofs of recursion theorem).

Answer by Andrej Bauer for On the large cardinals foundations of categories

2013-05-14T08:06:00Z

There is nothing wrong with that idea, execpt perhaps the questionable taste for countable models of ZFC. (That was half a joke. (That was 3/4 a joke. (I am sure you can see where this is going, so let us just agree that we have one whole joke.)))

In type theory it is common to have a countable sequence of universes $\mathcal{U}_0, \mathcal{U}_1, \mathcal{U_2}, \ldots$ This works pretty well and covers most of what people want, and category theory has been formulated like that. However, the annoying thing we want to avoid is book-keeping of universe levels. There are two techniques that we employ which greatly simplify matters:

We use universe polymorphism, i.e., by default we never refer to a specific universe but instead phrase all arguments so that they apply to any universe (or configuration of universes). This is like starting every theorem with "for any universe $\mathcal{U}_i$, ..." and then proving everything for that universe. (If several universes are involved, then the statement becomes more complicated.)
We use typical ambiguity, i.e., we say just "category" instead of "$\mathcal{U}$-small category" because we want to be ambiguous as to what level we are talking about. This gives the illusion that there is just a single universe. Nontheless, the illusion is quite useful.

There are some pitfalls. For example, one must never use the "function" $i \mapsto \mathcal{U}_i$, or any other construction which "climbs up the universe hierarchy". An example would be the sequence $$A_0 = \mathcal{U}_{0},$$

$$A_{n+1} = A_n \to \mathcal{U}_0.$$

Luckily, one rarely feels the temptation to think of such sequences. But more importantly, proof assistants handle universe polymorphism and ambiguity very well, so we actually do not have to worry about them in practice.

Mike Shulman wrote about this on the n-category cafe.

Answer by Andrej Bauer for Is rigour just a ritual that most mathematicians wish to get rid of if they could?

2013-05-08T21:40:02Z

I was not going to write anything, as I am a latecomer to this masterful troll question and not many are likely going to scroll all the way down, but Paul Taylor's call for Proof mining and Realizability (or Realisability as the Queen would write it) was irresistible.

Nobody asks whether numbers are just a ritual, or at least not very many mathematicians do. Even the most anti-scientific philosopher can be silenced with ease by a suitable application of rituals and theories of social truth to the number that is written on his paycheck. At that point the hard reality of numbers kicks in with all its might, may it be Platonic, Realistic, or just Mathematical.

So what makes numbers so different from proofs that mathematicians will fight a meta-war just for the right to attack the heretical idea that mathematics could exist without rigor, but they would have long abandoned this question as irrelevant if it asked instead "are numbers just a ritual that most mathematicians wish to get rid of"? We may search for an answer in the fields of sociology and philosophy, and by doing so we shall learn important and sad facts about the way mathematical community operates in a world driven by profit, but as mathematicians we shall never find a truly satisfactory answer there. Isn't philosophy the art of never finding the answers?

Instead, as mathematicians we can and should turn inwards. How are numbers different from proofs? The answer is this: proofs are irrelevant but numbers are not. This is at the same time a joke and a very serious observation about mathematics. I tell my students that proofs serve two purposes:

They convince people (including ourselves) that statements are true.
They convey intuitions, ideas and techniques.

Both are important, and we have had some very nice quotes about this fact in other answers. Now ask the same question about numbers. What role do numbers play in mathematics? You might hear something like "they are what mathematics is (also) about" or "That's what mathematicians study", etc. Notice the difference? Proofs are for people but numbers are for mathematics. We admit numbers into mathematical universe as first-class citizen but we do not take seriously the idea that proofs themselves are also mathematical objects. We ignore proofs as mathematical objects. Proofs are irrelevant.

Of course you will say that logic takes proofs very seriously indeed. Yes, it does, but in a very limited way:

It mostly ignores the fact that we use proofs to convey ideas and focuses just on how proofs convey truth. Such practice not only hinders progress in logic, but is also actively harmful because it discourages mathematization of about 50% of mathematical activity. If you do not believe me try getting funding on research in "mathematical beauty".
It considers proofs as syntactic objects. This puts logic where analysis used to be when mathematicians thought of functions as symbolic expressions, probably sometime before the 19th century.
It is largely practiced in isolation from "normal" mathematics, by which it is doubly handicapped, once for passing over the rest of mathematics and once for passing over the rest of mathematicians.
Consequently even very basic questions, such as "when are two proofs equal" puzzle many logicians. This is a ridiculous state of affairs.

But these are rather minor technical deficiencies. The real problem is that mainstream mathematicians are mostly unaware of the fact that proofs can and should be first-class mathematical objects. I can anticipate the response: proofs are in the domain of logic, they should be studied by logicians, but normal mathematicians cannot gain much by doing proof theory. I agree, normal mathematicians cannot gain much by doing traditional proof theory. But did you know that proofs and computation are intimately connected, and that every time you prove something you have also written a program, and vice versa? That proofs have a homotopy-theoretic interpretation that has been discovered only recently? That proofs can be "mined" for additional, hidden mathematical gems? This is the stuff of new proof theory, which also goes under names such as Realizability, Type theory, and Proof mining.

Imagine what will happen with mathematics if logic gets boosted by the machinery of algebra and homotopy theory, if the full potential of "proofs as computations" is used in practice on modern computers, if completely new and fresh ways of looking at the nature of proof are explored by the brightest mathematicians who have vast experience outside the field of logic? This will necessarily represent a major shift in how mathematics is done and what it can accomplish.

Because mathematicians have not reached the level of reflection which would allow them to accept proof relevant mathematics they seek security in the mathematically and socially inadequate dogma that a proof can only be a finite syntactic entity. This makes us feeble and weak and unable to argue intelligently with a well-versed sociologist who can wield the weapons of social theories, anthropology and experimental psychology. So the best answer to the question "is rigor just a ritual" is to study rigor as a mathematical concept, to quantify it, to abstract it, and to turn it into something new, flexible and beautiful. Then we will laugh at our old fears, wonder how we ever could have thought that rigor is absolute, and we will become the teachers of our critics.

Answer by Andrej Bauer for Definition of subobject classifier in presheaves

2013-05-06T14:31:41Z

Isn't $f^{*}(e)$ just the action of the functor $E$ on morphisms, i.e., it could be written instead as $E(f)(e)$? Perhaps Steve can confirm in person.

Answer by Andrej Bauer for Useful tricks in experimental mathematics

2013-05-05T19:38:25Z

My favorite trick in experimental mathematics is to prove things.

Answer by Andrej Bauer for Can Inequivalent Topologies Have Same Sheaves/Cohomology?

2013-04-24T06:58:13Z

Does this hold water?

If the sheaves are the same, they have the same subobject classifier, which is the sheaf of closed sieves, so both topologies have the same notion of closed sieves, so the same notion of covers, hence they are equivalent.

Answer by Andrej Bauer for A Model where Dedekind Reals and Cauchy Reals are Different

2013-04-24T06:48:23Z

With classical logic or countable choice Cauchy and Dedekind reals coincide. Therefore we must look at a model of intuitionistic mathematics without countable choice, such as a topos of sheaves over a space.

For example, let us consider the topos $\mathsf{Sh}(\mathbb{R})$ of sheaves over $\mathbb{R}$ (equipped with the standard topology). The Dedekind reals are the sheaf of continuous real-valued maps, i.e., $$\mathbb{R}_D(U) = \lbrace f : U \to \mathbb{R} \mid f \text{ continuous}\rbrace.$$ The Cauchy reals are the sheaf of locally constant real-valued maps, if I remember correctly.

These two sheaves are not isomorphic. One way to see this: in $\mathbb{R}_C$ the restriction map $\mathbb{R}_C(-1,1) \to \mathbb{R}_C(0,1)$ is a bijection, because every locally constant continuous map $(0,1) \to \mathbb{R}$ is in fact constant, and so is restriction of a constant map $(-1,1) \to \mathbb{R}$. But in $\mathbb{R}_D$ this is not the case, because $x \mapsto 1/x$ is a continuous map $(0,1) \to \mathbb{R}$ which is not the restriction of a continuous map $(-1,1) \to \mathbb{R}$.

Answer by Andrej Bauer for Connection between codata and greatest fixed points

2013-04-22T01:01:17Z

You've got the levels mixed up a bit because you are thinking too set-theoretically. While it is likely that you can get the carrier sets of inductive and coinductive datatypes as least and greatest fixed points, respectively, you will still wonder where to get constructors, destructors, recursion and corecursion.

An inductive type corresponds to an initial algebra for a functor $F : \mathsf{Set} \to \mathsf{Set}$. For example, the natural numbers are the initial algebra for the functor $F(X) = 1 + X$ where $1$ is the singleton set and $+$ is disjoint sum. Similarly, the set of binary trees is the initial algebra for the functor $F(X) = 1 + X^2$. An initial algebra consists of a set $I$ and a structure map $i : F(I) \to I$. The structure map gives us the constructors for the datatype, and the initiality of $I$ gives a recursion principle. Let's look at this for binary trees:

the initial algebra for $F(X) = 1 + X^2$ is the set $T$ of finite binary trees. Its structure map $t : 1 + T^2 \to T$ can be decomposed into two parts. The first part $\mathsf{nil} : 1 \to T$ is the empty tree, and the second part $\mathsf{cons} : T^2 \to T$ is the constructor which takes two trees and puts them together into a new tree.
the initiality of $T$ says that, given any set $A$ and a map $a : 1 + A^2 \to A$ there is a unique algebra homomorphism $h : (T,t) \to (A,a)$. We decompose $a$ into an element $x_0 \in A$ and a map $g : A^2 \to A$. Then the initiality says that there is a unique map $h : T \to A$ such that $$h(\mathsf{nil}) = x_0$$ and $$h(\mathsf{cons}(u, v)) = g(h(u), h(v)).$$ This is just definition of $h$ by recursion on the structure of the tree.

Now let us look at final coalgebras, which ought to correspond to coinductive types (codata). For example, the final coalgebra for $F(X) = 1 + X$ is the set $\mathbb{N} \cup \lbrace \infty \rbrace$, the final coalgebra for $F(X) = 1 + X^2$ contains finite and infinite binary trees, while the final coalgebra for $F(X) = 2 \times X$ is the set of infinite binary streams. Again, the structure map of such a final coalgebra gives us the destructors for codata, while finality gives a way of constructing maps into the codata.

For example, consider the final coalgebra $S$ for $F(X) = 2 \times X$. The structure map $s : S \to 2 \times S$ decomposes into two maps $\mathsf{hd} : S \to 2$ and $\mathsf{tl} : S \to S$ which I am suggestively calling "head" and "tail". Finality of $S$ means that, given any set $A$ and a map $a : A \to 2 \times A$, there is a unique coalgebra homomorphism $\phi : (A,a) \to (S,s)$. If we decompose $a$ into $h : A \to 2$ and $t : A \to A$, then $\phi$ is the unique map satisying $$\mathsf{hd}(\phi(x)) = h(x)$$ and $$\mathsf{tl}(\phi(x)) = \phi(t(x)).$$ I hope I got that right.

So it is indeed the case that inductive datatypes are "least fixed points" and the coinductive datatypes are the "greatest fixed points", but in the categories of algebras and coalgebras, respectively.

Answer by Andrej Bauer for Is there any nontrivial monad on the category of graphs?

2013-04-18T12:34:45Z

There are billions and billions of them. But it turns out I originally suggested two non-examples:

The non-monad which takes a graph and turns it into the complete graph on the same vertices.
The comonad which takes a graph and turns it into the discrete graph on the same vertices. (This example was edited after Andreas Blass made his comment.)

And two that still seem to be examples:

The monad which takes a graph and creates a new one with the same vertices, but connects two vertices iff there is a path between them in the original graph.
The monad arising from $\pi_0$: it takes a graph and returns the discrete graph whose vertices are the connected components of the original graph.

Answer by Andrej Bauer for Intermediate value theorem on computable reals

2009-12-21T23:40:04Z

I am afraid Joel has missed an important detail there, which is worth pointing out. Suppose $f$ is continuous and computable on $[a,b]$ and $f(a) \cdot f(b) < 0$. We must be careful to distinguish between

there exists a computable $x$ in $[a,b]$ such that $f(x) = 0$, and
there is an algorithm which accepts as input $f$, $a$, and $b$ and outputs $x$ in $[a,b]$ such that $f(x) = 0$.

In the first case we have a classical existence of a computable entity $x$, while in case (b) we have a computable existence of a computable entity.

I am pretty sure Weihrauch only proves 1., and it is impossible to prove 2., even if we further assume that $f$ is not only computable but computably continuous, or even Lipshitz with a known computable constant. The basic reason why 2. does not hold is that the $x$ cannot be chosen continuously with respect to the input data: essentially, a very small perturbation of $f$ can cause $x$ to jump around. Because all computable maps are continuos, we cannot have an algorithm computing $x$ (this is not a proof, just the idea, you have to work a bit harder to get all the details right).

However, you can impose fairly mild conditions on $f$ that are typically satisfied in practice. For example, if $f$ is locally non-constant, by which I mean that for every $y$ in $[a,b]$ we can compute nearby points $z$ and $w$ such that $f(z) \neq f(w)$, then IVT holds computably in the sense of 2. To see this, just perform bisection, but always avoid hitting a zero by going to a nearby non-zero point (because either $f(z)$ or $f(w)$ is non-zero, and we can compute which one). This condition is satisfied by non-trivial polynomials, for example, as well as for any differentiable function wose derivative only has isolated zeroes.

Let me also say a bit about the use of completeness of reals in IVT. Neel's remark translats from constructive mathematics to computability as follows: we can compute arbitrarily good approximations to the IVT. The trouble is that the approximations need not converge to anything, at least not computably. Classically they have an accumulation point, but we can't compute any information from it.

A second point is that IVT holds not because $\mathbb{R}$ is complete, but because it is connected. A very thorough analysis of this was made by Paul Taylor in his paper "A lambda-calculus for real analysis", see http://www.paultaylor.eu/ASD/lamcra/ . It's not easy reading, but it is very educational.

Answer by Andrej Bauer for What can be expressed in and proved with the internal logic of a topos?

2013-04-04T08:47:43Z

In general the internal language of a topos can only express those statements that make sense in every topos. In essence, this limits you to something like bounded Zermelo set theory, without global membership.

The right way to use the internal language of a particular topos, such as your topos of directed graphs, is to enrich the general internal language of toposes with new primitive types and new axioms. If you are lucky you may be able to add just axiom and define the new types (i.e., the new types can be characterized in the internal language). Let us see what these may be in the case of the topos of directed graphs.

Because we are dealing with a presheaf topos we can tell in advance that the (covariant) Yoneda embedding $y : \mathcal{G} \to \mathbf{Set}^\mathcal{G}$ will give us something important. Indeed, $y(V)$ is the graph with one vertex and no arrows, while $y(A)$ is the graph with two vertices and one arrow in between. Let me write $V$ and $A$ instead of $y(V)$ and $y(A)$, respectively. We might call $V$ "the vertex" and $A$ "the arrow". We call the objects of our topos "graphs", obviously.

Simple calculations reveal that, for a given graph $G$:

$G \times V$ is the associated discrete graph on the vertices of $G$.
$G^V$ is the associated complete graph on the vertices of $G$.
$G \times A$ is the following graph: for each vertex $g$ in $G$ we get two vertices $(g,s)$ and $(g,y)$ in $G \times A$ (think of them as "$g$ as a source" and "$g$ as a target"), and for each arrow $a : g \to g'$ in $G$ we get an arrow $a : (g,s) \to (g',t)$ in $G \times A$. This probably means something to graph theorists, I would not be surprised if they have a name for it.
$G^A$ is the associated "graph of arrows": the vertices of $G^A$ are pairs of vertices $(g,g')$ of $G$; and for each arrow $a : g \to h$ we get an arrow $a : (g,g') \to (h',h)$ in $G^A$. This makes more sense once you compute the global points of $G^A$: they correspond precisely to the arrows in $G$. Also, it is helpful to think of the vertices of $G^A$ as "potential arrows of $G$".

We can already answer some of your questions:

A graph $G$ is discrete when the projection $G \times V \to G$ is onto.
A graph $G$ is complete when the canonical map $G \to G^V$ is onto.

You would like to have the graph of paths $\mathsf{Path}(G)$ of a given graph $G$. I think you've described the wrong gadget, i.e., what you should be looking for is a graph whose global points are the paths in $G$, but there will be many other "potential" things floating around. We have so far not used the fact that there are two morphisms $s, t : A \to V$. These allow us to form "generic paths of length $n$" $P_n$ as pullbacks: $P_1 = A$, $P_2 = A \times_V A$ is the pullback of $s : A \to V$ and $t : A \to V$, and so on. With a little bit of care we should be able to form the object of "generic paths" $P$, equipped with a concatenation operation that turns it into a monoid. I am going to naively guess that the vertices of $P$ are pairs of natural numbers $(k,n)$ with $k < n$ and that arrows are of the form $(k,n) \to (k+1,n)$. But this needs to be checked, and in any case it should be possible to define the "correct" $P$ internally. The graph $\mathsf{Path}(G)$ that you are looking for ought to be the dependent sum $\sum_{p : P} G^p$ (and this looks a lot like a polynomial functor). The monoid structure on $P$ should give you a monad.

Regarding cyclic paths (you call them loops): if I am not mistaken the internally projective graphs are those graphs whose in- and out-degrees are all 1, in other words the cycles and the infinite path stretching in both directions. This should help with getting a grip on cyclic paths. That a graph $G$ is internally projective can be expressed in the internal language as "every $G$-indexed family of inhabited graphs has a choice function", i.e., these are the objects that satisfy the axiom of choice, internally.

The vertex $V$ is a subobject of the terminal object $1$, which is the graph with a single vertex and a single arrow. Thus, there is a corresponding truth value $v \in \Omega$, which is a kind of "intermediate" truth value. We can define a closure operator $j : \Omega \to \Omega$ (a modality) by $j(p) = (v \Rightarrow p)$. This modallity should be called "vertex-wise". Indeed, if $H \hookrightarrow G$ is a subgraph of $G$ then its $j$-closure $\bar{H} \hookrightarrow G$ is the subgraph of $G$ induced by the vertices of $H$. Ah, but this is then the same as the compleement of the complement of $H$, so we see that $j$ is just the double negation closure. (I hope I am doing this right, I am speaking off the top of my head.) If I am correct, then we can define $V$ in the internal language, using an axiom:

Axiom: there is a truth value $v \in \Omega$ such that $(v \Rightarrow p) = \lnot\lnot p$ for all $p \in \Omega$.

Then $V = \lbrace * \in 1 \mid v \rbrace$. We still have to do something about $A$, though.

In any case, my experience with internal languages is that they are well worth using. It takes a bit of effort, thoough, to figure out the optimal way of setting up the internal language of a particular topos. The general idea is to introduce as few new types as possible, characterize them with suitably chosen axioms, and figure out what other useful axioms are valid in your topos.

Answer by Andrej Bauer for Question on Godel completeness theorem

2013-03-27T01:40:04Z

I do not know from what angle you're coming, but "really exist" might mean "exists constructively". In this case you should look at Stefano Berardi, Silvio Valentini: Krivine's intuitionistic proof of classical completeness (for countable languages) Ann. Pure Appl. Logic 129(1-3): 93-106 (2004). Even though existence of the usual Tarski models for consistent theories cannot be proved construtively, one can still prove a slightly weaker version of completeness.

Answer by Andrej Bauer for Connections between topos theory and topology

2013-03-22T00:38:52Z

Here is one that is not too grand.

Suppose you want to embed some (essentially small) category of spaces into a cartesian-closed category, so as to extend it to a convenient category. Then you can use a gros topos to do it. The site is your category of spaces, a family $\lbrace e_i : X_i \to Y\rbrace_i$ is covering when the $e_i$ are open embeddings and they cover $Y$ (I hope I got that right). The Yoneda lemma embeds the original category.

It is not hard to come up with interesting exercises that are not too demanding.

Answer by Andrej Bauer for Was the early calculus inconsistent?

2013-03-20T13:27:58Z

I do not know whether the early calculus was consistent, but it surely can be made as consistent as modern mathematics, with practically no modifications of the basic setup. This goes under the name Synthetic differential geometry (SDG). Like Robinson's nonstandard analysis it is a calculus with infinitesimals. SDG should be closer to the 17th century ways of doing things because it works with nilpotent infinitesimals whereas nonstandard analysis does not. I believe the 17th century calculus used nilpotent infinitesimals. Can someone confirm this?

[Edit: many thanks to Lee Mosher for transcribing a piece of Berkeley's text. Here is the same piece of text, as it would be written in SDG in the 21st century.]

We would like to compute the derivative of $f(x) = x^n$ where $n$ is a positive integer. Let $x \in R$ and let $o$ be any nilpotent infinitesimal of degree 2. Then by the Binomial theorem $$(x + o)^n = x^n + n o x^{n-1} + \frac{n^2 - n}{2} o^2 x^{n-2} + \text{etc}.$$ Because $o$ is nilpotent of degree 2, we have $o^2 = 0$ and so all terms but the first two equal zero. Thus we get $$(x + o)^n = x^n + n o x^{n-1}$$ hence $$(x + o)^n - x^n = n o x^{n-1}$$ or $$f(x + o) - f(x) = n x^{n-1} o$$ Because $o$ here is an arbitrary infinitesimal (i.e., the equation holds for all $o$ whose square iz zero), we may use the Axiom of Microaffinity to conclude that $$f'(x) o = n x^{n-1} o$$ Now we use the Cancelation Principle to cancel $o$ on both sides, which yields $f'(x) = n x^{n-1}$.

I must say Berkeley's writting was a great deal more picturesque. The Axiom of Microaffinity and the Cancelation Principle are an axiom and a theorem of SDG, respectively. They circumvent the problem that Berkeley was complaining about, namely that first we pretend that $o$ is not zero (so that we can cancel it on both sides of equation), but then we pretend it is zero so that all those higher terms disappear. Instead, we can do the following: assume that $o^2 = 0$ (which does not imply that $o = 0$ because we are not assuming classical logic) so that the higher terms disappear, but then use a sort of weak cancelation property of infinitesimals which allows us to cancel them under certain conditions, even though they are not invertible.

Axiom of Microaffinity: For every $f : R \to R$ and $x \in R$ there exists a unique number $f'(x)$, called the derivative of $f$ at $x$, such that for all infinitesimals $o$ we have $f(x + o) - f(x) = f'(x) o$.

Cancelation principle: Let $a, b \in R$. If $a \cdot o = b \cdot o$ for all $o \in \Delta$ then $a = b$.

Is this weird? Yes, it sure is if you are classically trained. It gets weirder: if we let $\Delta = \lbrace o \in R \mid o^2 = 0 \rbrace$ be the set of square-nilpotent infinitesimals then

Potentially there exist non-zero infinitesimals: $\lnot \forall o \in \Delta, o = 0$.
There are no infinitesimals which are distinct from zero: $\lnot \exists o \in \Delta, o \neq 0$.

But it is precisely what we need to explain all the confusion about infinitesimals. Remember it this way: potentially there are some non-zero ones (we cannot exclude their existence) but they are all potentially zero (they are so small we cannot distinguish them from zero). Just don't ask yourself whether an infinitesimal is zero and all will be fine.

Here $R$ is the "smooth real line", which is an ordered field. Of course, it does not satisfy the Archimedean axiom, as that would force all infinitesimals to be zero. So it is a different kind of animal than the usual $\mathbb{R}$.

John Bell explained all this in his excellent booklet on Syntehtic Differential Analysis.

Answer by Andrej Bauer for Existence of a Sub-Category of the Category of Topological Spaces

2013-03-17T20:59:31Z

Spaces of the sort you are looking for are called universal.

Definition: A space $X$ is universal for a class of spaces $\mathcal{C}$ if it belongs to $\mathcal{C}$ and every space in $\mathcal{C}$ embeds into $X$.

Here are some examples:

Let $\Sigma = \lbrace{\bot, \top\rbrace}$ be the Sierpinski space, whose open subsests are $\emptyset$, $\lbrace\top\rbrace$ and $\Sigma$. The countable product $\Sigma^\omega$, of course equipped with the product topology, is a universal countably-based $T_0$-space. That is, every such space embeds in $\Sigma^\omega$. More generally, for any cardinal $\kappa$ the $\kappa$-fold product $\Sigma^\kappa$ is universal for $\kappa$-weighted $T_0$-spaces.
We can get rid of the $T_0$ condition by using instead of $\Sigma$ the space with three points, one of which is open, see "Universal Topological Spaces" by K. D. Magill, Jr. The American Mathematical Monthly , Vol. 95, No. 10 (Dec., 1988), pp. 942-946.
Urysohn universal space is universal for all separable metric spaces (even if we require an isometric embedding). This is by no means the only such space. A much simpler universal separable metric space is the space $C([0,1])$ of continuous real-valued maps, equipped with the compact-open topology.
A $0$-dimensional compact countably-based Hausdorff space embeds into Cantor space $2^\omega$, so that makes Cantor space universal for countably based Stone spaces. Again, we can go to higher weights by considering large products $2^\kappa$.
In domain theory there are universal domains (domains are certain kinds of posets with topologies and are important in theoretical computer science), and this has been studied quite systematically. In fact, there are general techchniques for constructing universal objects, see e.g., Droste, M., Göbel, R.: Universal Domains and the Amalgamation Property. Mathematical Structures in Computer Science (1993) 137-159. (Behind a paywall!)
The Hilbert cube is universal for countably based Tychonoff spaces.

One can also ask for spaces which are universal in a different way, namely spaces which cover all spaces of some class (rather than embed them). There are examples of these too:

Every inhabited complete separable metric space is a quotient of the Baire space, which is the countable product $\mathbb{N}^\omega$ of the discrete space of natural number $\mathbb{N}$.
If I am not mistaken (someone will correct me), the embedding of a countably based Stone space into Cantor space actually has a left inverse. So, every inhabited countably based Stone space is a quotient of Cantor space.

There are many other examples.

Answer by Andrej Bauer for New research on coding in reverse mathematics?

2013-03-11T15:35:08Z

I can offer a computational perspective. In computable mathematics we are interested in "computing with mathematical objects" such as integers, finite sets, real numbers, infinite-dimensional Banach spaces, compact subsets of $\mathbb{R}^n$, and many other "infinite" things. Some of these are pretty complicated, so the question arises how to represent them as a data structures, in other words, we face a coding problem, just like in Reverse Mathematics.

In computability theory we normally code everything with natural numbers. Another possibility is to code things with "reals", by which computability theorists mean infinite binary sequences. In actual implementations we code by elements of datatypes available to us in a programming language. But we always face the same question, namely what does it mean to correctly encode a given mathematical object.

To properly answer such a question we have to take a very important step: we must turn encodings themselves into honest mathematical objects and collect them all (even the allegedly sensless ones) into a manageable mathematical structure, say a category. We should be able to use the structure of the resulting category to bring some order and sense to the black art of "choosing appropriate codings".

When this is done in computable mathematics, the result is a realizability topos. This is great, as we can interpret higher-order (intuitionistic) logic in it, and that suffices to develop mathematics. To see how this works, consider an easy example, the natural numbers. Nobody ever questions encodings of natural numbers, but nevertheless it is possible to come up with some bad ones. Encodings are objects of a realizability topos. Thus, a candidate encoding for natural numbers lives inside the topos as an object $N$. If in the topos the object $N$ satisfies Peano axioms, then it correctly encodes natural numbers, otherwise it does not.

Our correctness criterion then is this: an encoding is correct when, seen as an object of the realizability topos, it corresponds to the expected mathematical object. Other examples are easy to come by:

An encoding of real numbers is correct if the corresponding object in the topos is a Cauchy-complete archimedean ordered field.
An encoding of c.e. sets is correct if in the corresponding object in the topos is the object of countable subsets of $\mathbb{N}$.
An encoding of functions $X \to Y$ is correct if in the topos it is the exponential object of $X$ and $Y$.
An encoding of a group is correct if in the topos it corresponds to a group.
etc.

As toposes and intuitionistic mathematics make snaicititamehtam queasy, and reverse mathematics happens in the context of classical logic anyway, realizaiblity toposes are not going to be the right answer for Reverse Mathematics. Nevertheless, we have a plan: what category, or (non-standard) model of (weak) set-theory captures the idea of coding in Recursive Mathematics? If you can find it, and it has good enough properties, it should give some answers. This sounds like somebody's PhD.

Where in ordinary math do we need unbounded separation and replacement?

2013-02-10T17:06:24Z

[I have updated the question after initial comments in the hope of clarifying it.]

I do quite a bit of reasoning, typically about topology and metric spaces, in "non-standard" foundations, such as inside of a particular topos, in type theory, or a predicative constructive setting. These typically do not have anything corresponding to unbounded separation or replacement (the constructive set theory CZF does have collection, though).

I have a pretty good feel when restricted forms of excluded middle and choice are needed, and what things powersets give us over predicative math, etc. But I never ever wish I had unbounded separation and replacement. Why is that? Is it just because of the kind of math I do, or are these two really not needed very much in ordinary math?

To make the question more specific: what are some well-known definitions and theorems in "ordinary" mathematics which require unbounded separation or replacement?

The obvious uses of replacement and unbounded separation come from set theory, so we should avoid listing those. Ideally, I am looking for theorems and definitions in algebra, topology, and analysis.

Here is a non example from order theory, which was suggested in the comments. Under the usual encoding of ordinals as hereditarily transitive transitive sets, the rank of the function $n \mapsto \omega + n$ is $\omega + \omega$ and so we need replacement to show its existence. However, even PA can speak about this sort of small countable ordinals, so we are seeing here an artifact of a particular encoding. A different encoding of countable ordinals would make this function easy to define (for example we could view the countable ordinals as orders of subsets of $\mathbb{N}$).

The only example of unbounded separation I can think of right now comes from category theory. In a large category $C$ the definition of epi is unbounded, as it requires quantification over all objects of $C$. I am looking for something that is not so directly linked to a question of size.

Answer by Andrej Bauer for Is there a constructive proof of Cantor–Bernstein–Schroeder theorem ?

2013-03-03T21:19:24Z

The Cantor-Bernstein-Schröder theorem (did I read somewhere that Dedekind was the first to prove it?) is not valid constructively. Here are a couple of reasons why.

There are models in which the theorem fails

Here is a pretty one. In the realizability topos over the infinite-time Turing machines there is an injection $\mathbb{R} \to \mathbb{N}$. Because the topos satisfies countable choice there is no surjection $\mathbb{N} \to \mathbb{R}$ (hence no bijection), but there clearly is an injection $\mathbb{N} \to \mathbb{R}$.

Todd mentioned a presheaf model in his answer.

The usual proofs are non-constructive

You asked what is non-constructive about König's proof. It uses excluded middle several times:

"the sequence can be extended on the left, depending on whether $a$ is in the image of $g$ or not",
"the sequence constructed in the proofs either terminates or not",
"the sequences so constructed partition the disjoint union of the two sets".

For a proof which uses excluded middle in a more controled way, see the one using Tarski's fixed point theorem, as outlined here. Excluded middle is used "only" in the last step, when the bijection $i$ is defined, depending on whether an element is in $C$ or not.

The theorem implies strange things, constructively speaking

Here is a strange consequence of the theorem, I will try to improve on it but do not have the time right now. Consider the Cantor space $C = 2^\mathbb{N}$ and the subspace of those sequences which contain a 1, $D = \lbrace \alpha \in C \mid \exists n . \alpha n = 1\rbrace$. As there are injections $C \to D$ and $D \to C$ there is a bijection $h : C \to D$. That is very strange, for it is consistent to assume that all maps on $C$ are uniformly continuous, but such a bijection cannot be uniformly continuous. I will try to improve on this.

Answer by Andrej Bauer for Why is there a formula for symbolic differentiation (chain and product rules) but not for symbolic integration?

2013-02-28T16:03:33Z

I think this question is not research-level, but nevertheless, since the answer is not generally known in the mathematical community, here it is.

You are mistaken. There is a "formula" for integration. It goes under the name "Risch algorithm". That is, there is a completely mechanical procedure which computes the closed form of an indefinite integral of a function which is a composition of elementary functions, if there is one and fails otherwise. However, the procedure is quite a bit more complicated, and is thus not generally taught in schools. In fact, it is so complicated that complete implementations are hard to come by. Caveat: there are parts of Risch's algorithm which are not known to be entirely algorithmic (see Wikipedia for a discussion of this point).

The general theory and problem of which the Risch algorithm is the solution was developed already by Liouville.

There is also a more simplistic answer. Many rules of differentiation can be inverted to give corresponding rules of integration, for example:

The product rule becomes integration by parts.
The chain rule becomes the substitution rule.
Integral of $x^n$ is deduced from the derivative of $x^{n+1}$.
Integral of $\sin x$ is deduced from the derivative of $\cos x$, etc.

The trouble is, while the rules of differentiation provide a complete set of rules for getting rid of all the derivatives in a systematic fashion, the corresponding rules for integration do not. So many think that integration is an art. It isn't, it's an algorithm invented by Risch.

Answer by Andrej Bauer for Axiom of Choice and Continuous function

2013-02-17T23:28:45Z

Let us improve slightly on Joel's answer by avoiding not only choice but also excluded middle (which is used in assuming that the minima $n_x$ exist). In passing we also generalize to an arbitrary metric codomain. Since the various notions of compactness are not equivalent intuitionistically, we have to specify which one we mean. We mean by "compact" the Heine-Borel finite subcover property.

Theorem: If a map $f : X \to Y$ from a compact metric space to a metric space is continuous then it is uniformly continuous.

Proof. (No excluded middle, no choice.) Let $\epsilon > 0$ be given. Consider the family of open balls $$\mathcal{F} = \lbrace B(x,r) \mid x \in X, r > 0, \forall x', x'' \in B(x,2r) . d(f(x'), f(x'')) < \epsilon \rbrace.$$ Beware, we put $B(x,r)$ in $\mathcal{F}$ if the larger ball $B(x,2 r)$ is mapped by $f$ to a sufficiently small set.

Because $f$ is continuous, $\mathcal{F}$ covers $X$. By the Heine-Borel property it has a finite subcover $$B(x_1, r_1), \ldots, B(x_n, r_n).$$ Let $\delta = \min (r_1, \ldots, r_n)$. Suppose $d(y,z) < \delta$ for some $y, z \in X$. There is $i$ such that $d(x_i, y) < r_i$, hence $d(x_i, z) \leq d(x_i, y) + d(y, z) < r_i + \delta \leq 2 r_i$. Thus, since both $y$ and $z$ are contained in $B(x_i, 2 r_i)$ we conclude $d(f(y), f(z)) < \epsilon$. QED.

As usual, the constructive proof is also the most elegant one. The above proof is an easy adaptation that avoids unecessary use of choice of 4.3.31 and 4.3.32 of Engelking's famous General Topology. Further reading: Hajime Ishihara and Peter Schuster, Compactness under constructive scrutiny. Math. Log. Quart. 50, No. 6, 540 – 550 (2004).

Answer by Andrej Bauer for Understanding Troelstra's Uniformity Principle in Constructive Mathematics

2013-02-16T08:12:48Z

You have stated Troelstra's Uniformithy Principle correctly (contrary to François's claim). There are two reasons why your counterexample does not work. First, we cannot show that every $X \subseteq \mathbb{N}$ is empty or not. Second, we cannot show that every inhabited subset of $\mathbb{N}$ has a minimal element. And we do not need any story about constructivism here. As soon as we assume the Uniformity Principle, it follows that:

Not every $X \subseteq \mathbb{N}$ is empty or not, because that would allows us to form the non-uniform total relation $(X = \emptyset \implies n = 1) \land (X \neq \emptyset \implies n = 42)$.
Not every inhabited subset $X \subseteq \mathbb{N}$ has a minimal element, because that would allow us to form the non-uniform total relation $\min (X \cup \lbrace 42 \rbrace) = n$.

[I added this paragraph later.] Even without the uniformity principle we cannot expect the two statements to be constructively valid because they imply (a restricted form of) excludded middle:

If every set is empty or not, given any truth value $p \in \Omega$, consider the set $\lbrace \star \mid p \rbrace$: it is either empty or not, therefore either $\lnot p$ or $\lnot\lnot p$, which is a restricted form of excluded middle. [EDIT: thanks to Andreas Blass for pointing out an error here.]
If every inhabited set of natural numbers has a minimum, given any truth value $p \in \Omega$, the minimum of the set $\lbrace n \in \mathbb{N} \mid n > 1 \lor p\rbrace$ is either $0$ or not, therfore either $p$ or $\lnot p$, which is excluded middle.

There is no hope to make the Uniformity Principle classically valid, even if we try to restrict to a subfamily of sets:

Theorem: Suppose excluded middle holds and $S \subseteq \mathcal{P}(\mathbb{N})$ is an inhabited family which satisfies the uniformity principle $(\forall X \in S \exists n \in \mathbb{N} . R(X,n)) \implies \exists n \in \mathbb{N} \forall X \in S . R(X, n)$. Then $S$ contains exactly one set.

Proof. Easy exercise. But let's do it anyway. There is an inhabitant $X_0 \in S$. Define the map $f : S \to \mathbb{N}$ by (use of excluded middle coming up...) $$f(X) = \begin{cases} 42 & \text{if $X = X_0$} \\ 23 & \text{if $X \neq X_0$} \end{cases}$$ Let $R(X,n)$ be the relation $f(X) = n$. Since $n = 42$ is the only $n$ related to $X_0$, by Uniformity Principle for $S$ we have $\forall X \in S . f(X) = 42$, therefore $\forall X \in S . X = X_0$. QED.

That is, Troelstra's Uniformity Principle is a very non-classical axiom. I disagree that it is a continuity principle. It does not allow one to prove any of the usual continuity statements "all maps are continuous".

Answer by Andrej Bauer for Mathematicians whose works were criticized by contemporaries but became widely accepted later

2013-02-12T10:52:07Z

Brouwer's intuitionistic mathematics was heavily criticized by his contemporaries, most notably Hilbert. For almost a century it was casually ridiculed by mathematicians who had no clue whatsoever about it. However, in the late 20th and early 21st century the importance of intuitionistic logic was recognized by mathematicians who worked in areas close to computer science. By the late 21st century the tables were turned and most mathematicians were educated in the tradition of Martin-Löf type theory (a starting development for many mathematicians born in the 20th century, who dismissed Martin-Löf's work on the grounds of it being useful exclusively for philosophically commited constructivists) . In their ignorace they now considered ridicule of Zermelo and Fraenkel an appropriate activity. Will they ever learn?

Answer by Andrej Bauer for Is there a natural measurable structure on the $\sigma$-algebra of a measurable space?

2013-02-10T09:25:04Z

One way to approach this would be to ask the same question inside a suitable topos in which "everything is measurable" and such that each object is naturally equipped with the structure of a $\sigma$-algebra. In effect you would be expanding the notion of measure space to accommodate better structure, as such toposes typically contain the "classical" measure spaces.

For example, Matthew Jackson's Ph.D. dissertation "A sheaf theoretic approach to measure theory" might be a starting point.

Answer by Andrej Bauer for The egg and the chicken

2013-02-09T08:56:55Z

I would like to question two statements you make because they paint an oversimplified picture, which unfortunately is alluring to mathematicians who do not want to think about foundations (and they should not be blamed for it anymore than I should be blamed for not wanting to think about PDEs).

"Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets." This is what mathematicians say, but most cannot even tell you what ZFC is. Mathematicians work at a more intuitive and informal manner. High party officials once declared that ZFC was being used by everyone, so it has become the party line. But if you read a random text of mathematics, it will be equally easy to interpret it in other kinds of foundations, such as type theory, bounded Zermelo set theory, etc. They do not use the language of ZFC. The language of ZFC is completely unusable for the working mathematician, as it only has a single relation symbol $\in$. As soon as you allow in abbreviations, your exposition becomes expressible more naturally in other formal systems that actually handle abbreviations formally. Informal mathematics is informal, and thankfully, it does not require any foundation to function, just like people do not need an ideology to think. If you doubt that, you have to doubt all mathematics that happened before late 19th century.
"They [logicians] realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead." I do not know of any logicians, and I know many, who would say that logic is "God-given", or anything like that. I do not think logicians are born into a life rich with the "full power of set theory" which they throw away in order to become ascetic first-order logicians. That is a nice philosophical story detached from reality. The logicians I know are usually quite careful, skeptical, and inquisitive about foundational issues, reflect carefully on their own experiences, and almost never give you a straight answer when you ask "where does logic come from?" Your view is naive and inaccurate, if not slightly demeaning.

If I understand your question correctly, you are asking whether there is a difference between the following two views:

We start with naive set theory and on top of it we formalize set theory.
We start with first-order logic and immediately formalize set theory.

Well, we are proceeding from two different meta-theories. The first one allows us a wide spectrum of semantic methods. We can refer to "the standard model of Peano arithmetic" because we "believe in natural numbers", and we can invent Tarskian model theory without worrying where it came from.

The second method is more restricted. It will lead to syntactic and proof-theoretic methods, since the only thing we have given ourselves initially are syntactic in nature, namely first-order theories. There will be careful analysis of syntax. For advanced methods, however, we will typically resort to at least some amount of "naive mathematics". Ordinals will come into play, it will be hard to live without completeness theorems (which involve semantics), etc.

However, this is not how real life works. The dilemma you present is not really there. A working mathematician does not concern himself with these issues, anyhow, while a logician will likely refuse to be categorized as one or the other breed.

That is my guess, based on the experience that my fellow logicians are complicated animals and it is hard to get to the bottom of their foundational guts.

Algorithms for finding rational points on an elliptic curve?

2010-10-13T13:50:46Z

I am looking for algorithms on how to find rational points on an elliptic curve $$y^2 = x^3 + a x + b$$ where $a$ and $b$ are integers. Any sort of ideas on how to proceed are welcome. For example, how to find solutions in which the numerators and denominators are bounded, or how to find solutions with a randomized algorithm. Anything better than brute force is interesting.

Background: a student worked on the Mordell-Weil theorem and illustrated it on some simple examples of elliptic curves. She looked for rational points by brute force (I really mean brute, by enumerating all possibilities and trying them). As a continuation of the project she is now interested in smarter algorithms for finding rational points. A cursory search on Math Reviews did not find much.

Answer by Andrej Bauer for Ring with three binary operations

2013-02-05T17:25:09Z

For experimenting you could use alg, a program which computes all finite models of a given theory. The best thing may be to pass the ball back to your student and ask him to use alg to find some interesting structures.

For example, suppse we want a structure $(R, 0, +, -, \times, \&)$ such that $(R, 0, +, -)$ is a commutative group, $\times$ and $\&$ are associative, $\times$ and $\&$ distribute over $+$ and $\&$ distributes over $\times$ (I am making stuff up, the point is to experiment until something interesting is found). In alg the input file would be:

Constant 0.
Unary ~.
Binary + * &.

# 0, + is a commutative group

Axiom plus_commutative: x + y = y + x.
Axiom plus_associative: (x + y) + z = x + (y + z).
Axiom zero_neutral_left: 0 + x = x.
Axiom zero_neutral_right: x + 0 = x.
Axiom negative_inverse: x + ~ x = 0.
Axiom negative_inverse: ~ x + x = 0.
Axiom zero_inverse: ~ 0 = 0.
Axiom inverse_involution: ~ (~ x) = x.

# * and & are associative

Axiom mult_associative: (x * y) * z = x * (y * z).
Axiom and_associative: (x & y) & z = x & (y & z).

# Distributivity laws

Axiom mult_distr_right: (x + y) * z = x * z + y * z.
Axiom mult_distr_left: x * (y + z) = x * y + x * z.

Axiom and_distr_right: (x + y) & z = (x & z) + (y & z).
Axiom and_distr_left: x & (y + z) = (x & y) + (x & z).

Axiom mult_and_distr_right: (x * y) & z = (x & z) * (y & z).
Axiom mult_and_distr_left: x & (y * z) = (x & y) * (x & z).

Let us count how many of these are, up to isomorphism, of given sizes:

$ ./alg.native --size 1-7 --count three.th

size | count
-----|------
   1 | 1
   2 | 4
   3 | 3
   4 | 36
   5 | 3
   6 | 12
   7 | 3

Check the numbers [4, 3, 36, 3, 12, 3](http://oeis.org/search?q=4,3,36,3,12,3)
on-line at oeis.org

We can also look at these structures, but that's the sort of thing a student should do. Here is a random one of size 4 that alg prints out when we omit --count:

~ |  0  a  b  c
--+------------
  |  0  a  b  c


+ |  0  a  b  c
--+------------
0 |  0  a  b  c
a |  a  0  c  b
b |  b  c  0  a
c |  c  b  a  0


* |  0  a  b  c
--+------------
0 |  0  0  0  0
a |  0  a  0  a
b |  0  0  b  b
c |  0  a  b  c


& |  0  a  b  c
--+------------
0 |  0  0  0  0
a |  0  0  0  0
b |  0  a  b  c
c |  0  a  b  c

Up to size 7 I cannot actually see any interesting ones, there are always large blocks of 0's in $\&$. Other things should be tried out.

Answer by Andrej Bauer for Finding a vertex equidistant from two given vertices in a digraph

2013-02-05T10:52:14Z

Form the product graph $\Gamma \times \Gamma$ whose vertices are pairs $(u, u') \in \Gamma \times \Gamma$ and edges $(p, p') : (u, u') \to (v, v')$ are pairs of edges $p : u \to v$, $p' : u' \to v'$. Let $\Delta = \lbrace (u, u) \mid u \in V(\Gamma) \rbrace$ be the diagonal. Your question is equivalent to the question whether $\Delta$ can be reached from a given vertex $(x,y)$ in the graph $\Gamma \times \Gamma$ (and finding such a vertex, but most algorithms automatically give you one). This does not seem to be that hard to solve as it is just a reachability problem. If you want it in classical form, attach every vertex in $\Delta$ to a special vertex $\infty$ and ask for a path from $(x,y)$ to $\infty$. There are algorithms which preprocess the graphs so that subsequent reachability queries can be answered fast, in case you have to do this a lot (Wikipedia explains some of this).

Answer by Andrej Bauer for Is an ultrafinitist Hilbert's program doomed?

2013-01-30T11:23:12Z

Ulrich Kohlenbach with his coworkers in proof mining has perhaps the best modern nonfatalist position about Hilbert program. Rather than stressing over Gödel's demolition of Hilbert's ideal, we can analyze the extent to which "non-finitary" methods play a role. This has lead to some very nice results and applications of proof theory. Lecture 1 of Ulrich's notes on "Proof mining" provides a quick but more careful explanation of the idea that proof mining is the natural outcome of Hilbert's program.

Answer by Andrej Bauer for What logic is modelled by generalized boolean algebra?

2013-01-30T11:03:43Z

Propositional logic captures the partial order of a Boolean algebra, i.e., logical entailment $p_1, \ldots, p_n \vdash q$ corresponds to $p_1 \land \cdots \land p_n \leq q$. To obtain a logic for a generalised Boolean algebra we should express its laws in terms of partial order. If the laws are written as adjunctions, the rules of inference will be clearly visible.

A GBA has finite binary meets $\land$ and joins $\lor$, a least element $\bot$, and relative complements $\setminus$. There will be no surprises in the rules for $\land$, $\lor$ and $\bot$.

Conjunction is the easiest. Meet is characterised as $$r \leq p \land q \quad\text{iff}\quad \text{$r \leq p$ and $r \leq q$}.$$ Reading this from left to right gives us the elimination rules (where I write $\Gamma$ to indicate an arbitrary number of hypotheses $p_1, \ldots, p_n$) $$\frac{\Gamma \vdash p \land q}{\Gamma \vdash p} \quad\text{and}\quad \frac{\Gamma \vdash p \land q}{\Gamma \vdash q} $$ while the other direction gives the introduction rule $$\frac{\Gamma \vdash p \quad \Gamma \vdash q}{\Gamma \vdash p \land q}.$$ Notice how $\Gamma$ took the role of $r$.

A naive conversion of the characterisation of $\bot$, namely $$\bot \leq p,$$ would give us the rule $\bot \vdash p$. We actually want $\Gamma, \bot \vdash p$, but this is ok because $\bot$ is just as well characterised by $$r \land \bot \leq p.$$ This is a small point which becomes very important when we think about disjunctions. Again, a naive conversion of $$p \lor q \leq r \quad\text{iff}\quad \text{$p \leq r$ and $q \leq r$}$$ would give us something without $\Gamma$. What we really need is the characterisation $$s \land (p \lor q) \leq r \quad\text{iff}\quad \text{$s \land p \leq r$ and $s \land q \leq r$}.$$ But does this really characterize joins? Yes, thanks to the distributivity law! And so by writing $\Gamma$ instead of $s$ we get the laws $$\frac{\Gamma, p \lor q \vdash r}{\Gamma, p \vdash r} \quad\text{and}\quad \frac{\Gamma, p \lor q \vdash r}{\Gamma, q \vdash r}$$ and $$\frac{\Gamma, p \vdash r \quad \Gamma, q \vdash r}{\Gamma, p \lor q \vdash r}.$$ You may find these rules for $\lor$ a bit odd, but they are equivalent to whatever variant you are used to.

The laws for disjunction baked in just enough distributivity to make the distributivity law provable from the rules stated so far. So we need not worry about distributivity.

The interesting connective is the relative complement. If we secretly think of $p \setminus q$ as "$p$ and not $q$", then it would seem that the relative complement is to be characterised in terms of its lower bounds because it is like a conjunction. Indeed, we have $$r \leq p \setminus q \quad\text{iff}\quad \text{$r \leq p$ and $r \land q \leq \bot$}$$ which suggests the rules $$\frac{\Gamma \vdash p \quad \Gamma, q \vdash \bot}{\Gamma \vdash p \setminus q}$$ and $$\frac{\Gamma \vdash p \setminus q}{\Gamma \vdash p} \quad\text{and}\quad \frac{\Gamma \vdash p \setminus q}{\Gamma, q \vdash \bot}$$ These seem perfectly reasonable to me.

The point here is not what precise rules I derived, but how I derived them in a principled way:

logical entailment corresponds to the partial order
logical operations correspond to the operations
logical rules corespond to adjunctions that characterize the operations

By the way, there is of course no truth $\top$ in this calculus. If we add it, we get the usual classical propositional calculus, just like a GBA with a top element is a Boolean algebra.

Answer by Andrej Bauer for Category and the axiom of choice

2013-01-21T11:21:37Z

The following is equivalent to the axiom of choice:

A full and faithful functor which is essentially surjective on objects is an equivalence

Here by "equivalence" I mean "has an up-to-natural-isomorphism inverse".

But wondering which things are equivalent to the axiom of choice is such a set-theoretic thing to do. It is also interesting to ask whether category theory allows us for a more "algebraic" formulation of the axiom of choice. And indeed, in a topos we can express the axiom of choice in two ways:

Externally: Every epi splits.
Internally: Exponentiation by an object preserves epis.

Comment by Andrej Bauer

2013-05-20T17:50:18Z

A special case of Lavwere's fixed point theorem is a special case of Recursion theorem.

Comment by Andrej Bauer

2013-05-20T07:23:09Z

That's an answer for logicians, yes. Are we all logicians here? I can be.

Comment by Andrej Bauer

2013-05-19T12:42:58Z

And this would be Paul Taylor: paultaylor.eu The photo is a bit blurry, but that's how I percieve Paul most of the time anyway.

Comment by Andrej Bauer

2013-05-19T12:41:44Z

Overtness is exactly as complicated as compactness. nLab has a bit written about it: ncatlab.org/nlab/show/overt+space

Comment by Andrej Bauer

2013-05-19T07:07:17Z

This might not be the right decade to make this comment, but separability seems to be just the poor man's version of overtness, something Paul Taylor has been pointing out. If this is indeed the case, then separability would indeed be a suboptimal notion.

Comment by Andrej Bauer

2013-05-15T05:24:02Z

@Michal: It is a joke of course, but what you seem to worry about is how many jokes it is. Well, the thing to notice is that it is a sequence, not a series.

Comment by Andrej Bauer

2013-05-15T05:23:15Z

@Asaf: perhaps this may help. The universes are typically taken to be such that $\mathcal{U}_i$ is an element of $\mathcal{U}_{i+1}$. Cummulativity means that $\mathcal{U}_i$ is also a subtype (subset in your parlance) of $\mathcal{U}_{i+1}$. So we can obviously distinguish them because each contains something that another does not.

Comment by Andrej Bauer

2013-05-15T05:17:29Z

@Asaf: the notion of a universe in type theory is quite flexible. It's good if the universe is closed under many operations, perhaps so many that it forms a small model of type theory, but it doesn't have to. Actually, I am not sure what you're getting at. What does "distinguish between them" mean?

Comment by Andrej Bauer

2013-05-14T08:47:14Z

The nice embedding is guaranteed by universe cummulativity. By the way, the entire Coq standard library fits into three or four universes.

Comment by Andrej Bauer

2013-05-09T10:09:57Z

The modern version is: tell me who your Facebook friends are and I will tell you not only who you are, but also how you use your credit cards.

Comment by Andrej Bauer

2013-05-09T07:01:46Z

Let's be honest here: category theorists are their own friends, which is why the slogan works.

Comment by Andrej Bauer

2013-05-09T06:16:28Z

We are not machines. Not. Damn you Freud!

Comment by Andrej Bauer

2013-05-09T06:16:08Z

This answer hit the nail on its head. We are machines, we trust other people, and prefer to hear what ideas they have than why they think those ideas might be true.

Comment by Andrej Bauer

2013-05-06T15:12:15Z

Steve says the first edition has a rather unfortunate number of typos.

Comment by Andrej Bauer

2013-04-28T13:53:53Z

I think this proves I am very smart. Had I been doing things randomly, at least some of these would be actual examples. It takes a special talent to produce four plausibly-sounding non-examples.