Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
This work addresses the problem of formalizing knowledge transfer in multi-agent distributed systems for researchers in logic and theoretical computer science, representing an incremental extension from classical to intuitionistic frameworks.
The paper introduces a decidable super-intuitionistic normal modal logic (LIiP) for intuitionistic interactive proofs, which enables durable transfer of disjunctive propositional knowledge in adversarial communication media by inducing perfect knowledge of proof goals. It also provides a short internalised proof of the Disjunction Property of Intuitionistic Logic.
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).