Completeness in Proof-Theoretic Semantics

Abstract We give an overview of completeness and incompleteness results within proof-theoretic semantics. Completeness of intuitionistic first-order logic for certain notions of validity in proof-theoretic semantics has been conjectured by Prawitz. For the kind of semantics proposed by him, this conjecture is still undecided. For certain variants of proof-theoretic semantics the completeness question is settled, including a positive result for classical logic. For intuitionistic logic there are positive as well as negative completeness results, depending on which variant of semantics is considered. Further results have been obtained for certain fragments of first-order languages.

Introduction

In proof-theoretic semantics (see Schroeder-Heister [34]; cf. Wansing [36]) for logical constants several related notions of validity have been proposed. We mention Kreisel (cf. Gabbay [6]), Prawitz [18–22], Dummett [3] and Sandqvist [26]. Overviews and discussions of such proof-theoretic notions of validity can be found in Schroeder-Heister [31] and Read [24].

What these notions of validity have in common is that the validity of an atomic formula, or atom, is defined in terms of the derivability of that atom in a given system of atomic rules, that is, of rules which can only contain atoms. Let a, b,... , a1, a2,... be atoms. Then

a b

a b c

is an example of a system S of atomic rules (the first two having the form of atomic axioms), in which c is derivable by

a b

c

and therefore valid with respect to S. Atomic rules are also called boundary rules (cf. Dummett [3]) or production rules. Atomic systems S are also called bases; they can have the form of Post systems, definite Horn clause logic programs etc.

The validity of complex formulas A, B,..., A1, A2,... (constructed as usual from atoms with logical constants) with respect to an atomic system S can then be

defined inductively by giving semantic clauses for the logical constants. The validity of implications A → B with respect to an atomic system S is usually defined by taking into account arbitrary atomic extensions St of S. Let FS stand for 'valid with respect to S'; then the semantic clause for implication has the form

FS A → B :⇐⇒ ∀St ⊇ S : (FSt A =⇒ FSt B)

where in the definiens all extensions St of S have to be considered. This ensures that implications A → B cannot become valid with respect to S just because some atom on which the validity of A depends is not derivable in S. Considering extensions thus guarantees monotonicity for validity with respect to S.

It was conjectured by Prawitz [19, 22] that intuitionistic first-order logic is complete with respect to certain notions of validity for inference rules. This conjecture is still undecided. There are, however, several negative as well as positive results about completeness for certain plausible variants of this notion of validity, formulated not for inference rules but for formulas. One kind of variants considers only certain fragments of first-order languages. Other variants are based on different kinds of atomic systems which allow for atomic rules of a more general form than production rules only. Further variants are given through different treatments of negation or absurdity, and by different notions of what an extension of an atomic system is.

In the following, we present several of these variants together with their respective completeness or incompleteness results.