Propositional Type Theory of Indeterminacy

  1. Aranda, Víctor
  2. Martins, Manuel
  3. Manzano, María
Revista:
Studia Logica

ISSN: 0039-3215,  1572-8730

Año de publicación: 2024

Tipo: Artículo

DOI: 10.1007/S11225-024-10099-0 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Studia Logica

Resumen

The aim of this paper is to define a partial Propositional Type Theory. Our system is partial in a double sense: the hierarchy of (propositional) types contains partial functions and some expressions of the language, including formulas, may be undefined. The specific interpretation we give to the undefined value is that of Kleene’s strong logic of indeterminacy. We present a semantics for the new system and prove that every element of any domain of the hierarchy has a name in the object language. Finally, we provide a proof system and a (constructive) proof of completeness.

€ Ver financiación

Información de financiación

Financiadores

Referencias bibliográficas

  • Andrews, P., A reduction of the axioms for the theory of propositional types, Fundamenta Mathematicae 52:345–350, 1963.
  • Andrews, P., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Applied Logic Series, Kluwer Academic Publishers, Dordrecht, 2002.
  • Andrews, P., A Bit of History Related to Logic Based on Equality, in M. Manzano, I. Sain, and E. Alonso, (eds.), 2014, pp. 67–71.
  • Aranda, V., A. Huertas, M. Manzano, and M. Martins, On the philosophy and mathematics of Hybrid Partial Type Theory, Springer’s “Outstanding Contributions to Logic” series, forthcoming.
  • Benzmüller, C., et al. (eds.), Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday, College Publications, London, 2008.
  • Blackburn, P., M. Martins, M. Manzano, and A. Huertas, Exorcising the phantom zone, Information and Computation 287:1–21, 2022.
  • Correia, F., Weak Necessity on Weak Kleene Matrices, in F. Walter et al (eds.), 2002, pp. 73–90.
  • Farmer, W.M., A partial functions version of Church’s simple theory of types, The Journal of Symbolic Logic 55:1269–1291, 1990.
  • Farmer, W.M., Andrews’ Type System with Undefinedness, in C. Benzmüller et al (eds.), 2008, pp. 223–242.
  • Farmer, W.M., Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas, Springer, Cham, 2023.
  • Ferguson, T.M., Logics of nonsense and parry systems, Journal of Philosophical Logic 44:65–80, 2014.
  • Henkin, L., A theory of propositional types, Fundamenta Mathematicae 52:323–344, 1963.
  • Henkin, L., Identity as a logical primitive, Philosophia 5:31–45, 1975.
  • Kleene, S.C., On notation for ordinal numbers, The Journal of Symbolic Logic 3:150–155, 1938.
  • Lapierre, S., A functional partial semantics for intensional logic, Notre Dame Journal of Formal Logic 33:517–541, 1992.
  • Lepage, F., Partial functions in type theory, Notre Dame Journal of Formal Logic 33:493–516, 1992.
  • Lepage, F., Partial Propositional Logic, in M. Marion and R. S. Cohen (eds.), 1995, pp. 23–39.
  • Manzano, M., I. Sain, and E. Alonso (eds.), The Life and Work of Leon Henkin, Birkhauser, Heidelberg, 2014.
  • Manzano, M., A. Huertas, P. Blackburn, M. Martins, and V. Aranda, Hybrid Partial Type Theory, The Journal of Symbolic Logic, 1–37. https://doi.org/10.1017/jsl.2023.33.
  • Marion, M. and R. S. Cohen (eds.), Québec Studies in the Philosophy of Science. Part I: Logic, Mathematics, Physics and History of Science. Essays in Honor of Hugues Leblanc, Kluwer Academic Publishers, Dordrecht, 1995.
  • Walter, F., et al (eds.), Advances in Modal Logic 3, World Scientific Publishing Co., Singapore, 2002.