[FOM] Friedman/Pratt reversed
Michael Lee Finney
michael.finney at metachaos.net
Wed Feb 22 15:12:39 EST 2012
>>> 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
More information about the FOM
mailing list