Search

In [2] S. Artemov introduced the logic of proofs LP describing provability in an arbitrary system. In this paper we present the logic LPM of the standard multiple conclusion proof predicate in Peano Arithmetic with the negative introspection operation. We establish the completeness of LPM with respect to the intended arithmetical semantics. Two useful artificial semantics for LPM were also found. The first one is an extension of the usual boolean truth tables, whereas the second one deals with so-called protocolling extension of a theory. For both cases the completeness theorem has been established. In the last section we consider first order version of the logic LPM. Arithmetical completeness of this logic is established too.

The logic \(\mathcal{L}\)(T) of an arbitrary first order theory T is the set of predicate formulas provable in T under every interpretation into the language of T. We prove that if T is an arithmetically correct theory in the language of arithmetic, or T is the theory of fields, the theory of rings, or an inessential extension of the theory of groups, then \(\mathcal{L}\)(T) coincides with the predicate calculus PC. We also study inclusion relations and decidability for the logics of Presburger's arithmetic of addition, Skolem's arithmetic of multiplication and other decidable theories.