Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-22T20:09:59.052Z Has data issue: false hasContentIssue false
  • English
  • Français

On a theory of weak implications

Published online by Cambridge University Press:  12 March 2014

Mitsuhiro Okada
Mitsuhiro Okada*
Affiliation:
16-15, Kamishyakujii-Minami, Nerimaku, Tokyo 177, Japan Departments of Computer Science and Mathematics, University of Illinois, Urbana, Illinois 61801 Department of Philosophy, Keio University, Tokyo, Japan
Get access Rights & Permissions [Opens in a new window]

Extract

The purpose of this paper is to study logical implications which are much weaker than the implication of intuitionistic logic.

In §1 we define the system SI (system of Simple Implication) which is obtained from intuitionistic logic by restricting the inference rules of intuitionistic implication. The implication of the system SI is called the “simple implication” and denoted by ⊃, where the simple implication ⊃ has the following properties:

(1) The simple implication ⊃ is much weaker than the usual intuitionistic implication.

(2) The simple implication ⊃ can be interpreted by the notion of provability, i.e., we have a very simple semantics for SI so that a sentence A ⊃ B is interpreted as “there exists a proof of B from A”.

(3) The full-strength intuitionistic implication ⇒ is definable in a weak second order extension of SI; in other words, it is definable by help of a variant of the weak comprehension schema and the simple implication ⊃. Therefore, though SI is much weaker than the intuitionistic logic, the second order extension of SI is equivalent to the second order extension of the intuitionistic logic.

(4) The simple implication is definable in a weak modal logic MI by the use of the modal operator and the intuitionistic implication ⇒ with full strength. More precisely, A ⊃ B is defined as the strict implication of the form ◽(A ⇒ B).

In §1, we show (3) and (4). (2) is shown in §2 in a more general setting.

Semantics by introduction rules of logical connectives has been studied from various points of view by many authors (e.g. Gentzen [4], Lorentzen [5], Dummett [1], [2], Prawitz [8]. Martin-Löf [7], Maehara [6]). Among them Gentzen (in §§10 and 11 of [4]) introduced such a semantics in order to justify logical inferences and the mathematical induction rule. He observed that all of the inference rules of intuitionistic arithmetic, except for those on implication and negation, are justified by means of his semantics, but justification of the inference rules on implication and negation contains a circular argument for the interpretation by introduction rules, where the natural interpretation of A ⊃ B by ⊃-introduction rule is “there exists a proof of B from A ” (cf. §11 of Gentzen [4]).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 53 , Issue 1 , March 1988 , pp. 200 - 211
Copyright
Copyright © Association for Symbolic Logic 1988

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] Dummett, M., Elements of intuitionism, Oxford University Press, Oxford, 1977.Google Scholar
[2] Dummett, M., The philosophical basis of intuitionistic logic, Logic Colloquum ’73, North-Holland, Amsterdam, 1975, pp. 5–40.Google Scholar
[3] Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1935), pp. 176–210, 405–431; English translation in his Collected papers , North-Holland, Amsterdam, 1969.CrossRefGoogle Scholar
[4] Gentzen, G., Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol. 112 (1936), pp. 493–565; English translation in his Collected papers , North-Holland, Amsterdam, 1969.CrossRefGoogle Scholar
[5] Lorentzen, P., Einführung in die operative Logik and Mathematik, Springer-Verlag, Berlin, 1969.CrossRefGoogle Scholar
[6] Maehara, S., Semi-formal finitist proof of the transfinite induction in an initial segment of Cantor's second number class, Logic symposia, Hakone 1979, 1980, Lecture Notes in Mathematics, vol. 891, Springer-Verlag, Berlin, 1981, pp. 67–79.CrossRefGoogle Scholar
[7] Martin-Löf, P., On the meaning of the logical constants and the justifications of the logical laws, Lecture notes, Siena, 04 1983.Google Scholar
[8] Okada, M., A formalization of Gentzen's standpoint on consistency proofs of arithmetic (to appear).Google Scholar
[9] Prawitz, D., Natural deduction, Almqvist & Wiksell, Stockholm, 1965.Google Scholar
[10] Prawitz, D., Ideas and results in proof theory, Proceedings of the second Scandinavian logic symposium (Oslo, 1970), North-Holland, Amsterdam, 1971, pp. 235–307.CrossRefGoogle Scholar
[11] Prawitz, D., Proofs and the meaning and completeness of the logical constants, Essays on mathematical and philosophical logic (Hintikka, J. et al., editors), Reidel, Dordrecht, 1978, pp. 25–40.Google Scholar
[12] Schütte, K., Proof theory, Springer-Verlag, Berlin, 1977.CrossRefGoogle Scholar
[13] Schwichtenberg, H., Proof theory: some applicatioons of cut-elimination, Handbook of mathematical logic, North-Holland, Amsterdam, 1977, pp. 867–895.CrossRefGoogle Scholar
[14] Takeuti, G., Proof theory, North-Holland, Amsterdam, 1975.Google Scholar