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 ;

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

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

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.

On the strong semantical completeness of the intuitionistic predicate calculus

1968 ◽  
Vol 33 (1) ◽  
pp. 1-7 ◽  
Author(s):  
Richmond H. Thomason
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
First Order ◽  
Semantic Tableaux ◽  
Weak Completeness ◽  
Skolem Theorem ◽  
Completeness Theorems

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

Craig interpolation theorem for intuitionistic logic and extensions Part III

1977 ◽  
Vol 42 (2) ◽  
pp. 269-271 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Possible Worlds ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Interpolation Theorem ◽  
Kripke Structure ◽  
Unary Predicate ◽  
The World ◽  
Image Position ◽  
Constant Domains ◽  
Positive Integers

This is a continuation of two previous papers by the same title [2] and examines mainly the interpolation property for the logic CD with constant domains, i.e., the extension of the intuitionistic predicate logic with the schemaIt is known [3], [4] that this logic is complete for the class of all Kripke structures with constant domains.Theorem 47. The strong Robinson consistency theorem is not true for CD.Proof. Consider the following Kripke structure with constant domains. The set S of possible worlds is ω0, the set of positive integers. R is the natural ordering ≤. Let ω0 0 = , Bn, is a sequence of pairwise disjoint infinite sets. Let L0 be a language with the unary predicates P, P1 and consider the following extensions for P,P1 at the world m.(a) P is true on ⋃i≤2nBi, and P1 is true on ⋃i≤2n+1Bi for m = 2n.(b) P is true on ⋃i≤2nBi, and P1 for ⋃i≤2n+1Bi for m = 2n.Let (Δ,Θ) be the complete theory of this structure. Consider another unary predicate Q. Let L be the language with P, Q and let M be the language with P1, Q.

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.

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 improved prenex normal form1

1962 ◽  
Vol 27 (3) ◽  
pp. 317-326 ◽  
Author(s):  
C. C. Chang ◽  
H. Jerome Keisler
Keyword(s):  
Positive Integer ◽  
Predicate Logic ◽  
Atomic Formula ◽  
First Order ◽  
Empty String ◽  
Image Position ◽  
First Order Predicate Logic

Let ℒ be the set of all formulas of a given first order predicate logic (with or without identity). For each positive integer n, let ℒn be the set of all formulas φ in ℒ logically equivalent to a formula of the form where Q is a (possibly empty) string of quantifiers, m is a positive integer, and each αij is either an atomic formula or the negation of an atomic formula.

Plural logic

2018 ◽  
Author(s):  
Alex Oliver ◽  
Timothy Smiley
Keyword(s):  
Special Class ◽  
Predicate Logic ◽  
Predicate Calculus ◽  
Fallow Period ◽  
The Everyday ◽  
Comprehensive Survey ◽  
The Subject ◽  
The Difference ◽  
Grammatical Number ◽  
Hippias Major

Plural phenomena are significant and inescapable. Granted, the plural idiom is sometimes reducible to the singular, e.g. ‘2 and 3 are prime is equivalent to ‘2 is prime and 3 is prime’. ‘Are prime’, however, belongs to the special class of predicates known as distributives. No such reductions are possible for the general case of collective (nondistributive) predicates, and they are to be found everywhere, from the everyday (‘Whitehead and Russell wrote Principia Mathematica’) to the heart of logic itself (‘The axioms are consistent’, ‘Those premises imply this conclusion’). It is no good dismissing grammatical number as a logically irrelevant complication like person or gender, since plural expressions are crucially involved in valid patterns of argument. To take an elementary example, ‘The Brontë sisters supported one another; the Brontë sisters were Anne, Charlotte and Emily; so Anne, Charlotte and Emily supported one another’. There can be no warrant for ignoring such patterns while attending to their singular counterparts. And some arguments do not even have a singular counterpart. For example, ‘Some numbers are prime. So some numbers are such that they are prime and a number is prime only if it is one of them.’ Logicians wedded to the singular logic of the predicate calculus typically try to dodge the issue of plurals by invoking sets, but we shall see that this is untenable. Socrates exploited the difference between distributive and collective predicates in Hippias Major, but little of interest happened subsequently until Russell put plurals at the centre of his project for providing a foundation for mathematics, through his idea of the ‘class as many’ in The Principles of Mathematics. After another fallow period, the subject revived in the 1970s and 80s with the work of Black, Morton, Sharvy, Simons and Boolos. It would be premature to attempt a comprehensive survey. This entry offers a nontechnical outline of plural predicate logic, including the major differences between it and singular logic and some matters still to be resolved.

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.

Sign in / Sign up

Export Citation Format

Share Document