Document Open Access Logo

New Formalized Results on the Meta-Theory of a Paraconsistent Logic

Author Anders Schlichtkrull

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2018.5.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Anders Schlichtkrull
  • DTU Compute - Department of Applied Mathematics and Computer Science, Technical University of Denmark, Richard Petersens Plads, Building 324, DK-2800 Kongens Lyngby, Denmark

Acknowledgements

Jørgen Villadsen, Jasmin Christian Blanchette and John Bruntse Larsen provided valuable feedback on the paper and the formalization. Thanks to Freek Wiedijk for discussions. Thanks to the anonymous reviewers for many constructive comments.

Cite AsGet BibTex

Anders Schlichtkrull. New Formalized Results on the Meta-Theory of a Paraconsistent Logic. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.5

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Logic and verification
  • Theory of computation → Higher order logic
  • Theory of computation → Logic and databases
Keywords
  • Paraconsistent logic
  • Many-valued logic
  • Formalization
  • Isabelle proof assistant
  • Paraconsistency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Seiki Akama, editor. Towards Paraconsistent Engineering, volume 110 of Intelligent Systems Reference Library. Springer, 2016. Google Scholar
  2. Christoph Benzmüller, Dov Gabbay, Valerio Genovese, and Daniele Rispoli. Embedding and automating conditional logics in classical higher-order logic. Annals of Mathematics and Artificial Intelligence, 66(1):257-271, 2012. Google Scholar
  3. Christoph Benzmüller and Lawrence C. Paulson. Quantified Multimodal Logics in Simple Type Theory. Logica Universalis, 7(1):7-20, 2013. Google Scholar
  4. Christoph Benzmüller and Dana S. Scott. Automating Free Logic in HOL, with an Experimental Application in Category Theory. Journal of Automated Reasoning, January 2019. Google Scholar
  5. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Higher-Order Modal Logics: Automation and Applications. In Wolfgang Faber and Adrian Paschke, editors, Reasoning Web (RW), volume 9203 of LNCS, pages 32-74. Springer, 2015. Google Scholar
  6. Walter Carnielli, Marcelo E. Coniglio, and João Marcos. Logics of Formal Inconsistency. In D.M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, pages 1-93. Springer, 2007. Google Scholar
  7. James Dugundji. Note on a Property of Matrices for Lewis and Langford’s Calculi of Propositions. J. Symbolic Logic, 5(4):150-151, December 1940. Google Scholar
  8. Kurt Gödel. Zum intuitionistischen Aussagenkalkül. Akademie der Wissenschaften in Wien, 69:65-66, 1932. Google Scholar
  9. John Harrison. Towards self-verification of HOL Light. In Ulrich Furbach and Natarajan Shankar, editors, International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of LNCS, pages 177-191. Springer, 2006. Google Scholar
  10. Andreas Schmidt Jensen and Jørgen Villadsen. Paraconsistent Computational Logic. In P. Blackburn, K. F. Jørgensen, N. Jones, and E. Palmgren, editors, 8th Scandinavian Logic Symposium: Abstracts, pages 59-61. Roskilde University, 2012. Google Scholar
  11. Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation. Journal of Automated Reasoning, 56(3):221-259, 2016. Google Scholar
  12. João Marcos. Automatic Generation of Proof Tactics for Finite-Valued Logics. In Ian Mackie and Anamaria Martins Moreira, editors, Tenth International Workshop on Rule-Based Programming, Proceedings, volume 21 of Electronic Proceedings in Theoretical Computer Science, pages 91-98. Open Publishing Association, 2010. Google Scholar
  13. Graham Priest, Koji Tanaka, and Zach Weber. Paraconsistent Logic. In Edward N. Zalta, editor, Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2018 edition, 2018. URL: https://plato.stanford.edu/archives/sum2018/entries/logic-paraconsistent/.
  14. Anders Schlichtkrull. Formalization of a Paraconsistent Infinite-Valued Logic (short abstract). Automated Reasoning in Quantified Non-Classical Logics - 3rd International Workshop - Program, 2018. URL: https://easychair.org/smart-program/FLoC2018/ARQNL-program.html.
  15. Anders Schlichtkrull. Formalization of Logic in the Isabelle Proof Assistant. PhD thesis, Technical University of Denmark, 2018. URL: http://matryoshka.gforge.inria.fr/pubs/schlichtkrull_phd_thesis.pdf.
  16. Anders Schlichtkrull and Jørgen Villadsen. IsaFoL: Paraconsistency. URL: https://bitbucket.org/isafol/isafol/src/master/Paraconsistency/.
  17. Anders Schlichtkrull and Jørgen Villadsen. Paraconsistency. Archive of Formal Proofs, December 2016. , Formal proof development. URL: http://isa-afp.org/entries/Paraconsistency.html.
  18. Alexander Steen and Christoph Benzmüller. Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic. Logic and Logical Philosophy, 25(4):535-554, 2016. Google Scholar
  19. Jørgen Villadsen. Combinators for Paraconsistent Attitudes. In P. de Groote, G. Morrill, and C. Retoré, editors, Logical Aspects of Computational Linguistics (LACL), volume 2099 of LNCS, pages 261-278. Springer, 2001. Google Scholar
  20. Jørgen Villadsen. A Paraconsistent Higher Order Logic. In B. Buchberger and J. A. Campbell, editors, Artificial Intelligence and Symbolic Computation (AISC), volume 3249 of LNCS, pages 38-51. Springer, 2004. Google Scholar
  21. Jørgen Villadsen. Paraconsistent Assertions. In G. Lindemann, J. Denzinger, I. J. Timm, and R. Unland, editors, Multi-Agent System Technologies (MATES), volume 3187 of LNCS, pages 99-113, 2004. Google Scholar
  22. Jørgen Villadsen. Supra-logic: Using Transfinite Type Theory with Type Variables for Paraconsistency. Logical Approaches to Paraconsistency, Journal of Applied Non-Classical Logics, 15(1):45-58, 2005. Google Scholar
  23. Jørgen Villadsen and Anders Schlichtkrull. Formalization of Many-Valued Logics. In H. Christiansen, M.D. Jiménez-López, R. Loukanova, and L.S. Moss, editors, Partiality and Underspecification in Information, Languages, and Knowledge, chapter 7. Cambridge Scholars Publishing, 2017. Google Scholar
  24. Jørgen Villadsen and Anders Schlichtkrull. Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant. In Abdelkader Hameurlain, Josef Küng, Roland Wagner, and Hendrik Decker, editors, Transactions on Large-Scale Data- and Knowledge-Centered Systems (TLDKS), volume 10620 of LNCS, pages 92-122. Springer, 2017. Google Scholar
  25. Zach Weber. Paraconsistent Logic, 2019. URL: https://www.iep.utm.edu/para-log/.
  26. Max Wisniewski and Alexander Steen. Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic. In Christoph Benzmüller and Jens Otten, editors, ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics, volume 33 of EPiC Series in Computing, pages 59-64. EasyChair, 2015. URL: https://doi.org/10.29007/dzc2.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact