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 A₁,…,A_n, 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 S₀ be the atomic system with only propositional variables as atoms and with no inference rules. Let L(S₀) be a set of derivation structures over S₀ together with a justification J . Let v be an assignment of S-formulas to propositional variables. Let D^v be obtained from D by substituting in D propositional variables p with v(p). Let J^v be the set of reductions which acts on derivations D^v in the same way as J acts on D (i.e., J^v is the homomorphic image of J under v). Then a derivation structure D in L(S₀) (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, D^v is S-valid with respect to J^v. It is easy to see that D is universally valid with respect to J iff D is S₀-valid with respect to J . This means that we can use the term “valid” (with respect to some J ) interchangeably for both universal and S₀-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 A₁,…,A_n with respect to S and J, formally A₁,…,A_n⊨_S,J A. If we consider universal validity with respect to J , we may speak of consequence with respect to J, formally A₁,…,A_n⊨_J A. Finally, if there is some J such that universal validity holds for J , then we may speak of logical consequence, formally A₁,…,A_n⊨ A.

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 A₁,…,A_n 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 D₁ and D₂ 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 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 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 D₁′ and D₂. 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 J_imp = {sr(→),sr(∧),r₁,r₂}, where sr(→) and sr(∧) are, as before, the standard reductions for implication and conjunction, and r₁ and r₂ are the following reductions:

We have to show that for every J ⊇J_imp 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 r₁ 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 D₁ reduces with respect to J to

which, by means of r₂, 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, R_imp can be shown to be valid with respect to J_imp′ = {sr(→),sr(∧),r₃}, where r₃ is defined as:

The comparison of the standard reductions (sr(→), sr(∧), sr(∨)) with the reductions r₁,r₂ and r₃ shows that the former are elementary in the sense that they just compose given subderivations, whereas r₁,r₂ and r₃ use additional steps to generate their output. r₁ uses → E and introduction rules, r₂ uses ∧E and introduction rules, and r₃ uses both → E and ∧E, and introduction rules. In using standard elimination inferences, both J_imp and J_imp′ have to rely on the standard reductions for the connectives involved. J_imp can be viewed more elementary than J_imp′ in that it not simply produces a natural deduction derivation, but requires first a reduction of the premiss derivation of R_imp in order to be able to apply r₁. In generating a derivation of the conclusion of R_imp from its premiss, J′_imp 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 A∧B is S-valid, if both A and B are S-valid.
3. A disjunction A∨B is S-valid, if either A or B is S-valid.
4. An implication A → B 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. Using ideas by de Campos Sanz and Piecha (2012—see Other Internet Resources), it can be shown that Mints's rule

is valid but not derivable in positive 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.