We saw that within proof-theoretic semantics several similar notions of validity have been proposed. For some of these notions completeness results are available for certain fragments of intuitionistic (propositional) logic or for full intuitionistic (propositional) logic. In other cases, such as validity based on higher-level atomic systems, completeness for minimal and intuitionistic logic does not hold. For yet another notion a completeness result holds for classical logic, provided that disjunction is understood classically.

The considered notions of validity have in common that they are not closed under substitution. As derivability in intuitionistic or classical logic is closed under substitution, it seems questionable to even consider these notions as candidates for completeness. Indeed, for intuitionistic logic the failure of completeness with respect to validity based on firstor higher-level atomic systems could be proved by showing the validity of instances of classical laws which are not valid as a schema. For a notion of validity based on atomic systems of level 0, that is, for sets of atoms alone, there are counterexamples of not even classically derivable valid formulas.

As a way out, strengthened notions of validity have been proposed, which are by definition closed under substitution. Thus a formula can now only be valid (in the strengthened sense), if each of its substitution instances, resulting from uniform substitutions of arbitrary formulas for atoms, is valid (in the sense of the underlying, non-strengthened notion of validity). Intuitionistic propositional logic is complete with respect to two of these strengthened notions considered here. In the case of Goldfarb's account, it is essential for completeness (Theorem 4) that only consistent extensions of atomic systems are taken into account. In the case of Sandqvist's completeness result for intuitionistic propositional logic and validity based on secondlevel atomic systems (Theorem 7) it is crucial that disjunction is explained by the given clause (T4), and not by a more standard clause like (S4).

An essential component of all the considered notions of validity is their dependency on atomic systems. In each notion the validity of atoms a with respect to an atomic system S is defined by derivability of a in S (or as membership in a set of atoms closed under the rules of S), and the validity of implications (or of logical consequences Γ FS A) with respect to atomic systems S is defined by making use

of extensions St of S. Using extensions guarantees that validity is monotone with

respect to atomic systems S. Whether extensions of atomic systems should be an integral part of any proof-theoretic notion of validity cannot be discussed here; we just point out that, for example, Prawitz has given up to consider extensions of atomic systems from the mid-1970s on and now emphasizes that this is not an intrinsic part of his analysis [personal communication]. His main argument is that atomic systems should not be looked at as descriptions of one's knowledge but as rules defining the meaning of atomic propositions (cf. Prawitz [22, 23]), which would be changed by considering extensions (see [17] for a critical discussion).

With respect to completeness, the choice of the kind of atomic systems can be critical. For example, certain counterexamples to completeness of intuitionistic logic, namely examples of valid classically derivable formulas, can be prevented, if one allows for second-level instead of only first-level atomic systems. With regard to the completeness result for classical logic (Theorem 8) this means that the choice of first-level atomic systems is essential, since completeness does no longer hold for second-level atomic systems. Other results, such as strong completeness for certain fragments of intuitionistic logic, depend on the availability of arbitrary higher-level atomic systems.

For the philosophical endeavor of justifying a certain logic one might want to restrict oneself to first-level atomic systems in the first place, since higher-level systems already presuppose a feature of implication at the atomic level by allowing for the discharge of atomic assumptions. This presupposition might be deemed too strong for any adequate justification. For a justification of intuitionistic logic one would therefore prefer a proof-theoretic semantics which is restricted to first-level atomic systems, possibly allowing for inconsistent extensions. The question of whether intuitionistic logic is complete for such a semantics is still open.

Found a mistake? Please highlight the word and press Shift + Enter