Home Philosophy Advances in Proof-Theoretic Semantics

## Prawitz's ConjecturePrawitz 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 [33], 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:
where the
[
The notation is the same as the one used for the logical rules of natural deduction (see Gentzen [7]). That is, rules of this form allow one to conclude
The notions [
It is
A Now
(ii) A closed canonical derivation structure is substructures are (iii) A closed non-canonical derivation structure is (iv) An open derivation structure
where all open assumptions of closed derivation structures
derivation structure
is Extensions 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 [19]. A completeness conjecture for intuitionistic logic and a similar notion of validity is made in Prawitz [22]:
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 [7]; cf. [1]) 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 [22], 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 |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2019