Re: size_question

["F. William Lawvere" <wlawvere@hotmail.com>]

In the absence of AC, we need to specify which notions of"finite" we are using. Certainly K-S (= locally quotient of standard numeral) while important is by no means the endof the story. We categorists do not seem to yet have a way of dealing  elegantly with the locally Noetherian, coherent,etcsheaves in terms of internal finiteness notions.
The SUBQUOTIENTS of standard numerals would surely be important. I recall the existence of intuitionist literature on this, but it seemed to assume that subquots of subquots etc would be an infinite sequence. Of course in a  category with reasonable pullbacks and pushouts this relation is already transitive (indeed an important subcategory of spans).
  But the original question actually had to do with the observation that for any qualitative definition of finite set, there are probably as many as there things in the ambient universe. We need an axiom of infinity to say that there is a category object that represents that metacategory UP TO EQUIVALENCE OF COURSE. 
The uniqueness is only relative to the ambient universe . The Incompleteness Theorem would seem to imply that there are an infinite number of non-elementarily-equivalent ambient universesand hence of these little metacategories in particular.
We really should overcome the ritual belief that such things must be defined by iteration (as opposed to being partially investigated via iteration). Already Peano misrepresented Grassmann's views on this.
Dedekind proposed that a set  A is finite if any idempotent whose fixed part is isomorphic to all of A is itself an automorphism. This seems difficultto relate to operations such as product. However note that it is an elementary axiom to require that all objects of a given topos satisfy it. It would see to propagate to any finite (in the sense of Artin) topos over such. Do basictheorems, such as the essentialness  of all geometric morphisms, extend to this axiomatic setting ?
A different elementary axiom on a topos is the requirement that every object A is fixed by the monad obtained by composing 3^( ) with its adjoint from the related topos of left actions of 3^3.
Are these two theories equivalent ? Such a finitely-axiomatized T defines "the" category of finite sets as any one that represents up to equivalence the submetacategory of the ambient universe consisting of all discrete categories that are finite in the stated sense.( But then of course there are many  models of T not equivalent to that)
I proposed the study of such an "Objective Number Theory" in Braga four years ago at a European computer science meeting without much response. It is known since Craig-Vaught that Peano's arithmetic can be embedded in a finitely axiomatizable theory,but it seems reasonable to try to find such an expansion with an objective content.If E is such a category, the Paris-Harrington theory seems to be about the topos E^Iwhere I is the arrow category; but don't the properties of that follow from those of E ?
Bill
PS Of course this ONT is not the same as (though related to) my ongoing  work with Schanuel and Menni.
> Date: Sat, 2 Jul 2011 22:05:05 +0200
> From: streicher@mathematik.tu-darmstadt.de
> To: andrej.bauer@andrej.com
> CC: jlipton@wesleyan.edu; categories@mta.ca
> Subject: categories: Re: size_question
> 
>> I should think that the hereditarily finite sets do not depend all
>> that much on the background setting. After all, there are not very
>> many of them and they are quite concrete. Can they really be hugely
>> different depending on whether we work in ZF, ZFC, IZF, CZF etc?
> 
> If we are not working classically subsets of finite sets need not be
> finite but the sets in V_\omega are closed under subsets.
> 
> Thomas

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]