skip to main content
research-article

Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)

Published: 17 September 2015 Publication History

Abstract

We produce a decidable super-intuitionistic normal modal logic of internalised intuitionistic (and thus disjunctive and monotonic) interactive proofs (LIiP) from an existing classical counterpart of classical monotonic non-disjunctive interactive proofs (LiP). Intuitionistic interactive proofs effect a durable epistemic impact in the possibly adversarial communication medium CM (which is imagined as a distinguished agent) and only in that, that consists in the permanent induction of the perfect and thus disjunctive knowledge of their proof goal by means of CM's knowledge of the proof: If CM knew my proof then CM would persistently and also disjunctively know that my proof goal is true. So intuitionistic interactive proofs effect a lasting transfer of disjunctive propositional knowledge (disjunctively knowable facts) in the communication medium of multi-agent distributed systems via the transmission of certain individual knowledge (knowable intuitionistic proofs). Our (necessarily) CM-centred notion of proof is also a disjunctive explicit refinement of KD45-belief, and yields also such a refinement of standard S5-knowledge. Monotonicity but not communality is a commonality of LiP, LIiP, and their internalised notions of proof. As a side-effect, we offer a short internalised proof of the Disjunction Property of Intuitionistic Logic (originally proved by Gödel).

References

[1]
R. Anderson. 2008. Security Engineering: A Guide to Building Dependable Distributed Systems (2nd ed.). Wiley, Hoboken, NJ.
[2]
C. Areces and B. Ten Cate. 2007. Hybrid Logics. In Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, P. Blackburn, J. van Benthem, and F. Wolters (Eds.). Elsevier, 821--868.
[3]
S. Artemov. 2008. The logic of justifications. The Review of Symbolic Logic 1, 4.
[4]
S. Artemov and R. Iemhoff. 2007. The basic intuitionistic logic of proofs. The Journal of Symbolic Logic 72, 2.
[5]
A. Baskar, R. Ramanujam, and S. Suresh. 2010. A DEXPTIME-complete Dolev-Yao theory with distributive encryption. In Proceedings of MFCS. LNCS, vol. 6281. Springer.
[6]
P. Blackburn and J. van Benthem. 2007. Modal Logic: A Semantic Perspective. In Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, P. Blackburn, J. van Benthem, and F. Wolters (Eds.). Elsevier, 1--84.
[7]
P. Blackburn, J. van Benthem, and F. Wolter, Eds. 2007. Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier.
[8]
T. Braüner and S. Ghilardi. 2007. Chapter First-Order Modal Logic. In Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, P. Blackburn, J. van Benthem, and F. Wolters (Eds.). Elsevier, 549--620.
[9]
V. de Paiva and E. Ritter. 2011. Basic Constructive Modality. In Logic without Frontiers: Festschrift for Walter Alexandre Carnielli on the occasion of his 60th birthday, Jean-Yves Beziau and Marcelo Esteban Coniglio (Eds.). Tribute Series, vol. 17. College Publications, London.
[10]
K. Došen. 1984. Intuitionistic double negation as a necessity operator. Publications de l'Institut Mathématique (Beograd) 35, 49.
[11]
R. Fagin, J. Halpern, Y. Moses, and M. Vardi. 1995. Reasoning about Knowledge. MIT Press, Cambridge, MA.
[12]
S. Feferman. 1964 (1989). The Number Systems: Foundations of Algebra and Analysis (2nd ed.). AMS Chelsea Publishing. Reprinted by the American Mathematical Society, 2003.
[13]
N. Ferguson, B. Schneier, and T. Kohno. 2010. Cryptography Engineering: Design Principles and Practical Applications. Wiley, Hoboken, NJ.
[14]
G. Fischer Servi. 1984. Axiomatisations for some intuitionistic modal logics. Rendiconti del seminario matematico del Politecnico di Torino 42, 3.
[15]
M. Fitting. 2007. Modal Proof Theory. In Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, P. Blackburn, J. van Benthem, and F. Wolters (Eds.). Elsevier, 85--138.
[16]
D. Gabbay, Ed. 1995. What Is a Logical System? Number 4 in Studies in Logic and Computation. Oxford University Press, New York, NY.
[17]
D. Gollmann. 2011. Computer Security (3rd ed). Wiley, Hoboken, NJ.
[18]
V. Goranko and M. Otto. 2007. Model Theory of Modal Logic. In Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, P. Blackburn, J. van Benthem, and F. Wolters (Eds.). Elsevier, 249--329.
[19]
V. Hendricks and O. Roy, Eds. 2010. Epistemic Logic: 5 Questions. Automatic Press, New York.
[20]
J. Hindley and J. Seldin. 2008. Lambda-Calculus and Combinators (2nd ed.). Cambridge University Press, New York, NY.
[21]
P. Hrubeš. 2007. A lower bound for intuitionistic logic. Annals of Pure and Applied Logic 146.
[22]
E. Jeřábek. 2008. Independent bases of admissible rules. Logic Journal of the Interest Group in Pure and Applied Logic 16, 3.
[23]
S. Kramer. 2012a. A logic of interactive proofs (formal theory of knowledge transfer). Technical Report 1201.3667, arXiv. http://arxiv.org/abs/1201.3667.
[24]
S. Kramer. 2012b. Logic of negation-complete interactive proofs (formal theory of epistemic deciders). Technical Report 1208.5913, arXiv. Retrieved August 30, 2015 from http://arxiv.org/abs/1208.5913.
[25]
S. Kramer. 2012c. Logic of non-monotonic interactive proofs (formal theory of temporary knowledge transfer). Technical Report 1208.1842, arXiv. Retrieved August 30, 2015 from http://arxiv.org/abs/1208.1842.
[26]
S. Kramer. 2013a. Logic of intuitionistic interactive proofs (formal theory of disjunctive knowledge transfer). Short paper presented at the Congress on Logic and Philosophy of Science, Ghent.
[27]
S. Kramer. 2013b. Logic of intuitionistic interactive proofs (formal theory of perfect knowledge transfer). Technical Report 1309.1328, arXiv. Retrieved August 30, 2015 from http://arxiv.org/abs/1309.1328.
[28]
S. Kramer. 2013c. Logic of non-monotonic interactive proofs. In Proceedings of ICLA. Lecture Notes in Computer Science, vol. 7750. Springer.
[29]
S. Kramer. 2014. Logic of negation-complete interactive proofs (formal theory of epistemic deciders). In Proceedings of IMLA. Electronic Notes in Theoretical Computer Science, vol. 300. Elsevier.
[30]
S. Kripke. 1965. Semantical Analysis of Intuitionistic Logic I. In Formal Systems and Recursive Functions. Studies in Logic and the Foundations of Mathematics, vol. 40. Elsevier.
[31]
J.-J. Meyer and F. Veltman. 2007. Handbook of Modal Logic, Chapter Intelligent Agents and Common Sense Reasoning. In Handbook of Modal Logic, Studies in Logic and Practical Reasoning, vol. 3, P. Blackburn, J. van Benthem, and F. Wolters (Eds.). Elsevier, 991--1029.
[32]
J. Moschovakis. 2010. Intuitionistic logic. In The Stanford Encyclopedia of Philosophy, Summer 2010 ed., E. N. Zalta (Ed.).
[33]
Y. Moschovakis. 2006. Notes on Set Theory (2nd ed.). Springer.
[34]
G. Plotkin and C. Stirling. 1986. A framework for intuitionistic modal logics. In Proceedings of the Conference on Theoretical Aspects of Rationality and Knowledge. Morgan Kaufmann Publishers Inc., Burlington, MA.
[35]
K. Pouliasis and G. Primiero. 2014. J-Calc: A typed lambda calculus for Intuitionistic Justification Logic. In Proceedings of IMLA. Electronic Notes in Theoretical Computer Science, vol. 300. Elsevier.
[36]
K. Ranalter. 2010. Embedding constructive K into intuitionistic K. Electronic Notes in Theoretical Computer Science 262.
[37]
A. Simpson. 1994. The proof-theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh, Edinburgh, UK.
[38]
R. Statman. 1979. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science 9.
[39]
G. Steren and E. Bonelli. 2014. Intuitionistic hypothetical logic of proofs. In Proceedings of IMLA. Electronic Notes in Theoretical Computer Science, vol. 300. Elsevier.
[40]
P. Taylor. 1999. Practical Foundations of Mathematics. Cambridge University Press, New York, NY.
[41]
A. Tiu, R. Goré, and J. Dawson. 2010. A proof theoretic analysis of intruder theories. Logical Methods in Computer Science 6, 3.
[42]
J. van Benthem. 1997. Modal Logic as a Theory of Information. In Logic and Reality: Essays on the Legacy of Arthur Prior, B. J. Copeland (Ed.). Clarendon Press, Oxford, UK.
[43]
J. van Benthem. 2009. The information in intuitionistic logic. Synthese 167.
[44]
D. Wijesekera. 1990. Constructive modal logic I. Annals of Pure and Applied Logic 50.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic
ACM Transactions on Computational Logic  Volume 16, Issue 4
November 2015
273 pages
ISSN:1529-3785
EISSN:1557-945X
DOI:10.1145/2802139
  • Editor:
  • Orna Kupferman
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 September 2015
Accepted: 01 July 2015
Revised: 01 May 2015
Received: 01 May 2014
Published in TOCL Volume 16, Issue 4

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Agents as proof-checkers
  2. communication networks
  3. constructive Kripke-semantics
  4. disjunctive explicit doxastic and epistemic logic
  5. interactive and oracle computation
  6. interpreted communication
  7. intuitionistic modal logic
  8. multiagent distributed systems
  9. proofs as sufficient evidence

Qualifiers

  • Research-article
  • Research
  • Refereed

Funding Sources

  • National Research Fund Luxembourg
  • Marie-Curie Actions of the European Commission

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)1
Reflects downloads up to 07 Jan 2025

Other Metrics

Citations

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media