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
- Every closed derivation in S is S-valid
with respect to
(for every . - A closed canonical derivation structure is S-valid
with respect to
, if all its immediate substructures are S-valid with respect to . - A closed non-canonical derivation structure is S-valid
with respect to
, if it reduces, with respect to , to a canonical derivation structure, which is S-valid with respect to . - An open derivation structure
where all open assumptions of are among , is S-valid with respect to , if for every extension of S and every extension of , and for every list of closed derivation structures which are -valid with respect to ,is
-valid with respect to .
(See Prawitz, 1973, p. 236; 1974, p. 73; 2006;
Schroeder-Heister, 2006.) In clause (iv), the reason for considering
extensions
A corresponding concept of universal validity can be defined
as follows: Let
Validity with respect to some
with respect to a justification
which are
is
this means that if it is S-valid with respect to
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
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
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
is
as well as the derivations
As our first example, we show that the rule of
the derivation
is
where
yields the derivation
This derivation is
As our second example, we show that the rule of importation
is valid with respect to the justification

We have to show that for every
the derivation
is
where
which is
which, by means of
The latter derivation structure is
Alternatively,

The comparison of the standard reductions
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 (see section 2.7 on sentence-based semantics in the main entry). 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
is S-valid, if both A and B are S-valid. - A disjunction
is S-valid, if either A or B is S-valid. - An implication
is S valid, if for every extension of S, if A if -valid then B is -valid.
This very much resembles Kripke-semantics of intuitionistic logic (see Troelstra and van Dalen, 1988, Ch. 2, and the entry on intuitionistic logic). 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) and, under weaker conditions, Piecha and Schroeder-Heister (2019) have shown that Harrop’s rule
which is not derivable in intuitionistic logic, is valid (see section 2.8 on semantical completeness).
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 gives 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 monotonicity, i.e., something shown to be valid in S need no longer be valid if S is extended, which is an inconvenient result. A possible 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 Piecha (2016).
At the epistemological level, validity-based semantics was further developed by Prawitz in his theory of grounds (Prawitz 2015). This approach has been significantly expanded by Piccolomini d’Aragona (2023) towards an encompassing formal theory of epistemic grounding, which, by using term-annotated propositions, is related to the formulae-as-types paradigm and thus to Martin-Löf’s proof-theoretic semantics (see section 2.2.3 on contructive type theory). For epistemological reasons, Prawitz himself is no longer pursuing the formal theory of proof-theoretic validity sketched in this supplement, which is based on the conceptual primacy of the validity of proofs over the validity of inferences. Instead he uses a general characterization of the interdependency of the concepts of inference, validity, argument, canonicality etc. without yet trying to bring these concepts into the well-founded order needed for an inductive definition (Prawitz 2024).