Craig Interpolation for Awareness Logics
摘要
In this paper, we establish the Craig interpolation theorems of awareness logics by introducing semi-analytic sequent calculi for them. For a semantic clause for an awareness operator, we choose an idea of propositional awareness, which is introduced by Fagin and Halpern and means that an agent is aware of a formula if and only if he is aware of all the atomic propositions contained in it. Although our sequent calculi are not cut-free (due to the fact that our epistemic logic is based on \(\textbf{S5}\) ), we are able to restrict all applications of the rule of cut to semi-analytic ones. This enables us to employ the Maehara method in order to compute Craig interpolants.