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.

The complexity of the modal predicate logic of “true in every transitive model of ZF”

1997 ◽  
Vol 62 (4) ◽  
pp. 1371-1378
Author(s):  
Vann McGee
Keyword(s):  
Lower Bound ◽  
Set Theory ◽  
Predicate Logic ◽  
Alternative Conception ◽  
Predicate Calculus ◽  
Modal Formula ◽  
Sentential Calculus ◽  
Transitive Model ◽  
Modal Predicate Logic

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕ is true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining an interpretation to be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement that ϕ* is true in every transitive model of ZF, and stipulating that a modal formula ϕ is valid if and only if, for every interpretation *, ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete .We also look at a variant notion of validity according to which a formula ϕ counts as valid if and only if, for every interpretation *, ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which is in the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.

A formalization of the theory of ordinal numbers

1965 ◽  
Vol 30 (3) ◽  
pp. 295-317 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Set Theory ◽  
Natural Extension ◽  
Mathematical Induction ◽  
Predicate Calculus ◽  
Transfinite Induction ◽  
First Order ◽  
Recursive Functions ◽  
Ordinal Numbers ◽  
Primitive Recursive ◽  
Order Predicate Calculus

Although Peano's arithmetic can be developed in set theories, it can also be developed independently. This is also true for the theory of ordinal numbers. The author formalized the theory of ordinal numbers in logical systems GLC (in [2]) and FLC (in [3]). These logical systems which contain the concept of ‘arbitrary predicates’ or ‘arbitrary functions’ are of higher order than the first order predicate calculus with equality. In this paper we shall develop the theory of ordinal numbers in the first order predicate calculus with equality as an extension of Peano's arithmetic. This theory will prove to be easy to manage and fairly powerful in the following sense: If A is a sentence of the theory of ordinal numbers, then A is a theorem of our system if and only if the natural translation of A in set theory is a theorem of Zermelo-Fraenkel set theory. It will be treated as a natural extension of Peano's arithmetic. The latter consists of axiom schemata of primitive recursive functions and mathematical induction, while the theory of ordinal numbers consists of axiom schemata of primitive recursive functions of ordinal numbers (cf. [5]), of transfinite induction, of replacement and of cardinals. The latter three axiom schemata can be considered as extensions of mathematical induction.In the theory of ordinal numbers thus developed, we shall construct a model of Zermelo-Fraenkel's set theory by following Gödel's construction in [1]. Our intention is as follows: We shall define a relation α ∈ β as a primitive recursive predicate, which corresponds to F′ α ε F′ β in [1]; Gödel defined the constructible model Δ using the primitive notion ε in the universe or, in other words, using the whole set theory.

Reduction to a dyadic predicate

1954 ◽  
Vol 19 (3) ◽  
pp. 180-182 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
Quantification Theory ◽  
Logical Type ◽  
Image Position ◽  
The Universe

Consider any interpreted theory Θ, formulated in the notation of quantification theory (or lower predicate calculus) with interpreted predicate letters. It will be proved that Θ is translatable into a theory, likewise formulated in the notation of quantification theory, in which there is only one predicate letter, and it a dyadic one.Let us assume a fragment of set theory, adequate to assure the existence, for all x and y without regard to logical type, of the set {x, y) whose members are x and y, and to assure the distinctness of x from {x, y} and {{x}}. ({x} is explained as {x, x}.) Let us construe the ordered pair x; y in Kuratowski's fashion, viz. as {{x}, {x, y}}, and then construe x;y;z as x;(y;z), and x;y;z;w as x;(y;z;w), and so on. Let us refer to w, w;w, w;w;w, etc. as 1w, 2w, 3w, etc.Suppose the predicates of Θ are ‘F1’, ‘F2’, …, finite or infinite in number, and respectively d1-adic, d2-adic, …. Now let Θ′ be a theory whose notation consists of that of quantification theory with just the single dyadic predicate ‘F’, interpreted thus:The universe of Θ′ is to comprise all objects of the universe of Θ and, in addition, {x, y) for every x and y in the universe of Θ′. (Of course the universe of Θ may happen already to comprise all this.)Now I shall show how the familiar notations ‘x = y’, ‘x = {y, z}’, etc., and ultimately the desired ‘’, ‘’, etc. themselves can all be defined within Θ′.

The consistency of classical set theory relative to a set theory with intu1tionistic logic

1973 ◽  
Vol 38 (2) ◽  
pp. 315-319 ◽  
Author(s):  
Harvey Friedman
Keyword(s):  
Set Theory ◽  
Classical Theory ◽  
Intuitionistic Logic ◽  
Classical Logic ◽  
Predicate Calculus ◽  
Basic Tool ◽  
Axiom Scheme ◽  
Power Set ◽  
Image Position

Let ZF be the usual Zermelo-Fraenkel set theory formulated without identity, and with the collection axiom scheme. Let ZF−-extensionality be obtained from ZF by using intuitionistic logic instead of classical logic, and dropping the axiom of extensionality. We give a syntactic transformation of ZF into ZF−-extensionality.Let CPC, HPC respectively be classical, intuitionistic predicate calculus without identity, whose only homological symbol is ∈. We use the ~ ~-translation, a basic tool in the metatheory of intuitionistic systems, which is defined byThe two fundamental lemmas about this ~ ~ -translation we will use areFor proofs, see Kleene [3, Lemma 43a, Theorem 60d].This - would provide the desired syntactic transformation at least for ZF into ZF− with extensionality, if A− were provable in ZF− for each axiom A of ZF. Unfortunately, the ~ ~-translations of extensionality and power set appear not to be provable in ZF−. We therefore form an auxiliary classical theory S which has no extensionality and has a weakened power set axiom, and show in §2 that the ~ ~-translation of each axiom of Sis provable in ZF−-extensionality. §1 is devoted to the translation of ZF in S.

A set of axioms for logic

1944 ◽  
Vol 9 (1) ◽  
pp. 1-19 ◽  
Author(s):  
Theodore Hailperin
Keyword(s):  
Mathematical Logic ◽  
Set Theory ◽  
Predicate Calculus ◽  
Set Membership ◽  
New Foundations

One of the preeminent problems confronting logicians is that of constructing a system of logic which will be adequate for mathematics. By a system's being adequate for mathematics, we mean that all mathematical theorems in general use can be deduced within the system. Several distinct logical systems, all having this end in view, have been proposed. Among these perhaps the best known are the systems referred to as “Principia Mathematica” and “set theory.” In both of these systems (we refer to the revised and simplified versions) there is a nucleus of propositions which can be derived by using only the axioms and rules of the restricted predicate calculus. However, if anything like adequacy for mathematics is to be expected, additional primitives and axioms must be added to the restricted predicate calculus. It is in their treatment of the additional primitive ε, denoting class or set membership, that the above-mentioned systems differ.In addition to these two, a third and a stronger system has been proposed by W. V. Quine in his paper New foundations for mathematical logic. It is with this system of Quine's that our work is concerned and of which we now give a brief description.

On an Ackermann-type set theory

1973 ◽  
Vol 38 (3) ◽  
pp. 410-412
Author(s):  
John Lake
Keyword(s):  
Set Theory ◽  
Measurable Cardinal ◽  
Large Cardinal ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Individual Constant ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Universal Closure

Ackermann's set theory A* is usually formulated in the first order predicate calculus with identity, ∈ for membership and V, an individual constant, for the class of all sets. We use small Greek letters to represent formulae which do not contain V and large Greek letters to represent any formulae. The axioms of A* are the universal closures ofwhere all free variables are shown in A4 and z does not occur in the Θ of A2.A+ is a generalisation of A* which Reinhardt introduced in [3] as an attempt to provide an elaboration of Ackermann's idea of “sharply delimited” collections. The language of A+ is that of A*'s augmented by a new constant V′, and its axioms are A1–A3, A5, V ⊆ V′ and the universal closure ofwhere all free variables are shown.Using a schema of indescribability, Reinhardt states in [3] that if ZF + ‘there exists a measurable cardinal’ is consistent then so is A+, and using [4] this result can be improved to a weaker large cardinal axiom. It seemed plausible that A+ was stronger than ZF, but our main result, which is contained in Theorem 5, shows that if ZF is consistent then so is A+, giving an improvement on the above results.

Natural models and Ackermann-type set theories

1975 ◽  
Vol 40 (2) ◽  
pp. 151-158 ◽  
Author(s):  
John Lake
Keyword(s):  
Set Theory ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Individual Constant ◽  
Image Position ◽  
Order Predicate Calculus

Our results concern the natural models of Ackermann-type set theories, but they can also be viewed as results about the definability of ordinals in certain sets.Ackermann's set theory A was introduced in [1] and it is now formulated in the first order predicate calculus with identity, using ∈ for membership and an individual constant V for the class of all sets. We use the letters ϕ, χ, θ, and χ to stand for formulae which do not contain V and capital Greek letters to stand for any formulae. Then, the axioms of A* are the universal closures ofwhere all the free variables are shown in A4 and z does not occur in the Θ of A2. A is the theory A* − A5.Most of our notation is standard (for instance, α, β, γ, δ, κ, λ, ξ are variables ranging over ordinals) and, in general, we follow the notation of [7]. When x ⊆ Rα, we use Df(Rα, x) for the set of those elements of Rα which are definable in 〈Rα, ∈〉, using a first order ∈-formula and parameters from x.We refer the reader to [7] for an outline of the results which are known about A, but we shall summarise those facts which are frequently used in this paper.

Sign in / Sign up

Export Citation Format

Share Document