This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

The first part of the paper is a reminder of fundamental results connected with the adequacy problem for sentential logics with respect to matrix semantics. One of the main notions associated with the problem, namely that of the degree of complexity of a sentential logic, is elucidated by a couple of examples in the second part of the paper. E.g., it is shown that the minimal logic of Johansson and some of its extensions have degree of complexity 2. This is (...) the first example of an exact estimation of the degree of natural complex logics, i.e. logics whose deducibility relation cannot be represented by a single matrix. The remaining examples of complex logics are more artificial, having been constructed for the purpose of checking some theoretical possibilities. (shrink)

Nelson has presented a constructive arithmetic with a negation opera- tion () dierent from the ordinary intuitionistic one . In [5] he presents a variant of Kleene's realization semantics for intuitionistic arithmetic, and proves that relative to this interpretation the arithmetic language with { has the same expressive power as the usual intuitionistic one, and fact certain theories of arithmetic incorporating his negation are equivalent to corresponding systems of intuitionistic arithmetic. A Fitch style natural deduction formulation ) of the pure (...) rst order logic that may be extracted, from Nelson's work may be obtained from that for intuitionistic rst order logic by rst dropping the intuitionistic rule of negation intro- duction and then adding rules guaranteeing the De Morgan equivalences, their quantier analogues, and the equivalence of anegated implication with the conjunction of its antecedent and the negation of its consequent. Given the De Morgan equivalences, conjunction and the existential quantier may he treated as dened operators. (shrink)