A semantics for equational hybrid propositional type theory
The definition of identity in terms of other logical symbols is a recurrent issue in logic. In particular, in First-Order Logic (FOL) there is no way of defining the global relation of identity, while in standard Second-Order Logic (SOL) this definition is not only possible, but widely used. In this...
| Authors: | ; ; |
|---|---|
| Format: | Article |
| Status: | Published version |
| Publication date: | 2014 |
| Country: | España |
| Institution: | Universitat Oberta de Catalunya (UOC) |
| Repository: | O2, repositorio institucional de la UOC |
| OAI Identifier: | oai:openaccess.uoc.edu:10609/123586 |
| Online Access: | https://hdl.handle.net/10609/123586 |
| Access Level: | Open access |
| Keyword: | propositional type theory first-order logic second-order logic equational hybrid logic lógica de primer orden lógica de segundo orden teoría de tipo proposicional lógica ecuacional híbrida lògica de primer ordre lògica de segon ordre teoria de tipus proposicional lògica equacional híbrida Logic, Modern Lògica moderna Lógica moderna |
| _version_ | 1878741722331086848 |
|---|---|
| author | Manzano Arjona, María |
| author2 | Martins, Manuel A. Huertas, M. Antonia |
| author2_role | author author |
| author_browse | Huertas, M. Antonia Manzano Arjona, María Martins, Manuel A. |
| author_facet | Manzano Arjona, María Martins, Manuel A. Huertas, M. Antonia |
| author_role | author |
| collection | O2, repositorio institucional de la UOC |
| description | The definition of identity in terms of other logical symbols is a recurrent issue in logic. In particular, in First-Order Logic (FOL) there is no way of defining the global relation of identity, while in standard Second-Order Logic (SOL) this definition is not only possible, but widely used. In this paper, the reverse question is posed and affirmatively answered: Can we define with only equality and abstraction the remaining logical symbols? Our present work is developed in the context of an equational hybrid logic (i.e. a modal logic with equations as propositional atoms enlarged with the hybrid expressions: nominals and the @ operator). Our logical base is propositional type theory. We take the propositional equality, abstraction, nominals, and @ operators as primitive symbols and we demonstrate that all of the remaining logical symbols can be defined, including propositional quantifiers and equational equality. |
| eu_rights_str_mv | openAccess |
| format | article |
| id | ES_ea40eadf4aec26b302beb8a76f7d28bf |
| institution | Universitat Oberta de Catalunya (UOC) |
| instname_str | Universitat Oberta de Catalunya (UOC) |
| network_acronym_str | ES |
| network_name_str | España |
| oai_identifier_str | oai:openaccess.uoc.edu:10609/123586 |
| publishDate | 2014 |
| publishDateSort | 2014 |
| publisher | Bulletin of the Section of Logic |
| publisherStr | Bulletin of the Section of Logic |
| reponame_str | O2, repositorio institucional de la UOC |
| spelling | A semantics for equational hybrid propositional type theory Manzano Arjona, María Martins, Manuel A. Huertas, M. Antonia propositional type theory first-order logic second-order logic equational hybrid logic lógica de primer orden lógica de segundo orden teoría de tipo proposicional lógica ecuacional híbrida lògica de primer ordre lògica de segon ordre teoria de tipus proposicional lògica equacional híbrida Logic, Modern Lògica moderna Lógica moderna The definition of identity in terms of other logical symbols is a recurrent issue in logic. In particular, in First-Order Logic (FOL) there is no way of defining the global relation of identity, while in standard Second-Order Logic (SOL) this definition is not only possible, but widely used. In this paper, the reverse question is posed and affirmatively answered: Can we define with only equality and abstraction the remaining logical symbols? Our present work is developed in the context of an equational hybrid logic (i.e. a modal logic with equations as propositional atoms enlarged with the hybrid expressions: nominals and the @ operator). Our logical base is propositional type theory. We take the propositional equality, abstraction, nominals, and @ operators as primitive symbols and we demonstrate that all of the remaining logical symbols can be defined, including propositional quantifiers and equational equality. Bulletin of the Section of Logic https://hdl.handle.net/10609/123586 |
| spellingShingle | A semantics for equational hybrid propositional type theory Manzano Arjona, María propositional type theory first-order logic second-order logic equational hybrid logic lógica de primer orden lógica de segundo orden teoría de tipo proposicional lógica ecuacional híbrida lògica de primer ordre lògica de segon ordre teoria de tipus proposicional lògica equacional híbrida Logic, Modern Lògica moderna Lógica moderna |
| status_str | publishedVersion |
| title | A semantics for equational hybrid propositional type theory |
| title_full | A semantics for equational hybrid propositional type theory |
| title_fullStr | A semantics for equational hybrid propositional type theory |
| title_full_unstemmed | A semantics for equational hybrid propositional type theory |
| title_short | A semantics for equational hybrid propositional type theory |
| title_sort | A semantics for equational hybrid propositional type theory |
| topic | propositional type theory first-order logic second-order logic equational hybrid logic lógica de primer orden lógica de segundo orden teoría de tipo proposicional lógica ecuacional híbrida lògica de primer ordre lògica de segon ordre teoria de tipus proposicional lògica equacional híbrida Logic, Modern Lògica moderna Lógica moderna |
| topic_facet | propositional type theory first-order logic second-order logic equational hybrid logic lógica de primer orden lógica de segundo orden teoría de tipo proposicional lógica ecuacional híbrida lògica de primer ordre lògica de segon ordre teoria de tipus proposicional lògica equacional híbrida Logic, Modern Lògica moderna Lógica moderna |
| url | https://hdl.handle.net/10609/123586 |