#### Supplement to Proof-Theoretic Semantics

## 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:

- Every closed derivation in
*S*is*S*-valid with respect to J (for every J). - A closed canonical derivation structure is
*S*-valid with respect to J, if all its immediate substructures are*S*-valid with respect to J. - 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. An open derivation structure

where all open assumptions of D are among

*A*_{1},…,*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 structureswhich 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*_{0} be the atomic system
with only propositional variables as atoms and with no inference rules.
Let L(*S*_{0}) be a set of derivation structures
over *S*_{0} 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*_{0}) (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*_{0}-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*_{0}-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*_{1}*,**…**,A*_{n}
*with respect to* *S* *and* J, formally
*A*_{1}*,**…**,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*_{1}*,**…**,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*_{1}*,**…**,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*_{1}*,**…**,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.

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_{1} and
D_{2} 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_{1} is closed J-valid, it is of the form, or reduces with respect to J to the
form

where D_{1}′ 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_{1}′ and D_{2}. 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*_{1}*,r*_{2}},
where *sr*(→) and *sr*(∧) are, as
before, the standard reductions for implication and conjunction, and
*r*_{1} and *r*_{2} 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*_{1} 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_{1} reduces with respect to J to

which, by means of
*r*_{2}, 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*_{3}},
where *r*_{3} is defined as:

The comparison of the standard reductions (*sr*(→),
*sr*(∧), *sr*(∨)) with the reductions
*r*_{1}*,r*_{2} and
*r*_{3} shows that the former are elementary in the
sense that they just compose given subderivations, whereas
*r*_{1}*,r*_{2} and
*r*_{3} use additional steps to generate their output.
*r*_{1} uses → E and introduction rules,
*r*_{2} uses ∧E and introduction rules, and
*r*_{3} 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*_{1}. 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.

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.

- An atomic formula
*A*is*S*-valid, if it is derivable in*S*. - A conjunction
*A*∧*B*is*S*-valid, if both*A*and*B*are*S*-valid. - A disjunction
*A*∨*B*is*S*-valid, if either*A*or*B*is*S*-valid. - 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. 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).