First-order homotopical logic

Intuitionistic first-order logic was interpreted in Martin-Löf type theory (MLTT) [\textit{P. Martin-Löf}, in: Twenty-five years of constructive type theory. Oxford: Clarendon Press. 127--172 (1998; Zbl 0931.03070)], which was interpreted homotopically in simplicial sets [\textit{S. Awodey} and \textit{M. A. Warren}, Math. Proc. Camb. Philos. Soc. 146, No. 1, 45--55 (2009; Zbl 1205.03065); \textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, J. Eur. Math. Soc. (JEMS) 23, No. 6, 2071--2126 (2021; Zbl 1471.18025)]. Therefore we have a homotopy-theoretic interpretation of Intuitionistic first-order logic. This paper gives a direct and simple one as the ordinary Tarskian semantics for first-order logic. The interpretation is taken in Kan complexes, being fibration as expected. The main result goes as follows.\N\NTheorem. Let \(M,N:\sigma\rightarrow\boldsymbol{Kan}\) be two interpretations of an algebraic signature \(\sigma\) in \(\boldsymbol{Kan}\). Let \((\varphi,\vec{x})\) be a formula-in-context over \(\sigma\), and let \(\widehat{M}_{\vec{x}}(\varphi)\in\boldsymbol{Kan}/M(\vec{x})\) and \(\widehat {N}_{\vec{x}}(\varphi)\in\boldsymbol{Kan}/N(\vec{x})\) be homotopical interprestations of \((\varphi,\vec{x})\). Then, for any homotopy equivalence \(\alpha:M\rightarrow N\), there exists a homotopy equivalence\N\[\N\widehat{M}_{\vec{x}}(\varphi)\rightarrow\widehat {N}_{\vec{x}}(\varphi)\N\]\Nlying over \(\alpha_{\mathrm{tp\,}\vec{x}}:M(\vec {x})\rightarrow N(\vec{x})\).

Cites work

This page was built for publication: First-order homotopical logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6953431)