Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-17T16:04:28.599Z Has data issue: false hasContentIssue false

Implicational logics in natural deduction systems

Published online by Cambridge University Press:  12 March 2014

E.G.K. López-Escobar*
Affiliation:
University of Maryland, College Park, Maryland 20742

Extract

In 1959 M. Dummett [3] introduced the logic LC obtained by adding the axiom ACpqCqp to the formalization of the intuitionistic prepositional calculus having modus ponens and substitution as its rules of inference. Later on R. A. Bull [1] showed, by quite a roundabout way, that the implicational theses of LC were precisely the theses of the implicational calculus obtained by adding the axiom CCCpqrCCCqprr to the system of positive implication. In 1964 Bull [2] gave another proof, this time using results of Birkhoff concerning subdirectly reducible algebras.

The aim of this short note is to emphasize that the use of Gentzen's natural deduction systems (see Prawitz [4]) allows us to give a much more direct proof.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1982

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

[1]Bull, R. A., The implicational fragment of Dummett's LC, this Journal, vol. 27 (1962), pp. 189192.Google Scholar
[2]Bull, R. A., Some results for implicational calculi, this Journal, vol. 29 (1964), pp. 3339.Google Scholar
[3]Dummett, M., A propositional calculus with denumerable matrix, this Journal, vol. 24 (1959), pp. 96107.Google Scholar
[4]Prawitz, D., Natural deduction, A proof theoretic study, Almquist & Wiksell, Stockholm, 1965.Google Scholar