A proof theoretic proof of Scott's general interpolation theorem

1972 ◽  
Vol 37 (4) ◽  
pp. 683-695 ◽  
Author(s):  
Henry Africk
Keyword(s):  
Interpolation Theorem ◽  
Original Model ◽  
Order System ◽  
First Order ◽  
Free Variables ◽  
Theoretic Proof ◽  
The One ◽  
Craig’S Interpolation Theorem

In [5] Scott asked if there was a proof theoretic proof of his interpolation theorem. The purpose of this paper is to provide such a proof, working with the first order system LK of Gentzen [2]. Our method is an extension of the one in Maehara [3] for Craig's interpolation theorem. We will also sketch the original model theoretic proof and show how Scott used his result to obtain a definability theorem of Svenonius [7].A language for LK contains the usual logical symbols: , ∧, ∨, ⊃, ∀, ∃; countably many free variables a0, a1, … and bound variables x0, x1, …; and some or all of the following nonlogical symbols: n-ary predicates ; n-ary functions ; and individual constants c0, c1, …. Semiterms are defined as follows: (1) Free variables, bound variables and individual constants are semiterms. (2) If f is an n-ary function and s1 …, sn are semiterms, then f(s1 …, sn), is a semiterm. A term is a semiterm that does not contain a bound variable. Formulas are defined as follows: (1) If R is an n-ary predicate and t1 …, tn are terms, then R(t1 …, tn) is a formula. (2) If A and B are formulas, then A, A ∧ B, A ∨ B and A ⊃ B are formulas. (3) If A(t) is a formula which has zero or more occurrences of the term t, and if x is a bound variable not contained in A(t), then ∀xA(x) and ∃xA(x) are formulas where A(x) is obtained from A(t) by substituting x for t at all indicated places.

An Interpolation Theorem

2000 ◽  
Vol 6 (4) ◽  
pp. 447-462 ◽  
Author(s):  
Martin Otto
Keyword(s):  
Interpolation Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
Elementary Model ◽  
Relation Symbol ◽  
First Order ◽  
Theoretic Proof ◽  
Universal Quantification ◽  
The Given ◽  
Interpolation Result

AbstractLyndon's Interpolation Theorem asserts that for any valid implication between two purely relational sentences of first-order logic, there is an interpolant in which each relation symbol appears positively (negatively) only if it appears positively (negatively) in both the antecedent and the succedent of the given implication. We prove a similar, more general interpolation result with the additional requirement that, for some fixed tuple of unary predicates U, all formulae under consideration have all quantifiers explicitly relativised to one of the U. Under this stipulation, existential (universal) quantification over U contributes a positive (negative) occurrence of U.It is shown how this single new interpolation theorem, obtained by a canonical and rather elementary model theoretic proof, unifies a number of related results: the classical characterisation theorems concerning extensions (substructures) with those concerning monotonicity, as well as a many-sorted interpolation theorem focusing on positive vs. negative occurrences of predicates and on existentially vs. universally quantified sorts.

scholarly journals On weak and strong interpolation in algebraic logics

2006 ◽  
Vol 71 (1) ◽  
pp. 104-118 ◽  
Author(s):  
Gábor Sági ◽  
Saharon Shelah
Keyword(s):  
Algebraic Logic ◽  
Amalgamation Property ◽  
Weak Form ◽  
Interpolation Theorem ◽  
Order Logic ◽  
Cylindric Algebras ◽  
First Order ◽  
Finite Dimensional ◽  
Craig’S Interpolation Theorem ◽  
Superamalgamation Property

AbstractWe show that there is a restriction, or modification of the finite-variable fragments of First Order Logic in which a weak form of Craig's Interpolation Theorem holds but a strong form of this theorem does not hold. Translating these results into Algebraic Logic we obtain a finitely axiomatizable subvariety of finite dimensional Representable Cylindric Algebras that has the Strong Amalgamation Property but does not have the Superamalgamation Property. This settles a conjecture of Pigozzi [12].

Interpolation theorems for Lk,k2+

1978 ◽  
Vol 43 (3) ◽  
pp. 535-549 ◽  
Author(s):  
Ruggero Ferro
Keyword(s):  
Natural Deduction ◽  
Interpolation Theorem ◽  
Positive Answer ◽  
Strong Limit ◽  
First Order ◽  
Limit Cardinal ◽  
Saturated Models ◽  
Order Language ◽  
Craig’S Interpolation Theorem

Chang, in [1], proves an interpolation theorem (Theorem I, remark b)) for a first-order language. The proof of Chang's theorem uses essentially nonsimple devices, like special and ω1-saturated models.In remark e) in [1], Chang asks if there is a simpler proof of his Theorem I.In [1], Chang proves also another interpolation theorem (Theorem II), which is not an extension of his Theorem I, but extends Craig's interpolation theorem to Lα+,ω languages with interpolant in Lα+,α where α is a strong limit cardinal of cofinality ω.In remark k) in [1], Chang asks if there is a generalization of both Theorems I and II in [1], or at least a generalization of both Theorem I in [1] and Lopez-Escobar's interpolation theorem in [7].Maehara and Takeuti, in [8], show that there is a completely different proof of Chang's interpolation Theorem I as a consequence of their interpolation theorems. The proofs of these theorems of Maehara and Takeuti are proof theoretical in character, involving the notion of cut-free natural deduction, and it uses devices as simple as those needed for the usual Craig's interpolation theorem. Hence this can be considered as a positive answer to Chang's question in remark e) in [1].

Remarks on identity and description in first-order axiom systems

1954 ◽  
Vol 19 (1) ◽  
pp. 14-20 ◽  
Author(s):  
Theodore Hailperin
Keyword(s):  
Subject Matter ◽  
Axiom System ◽  
Order System ◽  
Quantification Theory ◽  
Specific Subject ◽  
First Order ◽  
Finite Set ◽  
The One ◽  
Image Position ◽  
Axiom Systems

Hilbert and Ackermann ([1], p. 107) define a first order axiom system as one in which the axioms contain one or more predicate constants, but no predicate variables. Here “axiom” refers to the specific subject-matter axioms and not to the rules of the restricted predicate calculus (quantification theory), which rules are presupposed for each first-order system. It is pointed out by them that an exception could be made for the predicate of identity; for the axiom scheme for this predicate, namelywhich has in (b) the variable predicate F, could nevertheless be replaced, in any given first-order system, by a finite set of axioms without predicate variables. Thus, for example, if Φ[x, y) is the one constant predicate of such a system then PId(b) could be replaced byThus one postulates, in addition to the reflexivity, symmetry, and transitivity of identity, the substitutivity of identical entities in each of the possible “atomic” contexts of a variable (occurrences in the primitive predicates). In this method of introducing identity it has to be taken as an additional primitive predicate and further axioms are consequently needed. In such a system having PId(a), (b1)−(b3) as axioms, the scheme PId(b) can be derived as a meta-theorem of the system, F(x) then being any formula of the system.

On the derivative chain-rules in fractional calculus via fractional difference and their application to systems modelling

Open Physics ◽  
2013 ◽  
Vol 11 (6) ◽  
Author(s):  
Guy Jumarie
Keyword(s):  
Fractional Calculus ◽  
Short Note ◽  
Order System ◽  
Fractional Difference ◽  
First Order ◽  
Fractional Models ◽  
Derivative Chain ◽  
Systems Modelling ◽  
Fractional Differential ◽  
The One

AbstractIt has been pointed out that the derivative chains rules in fractional differential calculus via fractional calculus are not quite satisfactory as far as they can yield different results which depend upon how the formula is applied, that is to say depending upon where is the considered function and where is the function of function. The purpose of the present short note is to display some comments (which might be clarifying to some readers) on the matter. This feature is basically related to the non-commutativity of fractional derivative on the one hand, and furthermore, it is very close to the physical significance of the systems under consideration on the other hand, in such a manner that everything is right so. As an example, it is shown that the trivial first order system may have several fractional modelling depending upon the way by which it is observed. This suggests some rules to construct the fractional models of standard dynamical systems, in as meaningful a model as possible. It might happen that this pitfall comes from the feature that a function which is continuous everywhere, but is nowhere differentiable, exhibits random-like features.

An Adjustment of Reference Tracking PID Controllers for a First-order System with a Dead Time

2016 ◽  
Vol 136 (5) ◽  
pp. 676-682 ◽  
Author(s):  
Akihiro Ishimura ◽  
Masayoshi Nakamoto ◽  
Takuya Kinoshita ◽  
Toru Yamamoto
Keyword(s):  
Dead Time ◽  
Order System ◽  
Pid Controllers ◽  
Reference Tracking ◽  
First Order

scholarly journals Higher Dimensional Holonomy Map for Rules Submanifolds in Graded Manifolds

2020 ◽  
Vol 8 (1) ◽  
pp. 68-91
Author(s):  
Gianmarco Giovannardi
Keyword(s):  
Characteristic Direction ◽  
Fixed Degree ◽  
One Dimensional ◽  
First Order ◽  
Natural Choice ◽  
Higher Dimensional ◽  
Graded Manifold ◽  
The One ◽  
Graded Manifolds ◽  
Holonomy Map

AbstractThe deformability condition for submanifolds of fixed degree immersed in a graded manifold can be expressed as a system of first order PDEs. In the particular but important case of ruled submanifolds, we introduce a natural choice of coordinates, which allows to deeply simplify the formal expression of the system, and to reduce it to a system of ODEs along a characteristic direction. We introduce a notion of higher dimensional holonomy map in analogy with the one-dimensional case [29], and we provide a characterization for singularities as well as a deformability criterion.

Relational Chase Procedures Interpreted as Resolution with Paramodulation1

1991 ◽  
Vol 15 (2) ◽  
pp. 123-138
Author(s):  
Joachim Biskup ◽  
Bernhard Convent
Keyword(s):  
Alternative Interpretation ◽  
Order Logic ◽  
First Order Logic ◽  
Inference Problem ◽  
First Order ◽  
Inference Problems ◽  
The One ◽  
The Relationship ◽  
Theoretical Foundations ◽  
Insight Into

In this paper the relationship between dependency theory and first-order logic is explored in order to show how relational chase procedures (i.e., algorithms to decide inference problems for dependencies) can be interpreted as clever implementations of well known refutation procedures of first-order logic with resolution and paramodulation. On the one hand this alternative interpretation provides a deeper insight into the theoretical foundations of chase procedures, whereas on the other hand it makes available an already well established theory with a great amount of known results and techniques to be used for further investigations of the inference problem for dependencies. Our presentation is a detailed and careful elaboration of an idea formerly outlined by Grant and Jacobs which up to now seems to be disregarded by the database community although it definitely deserves more attention.

Interpolation in Conditional Equational Logic1

1991 ◽  
Vol 15 (1) ◽  
pp. 80-85
Author(s):  
P.H. Rodenburg
Keyword(s):  
Interpolation Theorem ◽  
Equational Logic ◽  
Craig’S Interpolation Theorem ◽  
Natural Formulation

In a natural formulation, Craig’s interpolation theorem is shown to hold for conditional equational logic.

Sign in / Sign up

Export Citation Format

Share Document