doctrine of classical first-order theories?

on the one hand, i'd like to think about whether there's a doctrine (in the sense that i've been defining it recently) of "classical first-order theories" (by which i really mean something like "classical first-order theory as conceived of by category-theorists", probably a bit different from how some logicians conceive of such theories).

(for this purpose it might be a good idea to look at the books by makkai and reyes and by makkai and pare, and at that section on "doctrines" in that logic handbook...)

on the other hand, i'd also like to think about the doctrine whose syntactic (groupoid-enriched) category is the opposite of the category of finitely presented groupoids (or something like that). i mentioned this doctrine to baez today as perhaps having its theories be equivalent to something like classical first-order theories, but when we discussed it further things seemed to get a bit more complicated.

hmm, the objects of the syntactic category of a doctrine of "classical first-order theories" should be something like "finitely axiomatized classical first-order theories"...



also i'd like to think about pro-finite groupoids (or something like that) and whether these give theories of the doctrine just mentioned.

anyway, suppose that i have a "classical first-order theory" (in a certain sense which i'll try to clarify as i proceed here). i should be able to extract from it a groupoid of "formulas"...