[FOM] Pratt on categorical foundations

[Michael Lee Finney]

David Roberts kindly pointed me (offline) to some foundations that are
inspired by category theory, ETCS and SEARS.

I would say that both of them are coherrent, but ETCS is based on a
categorical viewpoint, and except for category theorists, is not
especially understandable. However, SEARS is reasonably understandable.

Both of these are structural set theories. If you regard set theory as
a theory of "packaging", where {...} is the packaging operator, then
the difference between SEARS and ZF is that once a set has been
formed in SEARS it may not be a member of another set. Otherwise, as understand it, ETCS, SEARS and ZF are
equivalent and SEARS-C and ZFC are equivalent in the sense that each
can be modelled in the other.

Given that, and the increased difficultly of working in SEARS (or
worse ETCS) I do not see the advantage.

So, coherrent - yes, simple - no. In my judgement, of course.

Btw, why isn't there an unpackaging operator? So that we have
something like b = {B} and B = }b{ . That could be useful and
interesting. Among other options, you could identify the contents of a
set with a type, where the types are ordered with a least type. If
that were included in the first order logical quantification then you
would have a useful form of restricted quantification. There are other
interesting options as well. I don't especially favor the type option,
but many theorists seem to like types.


Michael Lee Finney

P.S. Here are two of the links that he gave me

http://ncatlab.org/nlab/show/ETCS
http://ncatlab.org/nlab/show/SEAR


HF> Is categorical foundations of mathematics philosophically coherent in
HF> the sense that set theoretic foundations of mathematics is, or finite
HF> set theory for finite mathematics, or PA is for restricted kinds of
HF> mathematics?

HF> How does simplicity figure in to the discussion? How would you compare
HF> the simplicity of categorical foundations versus set theoretic  
HF> foundations?

HF> Harvey Friedman

HF> On Feb 20, 2012, at 3:23 AM, Vaughan Pratt wrote:

HF> On 2/18/2012 11:15 AM, Michael Lee Finney wrote:
>> Category theory has the problem that it is based on functions which
>> only exist inside of limited sets. Therefore, trying to apply category
>> theory to larger areas has foundational issues. Even if you define
>> functions using classes, you only move the problem back a step. There
>> are some attempts to use Category theory as the foundations instead of
>> Set Theory, but so far as I know they have either not been succesful
>> or very awkward. I haven't gotten into category theory much, so I
>> can't give you any references here. I only care about it relative to
>> foundational issues.

HF> I would say category theory suffers much less from these sorts of
HF> technical problems than from the pedagogical problem of being two
HF> steps removed from logic.  These steps are not necessarily easily
HF> taken by those accustomed to thinking of every mathematical object as
HF> a set that is uniquely determined by those entities of the  
HF> mathematical universe that belong to it, as the heated debates here
HF> back in 1998 about the relevance to FOM of category theory made clear.

HF> The first step away from quantificational logic is to algebra.  This
HF> step shifts the emphasis from truth-valued sentences to mathematical
HF> objects denoted by terms valued in one or more domains of individuals.
HF> Equality emerges as the dominant relation, and functions fill in for
HF> existential quantification.

HF> Syntactically one can always skolemize, but the line between syntax
HF> and semantics is not as sharp in algebra as in logic.  Many operations
HF> arising in a given branch of mathematics that we take for granted as
HF> integral to the algebraic language of that branch might just as well
HF> be considered skolem functions derived from a formalization of that
HF> branch based on a logical language consisting of only a few  
HF> fundamental relations.

HF> The statement that f: A --> B is a bijection is a basic example for
HF> set theory as such a branch of mathematics.  In logic this property is
HF> expressed by saying that for all a,a', f(a) = f(a') implies a = a' (f
HF> is injective), and for all b there exists a such that f(a) = b (f is
HF> surjective).  Algebra skolemizes the existential quantifier in this
HF> definition of surjectivity by introducing the inverse f': B --> A into
HF> the language as an equal partner with f and restating the bijection
HF> property as the identities f'(f(a)) = a and f(f'(b)) = b.

HF> The second step is from algebra to category theory, which dispenses
HF> with the distinctions between elements and functions and between  
HF> application and composition.  It is hard to overestimate the value of
HF> this simplification, as I'll try to demonstrate with some examples
HF> from topos theory, which is just a small corner of category theory.
HF> My apologies in advance for the length, but my experience has been
HF> that merely listing the topos axioms conveys the subject about as well
HF> as E = mc^2 conveys general relativity.

HF> The bijection example can be simplified to f'f = 1_A: A --> A and ff'
= 1_B: B -->> B where 1_A and 1_B denote the identity functions on  
HF> respectively A and B.  Each equation constitutes a commutative diagram
HF> that eliminates elements and application altogether.

HF> But these equations can also be written f'fa = a and ff'b = b where a:
S -->> A is understood as an element of A of sort S, and likewise b: T
-->> B as an element of B of sort T.  This looks more like algebra,  
HF> except that a and b are now morphisms at the same level as f and g,
HF> application is realized as composition, and the shorter equations
HF> above can be recovered by canceling a and b on the right of their
HF> respective equations.

HF> This way of thinking simplifies the type structure of algebra by  
HF> eliminating the element-function distinction and the application- 
HF> composition distinction.  But it does far more than just that, by
HF> cleanly introducing a notion of sort.

HF> For set theory as a (rather degenerate) branch of mathematics there is
HF> only one sort of element, namely the atom, whose sort can be  
HF> identified with the singleton 1.  Up to isomorphism every set is  
HF> simply a sum (disjoint union, coproduct) of atoms, one for each element.

HF> Graph theory as another branch of mathematics is a slight but very
HF> important extension of set theory.  Whereas sets contain only atoms,
HF> graphs contain vertices (which work like atoms) and edges (whose  
HF> incidence relations are mediated by vertices).  There are sorts V for
HF> vertices and E for edges, identifiable with respectively the one- 
HF> vertex graph with no edges and the two-vertex graph with a single edge
HF> connecting them, just as we identified the sort "atom" of set theory
HF> with the singleton set 1.  A vertex of G is a morphism v: V --> G
HF> while an edge is a morphism e: E --> G.  The two vertices of E  
HF> manifest as the two morphisms from V to E, since vertices of G are
HF> morphisms from V to G.

HF> As stipulated, V has no edges.  Hence there cannot be a morphism from
HF> E to V, making this the category of irreflexive graphs.  (To digress
HF> for a moment, for reflexive graphs V would have an edge in the form of
HF> a morphism to it from E, necessarily representing a self-loop in V.
HF> This morphism would have the evident compositions at each end with
HF> each of the two morphisms from V to E, namely the identity function
HF> 1_V at one end and the two non-identity retractions on E at the other.)

HF> But whereas a set is just the disjoint union of its atoms, a graph is
HF> more than just the disjoint union of its vertices and edges.  The
HF> notion of incidence in a graph demands some quotienting, namely that G
HF> be the result of identifying certain endpoints of its edges.  That is,
HF> whereas the category of sets up to any given size is just the closure
HF> of the category containing the singleton 1 under sums (coproducts) up
HF> to that size, the category of graphs must be the closure of V and E
HF> under colimits, not just coproducts.  Unlike coproducts, colimits must
HF> take the possibility of quotienting into consideration or the only
HF> graphs we would obtain would be isolated edges with twice as many
HF> vertices as edges, aka the *free* graphs generated by pairs of sets.

HF> The singleton set 1 of set theory is not forgotten in graph theory
HF> however.  It has a counterpart among graphs, namely the *final* graph
HF> 1 with one vertex and one edge, a self-loop.  For any graph G there is
HF> an evident unique morphism !_G: G --> 1.  (For the category of  
HF> reflexive graphs, V coincides with 1, but not for that of irreflexive
HF> graphs.) The fact that 1 contains an edge will play a very important
HF> role in 11 paragraphs time (apologies that this message is so long).

HF> The identification of elements with functions extends to yet other
HF> very convenient identifications, namely of pairs (more generally n-
HF> tuples) with functions, and likewise subsets with functions.

HF> In the category of sets, an n-tuple of A is simply a morphism from n
HF> to A where n = 1 + 1 + ... + 1 is any n-element set.  The elements of
HF> n constitute the coordinates of the n-tuple.  A canonical choice of n
HF> is {0,1,...,n-1} as a subset (TBD below) of the set N of natural  
HF> numbers.

HF> Pairs arise as the case n = 2.  Writing Hom(A,B) for the (hom)set of
HF> morphisms from A to B, we have the bijections Hom(1+1, A) ~ Hom(1, A)
HF> x Hom(1, A) ~ Hom(1, AxA) (as a consequence of the homfunctor Hom:
C^op x C -->> Set preserving limits in both arguments, bearing in mind
HF> that the colimit 1+1 in C becomes the limit 1x1 in C^op).  These two
HF> bijections (however chosen) create a bijection between the elements of
HF> A of sort 1+1, i.e. the pairs of A, and the elements of AxA of sort 1,
HF> i.e. the atoms of AxA.

HF> A subset B of A with n elements differs from an n-tuple in two  
HF> respects: no element of A can be repeated in B, and order is  
HF> immaterial (indexing is disabled).

HF> The first property is easily achieved by taking an n-element subset of
HF> A to be an n-tuple of A, as a morphism from n to A, which is injective
HF> (more generally a monomorphism or monic, as a suitable generalization
HF> of "injective").

HF> The second property is a little more delicate.  It can be achieved via
HF> the notion of *subobject* of A as an equivalence class of isomorphic
HF> injections to A.  Two injections are isomorphic when their domains and
HF> images are both isomorphic, a condition formalizable with the  
HF> appropriate commutative diagram (exercise).  A set with m elements has
HF> 2^m subobjects, aka subsets, with C(m,n) of them having domains with n
HF> elements where C(m,n) is a binomial coefficient.

HF> Most of this carries over to graphs. It should come as no surprise
HF> that one can form n-tuples of graphs in the obvious way.  More  
HF> interesting is how subobjects of graphs, aka subgraphs, are formed, by
HF> analogy with subgraphs.

HF> One can form a subset B of A by deleting its complement relative to A.
HF> This process can be expressed via the characteristic function of B,
HF> namely the function ?_B: A --> 2 = {0,1} sending the elements for
HF> deletion to 0.

HF> A subgraph G' of G is not so easily formed.  In order to delete any
HF> vertex one must first delete all edges incident on it.  The  
HF> counterpart of the set 2 = {0,1} for graphs has the same vertices,
HF> namely {0,1}, but the corresponding set of two edges can only exist at
HF> vertex 1, since if either vertex of an edge is missing (the case of
HF> vertex 0), there is only one possibility for the edge, namely that it
HF> must be missing too.

HF> It follows that the graph Omega (as we shall call the *subobject  
HF> classifier*) playing the role of the set {0,1} has vertices {0,1}, and
HF> one edge between every pair of vertices (denoting a missing edge)
HF> except from 1 to 1, which permits two edges denoting presence or  
HF> absence of an edge at the corresponding place in G'.  That is, Omega
HF> is the directed clique K_2 with a fifth edge from 1 to 1.

HF> It follows that there are three morphisms from 1 to Omega.  The least
HF> one maps the vertex of 1 to the 0 vertex of Omega, and therefore maps
HF> the edge of 1 to the unique edge at that vertex.  The other two map
HF> the vertex of 1 to the 1 vertex of Omega, which has two edges to which
HF> the edge of 1 can be mapped, and these are ordered so that absent is
HF> below present for edges, as usual in the inclusion ordering.

HF> These three graph morphisms play the role for graphs that the two
HF> morphisms from the set 1 to the set 2 = {0,1} play for sets.  Just as
HF> the latter defines a two-valued logic, so do the former define a three-
HF> valued logic forming a linear order.

HF> The category of graphs is an instance of a presheaf category, which in
HF> turn is an instance of a topos.  In any topos the atoms (the 1-sorted
HF> elements, as distinct from the V-sorted and E-sorted elements) of
HF> Omega have an evident ordering by inclusion of subobjects so as to
HF> form a poset.  In every topos the atoms of Omega form a Heyting  
HF> algebra under this ordering.  They constitute the truth values of the
HF> internal logic of that topos.

HF> There is only one Heyting algebra with two elements, namely the two-
HF> element Boolean algebra, corresponding to the idea that the internal
HF> logic of set theory is Boolean.  There is likewise only one Heyting
HF> algebra with three elements, and it cannot be a Boolean algebra (which
HF> in the finite case must have cardinality a power of 2), corresponding
HF> to the idea that the internal logic of graph theory, as defined by the
HF> notion of subgraph by analogy with subset, is intuitionistic but not
HF> classical.

HF> Statman has shown that general intuitionistic logic is PSPACE- 
HF> complete.  The internal logic of graph theory however is essentially
HF> no harder than that of set theory, being coNP-complete.  This is  
HF> because failure of P = TOP (the topmost of the three truth values) can
HF> be witnessed by assigning one of three values to each variable of P
HF> and then evaluating P in linear time.   This does not work for general
HF> intuitionistic logic, for which counterexamples and their truth tables
HF> are in general massively larger.

HF> All this is one tiny little corner of category theory, a very rich and
HF> well-developed subject that comes nowhere near deserving Michael  
HF> Finney's characterization of it as: "There are some attempts to use
HF> Category theory as the foundations instead of Set Theory, but so far
HF> as I know they have either not been succesful or very awkward."

HF> Awkwardness is in the eye of the beholder.  Active users of category
HF> theory find it far from awkward, combining great conceptual economy
HF> with great expressive power.

HF> Vaughan Pratt


HF> _______________________________________________
HF> FOM mailing list
HF> FOM at cs.nyu.edu
HF> http://www.cs.nyu.edu/mailman/listinfo/fom