Logic in Topoi: Functorial Semantics for High-Order Logic

Dissertation, The University of Chicago (1997)
  Copy   BIBTEX


The category-theoretic notion of a topos is called upon to study the syntax and semantics of higher-order logic. Syntactical systems of logic are replaced by topoi, and models by functors on those topoi, as per the general scheme of functorial semantics. Each logical theory T gives rise to a syntactic topos ${\cal I}\lbrack U\sb{T}\rbrack$ of polynomial-like objects. The chief result is the universal characterization of ${\cal I}\lbrack U\sb{T}\rbrack$ as a so-called classifying topos: for any topos ${\cal E},$ the category ${\bf Log}$ of logical morphisms ${\cal I}\lbrack U\sb{T}\rbrack\to{\cal E}$ is naturally equivalent to the category ${\bf Mod}\sb{T}$ of models of T in ${\cal E}$,$${\bf Log}\simeq{\bf Mod}\sb{T}.$$In particular, there is a T-model $U\sb{T}$ in ${\cal I}\lbrack U\sb{T}\rbrack$ such that any T-model in any topos is an image of $U\sb{T}$ under an essentially unique logical morphism. In this sense, ${\cal I}\lbrack U\sb{T}\rbrack$ is freely generated by this "universal" model $U\sb{T}$ of T. ;Having cast the principal logical notions in familiar algebraic terms, it becomes possible to apply standard algebraic and functorial techniques to some classical logical topics, such as interpolation, definability, and completeness. For example, a well-known theorem of Grothendieck states that every commutative ring is isomorphic to the ring of global sections of a sheaf of local rings. A similar sheaf representation theorem for topoi is proved using the theory of stacks and indexed categories. Combining this result with the classifying topos theorem, one can infer the completeness of higher-order logic with respect to certain topoi that are much like Sets. A stronger version of the classical Henkin completeness theorem for higher-order logic follows as a corollary.



    Upload a copy of this work     Papers currently archived: 76,391

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Topological completeness for higher-order logic.S. Awodey & C. Butz - 2000 - Journal of Symbolic Logic 65 (3):1168-1182.
Classifying toposes for first-order theories.Carsten Butz & Peter Johnstone - 1998 - Annals of Pure and Applied Logic 91 (1):33-58.
Syntax and Semantics of the Logic.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
Relativized Grothendieck topoi.Nathanael Leedom Ackerman - 2010 - Annals of Pure and Applied Logic 161 (10):1299-1312.
What is an inference rule?Ronald Fagin, Joseph Y. Halpern & Moshe Y. Vardi - 1992 - Journal of Symbolic Logic 57 (3):1018-1045.
The Theory of Form Logic.Wolfgang Freitag & Alexandra Zinke - 2012 - Logic and Logical Philosophy 21 (4):363-389.
Normality and p(κ)/j.R. Zrotowski - 1991 - Journal of Symbolic Logic 56 (3):1064-1067.
Syntax and Semantics of the Logic $\mathcal{L}^\lambda_{\omega\omega}$.Carsten Butz - 1997 - Notre Dame Journal of Formal Logic 38 (3):374-384.
Concepts of Logical Consequence.Darcy Allen Cutler - 1997 - Dissertation, The University of Western Ontario (Canada)


Added to PP


6 months

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Author's Profile

Steve Awodey
Carnegie Mellon University

References found in this work

No references found.

Add more references