Predicate calculus and naive set theory in pure combinatory logic

1981 ◽  
Vol 21 (1) ◽  
pp. 169-177 ◽  
Author(s):  
M. W. Bunder
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
Combinatory Logic ◽  
Naive Set Theory

Set Theory based on Combinatory Logic.

1970 ◽  
Vol 35 (1) ◽  
pp. 147
Author(s):  
Jonathan P. Seldin ◽  
Maarten Wicher Visser Bunder
Keyword(s):  
Set Theory ◽  
Combinatory Logic

Naive Set Theory

2014 ◽  
pp. 1-8
Author(s):  
Ralf Schindler
Keyword(s):  
Set Theory ◽  
Naive Set Theory

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

1983 ◽  
Vol 48 (3) ◽  
pp. 771-776 ◽  
Author(s):  
M.W. Bunder
Keyword(s):  
Set Theory ◽  
Combinatory Logic ◽  
Weak Consistency ◽  
Consistency Proof ◽  
First Order ◽  
Formal Systems ◽  
Elementary Methods ◽  
Order Arithmetic ◽  
Strongly Consistent ◽  
Order Predicate Calculus

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

Combinator realizability of a constructive Morse set theory

1974 ◽  
Vol 39 (2) ◽  
pp. 226-234
Author(s):  
John Staples
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
Constructive Version

A constructive version of Morse set theory is given, based on Heyting's predicate calculus and with countable rather than full choice. An elaboration of the method of [5] is used to show that the theory is combinator-realizable in the sense defined there. The proof depends on the assumption of the syntactic consistency of the theory.The method is introduced by first treating a subtheory without countable choice of foundation.It is intended that the work can be read either classically or constructively, though whether the word constructive is correctly used as a description of either the theory or the metatheory is of course a matter of opinion.

Sign in / Sign up

Export Citation Format

Share Document