Refinements of subatomic 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.