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 logic stronger than intuitionism

1971 ◽  
Vol 36 (2) ◽  
pp. 249-261 ◽  
Author(s):  
Sabine Görnemann
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Predicate Calculus ◽  
Theoretical Methods ◽  
Axiom Scheme ◽  
Simple Notion ◽  
Image Position ◽  
Quasi Ordering

S. A. Kripke has given [6] a very simple notion of model for intuitionistic predicate logic. Kripke's models consist of a quasi-ordering (C, ≤) and a function ψ which assigns to every c ∈ C a model of classical logic such that, if c ≤ c′, ψ(c′) is greater or equal to ψ(c). Grzegorczyk [3] described a class of models which is still simpler: he takes, for every ψ(c), the same universe. Grzegorczyk's semantics is not adequate for intuitionistic logic, since the formulawhere х is not free in α. holds in his models but is not intuitionistically provable. It is a conjecture of D. Klemke that intuitionistic predicate calculus, strengthened by the axiom scheme (D), is correct and complete with respect to Grzegorczyk's semantics. This has been proved independently by D. Klemke [5] by a Henkinlike method and me; another proof has been given by D. Gabbay [1]. Our proof uses lattice-theoretical methods.

Completeness of global intuitionistic set theory

1997 ◽  
Vol 62 (2) ◽  
pp. 506-528 ◽  
Author(s):  
Satoko Titani
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Classical Logic ◽  
Mathematical Object ◽  
The Other ◽  
Logical System ◽  
Logical Operators ◽  
Logical Symbol ◽  
Image Position ◽  
Intuitionistic Set Theory

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequentsConsidering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence.The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani [6], we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic.Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀x, ∃x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.

Frege's theorem in a constructive setting

1999 ◽  
Vol 64 (2) ◽  
pp. 486-488 ◽  
Author(s):  
John L. Bell
Keyword(s):  
Set Theory ◽  
Natural Numbers ◽  
The Family ◽  
Power Set ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Image Position ◽  
Excluded Middle ◽  
Intuitionistic Set Theory

By Frege's Theorem is meant the result, implicit in Frege's Grundlagen, that, for any set E, if there exists a map υ from the power set of E to E satisfying the conditionthen E has a subset which is the domain of a model of Peano's axioms for the natural numbers. (This result is proved explicitly, using classical reasoning, in Section 3 of [1].) My purpose in this note is to strengthen this result in two directions: first, the premise will be weakened so as to require only that the map υ be defined on the family of (Kuratowski) finite subsets of the set E, and secondly, the argument will be constructive, i.e., will involve no use of the law of excluded middle. To be precise, we will prove, in constructive (or intuitionistic) set theory, the followingTheorem. Let υ be a map with domain a family of subsets of a set E to E satisfying the following conditions:(i) ø ϵdom(υ)(ii)∀U ϵdom(υ)∀x ϵ E − UU ∪ x ϵdom(υ)(iii)∀UV ϵdom(5) υ(U) = υ(V) ⇔ U ≈ V.Then we can define a subset N of E which is the domain of a model of Peano's axioms.

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 Θ′.

An intuitionistically plausible interpretation of intuitionistic logic

1977 ◽  
Vol 42 (4) ◽  
pp. 564-578 ◽  
Author(s):  
H. C. M. de Swart
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Calculus ◽  
Mathematical Treatment ◽  
First Order ◽  
The Past ◽  
Definition Of ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Made In

Let IPC be the intuitionistic first-order predicate calculus. From the definition of derivability in IPC the following is clear:(1) If A is derivable in IPC, denoted by “⊦IPCA”, then A is intuitively true, that means, true according to the intuitionistic interpretation of the logical symbols. To be able to settle the converse question: “if A is intuitively true, then ⊦IPCA”, one should make the notion of intuitionistic truth more easily amenable to mathematical treatment. So we have to look then for a definition of “A is valid”, denoted by “⊨A”, such that the following holds:(2) If A is intuitively true, then ⊨ A.Then one might hope to be able to prove(3) If ⊨ A, then ⊦IPCA.If one would succeed in finding a notion of “⊨ A”, such that all the conditions (1), (2) and (3) are satisfied, then the chain would be closed, i.e. all the arrows in the scheme below would hold.Several suggestions for ⊨ A have been made in the past: Topological and algebraic interpretations, see Rasiowa and Sikorski [1]; the intuitionistic models of Beth, see [2] and [3]; the interpretation of Grzegorczyk, see [4] and [5]; the models of Kripke, see [6] and [7]. In Thirty years of foundational studies, A. Mostowski [8] gives a review of the interpretations, proposed for intuitionistic logic, on pp. 90–98.

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.

Undecidability of modal and intermediate first-order logics with two individual variables

1993 ◽  
Vol 58 (3) ◽  
pp. 800-823 ◽  
Author(s):  
D. M. Gabbay ◽  
V. B. Shehtman
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Calculus ◽  
Single Individual ◽  
First Order ◽  
Short Summary ◽  
Binary Predicate ◽  
Individual Variables ◽  
Image Position ◽  
Classical Predicate

The interest in fragments of predicate logics is motivated by the well-known fact that full classical predicate calculus is undecidable (cf. Church [1936]). So it is desirable to find decidable fragments which are in some sense “maximal”, i.e., which become undecidable if they are “slightly” extended. Or, alternatively, we can look for “minimal” undecidable fragments and try to identify the vague boundary between decidability and undecidability. A great deal of work in this area concerning mainly classical logic has been done since the thirties. We will not give a complete review of decidability and undecidability results in classical logic, referring the reader to existing monographs (cf. Suranyi [1959], Lewis [1979], and Dreben, Goldfarb [1979]). A short summary can also be found in the well-known book Church [1956]. Let us recall only several facts. Herein we will consider only logics without functional symbols, constants, and equality.(C1) The fragment of the classical logic with only monadic predicate letters is decidable (cf. Behmann [1922]).(C2) The fragment of the classical logic with a single binary predicate letter is undecidable. (This is a consequence of Gödel [1933].)(C3) The fragment of the classical logic with a single individual variable is decidable; in fact it is equivalent to Lewis S5 (cf. Wajsberg [1933]).(C4) The fragment of the classical logic with two individual variables is decidable (Segerberg [1973] contains a proof using modal logic; Scott [1962] and Mortimer [1975] give traditional proofs.)(C5) The fragment of the classical logic with three individual variables and binary predicate letters is undecidable (cf. Surańyi [1943]). In fact this paper considers formulas of the following typeφ,ψ being quantifier-free and the set of binary predicate letters which can appear in φ or ψ being fixed and finite.

On the existence of a saturated solution of the differential equation x′ = f (t, x)

1977 ◽  
Vol 78 (1-2) ◽  
pp. 97-99
Author(s):  
Johann Walter
Keyword(s):  
Differential Equation ◽  
Set Theory ◽  
Saturated Solution ◽  
Open Domain ◽  
Recursive Definition ◽  
Power Set ◽  
Image Position

SynopsisLet (1) x′ = f(t, x) be any differential equation and S0 the set of solutions of (1) with open domain. It is known that for every g ∊ S0 a non-continuable (= saturated) ∊ S0 exists which is an extension of g. Usually is represented in the form is a sequence in S0 defined by some sort of a variant of what is called ‘recursive definition’ in set theory. It will be shown that a functionexists (P(S0) is the power set of S0) such that the above-mentioned variant can be given the form: There exists a sequence in S0 such that

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.

On the axiom of extensionality – Part I

1956 ◽  
Vol 21 (1) ◽  
pp. 36-48 ◽  
Author(s):  
R. O. Gandy
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Formal System ◽  
Free Variable ◽  
Simple Theory ◽  
Predicate Calculus ◽  
Simple System ◽  
System A ◽  
Image Position

In part I of this paper it is shown that if the simple theory of types (with an axiom of infinity) is consistent, then so is the system obtained by adjoining axioms of extensionality; in part II a similar metatheorem for Gödel-Bernays set theory will be proved. The first of these results is of particular interest because type theory without the axioms of extensionality is fundamentally rather a simple system, and it should, I believe, be possible to prove that it is consistent.Let us consider — in some unspecified formal system — a typical expression of the axiom of extensionality; for example:where A(h) is a formula, and A(f), A(g) are the results of substituting in it the predicate variagles f, g for the free variable h. Evidently, if the system considered contains the predicate calculus, and if h occurs in A(h) only in parts of the form h(t) where t is a term which lies within the range of the quantifier (x), then 1.1 will be provable. But this will not be so in general; indeed, by introducing into the system an intensional predicate of predicates we can make 1.1 false. For example, Myhill introduces a constant S, where ‘Sϕψχω’ means that (the expression) ϕ is the result of substituting ψ for χ in ω.

Sign in / Sign up

Export Citation Format

Share Document