8
$\begingroup$

Stone duality may be understood as providing a duality between syntax and semantics for propositional logic, so that a theory may be recovered from its models. In order to do likewise for first-order logic, Mihaly Makkai in Stone duality for first-order logic, Adv. Math. 65 (1987) no. 2, 97–170 (doi:10.1016/0001-8708(87)90020-X), constructed an adjunction between pretoposes (syntactic categories of first-order theories) and ultracategories. Jacob Lurie recently used a slightly different notion of ultracategory and different proof strategy in his paper Ultracategories. A further scheme-theoretic approach to this duality is provided by Steve Awodey and students, see Sheaf Representations and Duality in Logic (arXiv:2001.09195).

In Appendix A of Spectral Algebraic Geometry, Lurie develops a higher-categorical version of the theory above:

the theory of bounded ∞-pretopoi ... seems to provide a good language for extending concepts of first-order logic to the ∞-categorical setting.

Hence the question:

Does any known kind of ‘logical’ theory have bounded ∞-pretopoi as syntactic categories?

Might homotopy type theory have something to do with this?

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ My understanding is that the direction Jacob Lurie is following is that you do need syntax to talk about theories and model: Here a "theory" is an $\infty$-pretoi a model is a functor presering finite limits and colimits, and you can formulate any question you would have about ordinary model theory in this language. The question of having a "syntactic presentation" while interesting is highly "model dependant" as a syntax corresponds to a concrete description of the $\infty$-categories under consideration (hence depends on what kind of $\infty$-categories you want to use). $\endgroup$
    – Simon Henry
    Apr 20, 2020 at 23:22
  • 2
    $\begingroup$ HoTT contains a lot of higher order logic, so it is not suitable for this purpose, but there should be some fragement of HoTT that can play the role you have in mind (basically plain dependent type theory with just some inductive type, including identity type, Sigma types, and some more producing the colimits you want)... But completely different syntactical approach can lead to the same result up to equivalence of $\infty$-category. $\endgroup$
    – Simon Henry
    Apr 20, 2020 at 23:25
  • $\begingroup$ Thanks, Simon. Would you be able to give an example of a completely different syntactical approach that could play this role? $\endgroup$
    – David Corfield
    Apr 21, 2020 at 8:11
  • 1
    $\begingroup$ Nothing concrete has been developed so far, so I can't give you something very concrete, but here is an example of something that could work: "Simplicial geometric logic". Take ordinary geometric logic, where each sort is replaced by a simplicial sort. Some adjustment need to be made: equality is weakened to homotopy in many place, so that the syntactic categories are simplicial categories with finite homotopy limit and homotopy colimits (using some concrete model for these). $\endgroup$
    – Simon Henry
    Apr 21, 2020 at 13:17
  • $\begingroup$ I see there is 'first-order homotopical logic', arxiv.org/abs/1908.08944; 'dependently typed first-order logic'; and, 'first-order logic with dependent sorts', arxiv.org/abs/1605.01586. $\endgroup$
    – David Corfield
    May 6, 2020 at 13:07

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.