Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-26T12:00:37.473Z Has data issue: false hasContentIssue false

Normalized natural deduction systems for some relevant logics I: The logic DW

Published online by Cambridge University Press:  12 March 2014

Ross T. Brady*
Affiliation:
Philosophy Program, La Trobe University, Victoria, 3086, Australia. E-mail: [email protected]

Extract

Fitch-style natural deduction was first introduced into relevant logic by Anderson in [1960], for the sentential logic E of entailment and its quantincational extension EQ. This was extended by Anderson and Belnap to the sentential relevant logics R and T and some of their fragments in [ENT1], and further extended to a wide range of sentential and quantified relevant logics by Brady in [1984]. This was done by putting conditions on the elimination rules, →E, ~E, ⋁E and ∃E, pertaining to the set of dependent hypotheses for formulae used in the application of the rule. Each of these rules were subjected to the same condition, this condition varying from logic to logic. These conditions, together with the set of natural deduction rules, precisely determine the particular relevant logic. Generally, this is a simpler representation of a relevant logic than the standard Routley-Meyer semantics, with its existential modelling conditions stated in terms of an otherwise arbitrary 3-place relation R, which is defined over a possibly infinite set of worlds. Readers are urged to refer to Brady [1984], if unfamiliar with the above natural deduction systems, but we will introduce in §2 a modified version in full detail.

Natural deduction for classical logic was invented by Jaskowski and Gentzen, but it was Prawitz in [1965] who normalized natural deduction, streamlining its rules so as to allow a subformula property to be proved. (This key property ensures that each formula in the proof of a theorem is indeed a subformula of that theorem.)

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 2006

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1960] Anderson, A. R., Completeness theorems for the systems E of entailment and EQ of entailment with quantification, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, vol. 6 (1960), pp. 201216.CrossRefGoogle Scholar
[1975] Anederson, A. R. and Belnap, N. D. Jr., Entailment, the logic of relevance and necessity, vol. 1, Princeton University Press, 1975, [ENT1].Google Scholar
[1984] Brady, R. T., Natural deduction systems for some quantified relevant logics, Logique et Analyse, vol. 27 (1984), pp. 355377.Google Scholar
[1991] Brady, R. T., Gentzenization and decidability of some contraction-less relevant logics, Journal of Philosophical Logic, vol. 20 (1991), pp. 97117.CrossRefGoogle Scholar
[1996] Brady, R. T., Relevant implication and the case for a weaker logic, Journal of Philosophical Logic, vol. 25 (1996), pp. 151183.CrossRefGoogle Scholar
[2003] Brady, R. T., Relevant logics and their rivals. Vol.2: A continuation of the work of R. Sylvan, R. K. Meyer, V. Plumwood and R. T. Brady, Ashgate, Aldershot, 2003, [RLR2].Google Scholar
[2006] Brady, R. T., Universal logic, CSLI, Stanford, 2006, [UL].Google Scholar
[1965] Prawitz, D., Natural deduction, a proof-theoretical study, Almqvist and Wiksell, Stockholm, 1965.Google Scholar
[1982] Routley, R., Meyer, R. K., Plumwood, V., and Brady, R. T., Relevant logics and their rivals, vol. 1, Ridgeview, Atascadero, 1982, [RLR1].Google Scholar
[1984] Slaney, J. K., A metacompleteness theorem for contraction-free relevant logics, Studia Logica, vol. 43 (1984), pp. 159168.CrossRefGoogle Scholar
[1987] Slaney, J. K., Reduced models for relevant logics without WI, Notre Dame Journal of Formal Logic, vol. 28 (1987), pp. 395407.CrossRefGoogle Scholar