Logic of Negation-Complete Interactive Proofs (Formal Theory of Epistemic Deciders)
详细信息 查看全文
- 作者：Simon Kramer
- 关键词：Agents as proof checkers ; Constructive Kripke-semantics ; Disjunctive explicit doxastic and epistemic logic ; Epistemic deciders as decisive evidence ; Interactive and oracle computation ; Multi-agent systems ; Negation as failure ; Proofs as sufficient evidence ; Proof terms as truth values
- 刊名：Electronic Notes in Theoretical Computer Science
- 出版年：21 January, 2014
- 年：2014
- 卷：300
- 期：Complete
- 页码：47-70
- 全文大小：361 K
文摘
We produce a decidable classical normal modal logic of internalised negation-complete and thus disjunctive non-monotonic interactive proofs (LDiiP) from an existing logical counterpart of non-monotonic or instant interactive proofs (LiiP). LDiiP internalises agent-centric proof theories that are negation-complete (maximal) and consistent (and hence strictly weaker than, for example, Peano Arithmetic) and enjoy the disjunction property (like Intuitionistic Logic). In other words, internalised proof theories are ultrafilters and all internalised proof goals are definite in the sense of being either provable or disprovable to an agent by means of disjunctive internalised proofs (thus also called epistemic deciders). Still, LDiiP itself is classical (monotonic, non-constructive), negation-incomplete, and does not have the disjunction property. The price to pay for the negation completeness of our interactive proofs is their non-monotonicity and non-communality (for singleton agent communities only). As a normal modal logic, LDiiP enjoys a standard Kripke-semantics, which we justify by invoking the Axiom of Choice on LiiP始s and then construct in terms of a concrete oracle-computable function. LDiiP始s agent-centric internalised notion of proof can also be viewed as a negation-complete disjunctive explicit refinement of standard KD45-belief, and yields a disjunctive but negation-incomplete explicit refinement of S4-provability.