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.

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.

scholarly journals LOGIC IN THE TRACTATUS

2017 ◽  
Vol 10 (1) ◽  
pp. 1-50 ◽  
Author(s):  
MAX WEISS
Keyword(s):  
Set Theory ◽  
Classical Logic ◽  
Logical System ◽  
Image Position ◽  
Countably Infinite ◽  
The Universe

AbstractI present a reconstruction of the logical system of the Tractatus, which differs from classical logic in two ways. It includes an account of Wittgenstein’s “form-series” device, which suffices to express some effectively generated countably infinite disjunctions. And its attendant notion of structure is relativized to the fixed underlying universe of what is named.There follow three results. First, the class of concepts definable in the system is closed under finitary induction. Second, if the universe of objects is countably infinite, then the property of being a tautology is $\Pi _1^1$-complete. But third, it is only granted the assumption of countability that the class of tautologies is ${\Sigma _1}$-definable in set theory.Wittgenstein famously urges that logical relationships must show themselves in the structure of signs. He also urges that the size of the universe cannot be prejudged. The results of this paper indicate that there is no single way in which logical relationships could be held to make themselves manifest in signs, which does not prejudge the number of objects.

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.

scholarly journals Set Theory INC# ∞# Based on Innitary Intuitionistic Logic with Restricted Modus Ponens Rule. Hyper Inductive Denitions. Application in Transcendental Number Theory. Generalized Lindemann-Weierstrass Theorem

2021 ◽  
pp. 70-119
Author(s):  
Jaykov Foukzon
Keyword(s):  
Number Theory ◽  
Set Theory ◽  
Intuitionistic Logic ◽  
Theoretical Language ◽  
Modus Ponens ◽  
Transcendental Number ◽  
Weierstrass Theorem ◽  
Induction Principle ◽  
Intuitionistic Set Theory ◽  
Intuitionistic Arithmetic

In this paper intuitionistic set theory INC#∞# in infinitary set theoretical language is considered. External induction principle in nonstandard intuitionistic arithmetic were derived. Non trivial application in number theory is considered.The Goldbach-Euler theorem is obtained without any references to Catalan conjecture. Main results are: (i) number ee is transcendental; (ii) the both numbers e + π and e − π are irrational.

Modal semantics without possible worlds

1981 ◽  
Vol 46 (1) ◽  
pp. 77-86 ◽  
Author(s):  
John T. Kearns
Keyword(s):  
Possible Worlds ◽  
The Other ◽  
Modal Operator ◽  
Logical Operators ◽  
Semantic Account ◽  
Necessary Truth ◽  
Modal Semantics ◽  
Propositional Language ◽  
Image Position ◽  
Plain Truth

In this paper I will develop a semantic account for modal logic by considering only the values of sentences (and formulas). This account makes no use of possible worlds. To develop such an account, we must recognize four values. These are obtained by subdividing (plain) truth into necessary truth (T) and contingent truth (t); and by subdividing falsity into contingent falsity (f) and necessary falsity (impossibility: F). The semantic account results from reflecting on these concepts and on the meanings of the logical operators.To begin with, we shall consider the propositional language L0. The language L0 has (1) infinitely many atomic sentences, (2) the two truth-functional connectives ∼, ∨, and the modal operator □. (Square brackets are used for punctuation.) The other logical expressions are defined as follows:D1 [A & B] = (def)∼[∼A ∨ ∼ B],D2 [A ⊃ B] = (def)[∼A ∨ B],D3 ◊ A =(def)∼□∼A.I shall use matrices to give partial characterizations of the significance of logical expressions in L0. For negation, this matrix is wholly adequate:Upon reflection, it should be clear that this matrix is the obviously correct matrix for negation.

scholarly journals Set Theory INC# ∞# Based on Infinitary Intuitionistic Logic with Restricted Modus Ponens Rule (Part.II) Hyper Inductive Definitions

2021 ◽  
pp. 90-112
Author(s):  
Jaykov Foukzon
Keyword(s):  
Number Theory ◽  
Set Theory ◽  
Intuitionistic Logic ◽  
Theoretical Language ◽  
Modus Ponens ◽  
Inductive Definitions ◽  
Induction Principle ◽  
Intuitionistic Set Theory ◽  
Intuitionistic Arithmetic

In this paper intuitionistic set theory INC# ∞# in infinitary set theoretical language is considered. External induction principle in nonstandard intuitionistic arithmetic were derived. Non trivial application in number theory is considered.The Goldbach-Euler theorem is obtained without anyreferences to Catalan conjecture.

Finite sets and frege structures

1999 ◽  
Vol 64 (4) ◽  
pp. 1552-1556 ◽  
Author(s):  
John L. Bell
Keyword(s):  
Set Theory ◽  
Finite Sets ◽  
The Family ◽  
Image Position ◽  
Intuitionistic Set Theory

Call a family of subsets of a set E inductive if and is closed under unions with disjoint singletons, that is, ifA Frege structure is a pair (E, ν) with ν a map to E whose domain dom(ν) is an inductive family of subsets of E such thatIn [2] it is shown in a constructive setting that each Frege structure determines a subset which is the domain of a model of Peano's axioms. In this note we establish, within the same constructive setting, three facts. First, we show that the least inductive family of subsets of a set E is precisely the family of decidable Kuratowski finite subsets of E. Secondly, we establish that the procedure presented in [2] can be reversed, that is, any set containing the domain of a model of Peano's axioms determines a map which turns the set into a minimal Frege structure: here by a minimal Frege structure is meant one in which dom(ν) is the least inductive family of subsets of E. And finally, we show that the procedures leading from minimal Frege structures to models of Peano's axioms and vice-versa are mutually inverse. It follows that the postulation of a (minimal) Frege structure is constructively equivalent to the postulation of a model of Peano's axioms.All arguments will be formulated within constructive (intuitionistic) set theory.

scholarly journals CONSERVATIVELY EXTENDING CLASSICAL LOGIC WITH TRANSPARENT TRUTH

2012 ◽  
Vol 5 (2) ◽  
pp. 354-378 ◽  
Author(s):  
DAVID RIPLEY
Keyword(s):  
Classical Logic ◽  
The Other ◽  
Proof System ◽  
Truth Predicate ◽  
Logical System ◽  
Proof Systems ◽  
The Face

This paper shows how to conservatively extend a classical logic with a transparent truth predicate, in the face of the paradoxes that arise as a consequence. All classical inferences are preserved, and indeed extended to the full (truth-involving) vocabulary. However, not all classical metainferences are preserved; in particular, the resulting logical system is nontransitive. Some limits on this nontransitivity are adumbrated, and two proof systems are presented and shown to be sound and complete. (One proof system features admissible Cut, but the other does not.)

On Being in a Quandary

2021 ◽  
pp. 209-260
Author(s):  
Crispin Wright
Keyword(s):  
Intuitionistic Logic ◽  
Subject Matter ◽  
Classical Logic ◽  
The Other ◽  
Sorites Paradox ◽  
Metaphysical Realism ◽  
Specific Kind ◽  
Epistemic Conception ◽  
Broad Form

This chapter addresses three problems: the problem of formulating a coherent relativism, the Sorites paradox, and a seldom noticed difficulty in the best intuitionistic case for the revision of classical logic. A response to the latter is proposed which, generalized, contributes towards the solution of the other two. The key to this response is a generalized conception of indeterminacy as a specific kind of intellectual bafflement—Quandary. Intuitionistic revisions of classical logic are merited wherever a subject matter is conceived both as liable to generate Quandary and as subject to a broad form of evidential constraint. So motivated, the distinctions enshrined in intuitionistic logic provide both for a satisfying resolution of the Sorites paradox and a coherent outlet for relativistic views about, for example, matters of taste and morals. An important corollary of the discussion is that an epistemic conception of vagueness can be prised apart from the strong metaphysical realism with which its principal supporters have associated it, and acknowledged to harbour an independent insight.

scholarly journals On an Application of Intermediate Logics

1960 ◽  
Vol 16 ◽  
pp. 119-133
Author(s):  
Toshio Umezawa
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Logical System ◽  
Intermediate Logics ◽  
Individual Variables ◽  
Classical Predicate

In [1] I investigated some logics intermediate between intuitionistic and classical predicate logics. The purpose of this paper is to show the possibility of applying some intermediate logics to mathematics namely, to show that some mathematical theorems which are provable in the classical logic but not provable in the intuitionistic logic are provable in some intermediate logics. Let LZ be the logical system obtained from LJ′ a variant of Gentzen’s LJ [2], by adding as axioms all those sequents which can be obtained from a sequent scheme Z by substitution for propositional, predicate, or individual variables.

Sign in / Sign up

Export Citation Format

Share Document