A Modal Perspective on Proof-Dynamics

Presented at CAP in Europe 2004 Conference (Pavia, Italy)

Published in Computing, Philosophy, and Cognition. L. Magnani and R. Dossena (eds.). London, College Publications: 313—327.

Abstract. Core aim of this paper is to focus on the dynamics of real proofs by introducing the block-semantics from (Batens, 1995) as a dynamical counterpart for classical semantics. We first look briefly at its original formulation - with respect to natural deduction proofs - and then extend its use to tableau-proofs. This yields a perspective on proof-dynamics that (i) explains proofs as a series of steps providing us with an insight in the premises, and (ii) reveals an informational dynamics in proofs unknown to most dynamical logical systems. As the latter remark especially applies to Amsterdam-style dynamic epistemic logic, we consider a weak modal epistemic logic and combine it with dynamic modal operators expressing the informational proof-dynamics (as a natural companion for the informational dynamics due to new information known from dynamic epistemic logic).

The motivation for this approach is twofold. In a general way it is considered as (a first step in) the reconstruction of the proof-dynamics known from adaptive logics (revealed by its block-formulation) within a modal framework (i.e. using a relational structure); in a more restricted way it aims at the explicit application of some results on omniscience formulated in Batens' paper on block-semantics.

download