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.

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.

Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae

1958 ◽  
Vol 23 (3) ◽  
pp. 317-330 ◽  
Author(s):  
G. Kreisel
Keyword(s):  
Present Article ◽  
Intuitionistic Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Formal Proof ◽  
Predicate Calculus ◽  
Open Problems

The purpose of the present article is to formulate in an intuitionistically meaningful manner the completeness problems for the intuitionistic predicate calculus, and to establish the completeness of certain fragments of it. In these proofs certain translations of classical logic into intuitionistic logic are used, in particular those discovered by Kolmogorov [11] and Gödel [3], and a new one in which negations of prenex formulae are central. Since the last one is of interest also independently of the completeness problems, the details are presented separately at the end of this paper.All arguments are intended to be intuitionistically valid unless the opposite is stated; in particular, ‘proof’ means intuitionistic proof, and ‘formal proof’ means proof in the relevant system of Heyting [4], [5].Open problems are mentioned in Remarks 3.1 and 8.1.German capitals denote formulae of predicate logic, Latin (italic) capitals denote predicate symbols or propositional letters.

On the formalisation of indirect discourse

1958 ◽  
Vol 23 (4) ◽  
pp. 417-419 ◽  
Author(s):  
R. L. Goodstein
Keyword(s):  
Predicate Logic ◽  
Logical Truth ◽  
Predicate Calculus ◽  
Inference Rules ◽  
First Order ◽  
Indirect Discourse ◽  
Image Position ◽  
Order Predicate Calculus

Mr. L. J. Cohen's interesting example of a logical truth of indirect discourse appears to be capable of a simple formalisation and proof in a variant of first order predicate calculus. His example has the form:If A says that anything which B says is false, and B says that something which A says is true, then something which A says is false and something which B says is true.Let ‘A says x’ be formalised by ‘A(x)’ and let assertions of truth and falsehood be formalised as in the following table.We treat both variables x and predicates A (x) as sentences and add to the familiar axioms and inference rules of predicate logic a rule permitting the inference of A(p) from (x)A(x), where p is a closed sentence.We have to prove that from

Embedding first order predicate logic in fragments of intuitionistic logic

1976 ◽  
Vol 41 (4) ◽  
pp. 705-718 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Propositional Calculus ◽  
Expressive Power ◽  
Predicate Calculus ◽  
First Order ◽  
Intuitionistic Propositional Calculus ◽  
Individual Variables ◽  
The One ◽  
Order Predicate Calculus

Some syntactically simple fragments of intuitionistic logic possess considerable expressive power compared with their classical counterparts.In particular, we consider in this paper intuitionistic second order propositional logic (ISPL) a formalisation of which may be obtained by adding to the intuitionistic propositional calculus quantifiers binding propositional variables together with the usual quantifier rules and the axiom scheme (Ex), where is a formula not containing x.The main purpose of this paper is to show that the classical first order predicate calculus with identity can be (isomorphically) embedded in ISPL.It turns out an immediate consequence of this that the classical first order predicate calculus with identity can also be embedded in the fragment (PLA) of the intuitionistic first order predicate calculus whose only logical symbols are → and (.) (universal quantifier) and the only nonlogical symbol (apart from individual variables and parentheses) a single monadic predicate letter.Another consequence is that the classical first order predicate calculus can be embedded in the theory of Heyting algebras.The undecidability of the formal systems under consideration evidently follows immediately from the present results.We shall indicate how the methods employed may be extended to show also that the intuitionistic first order predicate calculus with identity can be embedded in both ISPL and PLA.For the purpose of the present paper it will be convenient to use the following formalisation (S) of ISPL based on [3], rather than the one given above.

On weak completeness of intuitionistic predicate logic

1962 ◽  
Vol 27 (2) ◽  
pp. 139-158 ◽  
Author(s):  
G. Kreisel
Keyword(s):  
Predicate Logic ◽  
Predicate Calculus ◽  
Closed Formula ◽  
Logical Constants ◽  
Weak Completeness ◽  
Image Position

Suppose the ri-placed relation symbols Pi, 1 ≦ i ≦ k, are all the non-logical constants occurring in the closed formula , also written as , of Heyting's predicate calculus (HPC). Then HPC is called complete for provided , i.e.Here D ranges over arbitrary species, and over arbitrary (possibly incompletely defined) subspecies of ;

A new version of Beth semantics for intuitionistic logic

1977 ◽  
Vol 42 (2) ◽  
pp. 306-308 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Tree Structure ◽  
Truth Conditions ◽  
Truth Definition ◽  
Image Position ◽  
Constant Domains ◽  
Condition B

We use the notation of Kripke's paper [1]. Let M = (G, K, R) be a tree structure and D a domain and η a Beth model on M. The truth conditions of the Beth semantics for ∨ and ∃ are (see [1]):(a) η (A ∨ B, H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B, either η(A, H′) = T or η(B, H′) = T.(b) η(∃xA(x), H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B there exists an a ∈ D such that η(A (a), H′) = T.Suppose we change the truth definition η to η* by replacing condition (b) by the condition (b*) (well known from the Kripke interpretation):Call this type of interpretation the new version of Beth semantics. We proveTheorem 1. Intuitionistic predicate logic is complete for the new version of the Beth semantics.Since Beth structures are of constant domains, and in the new version of Beth semantics the truth conditions for ∧, →, ∃, ∀, ¬ are the same as for the Kripke interpretation, we get:Corollary 2. The fragment without disjunction of the logic CD of constant domains (i.e. with the additional schema ∀x(A ∨ B(x))→ A ∨ ∀xB(x), x not free in A) equals the fragment without disjunction of intuitionistice logic.

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.

Extensional interpretations of modal logics

1966 ◽  
Vol 31 (1) ◽  
pp. 23-45 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Predicate Logic ◽  
Modal Logics ◽  
Predicate Calculus ◽  
First Order ◽  
Image Position ◽  
Order Predicate Calculus ◽  
First Order Predicate Logic

By ΡL we shall mean the first order predicate logic based on S4. More explicitly: Let Ρ0 stand for the first order predicate calculus. The formalisation of Ρ0 used in the present paper will be given later. ΡL is obtained from Ρ0 by adding the rules the propositional constant □ and

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.

scholarly journals Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic

1998 ◽  
Vol 63 (3) ◽  
pp. 869-890 ◽  
Author(s):  
Wil Dekkers ◽  
Martin Bunder ◽  
Henk Barendregt
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Lambda Calculus ◽  
Preceding Paper ◽  
Predicate Calculus ◽  
Combinatory Logic ◽  
First Order ◽  
Two Systems

AbstractIllative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. In a preceding paper, [2], we considered 4 systems of illative combinatory logic that are sound for first order intuitionistic propositional and predicate logic. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations are closely related in a canonical way. In the cited paper we proved completeness of the two direct translations. In the present paper we prove that also the two indirect translations are complete. These proofs are direct whereas in another version, [3], we proved completeness by showing that the two corresponding illative systems are conservative over the two systems for the direct translations. Moreover we shall prove that one of the systems is also complete for predicate calculus with higher type functions.

Sign in / Sign up

Export Citation Format

Share Document