On the interpolation theorem for the logic of constant domains

1981 ◽  
Vol 46 (1) ◽  
pp. 87-88 ◽  
Author(s):  
E. G. K. López-Escobar
Keyword(s):  
Simple Proof ◽  
Open Problem ◽  
Formal System ◽  
Kripke Model ◽  
Interpolation Theorem ◽  
Predicate Calculus ◽  
Weak Consistency ◽  
Simple Matter ◽  
Constant Domains

In Gabbay [1] it is stated as an open problem whether or not Craig's Theorem holds for the logic of constant domains CD, i.e. for the extension of the intuitionistic predicate calculus, IPC, obtained by adding the schema; . Then in the later article, [2], Gabbay gives a proof of it. The proof given in [2] is via Robinson's (weak) consistency theorem and depends on relatively complicated (Kripke-) model-theoretical constructions developed in [1] (see p. 392 of [1] for a brief sketch of the method). The aim of this note is to show that the interpolation theorem for CD can also be obtained, by simple proof-theoretic methods, from §80 of Kleene's Introduction to Metamathematics [3].GI is the classical formal system whose postulates are given on p. 442 of [3]. Let GD be the system obtained from GI by the following modifications: (1) the sequents of GD are to have at most two formulas in their succedents and (2) the intuitionistic restriction that Θ be empty is required for the succedent rules (→ ¬) and (→ ⊃). It is a simple matter to show that: , x not free in . It then follows that, using Theorem 46 of [3], if then .

Applications of trees to intermediate logics

1972 ◽  
Vol 37 (1) ◽  
pp. 135-138 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Kripke Model ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Geometric Properties ◽  
Intermediate Logics ◽  
Truth Value ◽  
Constant Domains ◽  
Completeness Theorems

We investigate extensions of Heyting's predicate calculus (HPC). We relate geometric properties of the trees of Kripke models (see [2]) with schemas of HPC and thus obtain completeness theorems for several intermediate logics defined by schemas. Our main results are:(a) ∼(∀x ∼ ∼ϕ(x) Λ ∼∀xϕ(x)) is characterized by all Kripke models with trees T with the property that every point is below an endpoint. (From this we shall deduce Glivenko type theorems for this extension.)(b) The fragment of HPC without ∨ and ∃ is complete for all Kripke models with constant domains.We assume familiarity with Kripke [2]. Our notation is different from his since we want to stress properties of the trees. A Kripke model will be denoted by (Aα, ≤ 0), α ∈ T where (T, ≤, 0) is the tree with the least member 0 ∈ T and Aα, α ∈ T, is the model standing at the node α. The truth value at α of a formula ϕ(a1 … an) under the indicated assignment at α is denoted by [ϕ(a1 … an)]α.A Kripke model is said to be of constant domains if all the models Aα, α ∈ T, have the same domain.

scholarly journals A Consecutive Lehmer Code for Parabolic Quotients of the Symmetric Group

2021 ◽  
Vol 28 (3) ◽  
Author(s):  
Wenjie Fang ◽  
Henri Mühle ◽  
Jean-Christophe Novelli
Keyword(s):  
Symmetric Group ◽  
Simple Proof ◽  
Open Problem ◽  
Lattice Isomorphism ◽  
Tamari Lattice ◽  
Lehmer Code

In this article we define an encoding for parabolic permutations that distinguishes between parabolic $231$-avoiding permutations. We prove that the componentwise order on these codes realizes the parabolic Tamari lattice, and conclude a direct and simple proof that the parabolic Tamari lattice is isomorphic to a certain $\nu$-Tamari lattice, with an explicit bijection. Furthermore, we prove that this bijection is closely related to the map $\Theta$ used when the lattice isomorphism was first proved in (Ceballos, Fang and Mühle, 2020), settling an open problem therein.

A Short Proof of an Interpolation Theorem

1974 ◽  
Vol 17 (1) ◽  
pp. 127-128 ◽  
Author(s):  
Edward Hughes
Keyword(s):  
Half Plane ◽  
Complex Plane ◽  
Simple Proof ◽  
Real Line ◽  
Short Proof ◽  
Interpolation Theorem ◽  
Operator Interpolation ◽  
Upper Half Plane ◽  
Positive Functions ◽  
Class Of Functions

In this note we give a simple proof of an operator-interpolation theorem (Theorem 2) due originally to Donoghue [6], and Lions-Foias [7].Let be the complex plane, the open upper half-plane, the real line, ℛ+ and ℛ- the non-negative and non-positive axes. Denote by the class of positive functions on which extend analytically to —ℛ-, and map into itself. Denote by ’ the class of functions φ such that φ(x1/2)2 is in .

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.

Sufficient conditions for the undecidability of intuitionistic theories with applications

1972 ◽  
Vol 37 (2) ◽  
pp. 375-384 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Decision Problem ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
The Other ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Symmetric Relation ◽  
Undecidable Theory ◽  
Classical Models ◽  
Classical Predicate

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC.Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not.Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

Solution of a problem of Leon Henkin

1955 ◽  
Vol 20 (2) ◽  
pp. 115-118 ◽  
Author(s):  
M. H. Löb
Keyword(s):  
Number Theory ◽  
Recursive Function ◽  
Formal System ◽  
Free Variable ◽  
Formal Proof ◽  
Predicate Calculus ◽  
First Order ◽  
Free Variables ◽  
Order Predicate Calculus

If Σ is any standard formal system adequate for recursive number theory, a formula (having a certain integer q as its Gödel number) can be constructed which expresses the proposition that the formula with Gödel number q is provable in Σ. Is this formula provable or independent in Σ? [2].One approach to this problem is discussed by Kreisel in [4]. However, he still leaves open the question whether the formula (Ex)(x, a), with Gödel-number a, is provable or not. Here (x, y) is the number-theoretic predicate which expresses the proposition that x is the number of a formal proof of the formula with Gödel-number y.In this note we present a solution of the previous problem with respect to the system Zμ [3] pp. 289–294, and, more generally, with respect to any system whose set of theorems is closed under the rules of inference of the first order predicate calculus, and satisfies the subsequent five conditions, and in which the function (k, l) used below is definable.The notation and terminology is in the main that of [3] pp. 306–326, viz. if is a formula of Zμ containing no free variables, whose Gödel number is a, then ({}) stands for (Ex)(x, a) (read: the formula with Gödel number a is provable in Zμ); if is a formula of Zμ containing a free variable, y say, ({}) stands for (Ex)(x, g(y)}, where g(y) is a recursive function such that for an arbitrary numeral the value of g() is the Gödel number of the formula obtained from by substituting for y in throughout. We shall, however, depart trivially from [3] in writing (), where is an arbitrary numeral, for (Ex){x, ).

Syntactical and semantical properties of simple type theory

1960 ◽  
Vol 25 (4) ◽  
pp. 305-326 ◽  
Author(s):  
Kurt Schütte
Keyword(s):  
Type Theory ◽  
Formal System ◽  
Predicate Calculus ◽  
Simple Type ◽  
Inference Rules ◽  
Positive Part ◽  
Negative Part ◽  
Simple Type Theory ◽  
Theoretical Investigations ◽  
Order Predicate Calculus

In my paper [10] I introduced the syntactical concepts “positive part” and “negative part” of logical formulas in first-order predicate calculus. These concepts make it possible to establish logical systems on inference rules similar to Gentzen's inference rules but without using the concept “sequent” and without needing Gentzen's structural inference rules. Proof-theoretical investigations of several formal systems based on positive and negative parts are published in [11]. In this paper I consider a similar formal system of simple type theory.A syntactical concept of “strict derivability” results from the formal system in [10] by generalization of the axioms and inference rules from first to higher-order predicate calculus and by addition of inference rules for set abstraction by means of a λ-symbol which allows us to form set expressions of arbitrary types from well-formed formulas.

Equivalence between semantics for intuitionism. I

1981 ◽  
Vol 46 (4) ◽  
pp. 773-780 ◽  
Author(s):  
E. G. K. López-Escobar
Keyword(s):  
Formal Logic ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Axiom Schema ◽  
Formal Systems ◽  
Consistency Results ◽  
Partial List ◽  
Image Position ◽  
Constant Domains

It is probably because intuitionism is founded on the concept of (abstract) proof that it has been possible to develop various kinds of models. The following is but a partial list: Gabbay [5], Beth [2], Kripke [8], Kleene [7], Läuchli [9], McKinsey and Tarski [10], Rasiowa and Sikorski [14], Scott [15], de Swart [16], and Veldman [17].The original purpose for having the models appears to have been for obtaining independence or consistency results for certain formalizations of intuitionism [see Beth [2], Prawitz [13]]; of course, if the models could be also justified as being plausible interpretations of intuitionistic thinking, so much the better. In fact, having some kind of plausible interpretation makes it much easier to work with the models. Occasionally the models were used to suggest possible extensions of the formal systems; for example, the Kripke models with constant domains have motivated interest in the formal logic CD which extends the Intuitionistic Predicate Calculus (IPC) by having the axiom schema

Sign in / Sign up

Export Citation Format

Share Document