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

TL;DR

This paper introduces a decidable modal logic LIiP that internalizes intuitionistic interactive proofs, demonstrating how such proofs induce lasting disjunctive knowledge transfer in multi-agent systems, with implications for belief and knowledge refinement.

Contribution

It develops a new super-intuitionistic modal logic LIiP from classical LiP, internalizing intuitionistic proofs and their epistemic impact in multi-agent communication.

Findings

LIiP is decidable and normal, extending classical LiP.

Intuitionistic proofs induce durable disjunctive knowledge transfer.

Provides an internal proof of the Disjunction Property of Intuitionistic Logic.

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 Goedel).