[FOM] Friedman/Pratt reversed

[Michael Lee Finney]

>>> Repost due to quoting errors. <<<

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.

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

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

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

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

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

VP> 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  
VP> respectively A and B.  Each equation constitutes a commutative diagram
VP> that eliminates elements and application altogether.

VP> 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,  
VP> except that a and b are now morphisms at the same level as f and g,
VP> application is realized as composition, and the shorter equations
VP> above can be recovered by canceling a and b on the right of their
VP> respective equations.

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

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

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

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

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

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

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

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

VP> Pairs arise as the case n = 2.  Writing Hom(A,B) for the (hom)set of
VP> morphisms from A to B, we have the bijections Hom(1+1, A) ~ Hom(1, A)
VP> 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
VP> that the colimit 1+1 in C becomes the limit 1x1 in C^op).  These two
VP> bijections (however chosen) create a bijection between the elements of
VP> A of sort 1+1, i.e. the pairs of A, and the elements of AxA of sort 1,
VP> i.e. the atoms of AxA.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

VP> Vaughan Pratt