## Examples of Proof-theoretic Validity

Prawitz’s definition of validity, of which there are several variants, can be reconstructed as follows. We consider only the constants of positive propositional logic (conjunction, disjunction, implication). We assume that an atomic system S is given determining the derivability of atomic formulas, which is the same as their validity. A formula over S is a formula built up by means of logical connectives starting with atoms from S. We propose the term “derivation structure” for a candidate for a valid derivation. (Prawitz uses various terminologies, such as “[argument or proof] schema” or “[argument or proof] skeleton”.) A derivation structure is composed of arbitrary rules. The general form of an arbitrary inference rule is the following, where the square brackets indicate assumptions which can be discharged at the application of the rule: in short Obviously, the standard introduction and elimination rules are particular cases of such rules. As a generalization of the standard reductions of maximal formulas it is supposed that certain reduction procedures are given. A reduction procedure transforms a given derivation structure into another one. A set of reduction procedures is called a derivation reduction system and denoted by J. Reductions serve as justifying procedures for non-canonical steps, i.e. for all steps, which are not self-justifying, i.e., which are not introduction steps. Therefore a reduction system J is also called a justification. Reduction procedures must satisfy certain constraints such as closure under substitution. As the validity of a derivation not only depends on the atomic system S but also on the derivation reduction system used, we define the validity of a derivation structure with respect to the underlying atomic basis S and with respect to the justification J:

1. Every closed derivation in S is S-valid with respect to J (for every J).
2. A closed canonical derivation structure is S-valid with respect to J, if all its immediate substructures are S-valid with respect to J.
3. A closed non-canonical derivation structure is S-valid with respect to J, if it reduces, with respect to J, to a canonical derivation structure, which is S-valid with respect to J.
4. An open derivation structure where all open assumptions of D are among A1,…,An, is S-valid with respect to J, if for every extension S′ of S and every extension J′ of J, and for every list of closed derivation structures which are S′-valid with respect to J′, is S′-valid with respect to J′.

(See Prawitz, 1973, p. 236; 1974, p. 73; 2006; Schroeder-Heister, 2006.) In clause (iv), the reason for considering extensions J′ of J and extensions S′ of S, is a monotonicity constraint. Derivations should remain valid if one’s knowledge incorporated in the atomic system and in the reduction procedures is extended.

A corresponding concept of universal validity can be defined as follows: Let S0 be the atomic system with only propositional variables as atoms and with no inference rules. Let L(S0) be a set of derivation structures over S0 together with a justification J . Let v be an assignment of S-formulas to propositional variables. Let Dv be obtained from D by substituting in D propositional variables p with v(p). Let Jv be the set of reductions which acts on derivations Dv in the same way as J acts on D (i.e., Jv is the homomorphic image of J under v). Then a derivation structure D in L(S0) (i.e. a derivation structure containing only propositional variables as atoms) is defined to be universally valid with respect to J iff for every S and every v, Dv is S-valid with respect to Jv. It is easy to see that D is universally valid with respect to J iff D is S0-valid with respect to J . This means that we can use the term “valid” (with respect to some J ) interchangeably for both universal and S0-validity.

Validity with respect to some J can be viewed as a generalized notion of logical validity. In fact, if we specialize J to the standard reductions of intuitionistic logic, then all derivations in intuitionistic logic are valid with respect to J (see below). The S-validity of a generalized inference rule with respect to a justification J means that for all derivations which are S′-valid with respect to J′ for extensions S′ and J′ of S and J , respectively, the derivation is S′-valid with respect to J′. For a simple inference rule this means that if it is S-valid with respect to J , it is S-valid with respect to J when viewed as a one-step derivation structure.

This gives rise to a corresponding notion of consequence (see also Prawitz, 1985). Instead of saying that the rule is S-valid with respect to J , we may say that A is a consequence of A1,,An with respect to S and J, formally A1,,AnS,J A. If we consider universal validity with respect to J , we may speak of consequence with respect to J, formally A1,,AnJ A. Finally, if there is some J such that universal validity holds for J , then we may speak of logical consequence, formally A1,,AnA.

This makes proof-theoretic consequence differ from constructive consequence according to which would be defined as valid with respect to a constructive function f, if f transforms valid arguments of the premisses A1,,An into a valid argument of the conclusion A. Actually, it is not always possible to extract such a constructive function from our derivation reduction system, as a reduction system J serving as a justification need not be deterministic, which means that it merely generates a constructive relation on arguments. However, constructive consequence may be viewed as a limiting case of proof-theoretic consequence.

Examples of proof-theoretic validity

The following are the standard reductions for conjunction, disjunction and implication, as used in proofs of normalization. For simplicity, we disregard atomic systems S and speak of J-validity for validity with respect to J . First we observe that any derivation that results from the composition of J-valid rules and/or J-valid derivations is itself J-valid. For example, the derivation is J-valid, if the rules as well as the derivations D1 and D2 are J-valid.

As our first example, we show that the rule of → elimination (modus ponens) is valid with respect to {sr(→)}, i.e., with respect to the justification consisting just of the standard reduction for implication. For that we have to show that for any J ⊇{sr(→)}, and for all closed J-valid derivations the derivation is J-valid. Since D1 is closed J-valid, it is of the form, or reduces with respect to J to the form where D1′ is J-valid. Applying sr(→), which is part of J , to yields the derivation This derivation is J-valid, as it is the result of a composition of the J-valid derivations D1′ and D2. In a similar way we can demonstrate the validity of ∧ and ∨ elimination with respect to the standard reductions sr(∧) and sr(∨) as justifications.

As our second example, we show that the rule of importation is valid with respect to the justification Jimp = {sr(→),sr(∧),r1,r2}, where sr(→) and sr(∧) are, as before, the standard reductions for implication and conjunction, and r1 and r2 are the following reductions: We have to show that for every JJimp and for every closed J-valid derivation the derivation is J-valid. Since D is closed J-valid, it is of the form, or reduces with respect to J to the form where D′ is J-valid. Applying r1 to this derivation yields which is J-valid, as it is composed of the J-valid derivation D′ and J-valid rules (note that → elimination is J-valid since sr(→) belongs to J , and introduction rules are trivially valid). This means that D1 reduces with respect to J to which, by means of r2, reduces to The latter derivation structure is J-valid as being composed of the J-valid derivation structure D′ and J-valid rules (∧ elimination and → elimination are J-valid, because sr(→) and sr(∧) are in J ).

Alternatively, Rimp can be shown to be valid with respect to Jimp′ = {sr(→),sr(∧),r3}, where r3 is defined as: The comparison of the standard reductions (sr(→), sr(∧), sr(∨)) with the reductions r1,r2 and r3 shows that the former are elementary in the sense that they just compose given subderivations, whereas r1,r2 and r3 use additional steps to generate their output. r1 uses → E and introduction rules, r2 uses ∧E and introduction rules, and r3 uses both → E and ∧E, and introduction rules. In using standard elimination inferences, both Jimp and Jimp′ have to rely on the standard reductions for the connectives involved. Jimp can be viewed more elementary than Jimp′ in that it not simply produces a natural deduction derivation, but requires first a reduction of the premiss derivation of Rimp in order to be able to apply r1. In generating a derivation of the conclusion of Rimp from its premiss, Jimp comes nearest to constructive semantics, where just a transformation of derivations is required. The example of importation shows that not every valid rule has a justification consisting of elementary reductions only. As soon as one has a right-iterated implication in the premiss of a rule, we have to rely on non-elementary reductions to establish its validity.

Remarks on Prawitz’s completeness conjecture

If we argue classically, we can disregard justifications and rephrase the definition of validity of proofs as a definition of validity of formulas as follows. We consider conjunction-disjunction-implication logic, which is essentially minimal logic.

1. An atomic formula A is S-valid, if it is derivable in S.
2. A conjunction AB is S-valid, if both A and B are S-valid.
3. A disjunction AB is S-valid, if either A or B is S-valid.
4. An implication AB is S valid, if for every extension S′ of S, if A if S′-valid then B is S′-valid.

This very much resembles Kripke-semantics of intuitionistic logic (see Troelstra and van Dalen, 1988, Ch. 2). The reference points (worlds) are atomic systems S, and accessibility is the extension relation between such systems. We can identify an atomic system with the set of atoms and rules derivable in it. Furthermore, we can identify rules with implications, as implications together with modus ponens behave like rules. The atomic systems S can thus be identified with deductively closed sets of implications. Together with the subset ordering as accessibility relation, we obtain exactly what in Kripke-style completeness proofs is known as the canonical model for implicational logic. Thus we can conclude that for implicational logic (and, in fact, for implication-conjunction logic), Prawitz’s completeness conjecture is correct, i.e., conjunction-implication logic is complete with respect to validity-based semantics.

However, the analogy to the canonical model breaks down if we add disjunction. In this case, in Kripke-style completeness proofs one has to require saturation, saying that, if a disjunction is member of a world of the canonical model, then so is one of its disjuncts. An explicit counterexample to Prawitz’s completeness conjecture can actually be given. Piecha, de Campos Sanz and Schroeder-Heister (2015) have shown that Harrop’s rule

 ¬A → (B∨C) (¬A → B) ∨ (¬A → C)

is valid but not derivable in intuitionistic logic.

It should be mentioned that even the above verification of Prawitz’s completeness conjecture for implicational logic only holds if we allow the atomic systems to contain primitive rules which discharge assumptions, and not solely production rules. Only then there is a full analogy between (iterated) implications and (higher-level) rules, which is needed for the parallelism between atomic systems and their extensions on one side and the canonical model on the other. Otherwise counterexamples to completeness can be constructed (see Sandqvist, 2009).

It should also be noticed that it is not fully clear of whether the validity-based semantics presented here is exactly what Prawitz intended. In Prawitz (1971) he formulates a clause for implication where he refers to arbitrary extensions of atomic systems, but in Prawitz (1973), where he formulates the completeness conjecture, and also in later papers, he does not consider extensions. Considering extensions in the clause for implication is crucial for the analogy to Kripke models on which we have drawn here. Without considering extensions we are loosing monotony, i.e., something shown to be valid in S need no longer be valid if S is extended, which is an inconvenient result. Therefore we have used extensions throughout this article. A rationale for not considering extensions would be to regard atomic systems as definitions in the sense of definitional reflection (see section 2.3.2) rather than just production systems describing an information state. For further discussions of this topic see de Campos Sanz, Piecha and Schroeder-Heister (2014), Piecha (2016), and Piecha and Schroeder-Heister (2016a).