Where does the name "geometric theory" come from?

Question

In mathematical logic, where does the adjective "geometric" comes from, in terms like "geometric theories" and "geometric logic"?

These terms come up in fields like topos theory, e.g. in works such as the following:

The unification of Mathematics via Topos Theory

Answer 1

This answer is CW, so I don't gain reputation for someone else's work.

To quite Kevin Arlin's answer to the same question on math.stackexchange:

Geometric logic constitutes the logic, models of whose theories are preserved by geometric morphisms between topoi. Geometric morphisms are those appropriate to toposes viewed as generalized spaces, for instance, identifying the topos of sheaves on a topological space, or on a locale, with the space itself. Historically, toposes were first introduced by Grothendieck's school to model generalized algebro-geometric spaces, which explains why these morphisms are called geometric, rather than topological.

Answer 2

Negri and collaborators call "geometric" theories that can be axiomatized by FOL formulas of a special sort, namely universal closures of $A\to B$, where $A$ and $B$ do not contain $\to$ or $∀$, see e.g. Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. The terminology goes back to, at least, Constructivism in Mathematics by Troelstra and van Dalen (1988), where it is used in exercise 2.6.14. Such theories have particularly nice proof theory, e.g. a classical proof of a geometric implication in a geometric theory can be transformed into a constructive proof (Barr's theorem). This was originally proved in what they call "classical geometric theories" modeled in Grothendieck topoi, hence the name:

"Examples of geometric theories are given by Robinson arithmetic, the theory of constructive plane affine geometry, the theory of ordered fields and of real closed fields... In the last section we apply our method to a general result on geometric theories. The result states that if a geometric implication is provable classically in a geometric theory, then it is provable intuitionistically.

This result is proved in topos theory by using a completeness theorem for geometric theories in Grothendieck topoi and the construction of a suitable Boolean topos out of a Grothendieck topos. By our method, the result reduces to a proof-theoretical triviality: A classical proof of a geometric implication in a geometric theory formulated as a sequent system with rules is an intuitionistic proof already."

The name is doubly apt since a recent formalization of Euclidean geometry by Avigad, Dean and Mumma, that attempts (unlike Hilbert's) to mirror Euclid's proofs as closely as possible, is (nearly) geometric in the above sense, and their proof of its completeness uses Negri's results:

"Those geometric formulas with only a single disjunct in the consequent (i.e. geometric formulas in which $∨$ does not appear) are called regular. Note that, on our modeling, Euclid’s propositions are almost of this latter form, the difference being that arbitrary literals (negated atomic formulas as well as atomic formulas) are allowed in the antecedent and consequent. Sara Negri [42], building on earlier joint work with Jan von Plato [43], has established a cut-elimination theorem for geometric theories that we can put to use in our completeness proof."

Answer 3

The geometry in geometric theories, as in topoi, comes from topology and hence also the name topos. They, that is the topoi, are seen as generalisation of a topology. This generalisation was by Grothendieck and generalises that of a topological covering which is, in his language, a sieve. And in this way we get elementary topoi, which was lawvere's axiomatisation of Grothendieck topoi, that is of sheaves on the poset of opens of underlying topological space, reverse ordered by inclusion.

Every topos has an internal language as generally seen in the underlying language of logic and it turns out that each topos has an intuitionistic logic.

Generally, in mathematics, geometry refers to the metric as this is used to measure distances and angles; here, it refers to the aspect of continuity of geometry and hence the geometric moniker.

Given that each topos has a logic, this is why these logics are termed geometric logic.