🚀 go-pugleaf

Several weeks ago I posted a request for further pointers to
the literature on the relationship between predicate logics,
topology, and geometry as described in Steven Vickers' book, 
"Topology Via Logic". I summarize two of the responses and 
all of the references I received below. My thanks to those who 
kindly provided this information (and their words of encouragement).

*Justin Pearson (U of Kent at Canterbury U.K.) writes, in part:

> ... The geometric input to Vickers work comes from work that 
> Johnstone did, on Local theory and stone spaces. The stone 
> duality theorem gives you a geometric way of thinking about 
> certain algebraic objects. All this can be tied together by 
> something called sheaf theory. I suppose the best way get an 
> understanding is to think of the history. Sheaf theory, comes 
> from Algebraic topology, it is an essenatially geometric 
> construct. Algebraic toplogy as devoloped by Gothendick etal. 
> gives us the Gothendick topoi. When people started to look at 
> catogriacal logic, all the same constructions started appearing, 
> sheafs, topoi, etc....
> ...Another way of thinking about it (this is not formal but only 
> a way of thinking about it).
> Theorys of Logic are modeled by Topoi,
> Theorys of geometry are also modeled by Topoi.
> SO the connection comes in at the top...

*William Boshuck (Dept of Math, McGill U) writes, in part:

> ...geometric logic. Roughly speaking, the theories are theories 
> in infinitary first order logic which allows the formation of finite
> conjuncitons and arbitrary disjuctions of formulas, as well as existential 
> quantification over finitely many variables (formulas in this fragment 
> are only allowed to have a finite number of free variables .... this of 
> course imposes a restriction on the disjunctions metioned above). This 
> is the part corresponding to the propositinal geometric logic you mentioned.
> The notion which corresponds to the 'Lindenbaum-Tarski' construction which,
> in your case is a frame (also called locale, complete heyting algebra, or
> even just space by some) is that of Grothendieck topos. Unfortunately, the 
> literature in this is pretty inaccessible. First, here is the idea. 
> There is a further step one can take when we replace the opens of a space
> with a frame. Namely to relax the requirement that the entity we wind up 
> with is a partially (or pre-) ordered set to the requrement that it be 
> a category. In this broader generality, the finite meets are replaced
> by finite limits, and joins are replaced by colimits. When some 
> exactness conditions (='identities') are imposed (as well as another
> sort of smallness condition which is best not to go into right now) which
> are analogous to the laws requred in frames are imposed, we arrive at the
> notion of G(rothendieck) topos. A theorem (by Giraud) tells us that these
> are exactly the categories which are obtained by a 'Lindenbaum-Tarski'
> typo type construction from the theories mentioned above...
> Also, I think that the idea of the elements of a locale goes back before
> the Smyth guy you mention. The general idea is related to the forcing 
> constructions of Paul Cohen (the independence ot the continuum 
> hypothesis). The idea of elements of a frame as finitary conditions
> of some abstract thing was made explicit by Fourman and Grayson (if not
> before) in a paper called Formal Spaces which was in some logic proceedings
> or other around 1980 (probably can be tracked down in the math reviews).

*Bibliography received - WARNING: These references are clipped verbatum 
 (almost) from the original replies, and most are incomplete. Some digging 
 will be required (I'm currently in this mode). 

 Abramsky: 
    Direct FTP from Imperial College theory.doc.ic.ac.uk" (146.169.2.37)
    log in as "ftp" or "anonymous" with your email address as password
    Papers are now found in, eg,	/theory/papers/Abramsky/cill.dvi.Z
    PK files are in, eg,		/tex/fonts/pk/300/cmbx14.pk

 Artin, Grothendieck, and Verdier, SGA4 Cohomologie des schemas et 
    .... theories des topos.... ?, Lecture Notes in Mathematics 269, 270

 Barr, M., Wells, C., Toposes, Triples, and Theories, Springer

 Golblatt, Topoi a categorical analysis of Logic

 Johnstone, P.T., Topos Theory, Academic press

 Johnstone, P.T., Topos Theory, Academic press

 Lambek, J., Scott, P., Introduction to Higher Order Categorical Logic

 Makkai M., Reyes, G.E., Lecture Notes in Mathmatics 611, Springer

 Vickers, S., Topology Via Logic, 1989, Cambridge University Press, 
    ISBN 0 521 36062 5

*For those interested, Irving H. Anellis (Editor at Modern Logic 
 Publishing) also provided a number of historical references on the 
 use of the logic of relations to treat geometric constructs:

 'A Memoir on the Theory of Logical Form,' Philosophical
 Transactions of the Royal Society 177 (1886), 1-70;
 'Note to "A Memoir on the Theory of Logical Form'."
 Proceedings of the Royal Society of London 42 (1887), 193-
 196;
 'On the Relation Between the Logical Theory of Classes and
 The Geometrical Theory of Points,' Proceedings of the London
 Mathematical Society 21 (1889-1890), 147-182;
 'On the Subject-Matter of Exact Thought,' Nature 43 (1890),
 156-162.
 Josiah Royce's paper 'The Relation of the Principles of Logic
 to the Foundations of Geometry,' Transactions of the American
 Mathematical Society (1) 24, 353-415. 
 R.C. Lyndon's paper "Relation Algebras and Projective Geometry,'
 Michigan Math. Journal 8 (1961), 21-28.