Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
Simon Kramer · ACM Transactions on Computational Logic · 2015
We produce a decidablesuper-intuitionisticnormal modal logic of internalisedintuitionistic(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 theperfectand thusdisjunctiveknowledge of their proof goal by means of CM's knowledge of the proof: If CM knew my proof then CM would persistently and alsodisjunctivelyknow 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).