A reduction theorem for predicate logic

1972 ◽  
Vol 37 (2) ◽  
pp. 352-354 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Predicate Logic ◽  
Complete List ◽  
Reduction Theorem ◽  
Logical Connectives ◽  
Image Position

It is well known that in prepositional logic not every propositional connective is definable in terms of equivalence nor indeed in terms of equivalence together with negation. It is the purpose of this note to show that in a certain sense this is, however, possible within predicate logic.Let F1 be the class of predicate logical formulae containing only the logical connectives ¬ (not), ∨ (or), E (exists), and F2 the class of predicate logical formulae containing only the logical connectives ≡ (if and only if) and E.Our object will be to find a method for reducing any formulae ϕ of F1 to a formula ψ of F2 such that ϕ is valid if and only if ψ is valid.Note first that for every domain D containing at least two individuals we can for every n-place relation R defined over D find an n + 1-place relation S defined over D such that for all x1, …, xn ∈ D,holds. For instance, let S(y, x1, …, xn) be the relation y = x1 & R(x1, …, xn).Now let ϕ be an arbitrary formula of F1 and A1, …, A3 a complete list of predicate letters occurring in ϕ of degree g1, …, gi, respectively. Let ϕ′ be the formula obtained from ϕ by replacing every prime formula Ai(x1, …, xgi) byThen it follows immediately from the previous observation that (a) ϕ is satisfiable in D if and only if ϕ′ is satisfiable in D.

On the logic of incomplete answers

1965 ◽  
Vol 30 (1) ◽  
pp. 65-68 ◽  
Author(s):  
M. J. Cresswell
Keyword(s):  
Formal Analysis ◽  
Complete List ◽  
Strict Implication ◽  
Complete Answer ◽  
Questions And Answers ◽  
Image Position

I have argued in [1] that a concept bearing some resemblance to ‘p is the answer to d’ (p a proposition and d a question) can be defined wherever d has the form,‘For which a's is it the case that A (a)?’ (Qa)A(a)where a is a variable and A a wff containing a. To say that p is the true and complete answer to (Qa)A(a) is expressed as saying that p is logically equivalent to the true conjunction of A(a) or ~A(a) for each a. It is defined as;Such a concept of answer is like Belnap's [2] direct true answer to a complete list question, or like Harrah's use [3] (p. 43) of the notion of a state description. The main difference between my approach and that of Belnap and Harrah is that while they are concerned to develop a formal metalanguage for discussion of questions and answers I am concerned to express, as far as possible in existing systems, certain interrogative statements; in particular statements of the form ‘— is the (an) answer to —’.While the account in [1] does give a formal analysis of one ‘answer’ concept there are respects in which it is inadequate.1. Since it uses entailment (or strict implication) to define the relation between p the answer and d the question we can shew that if p is the answer to d and q is logically equivalent to p then q is the answer to d.

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.

Simple reduction theorems for extension and torsion functors

1961 ◽  
Vol 57 (3) ◽  
pp. 483-488
Author(s):  
D. G. Northcott
Keyword(s):  
Commutative Ring ◽  
Zero Divisor ◽  
Residue Class ◽  
Identity Element ◽  
Negative Integer ◽  
Reduction Theorem ◽  
Residue Class Ring ◽  
Image Position ◽  
Class Ring ◽  
Simple Reduction

Let Λ be a commutative ring with an identity element and c an element of Λ which is not a zero divisor Denote by Ω the residue class ring Λ/Λc. If now M is a Λ-module for which c is not a zero divisor, and A is an Ω-module, then a theorem of Rees (2) asserts that, for every non-negative integer n, we have a Λ-isomorphismThis reduction theorem has found a number of useful and interesting applications.

scholarly journals Note on a theorem of Magnus

1969 ◽  
Vol 10 (3-4) ◽  
pp. 469-474 ◽  
Author(s):  
Norman Blackburn
Keyword(s):  
Normal Subgroup ◽  
Free Group ◽  
Reduction Theorem ◽  
The South ◽  
Cup Product ◽  
South West ◽  
Image Position ◽  
Independent Parameters

Magnus [4] proved the following theorem. Suppose that F is free group and that X is a basis of F. Let R be a normal subgroup of F and write G = F/R. Then there is a monomorphism of F/R′ in which ; here the tx are independent parameters permutable with all elements of G. Later investigations [1, 3] have shown what elements can appear in the south-west corner of these 2 × 2 matrices. In this form the theorem subsequently reappeared in proofs of the cup-product reduction theorem of Eilenberg and MacLane (cf. [7, 8]). In this note a direct group-theoretical proof of the theorems will be given.

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

The mean value theorem in second order arithmetic

2001 ◽  
Vol 66 (3) ◽  
pp. 1353-1358 ◽  
Author(s):  
Christopher S. Hardin ◽  
Daniel J. Velleman
Keyword(s):  
Mean Value ◽  
Second Order ◽  
Mean Value Theorem ◽  
Natural Numbers ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Logical Connectives ◽  
The Mean ◽  
Order Arithmetic ◽  
Image Position

This paper is a contribution to the project of determining which set existence axioms are needed to prove various theorems of analysis. For more on this project and its history we refer the reader to [1] and [2].We work in a weak subsystem of second order arithmetic. The language of second order arithmetic includes the symbols 0, 1, =, <, +, ·, and ∈, together with number variables x, y, z, … (which are intended to stand for natural numbers), set variables X, Y, Z, … (which are intended to stand for sets of natural numbers), and the usual quantifiers (which can be applied to both kinds of variables) and logical connectives. We write ∀x < t φ and ∃x < t φ as abbreviations for ∀x(x < t → φ) and ∃x{x < t ∧ φ) respectively; these are called bounded quantifiers. A formula is said to be if it has no quantifiers applied to set variables, and all quantifiers applied to number variables are bounded. It is if it has the form ∃xθ and it is if it has the form ∀xθ, where in both cases θ is .The theory RCA0 has as axioms the usual Peano axioms, with the induction scheme restricted to formulas, and in addition the comprehension scheme, which consists of all formulas of the formwhere φ is , ψ is , and X does not occur free in φ(n). (“RCA” stands for “Recursive Comprehension Axiom.” The reason for the name is that the comprehension scheme is only strong enough to prove the existence of recursive sets.) It is known that this theory is strong enough to allow the development of many of the basic properties of the real numbers, but that certain theorems of elementary analysis are not provable in this theory. Most relevant for our purposes is the fact that it is impossible to prove in RCA0 that every continuous function on the closed interval [0, 1] attains maximum and minimum values (see [1]).Since the most common proof of the Mean Value Theorem makes use of this theorem, it might be thought that the Mean Value Theorem would also not be provable in RCA0. However, we show in this paper that the Mean Value Theorem can be proven in RCA0. All theorems stated in this paper are theorems of RCA0, and all of our reasoning will take place in RCA0.

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.

The diversity of quantifier prefixes

1973 ◽  
Vol 38 (1) ◽  
pp. 79-85 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wilbur Walkoe
Keyword(s):  
Positive Integer ◽  
Analogous Result ◽  
Predicate Logic ◽  
Finite Sequence ◽  
Arithmetical Hierarchy ◽  
First Order ◽  
Free Variables ◽  
The Standard Model ◽  
Image Position ◽  
Identity Symbol

The Arithmetical Hierarchy Theorem of Kleene [1] states that in the complete theory of the standard model of arithmetic there is for each positive integer r a Σr0 formula which is not equivalent to any Πr0 formula, and a Πr0 formula which is not equivalent to any Πr0 formula. A Πr0 formula is a formula of the formwhere φ has only bounded quantifiers; Πr0 formulas are defined dually.The Linear Prefix Theorem in [3] is an analogous result for predicate logic. Consider the first order predicate logic L with identity symbol, countably many n-placed relation symbols for each n, and no constant or function symbols. A prefix is a finite sequenceof quantifier symbols ∃ and ∀, for example ∀∃∀∀∀∃. By a Q formula we mean a formula of L of the formwhere v1, …, vr are distinct variables and φ has no quantifiers. A sentence is a formula with no free variables. The Linear Prefix Theorem is as follows.Linear Prefix Theorem. Let Q and q be two different prefixes of the same length r. Then there is a Q sentence which is not logically equivalent to any q sentence.Moreover, for each s there is a Q formula with s free variables which is not logically equivalent to any q formula with s free variables.For example, there is an ∀∃∀∀∀∃ sentence which is not logically equivalent to any ∀∃∃∀∀∃ sentence, and vice versa. Recall that in arithmetic two consecutive ∃'s or ∀'s can be collapsed; for instance all ∀∃∀∀∀∃ and ∀∃∃∀∀∃ formulas are logically equivalent to Π40 formulas. But the Linear Prefix Theorem shows that in predicate logic the number of quantifiers in each block, as well as the number of blocks, counts.

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 ;

CONSTRUCTIVE REFLECTIVITY PRINCIPLES FOR REGULAR THEORIES

2019 ◽  
Vol 84 (4) ◽  
pp. 1348-1367
Author(s):  
HENRIK FORSSELL ◽  
PETER LEFANU LUMSDAINE
Keyword(s):  
Set Theory ◽  
Predicate Logic ◽  
Small Object ◽  
Basic Construction ◽  
Weak Reflection ◽  
Small Object Argument ◽  
Regular Theory ◽  
Image Position

AbstractClassically, any structure for a signature ${\rm{\Sigma }}$ may be completed to a model of a desired regular theory ${T}}$ by means of the chase construction or small object argument. Moreover, this exhibits ${\rm{Mod}}\left(T)$ as weakly reflective in ${\rm{Str}}\left( {\rm{\Sigma }} \right)$.We investigate this in the constructive setting. The basic construction is unproblematic; however, it is no longer a weak reflection. Indeed, we show that various reflectivity principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e., set) models.Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

Sign in / Sign up

Export Citation Format

Share Document