[FOM] Friedman/Pratt reversed

[David Roberts]

I would like to just correct a point Michael made. ETCS is equiconsistent
with BZC, SEAR is equiconsistent with ZF and SEAR-C is strongly equivalent
to ZFC.

David Roberts
On Feb 23, 2012 7:34 AM, "Michael Lee Finney" <michael.finney at metachaos.net>
wrote:

> >>> 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
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20120223/96e26710/attachment-0001.html>