Home Philosophy Advances in Proof-Theoretic Semantics

Prawitz's Conjecture

Prawitz has given several definitions of proof-theoretic validity (see Prawitz [18– 22]), and he has conjectured completeness of intuitionistic first-order logic for some of them. We here present a formulation for the fragment {→, ∨, ∧} as given by Schroeder-Heister , which captures the main ideas underlying Prawitz's definitions. The restriction to the fragment {→, ∨, ∧} is only made to keep the exposition simple; the definitions can be extended to the first-order case in a more or less straightforward way.

We first define some preliminary notions:

Definition 1 A (first-level) atomic system S is a (possibly empty) set of atomic rules of the form

a1 ... an b

where the ai and b are atoms. The set of premises {a1,..., an } in a rule can be empty; in this case the rule is an atomic axiom and of level 0. First-level atomic systems that do not contain atomic axioms are called proper first-level atomic systems.

Definition 2 An arbitrary inference rule has the form

[ A11,..., A1m1 ]

B1 ...

C [ An1,..., Anmn ]

Bn

The notation is the same as the one used for the logical rules of natural deduction (see Gentzen ). That is, rules of this form allow one to conclude C from the set of premises {B1,..., Bn } and to discharge any of the assumptions Aij , written in square brackets [ ], on which premises Bi might depend.

Definition 3 A derivation structure is a derivation tree composed of arbitrary inference rules. (Derivation structures correspond to what Prawitz calls '(argument or proof) schemata' or '(argument or proof) skeletons'.)

The notions open/closed and canonical/non-canonical as used for derivations in natural deduction are carried over to derivation structures. That is, a derivation structure with no open assumptions is closed, otherwise open. It is canonical, if it ends with one of the introduction rules

[ A] B

AB Ai (i 1 or 2)

A1 ∨ A2 A B

AB

It is non-canonical, if it does not.

Definition 4 A reduction procedure transforms a given derivation structure into another derivation structure.

A justification J of an arbitrary inference rule R, excluding introduction rules, is a set of reduction procedures which transform derivation structures D ending with an application of R into another derivation structure with the same end formula as D and having no more open assumptions than D (see Prawitz ).

Now validity with respect to atomic systems S and justifications J (short: (S, J )validity) can be defined as follows:

Definition 5 (i) Every closed derivation in an atomic system S is (S, J )-valid (for every justification J ).

(ii) A closed canonical derivation structure is (S, J )-valid, if all its immediate

substructures are (S, J )-valid.

(iii) A closed non-canonical derivation structure is (S, J )-valid, if it reduces, with respect to J , to a canonical derivation structure, which is (S, J )-valid.

(iv) An open derivation structure

A1 ... An

D

B

where all open assumptions of D are in { A1,..., An }, is (S, J )-valid, if for every extension St of S and every extension J t of J , and for every list of

closed derivation structures Di

Ai (for 1 ≤ in) which are (St, J t)-valid, the

derivation structure

D1 Dn

A1 ... An

D

B

is (St, J t)-valid.

Extensions St of S and J t of J are here understood in the set-theoretic sense as St ⊇ S and J t ⊇ J . Taking extensions into account ensures that (S, J )-validity of derivation structures is monotone with respect to extensions of S and J . This is an important constraint, if atomic systems S and justifications J are understood to represent, for example, states of knowledge.

In [18, Appendix A.1], Prawitz gave a definition of 'valid derivation', which makes use of extensions of atomic systems. However, in definitions of the more general notion of 'valid derivation structure' (i.e., of 'valid argument schema' or 'valid argument') he uses (consistent) extensions of justifications, but no extensions of atomic systems. Completeness of minimal logic for one such notion was conjectured in Prawitz . A completeness conjecture for intuitionistic logic and a similar notion of validity is made in Prawitz :

Conjecture 1 (Prawitz [22, p. 274]) Every valid inference rule that can be formulated within first-order languages holds as a derivable inference rule within the system of natural deduction for intuitionistic logic.

Prawitz's motivation for considering proof-theoretic notions of validity is to give an answer to the question of whether the elimination rules of Gentzen's intuitionistic system of natural deduction are the strongest possible ones justifiable in terms of the introduction rules of that system. Gentzen's idea that the introduction rules define the logical constants and that the elimination rules have to be justified on the basis of the introduction rules (see Gentzen ; cf. ) is reflected in the notion of validity by the fact that priority is given to canonical derivation structures, that is, to derivation structures ending with an introduction rule, to which non-canonical derivation structures have to be reduced. The (as yet unsettled) completeness conjecture implies a positive answer to that question.

In , Prawitz also gives a further modification of the notion of validity with respect to the role played by justifications. We will not discuss this modification here. Moreover, in what follows we will focus on proof-theoretic notions of validity for formulas instead of validity for derivation structures or inference rules. This approach has the advantage that justifications J (i.e., sets of reduction procedures for derivation structures) do not need to be considered at all. We here only mention that certain notions of validity for inference rules were given in Schroeder-Heister [28, 30], and that intuitionistic logic was claimed to be complete with respect to them there. Found a mistake? Please highlight the word and press Shift + Enter Subjects