Foundations

October 30, 2006

Posted by David Corfield

Something that has long troubled me is the question of why philosophers have shown what to my mind is an unwarranted interest in ‘foundational’ mathematical theories which make little or no contact with mainstream mathematics. Two posts have made me reconsider the problem. Alexandre Borovik discusses Zilber’s work on the Schanuel conjecture, while Kenny Easwaran wonders whether string theorists may use mathematics which depends on conjectured axioms of set theory.

In comments to both I mention the model theorist Angus MacIntyre’s interest in foundational theories which do make contact with the mainstream. He personally wants to relate some of Gropthendieck’s ideas to model theory. To return to the philosophers, is their interest in disconnected theories just a vestige of earlier failed foundationalist projects, or is there a continuing rationale?

For myself, I find Yuri Manin’s notion of foundations very attractive:

I will understand ‘foundations’ neither as the para-philosophical preoccupation with the nature, accessibility, and reliability of mathematical truth, nor as a set of normative prescriptions like those advocated by finitists or formalists. I will use this word in a loose sense as a general term for the historically variable conglomerate of rules and principles used to organize the already existing and always being created anew body of mathematical knowledge of the relevant epoch. At times, it becomes codified in the form of an authoritative mathematical text as exemplified by Euclid’s Elements. In another epoch, it is better expressed by the nervous self-questioning about the meaning of infinitesimals or the precise relationship between real numbers and points of the Euclidean line, or else, the nature of algorithms. In all cases, foundations in this wide sense is something which is relevant to a working mathematician, which refers to some basic principles of his/her trade, but which does not constitute the essence of his/her work. (Georg Cantor and His Heritage: 6)

This notion of foundations is closely related to what I’m driving at in this post about getting the ‘causal’ ordering of concepts right.

Posted at October 30, 2006 9:01 AM UTC

TrackBack URL for this Entry: http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1010

132 Comments & 2 Trackbacks

Re: Foundations

$MathML-enabled post (click for more details).$

Kenny Easwaran wonders whether string theorists may use mathematics which depends on conjectured axioms of set theory.

I doubt that there is anything in the relation of string theory (as currently understood) to set theory that is not already in the relation of quantum field theory to set theory.

From time to time I hear physicists chat about whether or not Gödel’s incompleteness theorem has any implication on physics. But I have never seen a convincing argument.

I could imagine that parts of physics depend on the axiom of choice. But I don’t know to which degree.

Posted by: urs on October 30, 2006 10:37 AM | Permalink | Reply to this

Re: Foundations

I could imagine that parts of physics depend on the axiom of choice.

You’d be surprised where AC shows up. One place in particular is algebraic geometry, where from what I can tell you basically can’t do without it. From what I hear, a certain chunk of the mathematics we’ve managed to fill in for string theory is essentially algebraic geometry, so that puts AC in play for string theory.

Posted by: John Armstrong on October 30, 2006 11:50 AM | Permalink | Reply to this

Re: Foundations

Kenny was imagining axioms beyond ZFC, and so beyond Choice. Choice has been given a thorough category theoretic going over. I wonder whether one could say something general here, that foundational concepts not easily expressible in category theoretic terms are unlikely to be useful. MacIntyre says something to this effect: “In much of modern mathematics, the set-theoretic component is of minor interest, and basic notions are geometric or category-theoretic.” (p. 197 of this).

Posted by: David Corfield on October 30, 2006 1:03 PM | Permalink | Reply to this

Re: Foundations

“In much of modern mathematics, the set-theoretic component is of minor interest, and basic notions are geometric or category-theoretic.”

This is very true, and part of why I reflexively shy away from Platonism/formalism debates, since they are based in the mathematics that was done a hundred years ago. I think most mathematicians realize this on some level and that leads to a general disinterest/distrust of the philosophy of mathematics since the philosophy hasn’t kept up with the mathematics.

Of course, then I ran into a book about structuralism and nothing has been the same since. Now I don’t see how anyone who takes Lawvere seriously can be anything but an ardent structuralist of some flavor or another.

—–

note to the administrators: why is it that many times I’ll hit preview and the site says that the comment is valid, but when I then hit ‘post’ it spits back, “Please preview your modified entry before posting it.” Usually this seems accompanies by changing ” into some control string or another, but not always.

Posted by: John Armstrong on October 30, 2006 1:18 PM | Permalink | Reply to this

Re: Foundations

…then I ran into a book about structuralism and nothing has been the same since

Which book was that? Many have been written with only a passing nod in the direction of category theory. If yours was one of these, did you think it got to the heart of the matter, or were you just glad that it didn’t seem to be a century out of date?

Regarding the ‘Preview’ request, as far as I encounter it, whenever I have made an alteration to the comment, including the first writing, it asks me to preview before posting. You seem to be getting this even without making alterations. Which browser are you using?

Posted by: David Corfield on October 30, 2006 1:27 PM | Permalink | Reply to this

Re: Foundations

The book was Shapiro’s Philosophy of Mathematics: Structure and Ontology. It didn’t really have that much directly on category theory, but the subject was raised a few times. Just providing that framework was enough for my own preconscious thoughts to click into place and fill in his category theory gaps.

—–

I’m using Safari 2.0.4 on OS 10.4.8

Posted by: John Armstrong on October 30, 2006 2:09 PM | Permalink | Reply to this

Re: Foundations

Is this just ‘catch-up’ philosophy, or did you see lines of research opening up in Shapiro’s theses? Around 1900 philosophical ideas did some work in the development of foundational languages. Philosophical ideas have also had their effect on category theory via Mac Lane and Lawvere. If we are to live up to Michael Friedman’s demand that philosophy be involved in prospective rationality, the development of new constitutive langauges, then we need to act like them.

Posted by: David Corfield on October 30, 2006 6:13 PM | Permalink | Reply to this

Re: Foundations

Honestly I must confess that I don’t know enough of the SotA to say whether it was catch-up or new. It was aimed at a popular audience, or at least more popular than it could have been. On that I’d guess it skews towards catch-up but I can’t say for sure.

Posted by: John Armstrong on October 30, 2006 11:08 PM | Permalink | Reply to this

Re: Foundations

It seems like a lot of this categorical stuff gets justified using Grothendieck universes which have something to do with “strongly inaccessible cardinals” about which I know nothing, but apparently their existence is outside of ZFC.

Posted by: Aaron Bergman on October 30, 2006 3:18 PM | Permalink | Reply to this

Re: Foundations

MacIntyre seems to be concerned with the ‘serious’ use of set theory in model theory, in the sense Urs used it for category theory:

There is still a difference between using a category here and there and taking things seriously.

So one might need to distinguish between a ‘here and there’ use and a ‘serious’ use of set theoretic principles. Perhaps one might invoke the continuum I have discussed elsewhere which runs from useless to useful to essential.

Posted by: David Corfield on October 30, 2006 5:57 PM | Permalink | Reply to this

Re: Foundations

$MathML-enabled post (click for more details).$

A Grothendieck universe $U$ is just a set of sets that contains the empty set and is closed under all the operations you ever use, as listed here.

So, working in $U$ is almost like like working in the class of all sets.

The advantage is that when you want to say “the set of all sets”, you can do it without Bertrand Russell’s ghost rapping you over the knuckles with a paradox. You just say “the set of all sets in $U$ ” - or in other words, “ $U$ ”.

This is handy, because in category theory there are lots of very important theorems about “the category of all categories” - the one problem being that in normal set theory, there is no category of all categories.

So, we say a category is small if its set of objects lies in $U$ and its set of morphisms lies in $U$ . Then we can talk about the “category of all small categories” - and this really exists. It’s just not small.

There are times when we need to play this trick more than once. For example, the category of all categories really comes with extra structure - it’s a 2-category! Let’s call this $Cat$ . There are lots of nice theorems about “the 2-category of all small 2-categories”, but alas, $Cat$ does not live in there: it’s not small.

To get around this, we just assume our Grothendieck universe $U$ is an element of some bigger Grothendieck universe, say $U'$ .

As you can see, we might need to keep doing this. So, we adopt the Axiom of Universes: every set is a member of some Grothendieck universe.

The key thing to keep in mind is that all this is just a trick to do perfectly reasonable mathematics without having to worry about Russell’s paradox. It’s not that we’re wild-eyed logicians desperately eager to construct ever-larger sets. It’s just that a good way way to state theorems about categories is to talk about $Cat$ , the 2-category of all categories. And, a good way to state theorems about things like $Cat$ (namely 2-categories) is to talk about $2 Cat$ , the 3-category of all 2-categories. And so on. But, it’s no fun having Russell’s ghost rapping us on the knuckles all the time. So, we beat him back with the Axiom of Universes.

Of course, you may think it’s a bit wild-eyed to prove theorems about all 3-categories so you can deduce consequences about $2 Cat$ so you can deduce consequences about 2-categories so you can deduce consequences about $Cat$ so you can deduce consequences about categories so you can deduce consequences about some specific category so you can deduce consequences about objects in there. But honest - it’s perfectly reasonable, and lots of fun.

Posted by: John Baez on October 30, 2006 6:16 PM | Permalink | Reply to this

Re: Foundations

$MathML-enabled post (click for more details).$

The general theorems of mathematical physics are quite heavily influenced by the axiom of choice - mainly theorems that involve real or functional analysis. But concrete computations are, I believe, completely unaffected by the axiom of choice.

The discussion over at Antimeta that David was referring to raised the point that one might want to check which additional axioms are actually required for describing the observed world around us - or which are required for describing the speculative world of quantum gravity.

Let $T$ be a “physical theory” of your choice, for you favorite notion of “theory”, like $T =$ classical mechanics, $T =$ quantum mechanics or $T =$ quantum field theory.

Does $T$ require the axiom of choice?

Or is it like this: $T$ is most conveniently formulated using AC, but for practical purposes we could do without?

Posted by: urs on October 30, 2006 7:00 PM | Permalink | Reply to this

Re: Foundations

$MathML-enabled post (click for more details).$

These different “ $T$ ’s” - classical mechanics, quantum mechanics, quantum field theory - sound quite vague to me.

We can formulate any of these theories in a stripped-down way using a minimum of logical infrastructure. But then, we need more infrastructure to prove deeper theorems.

If by “quantum mechanics” you mean “everything about quantum mechanics that you’ll find proved in Reed and Simon’s 4-volume masterpiece”, then you definitely need some powerful infrastructure, to get the Hahn-Banach and Tychonoff theorems - they use ZFC, and the axiom of choice is essential in their approach.

For an easier example, you might let $T$ be “the theory of groups”. If we simply mean “theory” in the sense of Lawvere’s “algebraic theories”, we can formulate this using very stripped-down logic. But then, we can only prove theorems like $((g h) h^{- 1}) g^{- 1} = 1 .$ If we want to get the classification of finite simple groups, we need more logical infrastructure. And if we want to settle the Whitehead problem, we’ll need to go beyond ZFC!

In physics I think it’s important to identify the amount of infrastructure needed to do concrete calculations - the sort we check against experiment. This is less than the amount we need to prove general theorems.

An interesting case is Penny Smith’s (sadly erroneous) proof that the Navier-Stokes equations have global solutions. I don’t know if she used results relying on the axiom of choice, but I wouldn’t be surprised, because the Hahn-Banach theorem and Tychonoff theorem are so basic in functional analysis. Interestingly, even when she thought she’d proved existence of global solutions, she emphasized that her method would not provide an algorithm to numerically solve the equations. This suggests she was using nonconstructive methods, e.g. proof by contradiction or the axiom of choice. That’s pretty common in this subject.

Posted by: John Baez on October 30, 2006 8:26 PM | Permalink | Reply to this

Re: Foundations

“It’s not that we’re wild-eyed logicians desperately eager to construct ever-larger sets.”

This comparison doesn’t exactly seem fair to me. The Axiom of Universes is exactly the axiom that states there is a proper class of strongly inaccessible cardinals. Grothendieck postulated it to make various proofs easier (namely ones about categories of categories). Set theorists postulated it to make other proofs easier (namely ones about the consistency of ZFC and the like).

It turns out that the desires of the set theorist drive an endless search for new axioms (because the issues they’re interested in are very often things about consistency and construction of models and the like) while the desires of algebraists so far only go up to this point. But the set theorists aren’t after these things just because they’re big - they’ve just got their own sort of evidence.

And especially once one gets past measurable cardinals, the evidence does become more mathematically interesting, involving determinacy considerations for sets of real numbers and the like, rather than just consistency.

Posted by: Kenny Easwaran on October 31, 2006 6:39 PM | Permalink | Reply to this

Re: Foundations

John wrote about Grothendieck’s universe axiom:

Of course, you may think it’s a bit wild-eyed to prove theorems about all 3-categories so you can deduce consequences about 2Cat so you can deduce consequences about 2-categories so you can deduce consequences about Cat so you can deduce consequences about categories so you can deduce consequences about some specific category so you can deduce consequences about objects in there. But honest - it’s perfectly reasonable, and lots of fun.

But at the same time, you should remember that you really are making your axiom system stronger. That is, even if you intend to use this axiom only to simplify the overhead as you prove a theorem about objects in a specific category, it may (in principle) turn out that this theorem actually cannot be proved in the weaker axiom system (ZFC, say).

Now, the only examples that I know of this are terribly artificial, piggy-backing on Gödel’s incompleteness theorems. But they are always there. This is because each stage of the universe axiom (assuming that you do apply it only one universe at a time, as usual) proves the consistency of the previous stage; but that previous stage (if in fact consistent) cannot prove its own consistency.

I somehow doubt that there are any interesting examples. But there really ought to be a way to know for sure.

Posted by: Toby Bartels on November 1, 2006 10:51 AM | Permalink | Reply to this

Re: Foundations

$MathML-enabled post (click for more details).$

Urs Schreiber wrote:

I could imagine that parts of physics depend on the axiom of choice.

The general theorems of mathematical physics are quite heavily influenced by the axiom of choice - mainly theorems that involve real or functional analysis. But concrete computations are, I believe, completely unaffected by the axiom of choice.

For example, when kids in math grad school get serious about integrals, they learn Lebesgue integration. The standard theory of Lebesgue integration says there are nasty things called nonmeasurable sets: subsets of the line whose length is undefined. But, you use the axiom of choice to show these nonmeasurable sets exist! If you’re willing to drop the axiom of choice and use the axiom of determinacy instead, you can show that all subsets of the real line are measurable.

When you actually come to doing integrals, you never meet a nonmeasurable set, so none of this matters when it comes to concrete computations.

Another thing we use a lot in analysis is Tychonoff’s theorem: any product of compact spaces is compact. This implies the Banach-Alaoglu theorem: the unit ball in the dual of any Banach space is weak- $⋆$ compact. People use this a lot to prove existence of solutions of differential equations.

But again, if you actually want to exhibit a solution of a differential equation, you don’t use these general theorems. Everything the axiom of choice helps you do is nonconstructive: it doesn’t really let you do anything concrete, it just lets you prove you “could” do it.

People also use the axiom of choice to prove the Hahn-Banach theorem, another basic tool in analysis. This says that you can always extend a bounded linear operator from a subspace of a Banach space to the whole thing.

The point is that the axiom of choice guarantees you can do various things, without saying how. In concrete situations you often can see how.

So, the axiom of choice just lets you prove theorems without worrying about certain “details” that become crucial when you’re doing concrete calculations. However, you pay a price for this: it lets you construct nasty things like nonmeasurable sets, which you’d never see how to construct in practice.

All this suggests we should adopt a flexible attitude towards axiom systems: instead of believing in one and regarding its consequences as true, we should think of each extra axiom as giving us extra powers, and pay some attention to what each extra power lets us do. Even if we don’t “really” have these extra powers in general, we may have them in certain circumstances.

Of course it’s a lot of work keeping track of more than one axiom system, so most mathematicians don’t have the patience for it.

Posted by: John Baez on October 30, 2006 5:48 PM | Permalink | Reply to this

Re: Foundations

Actually, all this determining where exactly AC comes up ties into a question Zuckerman asked me today.

Consider a rooted tree so that
(a) every vertex has a finite number of children
(b)every path from the root terminates (in a finite number of steps)

Does it follow from this that the tree is finite?

I gave two different proofs off the top of my head that it does, which led him to ask the follow-up: do those require the Axiom of Choice? I didn’t think so, but I had trouble convincing him of that fact. Maybe someone here has an idea how to settle it?

Posted by: John Armstrong on October 30, 2006 11:06 PM | Permalink | Reply to this

Choice.

It’s often hard to notice use of dependent choice. Look up “König’s Lemma”.

Posted by: Toby Bartels on October 31, 2006 12:22 AM | Permalink | Reply to this

Re: Foundations

AC really only applies to infinite sets: you can always apply the choice “trick” on finite sets.

It seems obvious to me that the tree is finite: if the largest number of child nodes for any node is m and the longest path in the tree is of length n, the total number of nodes in the tree is going to be bounded by m to the n, which is clearly finite for any finite m and n.

König’s Lemma only applies to graphs taken by assumption to have an infinite number of nodes.

If you had to use it or AC in this proof, it would suggest that you had an infinite tree. ;-)

Posted by: Marc Hamann on October 31, 2006 3:03 AM | Permalink | Reply to this

Re: Foundations

So what’s the a priori finite set you think you’re making a choice over? The dual to your statement about when you need AC is that if you assert that you don’t need AC you’re assuming that a given set is finite.

Posted by: John Armstrong on October 31, 2006 3:19 AM | Permalink | Reply to this

Re: Foundations

So what’s the a priori finite set you think you’re making a choice over?

I’m not taking any a priori set. I’m saying that you don’t need to invoke the AC until you know you have an infinite set.

To grasp this, consider a different approach to solve the problem: show that you can do choice on this set (for example that in a finite number of steps, using plain ZF, you can select any particular path from any particular directed subset) without invoking the AC: you would thereby prove that the set is finite.

Posted by: Marc Hamann on October 31, 2006 4:21 AM | Permalink | Reply to this

Re: Foundations

Okay, let’s see it. I’ve got two proofs and both seem to use Dependent Choice (which if you paid attention is what we’re considering). It’s easy enough to wave your hands and say “it all works out”, but it’s harder to step up and prove it.

1. Assume each node has finitely many children and the tree is infinite. Then the root has at least one infinite child. Choose one (finite) and recurse: that child has at least one infinite child. Choose one (finite) and so on. This gives an infinite path, so the first condition cannot be satisfied.

The problem is that even though each choice is finite, which choice is to be made depends on the choices that came before. This is DC.

2. Consider the algorithm for a breadth-first search. This walks through the tree and visits every node. An infinite recursion is not possible since that would mean an infinite depth path. Also, no node requires more than a finite number of iterations of its for-loop.

It seems that the algorithm must terminate, but something still feels uneasy to me. Besides that, the tree only comes with a set of children rather than an ordered set, so the algorithm must choose an order (finite) at each node. It doesn’t seem to depend on anything outside the node itself, but I think I’m right to be cautious here.

So, if you can prove that the second one actually is tight and never uses DC, great. If not, what’s your proof?

Posted by: John Armstrong on October 31, 2006 4:56 AM | Permalink | Reply to this

Re: Foundations

Suppose for contradiction that this tree is infinite. At a finite depth there are only a finite number of nodes (by induction), so the depth must be unbounded.

Step 1

Choose one vertex at depth 1, one at depth 2 etc. We get an infinite sequence of vertices a_1, a_2….

Step 2

For each of a_1, a_2, etc in turn, we check if the depth 1 grandparent vertex has an infinite number of members of the sequence {a_n} in its subtree. When we find an a_m that this is true, we halt* and throw out any members of {a_n} that don’t belong to this subtree.

Repeat the process on the new subtree, with the (still infinite) subsequence of {a_n}, and so on to get an infinite path, which is a contradiction.

*We know that this process will halt after a finite number of steps, since the number of depth 1 vertices is finite, and so at least one depth 1 vertex must have an infinite subsequence of {a_n} in its subtree, while only a finite subset of {a_n} can have depth 1 grandparent vertices that don’t have this property, so they will be exhausted in a finite number of steps.

Step 1 involves finite choice, and the choices are independent.

Step 2 is deterministic.

Does this solve the problem?

Posted by: simon on October 31, 2006 7:35 AM | Permalink | Reply to this

Re: Foundations

That was needlessly complicated. Since the set of vertices at depth n is finite, we can order it with no problem.

So first, choose such an ordering, for the whole tree at each depth independently.

Now choose the first vertex at depth 1 with an infinite subtree, then the first at depth 2 that belongs to that subtree, and has its own infinite subtree, etc.

We aren’t really making dependent choices since we are “choosing” deterministicly using an ordering independent of our choices.

Posted by: simon on October 31, 2006 7:53 AM | Permalink | Reply to this

Re: Foundations

So first, choose such an ordering, for the whole tree at each depth independently.

So for each depth (which may be infinite a priori) choose one of a finite set of orders on the nodes of that depth. Sorry, that’s CC.

Posted by: John Armstrong on October 31, 2006 3:58 PM | Permalink | Reply to this

Re: Foundations

I believe these proofs still require Choice. I remember hearing that without Choice, it is consistent that there is an infinite sequence of finite sets (in fact, sets of cardinality 2) with no choice function on them. The analogy is that with an infinite set of pairs of socks, one can’t choose one sock from each pair.

If you could order the whole tree, then you could order this infinite set of socks, and then pick the first element of each. So your proof (either requiring an ordering of the tree, or a choice of one element at each level) seems to require Choice.

Posted by: Kenny Easwaran on October 31, 2006 6:48 PM | Permalink | Reply to this

Re: Foundations

I should have reviewed the axiom of choice, and not assumed that I could guess the meanings of terms like dependent choice from context, before commenting. Embarrassing, but thanks for the correction.

Posted by: simon on November 8, 2006 2:51 AM | Permalink | Reply to this

Re: Foundations

If not, what’s your proof?

My joke about König’s Lemma notwithstanding, Toby’s idea is actually the easiest.

Towards a contradiction, assume there are infinite nodes in the tree. Then by König’s Lemma, there would be at least one infinite path, which contradicts the premise.

As with AC, DC still only adds power to ZF for infinite sets: you already have all you need to make the choice for strictly finite cases, as simon has demonstrated.

Posted by: Marc Hamann on October 31, 2006 3:22 PM | Permalink | Reply to this

Re: Foundations

Yes, I follow the use of König’s lemma. That uses DC, though, and you seemed to indicate that you could do it without DC.

Posted by: John Armstrong on October 31, 2006 3:56 PM | Permalink | Reply to this

Re: Foundations

Since ultimately I’m a computer scientist, the easiest way to show the reasoning here is to describe an algorithm and give an indication how it uses ZF.

My claim is that a traversal of the tree described (finite branching/finite paths) necessarily terminates (and hence finite).

Start at the root (which was given), iterate (in random order) over the finite list of children and recursing on each.

Surely you will accept I can do this on a finite set without using any kind of choice axiom? If not, even membership and subset would imply choice.

Since each iteration is over a finite number of elements, it will terminate. Since each recursive path down the tree is stipulated by assumption to be finite, it will terminate.

Therefore, the traversal as a whole will terminate. Therefore, there are a finite number of nodes.

We can easily model this in pure set theory by representing the tree as a set whose members are the root’s children, each child’s members are its child nodes, etc.
The requirement that all paths are finite is the Axiom of Foundation, and the bound on the size of each node set ensures that we can iterate over each of these using only basic set-theoretic operations.

Posted by: Marc Hamann on October 31, 2006 4:41 PM | Permalink | Reply to this

Re: Foundations

Maybe increasing the pseudocode to include a list node.visited_children so the random selection won’t repeat. That gives a decision process.. I think that might plaster over the handwaving I did in proof 2.

Actually, I just thought of another that might work in a different way: Tree = {*} or {finite set of Trees}. * is finite, and if each of finitely many children is finite then the tree is finite, so by induction all such trees constructible in finitely many steps are finite. Since every path from the root terminates, the tree is constructible in finitely many steps.

Or is there a hidden choice in there?

Posted by: John Armstrong on October 31, 2006 4:54 PM | Permalink | Reply to this

Re: Foundations

We can do it purely set theoretically too. To simplify things, let’s assume urelements with a distinct one for each leaf node.

Starting from our root set, which has a finite cardinality, take the grand union. The cardinality of the resulting set will be finite, since it will grow at most by a finite number.
Continue taking the grand union, each time adding only finitely many, until you have only urelements in the set.
This state must be arrived at in a finite number of steps by the well-foundedness condition.

Since each step added only finitely many to the cardinality, the final set also has finite cardinality.

Posted by: Marc Hamann on October 31, 2006 7:11 PM | Permalink | Reply to this

Re: Foundations

Well-foundedness says that each branch is only finitely deep, not that there is a single depth that no branch exceeds.

Posted by: Kenny Easwaran on November 2, 2006 10:42 PM | Permalink | Reply to this

Re: Foundations

Well-foundedness says that each branch is only finitely deep, not that there is a single depth that no branch exceeds.

I’m starting to wonder if I’m being put on…
But, please remember the OTHER condition that there is finite branching. If there is a finite number of branches (which has gone over ad nauseam) and each branch is finite, there must be a maximum length of branches.

Another thing for the doubters to remember is that just because the infinite case is not constructively provable does NOT mean that the finite case in not constructively provable. The excluded middle doesn’t hold in intuitionistic math, and provability can be expected to be different across the finite/infinite divide.

Posted by: Marc Hamann on November 3, 2006 4:35 AM | Permalink | Reply to this

Re: Foundations

Finite branching just means that at each branch point there are only finitely many immediate successors. Without some form of Choice, finite branching and no infinite paths don’t entail that there are only finitely many branches in total, with a uniform upper bound on their length.

If you assume that the tree is finite, everything’s fine - there’s no need for choice. But proving that the tree is finite is exactly what we need to do here! Contrary to what someone said earlier, Choice is unnecessary only when we know the relevant collection of sets to be finite, but it is often necessary when we don’t know whether it’s finite or infinite. (That earlier comment suggested that it was only necessary when we knew the collection to be infinite.)

Posted by: Kenny Easwaran on November 4, 2006 1:43 AM | Permalink | Reply to this

Re: Foundations

Contrary to what someone said earlier, Choice is unnecessary only when we know the relevant collection of sets to be finite, but it is often necessary when we don’t know whether it’s finite or infinite. (That earlier comment suggested that it was only necessary when we knew the collection to be infinite.)

As over-played as this thread has gotten now, I think we actually might have learned/been reminded of some important things.

First, there is a bigger gulf between constructive mathemetics and traditional formalist mathematics than arguing about a couple axioms: the systems generated can be quite different in their interpretations of particular structures, for example, in this case, the notion of infinity.

Second, as Gödel proved, you often can’t coherently formulate a proof about a system from within the system. In the current instance, the proof about infinity is dependent upon whether you admit infinity as a given rather than a constructed entity.

Third, foundational discussions are fractious and difficult. Maybe CT shouldn’t want to become a foundation; it might bring an end to the relative harmony of the CT community. ;-)

Posted by: Marc Hamann on November 4, 2006 7:51 PM | Permalink | Reply to this

Re: Foundations

“Actually, I just thought of another that might work in a different way: Tree = {*} or {finite set of Trees}. * is finite, and if each of finitely many children is finite then the tree is finite, so by induction all such trees constructible in finitely many steps are finite. Since every path from the root terminates, the tree is constructible in finitely many steps.

Or is there a hidden choice in there?”

There’s no hidden choice, but there’s a hidden assumption: that if every path is finite, then there is a finite number n such that every path has length not greater than n. This isn’t true a priori (it’s false if we drop the stipulation that each node has a finite number of children, for example), and in this case it’s equivalent to what you’re trying to prove.

Posted by: Adam Stephanides on November 2, 2006 3:23 PM | Permalink | Reply to this

Re: Foundations

We can easily model this in pure set theory by representing the tree as a set whose members are the root’s children, each child’s members are its child nodes, etc.

Incidentally, this is exactly what got Zuckerman started in the first place: the topos of hereditarily finite sets.

Posted by: John Armstrong on October 31, 2006 4:57 PM | Permalink | Reply to this

Re: Foundations

Incidentally, this is exactly what got Zuckerman started in the first place: the topos of hereditarily finite sets.

My best guess to a response (without knowing the actual content of his beef) is that it is easy to confuse performing a choice operation constructively with invoking a choice axiom ex machina, even though they are quite different beasts. ;-)

Posted by: Marc Hamann on October 31, 2006 7:21 PM | Permalink | Reply to this

Re: Foundations

He wasn’t complaining, just exploring, so I think “beef” is overstating it a bit. He’s gotten into set theory lately, and even poking into ill-founded set theory. One of his latest toys is this topos.

Basically, at the department’s tea he asked me about the finiteness of that tree, and it was obvious to me. Then he asked if I could do it without even dependent choice and I’m still not entirely sure.

Posted by: John Armstrong on October 31, 2006 8:00 PM | Permalink | Reply to this

Re: Foundations

I don’t see how this is different from the approaches above. Each particular iteration will eventually terminate by reaching an end node, but it’s not clear that there are only finitely many iterations unless you already know the entire tree is finite (after all, you have one iteration for each node).

I believe that given a countably infinite set of pairs with no choice function, it should be quite easy to construct an infinite tree with only pairwise branching and no infinite branches. So there should be no way to prove this theorem without assuming some fairly weak form of choice that prevents this situation. König’s Lemma seems like exactly what we want.

Posted by: Kenny Easwaran on October 31, 2006 7:14 PM | Permalink | Reply to this

Re: Foundations

I believe that given a countably infinite set of pairs with no choice function, it should be quite easy to construct an infinite tree with only pairwise branching and no infinite branches

Well, all I can say is prove (or demonstrate) that and we might have more to talk about.

;-)

Posted by: Marc Hamann on October 31, 2006 7:29 PM | Permalink | Reply to this

Re: Foundations

“I believe that given a countably infinite set of pairs with no choice function, it should be quite easy to construct an infinite tree with only pairwise branching and no infinite branches.”

I’ll give it a go: suppose S = {S_1, S_2, S_3, …} is such a set. Then let the tree’s nodes be the empty set (the root), and all finite sets of the form {a_1, a_2, …, a_n} for some n, where a_i is a member of S_i for all i less than or equal to n. The children of any node N are the two nodes which contain all of N’s elements and one additional element. This tree is infinite, but it has no infinite branch, because an infinite branch would define a choice function on S.

Note that though there is no infinite branch, there are branches of any finite length. Also, the tree has no leaves, and so the traversal described by Marc Hamann in his Oct. 31 4:41 PM post never completes a single path.

(Apologies for the poor formatting.)

Posted by: Adam Stephanides on November 1, 2006 3:03 PM | Permalink | Reply to this

Re: Foundations

Also, the tree has no leaves, and so the traversal described by Marc Hamann in his Oct. 31 4:41 PM post never completes a single path.

How could a tree with no leaves have finite paths? A path in a tree is finite precisely because it terminates in a leaf.

Posted by: Marc Hamann on November 1, 2006 3:31 PM | Permalink | Reply to this

Re: Foundations

Yes, it’s a counter-intuitive situation: we can always extend any finite path by one more step, but we can’t “take the limit,” so to speak, of this process to get an infinite path. This is the sort of thing that can happen when you don’t have any form of choice.

If the absence of leaves bothers you, you can enlarge the tree by attaching to each node a single child node with no successors. There will still be no infinite paths.

Posted by: Adam Stephanides on November 2, 2006 3:13 PM | Permalink | Reply to this

Re: Foundations

we can always extend any finite path by one more step

The specific requirement was: “Every path from the root terminates”. That flies directly in the face of this statement. If any finite path can be extended, then how can any be said to terminate?

Posted by: John Armstrong on November 2, 2006 4:17 PM | Permalink | Reply to this

Re: Foundations

we can always extend any finite path by one more step

The specific requirement was: “Every path from the root terminates”. That flies directly in the face of this statement. If any finite path can be extended, then how can any be said to terminate?

There is no contradiction. In this example, it is true that every path terminates and that no path terminates. That’s because there are no (maximal) paths!

There are, of course, plenty of partial paths (that is paths in the general sense without regard to whether they can be extended). However, there are no maximal paths (that is paths that cannot be extended).

(Note that a lot of people are using the word “path” on this thread to refer to partial paths, and that’s how I would use the word by default. However, the requirement “Every path from the root terminates” is obviously intended to apply only to maximal paths; for paths in general, it’s true only for the empty tree!)

Posted by: Toby Bartels on November 2, 2006 8:29 PM | Permalink | Reply to this

Re: Foundations

This feels incredibly like cheating. For one I don’t see how it’s “obvious” at all that “path” really means “maximal path”.

Posted by: John Armstrong on November 2, 2006 9:42 PM | Permalink | Reply to this

Re: Foundations

Requiring that every partial path be contained in some maximal path would do what you want. It is a consequence of choice that in every tree, every partial path is contained in some maximal path. You might be able to prove this result without choice if you restrict to trees with this property - but note how that changes the theorem!

Posted by: Kenny Easwaran on November 2, 2006 10:46 PM | Permalink | Reply to this

Re: Foundations

I don’t see how it’s “obvious” at all that “path” really means “maximal path”.

Because otherwise:

the requirement “Every path from the root terminates” […] for paths in general, it’s true only for the empty tree!

But Kenny (below) has a different interpretation by defining “terminates” to mean «is contained in a finite maximal path». Then we can take the requirement to refer to all (partial) paths, which (as Kenny points out) in principle changes the meaning of the theorem. (In particular, it makes Adam’s first counterexample fail.)

However, Adam’s second counterexample, using the trick of adding an extra (third) leaf to each node, still works.

Posted by: Toby Bartels on November 2, 2006 11:17 PM | Permalink | Reply to this

Re: Foundations

I must confess this thread is starting to seem like sophistry or trolling, but in the hope that it is a sincere pursuit of understanding, and that you aren’t working with some definition of tree which is incommensurate with mine, here is my simplest explanation of how König’s lemma can require choice, but what I’ll call the “Darn Useful Heuristic” (DUH for short) lemma does not.

Let F be a predicate meaning “is finite”. The form of König’s lemma is:
¬ F(tree) → ¬ F(branching) ∨ ¬ F(paths)

The form of the DUH lemma is:
F(branching) ∧ F(paths) → F(tree)

At first glance, the classical logicians among you will say that these are logically equivalent statements. However, you can also see that they are only equivalent using the law of the excluded middle. So if we are doing purely constructive proofs (otherwise why quibble about choice?), these two statements are NOT the same fact.

An important thing to note is that the premise of the DUH lemma introduces no infinite values. In contrast, König’s starts with an infinite premise, and has already disqualified itself from constructive proof.

Another interesting thing to note is that, even in purely constructive proofs, you can start with finite premises and end up with infinite conclusions (non-terminating proofs). So if you find a terminating proof of DUH (as I have shown) it is true, but you still had enough power prove that a proof will NOT terminate (though some proofs may not be able to terminate and you can’t prove that.)

So the very basic fact from computer science about one of the most studied mathematical structures in human history is true and constructive, even though the most common formulation of it “from the infinite end” is not constructively true.

Posted by: Marc Hamann on November 3, 2006 2:44 PM | Permalink | Reply to this

Re: Foundations

So if we are doing purely constructive proofs (otherwise why quibble about choice?)

Plenty of people trust the principle of excluded middle but not the full axiom of choice, going back at least to Russell & Whitehead (and possibly further, but I’m not sure if anybody ealier was this explicit). AC implies LEM, but not conversely.

An important thing to note is that the premise of the DUH lemma introduces no infinite values. In contrast, König’s starts with an infinite premise, and has already disqualified itself from constructive proof.

There are plenty of constructive proofs involving infinite sets. Furthermore, the DUH lemma makes reference to a tree not known (a priori) to be finite, so at the very least any proof of it must use principles that apply to infinite sets, lest the proof beg the question.

Another interesting thing to note is that, even in purely constructive proofs, you can start with finite premises and end up with infinite conclusions (non-terminating proofs). So if you find a terminating proof of DUH (as I have shown) it is true, but you still had enough power prove that a proof will NOT terminate (though some proofs may not be able to terminate and you can’t prove that.)

I have no idea what this paragraph means!

Anyway, the DUH lemma implies the principle of denumerable choice from finite sets, as I have just shown. That argument is perfectly constructive; that is, it doesn’t use the principle of excluded middle (nor any other form of the axiom of choice, nor other constructively suspect principles like impredicative definitions), although of course it requires an axiom of infinity to even state (so finitists would consider it meaningless, at least as it stands). I’m pretty sure that the proof of the converse is also constructive, but I’m not positive, since I haven’t written it out in detail. All the same, I think that we should understand things first using (possibly) classical logic, since this is probably more familiar to us all.

Let me emphasise one point: Any valid proof of the DUH lemma must use principles that apply to denumerable (as well as finite) sets. To assume that (the set of nodes of) the tree is finite is to assume the conclusion. One must allow for the possibility that the tree is infinite until one has shown otherwise.

Posted by: Toby Bartels on November 4, 2006 12:09 AM | Permalink | Reply to this

Re: Foundations

I have no idea what this paragraph means!

I will have to assume at this point that we are talking about some completely different notion of “tree”, “finite branching” or “finite path” or otherwise live in different mathematical universes.

I hope yours brings you useful insights and accomplishes for you what you want it to.

Posted by: Marc Hamann on November 4, 2006 1:27 AM | Permalink | Reply to this

Re: Foundations

Marc wrote:

I [Toby] wrote:

Marc wrote:

[something about non-terminating proofs]

I have no idea what this paragraph means!

I will have to assume at this point that we are talking about some completely different notion of “tree”, “finite branching” or “finite path” or otherwise live in different mathematical universes.

Well, my mathematical universe for this discussion has basically been ZF set theory, since that’s the universe most familiar to mathematicians (at least when they get down to details, for the record) in the absence of the axiom of choice. But actually everything that I’ve said works perfectly well in a type-theoretic version, such as Zermelo type theory (and therefore internal to any Boolean topos) or even weaker, predicative type theories (categorically speaking, internal to a pretopos, more or less). When practical, I’ve also avoided (and at least noted my use of) the law of excluded middle; except where that appears, things could be formalised in CZF set theory or a Martin-Löf type theory (and internalised to any LCC pretopos).

Of course I don’t make any specific reference to such formalisations, keeping things loose as mathematicians usually do (even without thinking about it). But for the record, those are formalisations that could be used. (Some parts of this thread did interpret the tree as the membership tree of a hereditarily well founded set, which can be formalised in type/category theory but is much nicer in set theory. But I didn’t go there.)

In all of these contexts, proofs are necessarily finite things. I don’t mind talking about non-terminating proofs, but I don’t see the connection.

I have definitely required the set of finite sequences from a given infinite sequence of sets. If you don’t believe in that, then you don’t believe in Adam’s counterexamples (at least not as I’ve spelt out the details). However, as long as accepting such a set is consistent with your universe (in the sense that there is a consistent formal system interpreting your universe together with that construction), then those counterexamples are still enough to show that the theorem cannot be proved without a choice principle.

If you’re still interested: What is your universe?

Posted by: Toby Bartels on November 6, 2006 10:53 PM | Permalink | Reply to this

Re: Foundations

I wrote in part:

[T]he DUH lemma implies the principle of denumerable choice from finite sets, as I have just shown. That argument is perfectly constructive[.]

But that’s not right, since the form of the theorem that I used isn’t (constructively) equivalent (AFAICT) to the DUH Lemma. (I was so pleased to tell Marc that my proof was constructive that I neglected to notice that it did not prove what he wanted!) In fact, it was basically König’s Lemma, at least if you write König’s Lemma as I’ve most often seen it phrased:
F(branching) ∧ ¬ F(tree) → ¬ F(paths)
where ‘¬’ is taken in a strong sense (existence of an infinite counterexample).

However, the metamathematical argument still works, as follows:

Postulate. The principle of denumerable choice from finite sets (the ‘principle’) cannot be proved, even using LEM.

To verify the postulate is beyond the scope of this comment (because I don’t know enough metamathematics to do it), but can be found in references on set theory. Even the truth of the postulate, of course, depends on one’s formal system; but it is true for ZF and hence also for any weaker (intuitionistic, predicative, whatever) system.

Proposition 1. Using LEM, the DUH Lemma and König’s Lemma are equivalent.

Proposition 2. Using LEM, the weak form of the DUH Lemma (with the requirement that every path be contained in a maximal path) and the (similarly) weak form of König’s Lemma (‘the theorem’) are equivalent.

Proposition 3. The strong form of each lemma (from Proposition 1) implies the weak form of that lemma (from Proposition 2).

These Propositions are all immediate; note that Proposition 3 does not require LEM.

Theorem. The theorem implies the principle.

This is what I proved (without using LEM) in this comment (which was based on an example by Adam’s second counterexample).

Corollary. The DUH Lemma cannot be proved, even using LEM.

This is what you get by tossing all of the above together, in the style of Lewis Carroll, and seeing what pops out.

Now, an interesting variation on this question would be to use some system of reasoning (still constructive) that is not weaker than (but rather incomparable with) ZF, such as full-blown intuitionism (as practised by Brouwer and still studied in Nijmegen and elsewhere). In particular, Brouwer’s Fan Theorem is probably relevant. But you will need some additional assumptions, whatever they may be, to prove the DUH Lemma, or ‘the theorem’, or ‘the principle’.

Posted by: Toby Bartels on November 7, 2006 5:12 PM | Permalink | Reply to this

Re: Foundations

I was going to let sleeping dogs lie, Toby, but you have been so persistent in your interest in the problem I feel obliged explain where I’m coming from. ;-)

A very close reading of the Wikipedia article for the (graph theoretic) König’s Lemma has enough information to see where I’m coming from, but it requires being sensitive to certain unstated assumptions to see it.

In particular, note:

This issue cannot arise if the graph is assumed to be countable.

One thing to understand is that from a strict comptational constructive point of view, you can’t build ANY uncountable set at all.
But even in a system that admits uncountable sets, such as ZF, you would need choice to show that an uncountable TREE could exist. (Consider that the relation parent-of(x, y) establishes a complete partial order on the elements of the tree.)

Many of the set-theoretic axioms are like this: you only need them if you admit uncountable sets (or certain kinds of operations on countable sets that ultimately imply uncountable sets) and want to impose some additional structure on them.

To understand the objection to the “counter-example” that you and Adam were proposing, add to the previous assumption/theorem that uncountable trees are inadmissible the notion that “a tree has finite paths” implies for me that all paths are closed; if the path is not closed it would be infinite.

Another way to express my position that uncountable trees are inadmissible, and finite paths are closed is to say that for me trees are by definition discrete (all subsets are clopen). With a discrete structure, if you can’t expand infinitely horizontally and you can’t expand infinitely vertically, and there aren’t any other dimensions, where would the infinity be hiding?

Anyway, I hope my explanation of my position has been illuminating (if of nothing else, that foundations discussions are very tricky and have many hidden assumptions and consquences), and we will end up either agreeing or agreeing to disagree. ;-)

Posted by: Marc Hamann on November 7, 2006 9:34 PM | Permalink | Reply to this

Re: Foundations

One thing to understand is that from a strict comptational constructive point of view, you can’t build ANY uncountable set at all.

I don't really like this attitude, even for constructive mathematics intended for a computational interpretation, because IMO uncountable sets (like the set N^N of all infinite sequences of natural numbers) should sometimes be used as a type of arbitrary procedures (themselves not necessarily computable) coming as inputs to a computation from somewhere outside: a computer user, a scientific measurement, or some other oracle. Thus even in Markov's Russian school of recursive constructive mathematics (where it is taken as axiomatic that every element of N^N, and even every partial sequence, is recursive), still the set N^N exists (and can be proved uncountable by Cantor's diagonal argument).

But this is only a side remark; I'll put away my philosophical prejudices for now.

But even in a system that admits uncountable sets, such as ZF, you would need choice to show that an uncountable TREE could exist.

OK, I'll accept this. (I might quibble over the meaning of the word ‘tree’, but I don't think that this affects anything here.) However, just because you need choice to refute the claim that all trees are countable, that doesn't mean that you can prove that claim just because you don't accept choice.

In fact, if I understand your position correctly now, then you are using the following ‘additional assumption’ (as I put it last time): Every set (or at least every set that can be the set of nodes of a tree) is countable. Even better (again if I understand your position correctly), it ought to be a theorem (in a very stripped down constructive mathematics, with neither any axioms of choice nor any classically false axioms) that every countable tree satisfies the DUH Lemma.

So, with this proviso, I no longer believe that you are wrong. (That's good, right? $-_^$ ) In particular, in Adam's counterexample, given that the set of nodes is countable, we can enumerate them once and for all, then construct an infinite path (without any axiom of choice) by always picking the first regular child. In fact, if I'm not messing up, this actually shows that the principle of countability (if I may call it that) implies the principle of denumerable choice from finite sets. (And thus, the principle of countability and the principle of excluded middle together imply both the principle of countable choice from finite sets and König's Lemma.)

Actually, the only thing that I don't see yet is how the principle of countability implies the DUH Lemma! (I can prove it if I use excluded middle as well, since then it's equivalent to König's Lemma, but that's not very interesting.) I'm willing to take your word for it (especially since Wikipedia, in the form of Carl Mummert seems to confirm this), but I'd appreciate it if you could explain to me:

Given an enumeration of the nodes of a tree, finitely branching and with all paths finite, how do you (preferably without using any axiom of choice, but if necessary then using discrete choice from finite sets) construct an upper bound on the number of nodes? (In particular, you might explain why this program must terminate, in light of Kenny's response to it.)

Posted by: Toby Bartels on November 8, 2006 4:42 PM | Permalink | Reply to this

Re: Foundations

I don’t really like this attitude, even for constructive mathematics intended for a computational interpretation

If I want to model something that could actual be turned into a terminating program, I necessarily have to put such limitations on my proofs.

If I’m studying a mathematical principle in more general terms as a kind of theoretical upper bound on computational ideas, I will by all means use a more powerful mathematics. In such a case, though, I don’t shy away from using some kind of choice axiom… in for a penny, in for a pound. ;-)

However, just because you need choice to refute the claim that all trees are countable, that doesn’t mean that you can prove that claim just because you don’t accept choice.

From my point of view, I would say that what is really happening is that the actual content of the claim changes depending on what system it is formulated in.

This is actually an interesting philosophical point that would distinguish a mathematical Realist from a Constructivist or a Formalist (at least as verifiable proof-theoretic methodologies rather than as self-identifications. ;-) )

As a member of the latter camp (hybrid constructivist/formalist), I feel inherently that concepts that can’t be generated from my axioms are outside the realm of discourse for the proof. I’m comfortable that the objects picked out by the predicate infinite(x) is actually different in each case.

A mathematical Realist might take a different position and say “Uncountable sets are a real mathematical phenomenon, so it is reasonable to judge a system’s power with respect to it even if it inadmissible in that system, i.e. not already a consequence of the predefined axioms.”

I think one of the problems is that most people haven’t really thought about which of these they are: they just happen to be whichever. ;-)

Given an enumeration of the nodes of a tree, finitely branching and with all paths finite, how do you (preferably without using any axiom of choice, but if necessary then using discrete choice from finite sets) construct an upper bound on the number of nodes?

I’ve been trying to figure out the best way to present this given the limitations of the medium (and my spare time ;-) ), and the clearest approach I’ve come up with is to use a simple game semantics.

The game is between two people, Verifier and Falsifier.

Falsifier’s goal is to build an infinite tree with finite branching and finite paths. He starts with a countably infinite store of nodes to add to the tree and a pre-placed node, the root, that is coloured green.

Falsifier can add any finite number of children to a green node per turn, each of which will be introduced coloured red. At any time, Falsifier can choose to colour the current green node red, and make any other node in the tree green, thus opening that node for expansion. To generate a chain, he can successively shift the green marking to a child, add a new child and shift the green to that new child, etc.

So a green node represents a potentially infinite sub-tree, a “slot” either for infinite branching or an infinite path.

At any turn, Falsifier can claim victory and turn the tree over to Verifier, whose goal is to traverse the entire tree, rejecting the tree as not meeting the specification if he finds a green node, whereby he wins. If the Verifier’s traversal doesn’t terminate in a finite number of steps, he loses.

It becomes obvious that Falsifier can’t win, because on any turn n he can either colour the green node red and not add a new green one to meet the preconditions, thus shutting off the opportunity to add the rest of his infinite store or he can pass the tree back to Verifier with the green node still there, leaving the tree potentially infinite, but losing because he fails the preconditions.

You can see that even if we allow any finite number of nodes to be added per turn, and allow as many green nodes as you like at any turn, Verifier will STILL be able to accept or reject any tree in a finite number of steps for any turn n (a simple induction).

The only way that Falsifier could win is if he was allowed to add an infinite tree pre-coloured to red in one go, and of course that would be a petitio principii.

Posted by: Marc Hamann on November 8, 2006 8:05 PM | Permalink | Reply to this

Re: Foundations

This proof seems to implicitly assume that the game terminates in a finite number of steps: i.e., Falsifier can only make a finite number of moves. But of course, if Falsifier can only make a finite number of moves, and can only add a finite number of nodes at each move, then the final tree must be finite. To put it another way, if your proof were valid, it would still be valid without the assumption that each node has a finite number of children; but without this assumption the theorem is clearly false.

“The only way that Falsifier could win is if he was allowed to add an infinite tree pre-coloured to red in one go, and of course that would be a petitio principii.”

On the contrary, assuming that Falsifier can’t do this is the petitio principii, since that’s equivalent to the assertion you’re trying to prove. (If the objective were to prove that an infinite tree satisfying Armstrong’s conditions exists, then you’d be correct; but we already know that can’t be done in ZF, since it contradicts AC.)

Posted by: Adam Stephanides on November 12, 2006 8:44 PM | Permalink | Reply to this

Re: Foundations

This proof seems to implicitly assume that the game terminates in a finite number of steps: i.e., Falsifier can only make a finite number of moves.

No: this is a straightforward induction on N (which of course is infinite). Even if (especially if)we allow the game to go on for ever, Falsifier can never both meet the requirements for the tree and the contra-requirement that it is infinite. This works because each step is finitary, even if we admit infinite steps.

On the contrary, assuming that Falsifier can’t do this is the petitio principii, since that’s equivalent to the assertion you’re trying to prove.

I must respectfully disagree: the onus placed on each player is quite clear: it is falsifier’s job to build such a tree. Perhaps, if you are not familiar with game semantics or proof theory, this might be a bad formulation for convincing you. If that is so, my apologies; it meets my criteria for being convincing, and I can’t see how to make it more so.

Posted by: Marc Hamann on November 12, 2006 9:53 PM | Permalink | Reply to this

Re: Foundations

“Given an enumeration of the nodes of a tree, finitely branching and with all paths finite, how do you (preferably without using any axiom of choice, but if necessary then using discrete choice from finite sets) construct an upper bound on the number of nodes? (In particular, you might explain why this program must terminate, in light of Kenny’s response to it.)”

I think I can do this, actually. (That is, I know I have a proof, but I’m not completely sure it avoids LEM.) So, suppose we have a tree T with an enumeration, satisfying the conditions of DUH. (Actually, we only need to assume that the nodes of T can be totally ordered.) Construct a sequence of nodes of T as follows: a_0 is the root node r. If a_n has children not yet visited by the sequence, then a_(n+1) is the lowest-numbered of these. Otherwise a_(n+1) is the parent node of a_n, unless a_n = r, in which case the sequence terminates. Clearly, if the sequence terminates, then it’s a traversal of T and T is finite.

But in any case, we know that any node only appears a finite number of times: in fact, if it has n children it appears at most n+1 times. So we can construct another sequence as follows: b_0 = a_0 = r, and b_(n+1) is the node which immediately follows the last occurrence of the node b_n in the sequence of a’s, if one exists. Otherwise the sequence terminates at b_n.

At some point this sequence must terminate, since otherwise it would be an infinite path. Say it terminates at b_i. But by construction, this is only possible if the sequence of a’s also terminates at the node b_i (which therefore must equal a_0 = r). So the sequence of a’s terminates, and therefore is a traversal, and T is finite.

Posted by: Adam Stephanides on November 14, 2006 2:54 AM | Permalink | Reply to this

Re: Foundations

Thanks, Adam! I think that your argument here is probably essentially the same as the argument that Marc was making, but I understand yours better.

I’m pretty sure that your construction of the sequence (b_0, b_1, …) is legitimate (without any form of choice, note even LEM). Only the final step is problematic; you assume that since this sequence can’t be infinite, then it must be finite. This is an example of LEM, but (in this context) it follows from Markov’s Principle (MP), a (very) weak form of LEM accepted by (as the name implies) the Markovian school of constructivism (and also by at least one Brouwerian intuitionist).

Furthermore, it’s easy to see that DUH (applied to denumerable trees) implies Markov’s Principle: Given any infinite sequence of 0s and 1s that is not all 0s, form an unbranching tree whose nodes are all initial segments that consist of all 0s. Then DUH implies that this is finite, so the original sequence has at least one 1 (immediately following the final node) —and this is precisely what MP states.

So to Marc: I now agree that you are correct, given Markov’s Principle (which is classically true) and the Principle of Countability. So as far as I’m concerned, this thread may now die. $^_^$

Posted by: Toby Bartels on November 17, 2006 12:36 AM | Permalink | Reply to this

Re: Foundations

“Only the final step is problematic; you assume that since this sequence can’t be infinite, then it must be finite. This is an example of LEM”

Wouldn’t that depend upon whether the condition on paths is expressed positively,as “every path is finite,” or negatively,as “no path is infinite”? In Marc Hamann’s formulation, it’s expressed positively, although I phrased the step as if it were expressed negatively (not having much experience with constructive math).

“but (in this context) it follows from Markov’s Principle (MP), a (very weak form of LEM accepted by (as the name implies) the Markovian school of constructivism(and also by at least one Brouwerian intuitionist).

“Furthermore, it’s easy to see that DUH (applied to denumerable trees) implies Markov’s Principle: Given any infinite sequence of 0s and 1s that is not all 0s, form an unbranching tree whose nodes are all initial segments that consist of
all 0s. Then DUH implies that this is finite”

Again, it seems to me that this is true if the condition on paths is expressed negatively, but not if it’s expressed positively.

Posted by: Adam Stephanides on November 24, 2006 8:48 PM | Permalink | Reply to this

Re: Foundations

To be honest, I’m getting more confused the more that I look at this. To respond to you, I have to look precisely at the definition of path, which then seems to expose a flaw in your argument (that MP —if even this is necessary— implies DUH for countable trees), wich I can fix by looking precisely at the definition of tree, which then casts doubt on my argument (that DUH implies MP), and I get all turned around.

Suffice to say: * DUH definitely follows from MP and the Axiom of Countability (even if MP is not actually necessary) without requiring any other form of AC or EM; * the necessity of MP depends carefully on details of definitions that have so far been unstated.

Since Marc probably believes in MP anyway (at least, it seems pretty common among constructivists motivated by computability issues —going back to Markov himself), I’m not going to worry about it.

Posted by: Toby Bartels on November 25, 2006 12:19 AM | Permalink | Reply to this

Re: Foundations

$MathML-enabled post (click for more details).$

Maybe everyone’s getting caught up on “paths” and “trees” when that’s not how the question originally arose. To wit:

Consider a hereditarily finite set. That is, a finite set all of whose elements are hereditarily finite. Foundation tells us that we can’t find an infinite path ${x_{i}}_{i \in Z}$ with $x_{i + 1} \in x_{i}$ for all $i$ . The question is: are there only a finite number of elements “in” the set at all?

Posted by: John Armstrong on November 25, 2006 2:47 AM | Permalink | Reply to this

Re: Foundations

This is a different question than the one you originally asked, though: the Axiom of Foundation states that any non-empty set S has a member disjoint from S, and without AC this is stronger than the “no infinite descending membership chain” principle.

In fact, your present question can be answered affirmatively without AC. Let S be the given set. Suppose T(S), the transitive closure of S (that is, the set of all members of S, all members of members of S, all members of members of members of S, and so on), is infinite. Then let S’ be the subset of T(S) containing those elements whose transitive closures are themselves infinite. By the same argument as in the usual proof of Konig’s Lemma, the set {S} U S’ contains no element disjoint from itself, contradicting the Axiom of Foundation.

If, in your original question, you replace the “no infinite paths” condition with “every subset of nodes contains a node which is not the parent of any node in that subset,” then we can similarly prove that the tree is finite without using AC.

It’s also easy to prove that “hereditarily finite” is equivalent to “having finite transitive closure” by transfinite induction, where it’s the full Axiom of Foundation that ensures that transfinite induction works.

Posted by: Adam Step

The n-Category Café

Skip to the Main Content

October 30, 2006

Foundations

Posted by David Corfield

Some Related Entries

132 Comments & 2 Trackbacks

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Choice.

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations

Re: Foundations