5
$\begingroup$

I have been reading this discussion by John Baez and Michael Weiss and I find this approach to model theory using boolean hyper-doctrines very interesting. One of their goal was to arrive at a proof of Godel's completeness theorem in this language, which I was very hyped for, but unfortunately, it seems like they never really finished that series of blog posts.

I was therefore wondering if there is any other place where I can read further on classical first-order model theory done in the categorical language of hyperdoctrines. I am not a logician at all, so I'm looking for something fairly introductory that doesn't already assume a good knowledge of model theory.

Improve this question
$\endgroup$
5
  • $\begingroup$ The nLab article on Goedel incompleteness takes a hyperdoctrinal approach. $\endgroup$
    – Todd Trimble
    Commented Jan 11 at 16:09
  • $\begingroup$ @ToddTrimble That's the incompleteness theorem. This question is about the completeness theorem, which nLab doesn't seem to have a very complete article on. $\endgroup$
    – James E Hanson
    Commented Jan 11 at 17:14
  • $\begingroup$ @JamesHanson Golly, I'm aware of that, and it's why I didn't post my comment as an answer, but just as a possible point of interest. $\endgroup$
    – Todd Trimble
    Commented Jan 11 at 17:21
  • $\begingroup$ @ToddTrimble Ah, sorry, it's just a fairly common confusion. $\endgroup$
    – James E Hanson
    Commented Jan 11 at 17:24
  • $\begingroup$ Lawvere's notion of hyperdoctrine is very heavy machinery, incorporating dependent types but also restricting to a logic similar to that of $\mathbf{Set}$ (or a topos). The most important point is that the quantifiers $\forall$ and $\exists$ are the right and left adjoints to (Lawvere said substitution, but more accurately) weakening. Weakening means pretending that a formula involves more variables than actually appear in it. By the way, classical logic doesn't simplify anything. $\endgroup$
    – Paul Taylor
    Commented Jan 15 at 13:42

0

Reset to default

You must log in to answer this question.