Hostname: page-component-8448b6f56d-c47g7 Total loading time: 0 Render date: 2024-04-16T09:10:45.583Z Has data issue: false hasContentIssue false
  • English
  • Français

Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems1

Published online by Cambridge University Press:  12 March 2014

Ronald Harrop
Ronald Harrop*
Affiliation:
University of Durham, Newcastle Upon Tyne
Get access Rights & Permissions [Opens in a new window]

Extract

In a previous paper [1] it was proved, among other results, that a closed disjunction of intuitionistic elementary number theory N can be proved if and only if at least one of its disjunctands is provable and that a closed formula of the type (Ex)B(x) is provable in N if and only if B(n) is provable for some numeral n. The method of proof was to show that, as far as closed formulas are concerned, N is equivalent to a calculus N1 for which the result is immediate. The main step in the proof consisted in showing that the set of provable formulas of N1 is closed under modus ponens. This was done by obtaining a subset of the set which is closed under modus ponens and contains all members of the original set, with which it is therefore identical.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 25 , Issue 1 , March 1960 , pp. 27 - 32
Copyright
Copyright © Association for Symbolic Logic 1960

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.)

Footnotes

1

The author wishes to thank the editor for many valuable suggestions regarding the presentation of this paper.

References

[1]Harrop, R., On disjunctions and existential statements in intuitionistic systems of logic, Mathematische Annalen, vol. 132 (1956), pp. 347–361.CrossRefGoogle Scholar
[2]Kleene, S. C., Introduction to metamathematics, New York and Toronto (Van Nostrana), Amsterdam (North Holland) and Groningen (Noordhoff), 1952.Google Scholar
[3]Kreisel, G., The non-derivability of ℸ (x)A(x) → (Ex)A(x), A primitive recursive, in intuitionistic formal systems (abstract), this Journal, vol. 23 (1958), p. 456–457.Google Scholar
[4]Kreisel, G., Interpretation of analysis by means of constructive functionals of finite types, Constructivity in mathematics, Amsterdam (North Holland), 1958, pp. 101–128.Google Scholar