A Gödel-Artemov-Style Analysis of Constructible Falsity

  • Thomas Macaulay FergusonEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


David Nelson’s logic of constructible falsity \(\mathsf {N}\) is a well-known conservative extension to intuitionistic logic \(\mathsf {Int}\). Heinrich Wansing has suggested that extending the provability interpretation of \(\mathsf {Int}\) to such extensions requires that one enriches the single category of formal proofs assumed intuitionistically with further categories representing formal refutations. This paper adapts the framework of Sergei Artemov’s justification logic—which has provided incredible insight into \(\mathsf {Int}\)—to capture a proof/refutation interpretation of \(\mathsf {N}\). To represent distinct types of justification, we identify the distinct agents of Tatiana Yavorskaya-Sidon’s two-agent logic of proofs \(\mathsf {LP}^{2}_{\uparrow {\uparrow }}\) with categories of proof and refutation, permitting an embedding of \(\mathsf {N}\) into \(\mathsf {LP}^{2}_{\uparrow {\uparrow }}\). In conclusion, we describe how a Gödel-Artemov-style analysis can be given for Cecylia Rauszer’s Heyting-Brouwer logic and show that Melvin Fitting’s semantic realization proof can be extended to normal multimodal logics in general.


Justification logic Constructible falsity Refutation Intuitionistic logic Logic of proofs 


  1. 1.
    Achilleos, A.: On the complexity of two-agent justification logic. In: Bulling, N., van der Torre, L., Villata, S., Jamroga, W., Vasconcelos, W. (eds.) CLIMA 2014. LNCS (LNAI), vol. 8624, pp. 1–18. Springer, Cham (2014). Google Scholar
  2. 2.
    Artemov, S.: Operational modal logic. Technical report MSI 95–29, Cornell University (1995)Google Scholar
  3. 3.
    Artemov, S.: On two models of provability. In: Gabbay, D., Zakharyaschev, M., Goncharov, S.S. (eds.) Mathematical Problems from Applied Logics II, pp. 1–52. Springer, New York (2007). Google Scholar
  4. 4.
    Artemov, S.: The ontology of justifications in the logical setting. Stud. Logica. 100(1–2), 17–30 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Fitting, M.: The logic of proofs, semantically. Ann. Pure Appl. Logic 132(1), 1–25 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Fitting, M.: Realization implemented. Technical report TR-2013005, City University of New York (2013)Google Scholar
  7. 7.
    Fitting, M.: Justification logics and realization. Technical report TR-2014004, City University of New York (2014)Google Scholar
  8. 8.
    Fitting, M.: Paraconsistent logic, evidence, and justification. Stud. Logica, 1–18 (2017, to appear)Google Scholar
  9. 9.
    Gödel, K.: Eine Interpretation des intuitionistischen Aussagenkalküls. In: Ergebnisse eines mathematischen Kolloquiums, vol. 4, pp. 39–40 (1933)Google Scholar
  10. 10.
    López-Escobar, E.G.K.: Refutability and elementary number theory. Indagationes Math. 75(4), 362–374 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Łukowski, P.: Modal interpretation of Heyting-Brouwer logic. Bull. Sect. Logic 25(2), 80–83 (1996)MathSciNetzbMATHGoogle Scholar
  12. 12.
    McKinsey, J., Tarski, A.: Some theorems about the sentential calculi of Lewis and Heyting. J. Symbolic Logic 13(1), 1–15 (1948)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Mkrtychev, A.: Models for the logic of proofs. In: Adian, S., Nerode, A. (eds.) LFCS 1997. LNCS, vol. 1234, pp. 266–275. Springer, Heidelberg (1997). CrossRefGoogle Scholar
  14. 14.
    Nelson, D.: Constructible falsity. J. Symbolic Logic 14(1), 16–26 (1949)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Nelson, D.: Negation and separation of concepts in constructive systems. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 208–225. North-Holland, Amsterdam (1959)Google Scholar
  16. 16.
    Nelson, D., Almukdad, A.: Constructible falsity and inexact predicates. J. Symbolic Logic 49(1), 231–233 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Odintsov, S.: Constructive Negations and Paraconsistency. Springer, Dordrecht (2008). CrossRefzbMATHGoogle Scholar
  18. 18.
    Pinto, L., Uustalu, T.: Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 295–309. Springer, Heidelberg (2009). CrossRefGoogle Scholar
  19. 19.
    Rauszer, C.: A formalization of the propositional calculus of H-B logic. Stud. Logica. 33(1), 23–34 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Rauszer, C.: Semi-Boolean algebras and their application to intuitionistic logic with dual operations. Fundamenta Math. 83(1), 219–249 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Rubtsova, N.: Evidence reconstruction of epistemic modal logic S5. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 313–321. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  22. 22.
    Shramko, Y.: A modal translation for dual-intuitionistic logic. Rev. Symbolic Logic 9(2), 251–265 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Thomason, R.H.: A semantical study of constructible falsity. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 15(16–18), 247–257 (1969)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 8, pp. 61–145. Kluwer, Boston (2002)CrossRefGoogle Scholar
  25. 25.
    Wansing, H.: Constructive negation, implication, and co-implication. J. Appl. Non-class. Logics 18(2–3), 341–364 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Wansing, H.: Proofs, disproofs, and their duals. In: Areces, C., Goldblatt, R. (eds.) Advances in Modal Logic, vol. 7, pp. 483–505. College Publications, London (2008)Google Scholar
  27. 27.
    Wansing, H.: Falsification, natural deduction and bi-intuitionistic logic. J. Logic Comput. 26(1), 425–450 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Wolter, F.: On logics with coimplication. J. Philos. Logic 27(4), 353–387 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Yavorskaya (Sidon), T.: Multi-agent explicit knowledge. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 369–380. Springer, Heidelberg (2006). CrossRefGoogle Scholar
  30. 30.
    Yavorskaya (Sidon), T.: Interacting explicit evidence systems. Theory Comput. Syst. 43(2), 272–293 (2008)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.CycorpAustinUSA
  2. 2.Saul Kripke CenterCUNY Graduate CenterNew YorkUSA

Personalised recommendations