CLASP
The Centre for Linguistic Theory and Studies in Probability

Intuitionistic multi-agent subatomic natural deduction for belief and knowledge

In this talk, we will consider a natural deduction system which aims at the proof-theoretic analysis of reasoning with complex multi-agent belief (resp. knowledge) constructions (involving, e.g., forms of reciprocating or universal belief, or intentional identity). Making use of a normalization result for the system, we shall propose a proof-theoretic semantics for the intensional operators for intuitionistic belief and knowledge which explains their meaning entirely by appeal to the structure of derivations. Since the system enjoys the subexpression property, a refinement of the subformula property, it is fully analytic. We will also compare this approach to the logic and semantics of belief and knowledge with other intuitionistic approaches.