Abstract This paper proposes natural deduction systems for the representation of inferences in which several agents participate in deriving conclusions about what they believe or know, where belief and knowledge are understood in an intuitionistic sense. Multi-agent derivations in these systems may involve relatively complex belief (resp. knowledge) constructions which may include forms of nested, reciprocal, shared, distributed or universal belief/knowledge as well as attitudes de dicto/re/se. The systems consist of two main components: multi-agent belief bases which assign to each agent a subatomic system that represents the agent’s beliefs concerning atomic sentences and a set of multi-agent labelled rules for logically compound formulae. Derivations in these systems normalize. Moreover, normal derivations possess the subexpression property (a refinement of the subformula property) which makes them fully analytic. Relying on the normalization result, a proof-theoretic approach to the semantics of the intensional operators for intuitionistic belief/knowledge is presented which explains their meaning entirely by appeal to the structure of derivations. Importantly, this proof-theoretic semantics is autarkic with respect to its foundations as the systems (unlike, e.g. external/labelled proof systems which internalize possible worlds truth conditions) are not defined on the basis of a possible worlds semantics. Detailed applications to a logical puzzle (McCarthy’s three wise men puzzle) and to a semantical difficulty (Geach’s problem of intentional identity), respectively, illustrate the systems. The paper also provides comparisons with other approaches to intuitionistic belief/knowledge and multi-agent natural deduction.

Subatomic natural deduction combines natural deduction rules with subatomic systems [ 21 ]. The latter make proofs of atomic sentences and the study of their component structure accessible to methods of structural proof theory and, thereby, admit a proof-theoretic account of the semantics of atomic sentences and their components. The article proposes two refinements of subatomic natural deduction. The first combines it with algebraic degree functions into systems of graded natural deduction which allow us to model, in a proof-theoretic manner, how the degree of assent to a conclusion may depend on the degrees of assent to its premisses. The second refinement consists in the introduction of term assumption rules which allow us to add (resp. subtract) contents to (from) term assumptions, thereby allowing us to represent aspects of dynamic reasoning in a natural deduction setting. Normalization is established for graded, and with certain limitations, for dynamic, as well as for dynamic graded systems of minimal and intuitionistic first-order logic.