-
-
->>Or is it just that groupoids are needed for the deep homotopy
->>connection?
-
->that's part of my motivation by now, but i think my original
->motivation had less to do with the "dictionary" that relates groupoid
->theory to a special part of homotopy theory than with a different but
->in its own way equally powerful "dictionary" relating groupoid theory
->to a special kind of predicate logic.  in the world of predicate logic
->there's an obvious sense in which adding extra "properties" to the
->models of a theory means adding new axioms to the theory, adding extra
->"structure" to the models means adding new predicate symbols (possibly
->supplemented by new axioms) to the theory, and adding extra "stuff" to
->the models means adding new "types" (possibly supplemented by new
->predicate symbols and axioms) to the theory.  this
->property/structure/stuff distinction in predicate logic matches
->perfectly the property/structure/stuff distinction in groupoid theory
->if groupoids are interpreted as a certain sort of logical theories in
->a certain way.
-
-OK, I tried to think about this, but I don't really know where to
-start.  Give me a clue: what famous groupoid corresponds to what I've
-been taught to regard as the basic predicate calculus: ordinary logic
-with forall, forsome, and equality?

the correspondence is between individual groupoids and individual
_theories_ of a particular form of predicate logic.  the particular
form of predicate logic involved is pretty much just "the basic" form,
with the allowed syntactic constructions including:

1.  the usual finitary boolean connectives obeying the usual finitary
boolean equational laws

2.  the universal quantifier "for all" (and therefore also the
existential quantifier "for some" via the equivalence between "for
some x, p(x)" and "not (for all x, (not p(x)))")

3.  the built-in binary predicate "equality" with it's usual built-in
reflexivity, symmetry, transitivity, and substitutability properties

plus one more construction going beyond what's ordinarily considered
"the basic":

4.  the restriction in #1 above against the _infinitary_ boolean
connectives (such as n-fold conjunction for an arbitrary infinite
cardinality n) is lifted.

given a theory t expressed in this kind of logic, we obtain the
groupoid of models of t.  when all the i's are dotted and the t's
crossed in the right way, this process of passing from the theory t to
the groupoid of models of t becomes a "bi-equivalence from the
bi-category of theories to the bi-category of groupoids".

for example, let t be the theory presented by giving no predicate
symbols, plus the one axiom "there are exactly seven things".  (of
course this axiom can be expressed using the allowed syntatic
constructions.)  the groupoid of models of t is the groupoid of
seven-element sets.  this groupoid has just one isomorphism class
because the theory t is "categorical" (in a sense of the word
"categorical" having not much relationship to category theory!).

that's not a complete exposition of the situation, rather just a clue
of the sort i hope you wanted.  i will mention further though that to
develop the full correspondence between theories and groupoids, the
theories should be allowed to be "multi-typed".  if only
"single-typed" theories are considered then the most straightforward
correspondence is not with "abstract" groupoids but rather with
"concrete" groupoids, a "concrete groupoid" being a groupoid equipped
with a faithful functor to the groupoid of sets.  it might be a good
idea to develop the correspondence between single-typed theories and
concrete groupoids before developing the full correspondence between
multi-typed theories and abstract groupoids.  one of the basic lemmas
you should try to understand is as follows:

let x be a set.  let c be the collection of all pairs (s,p) with s a
(possibly infinite) set and p an s-ary relation on x.  let d be the
hyper-collection of all sub-collections of c that are closed under all
of the operations on relations alluded to in #1-#4 above.  then d is
in canonical bijection with the set of subgroups of the group of
permutations of x (taking "permutation" to mean "auto-bijection").

(in the above lemma, among the operations that should count as
"alluded to" is the operation of replacing an s-ary relation by the
obvious corresponding t-ary relation given a bijection from s to t,
even though this operation was perhaps _not_ very explicitly alluded
to.)