Misc,
A Logic of Interactive Proofs (Formal Theory of Knowledge Transfer)
(2012)cite arxiv:1201.3667.
Abstract
We propose a logic of interactive proofs as the first and main step towards
an intuitionistic foundation for interactive computation to be obtained via an
interactive analog of the Gödel-Kolmogorov-Artëmov definition of
intuitionistic logic as embedded into a classical modal logic of proofs, and of
the Curry-Howard isomorphism between intuitionistic proofs and typed programs.
Our interactive proofs effectuate a persistent epistemic impact in their
intended communities of peer reviewers that consists in the induction of the
(propositional) knowledge of their proof goal by means of the (individual)
knowledge of the proof with the interpreting reviewer. That is, interactive
proofs effectuate a transfer of propositional knowledge (knowable facts) via
the transfer of certain individual knowledge (knowable proofs) in distributed
and multi-agent systems. In other words, we as a community can have the formal
common knowledge that a proof is that which if known to one of our peer members
would induce the knowledge of its proof goal with that member.
