# Can logic be significantly geometrised?

Descarte has been lauded for putting together geometry and algebra, and his achievement allowed the invention of calculus by Leibniz & Newton and allowed its efficacious and explosive development by subsequent mathematicians & physicists in contrast to the rudimentary and primitive steps taken by Archimedes in integration and the Keralan school in power series.

Now various propositional Logic can be algebraised:

classical propositional logic -> boolean algebras

intuitionistic propositional logic -> heyting algebra

modal logic -> modal algebra

The question: is there a significant geometric form of these logics? Significant, simply in not being just a translation into geometric form, as in Venn Diagrams for boolean algebras (first being represented as some system of sets), but that allows for something deeper to be said about logic itself?

There is of course the Stone representation for a Boolean Algebra, but what does this significantly say about logic?

• There are strong connections between model theory and algebraic geometry, that have been exploited successfully in recent years. Sep 26 '13 at 5:32

One direction you could explore is mapped out e.g. by Saunders Mac Lane and Ieke Moerdijk's Sheaves in Geometry and Logic: A First Introduction to Topos Theory (Springer, 1992). Their Prologue begins

A startling aspect of topos theory is that it unifies two seemingly wholly distinct mathematical subjects: on the one hand, topology and algebraic geometry, and on the other hand, logic and set theory. Indeed, a topos can be considered both as a "generalized space" and as a "generalized universe of sets" ...

Another direction you could explore is Homotopy Type Theory -- here is an introductory paper by Steve Awodey: http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf His opening words are

The purpose of this informal survey article is to introduce the reader to a new and surprising connection between Geometry, Algebra, and Logic, which has recently come to light in the form of an interpretation of the constructive type theory of Per Martin-Löf into homotopy theory, ...

So those are two initial pointers to areas where deep geometry/logic connections are indeed made.

But -- and it is rather a big 'but'! -- these are mathematical investigations at a level of conceptual sophistication and difficulty that go far beyond that of introductory mathematical logic. Are there more elementary geometry/logic links to be made, at a comparable level of sophistication/difficulty to the material in a standard logic text like Enderton's or van Dalen's, say? That's an interesting question, but nothing springs immediately to my mind ...

• Thanks. Awodey, in his paper points out that the application of geometry, in this form, resulted in'sheaf-theoretic independence proofs [ie forcing], topological semantics for many non-classical systems, and an abstract treatment of realizability', he also considers that roughly, 'a higher topos is to homotopy what a topos is to topology' which I think is a nice slogan. Sep 26 '13 at 10:04