Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-25T07:06:56.562Z Has data issue: false hasContentIssue false
  • English
  • Français

A weak absolute consistency proof for some systems of illative combinatory logic

Published online by Cambridge University Press:  12 March 2014

M.W. Bunder
M.W. Bunder*
Affiliation:
The University of Wollongong, Wollongong NSW 2500, Australia
Get access Rights & Permissions [Opens in a new window]

Extract

A large number of formal systems based on combinatory logic or λ-calculus have been extended to include first order predicate calculus. Several of these however have been shown to be inconsistent, all, as far as the author knows, in the strong sense that all well formed formulas (which here include all strings of symbols) are provable. We will call the corresponding consistency notion—an arbitrary wff ⊥ is provable—weak consistency. We will say that a system is strongly consistent if no formula and its negation are provable.

Now for some systems, such as that of Kuzichev [11], the strong and weak consistency notions are equivalent, but in the systems of [5] and [6], which we will be considering, they are not. Each of these systems is strong enough to have all of ZF set theory, except Grounding and Choice, interpretable in it, and the system of [5] can also encompass first order arithmetic (see [7]). It therefore seems unlikely that a strong consistency result could be proved for these systems using elementary methods. In this paper however, we prove the weak consistency of both these systems by means that could be formulated, at least within the theory of [5]. The method also applies to the typed systems of Curry, Hindley and Seldin [10] and to Seldin's generalised types [12].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 48 , Issue 3 , September 1983 , pp. 771 - 776
Copyright
Copyright © Association for Symbolic Logic 1983

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]Bunder, M.W., Propositional and predicate calculuses based on combinatory logic, Notre Dame Journal of Formal Logic, vol. 15 (1974), pp. 25–34.CrossRefGoogle Scholar
[2]Bunder, M.W., Consistency notions in illative combinatory logic, this Journal, vol. 42 (1977), pp. 527–529.Google Scholar
[3]Bunder, M.W., Illative combinatory logic without equality as a primitive predicate, Notre Dame Journal of Formal Logic, vol. 23 (1982), pp. 62–70.CrossRefGoogle Scholar
[4]Bunder, M.W., Predicate calculus of arbitrarily high finite order, Archiv für Mathematische Logik und Grundlagenforschung, vol. 22 (1982), pp. 1–10.Google Scholar
[5]Bunder, M.W., A one axiom set theory based on higher order predicate calculus, Archiv für Mathematische Logik und Grundlagenforschung (to appear).Google Scholar
[6]Bunder, M.W., Set theory in predicate calculus with equality, Archiv für Mathematische Logik und Grumtlagenforschung (to appear).Google Scholar
[7]Bunder, M.W., Cardinal and natural numbers in illative combinatory logic, The University of Wollongong, Department of Mathematics, Preprint Series No. 25/80.Google Scholar
[8]Bunder, M.W., A characterization of inconsistency proofs in illative combinatory logic, The University of Wollongong, Department of Mathematics, Preprint Series No. 3/81.Google Scholar
[9]Curry, H.B. and Feys, R., Combinatory Logic, vol. 1, North-Holland, Amsterdam, 1959.Google Scholar
[10]Curry, H.B., Hindley, J.R.,and Seldin, J.P., Combinatory Logic, vol. 2, North-Holland, Amsterdam, 1972.Google Scholar
[11]Kuzichev, A.S., Sequential systems of λ-conversion and of combinatory logic, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Seldin, J.P. and Hindley, J.R., editors), Academic Press, London, 1980, pp. 141–155.Google Scholar
[12]Seldin, J.P., Progress report on generalised functionality, Annals of Mathematical Logic, vol. 17 (1979), pp. 29–59.CrossRefGoogle Scholar