Abstract
Classical logics are explosive, meaning that everything follows from a contradiction. Paraconsistent logics are logics that are not explosive. This paper presents the meta-theory of a paraconsistent infinite-valued logic, in particular new results showing that while the question of validity for a given formula can be reduced to a consideration of only finitely many truth values, this does not mean that the logic collapses to a finite-valued logic. All definitions and theorems are formalized in the Isabelle/HOL proof assistant.
Original language | English |
---|---|
Title of host publication | 24th International Conference on Types for Proofs and Programs |
Editors | Peter Dybjer, José Espírito Santo, Luís Pinto |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication date | 2019 |
Pages | 5:1–5:15 |
Article number | 5 |
ISBN (Print) | 978-3-95977-106-1 |
Publication status | Published - 2019 |
Event | 24th International Conference on Types for Proofs and Programs - University of Minho, Braga, Portugal Duration: 18 Jun 2018 → 21 Jun 2018 https://types2018.projj.eu/ |
Conference
Conference | 24th International Conference on Types for Proofs and Programs |
---|---|
Location | University of Minho |
Country/Territory | Portugal |
City | Braga |
Period | 18/06/2018 → 21/06/2018 |
Internet address |
Series | Leibniz International Proceedings in Informatics |
---|---|
ISSN | 1868-8969 |
Keywords
- Paraconsistent logic
- Many-valued logic
- Formalization
- Isabelle proof assistant
- Paraconsistency