A remark on Scott's interpolation theorem for Lω1ω

1977 ◽  
Vol 42 (1) ◽  
pp. 63-63 ◽  
Author(s):  
Nobuyoshi Motoháshi
Keyword(s):  
Atomic Formula ◽  
Interpolation Theorem ◽  
Infinitary Logic ◽  
Closed Formula ◽  
Free Variables ◽  
Universal Quantification ◽  
Infinite Sets ◽  
Existential Quantification

In [1], H. Africk proved that Scott's interpolation theorem does not hold in the infinitary logic Lω1ω. In this paper we shall show that there is an interpolation theorem in Lω1ω which can be considered as an extension of Scott's interpolation theorem in Lω1ω by using a technique developed in Motohashi [2] and [3]. We use the terminology in [1]. Therefore {Ri; i ∈ J} is the set of predicate symbols in our language. Now let us divide the set of all the free variables into mutually disjoint infinite sets {VI; I ⊆ J}. Suppose that ℱ ⊆ (J). Then a formula in Lω1ω is said to be an ℱ′-formula if it is obtained from atomic formula of the form Ri(X1, …, Xn) for some I ∈ i ∈ I and X1, …, Xn in V1,, by applying ¬ (negation), ∧ (countable conjunction), ∨ (countable disjunction), → (implication), ∀ (universal quantification), and ∃ (existential quantification). Notice that every ℱ-sentence in [1] is an ℱ′. sentence (ℱ′-closed formula) in our sense.Then we have the following theorem which is an immediate consequence of the interpolation theorem in [2].Theorem. Let A and ? be sentences. There is an ℱ′-sentence C such that A→C and C→B are provable iff whenever and are ℱ-isomorphic structures and satisfies A, then satisfies B.

scholarly journals On Quantifying Literals in Boolean Logic and its Applications to Explainable AI

2021 ◽  
Vol 72 ◽  
pp. 285-328
Author(s):  
Adnan Darwiche ◽  
Pierre Marquis
Keyword(s):  
Boolean Logic ◽  
Fine Grained ◽  
Explainable Ai ◽  
Boolean Formulas ◽  
Universal Quantification ◽  
Existential Quantification

Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. In this paper, we complement this by introducing and studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification, discuss the interplay between variable/literal and existential/universal quantification, and identify some classes of Boolean formulas and circuits on which quantification can be done efficiently. Literal quantification is more fine-grained than variable quantification as the latter can be defined in terms of the former, leading to a refinement of quantified Boolean logic with literal quantification as its primitive.

scholarly journals Decidability of Definability

2013 ◽  
Vol 78 (4) ◽  
pp. 1036-1054 ◽  
Author(s):  
Manuel Bodirsky ◽  
Michael Pinsker ◽  
Todor Tsankov
Keyword(s):  
Random Graph ◽  
Topological Dynamics ◽  
Homogeneous Structure ◽  
First Order ◽  
Computational Problem ◽  
Random Tournament ◽  
Universal Quantification ◽  
Countably Infinite ◽  
Existential Quantification

AbstractFor a fixed countably infinite structure Γ with finite relational signature τ, we study the following computational problem: input are quantifier-free τ-formulas ϕ0, ϕ1, …, ϕn that define relations R0, R1, …, Rn over Γ. The question is whether the relation R0 is primitive positive definable from R1, …, Rn, i.e., definable by a first-order formula that uses only relation symbols for R1, …, Rn, equality, conjunctions, and existential quantification (disjunction, negation, and universal quantification are forbidden).We show decidability of this problem for all structures Γ that have a first-order definition in an ordered homogeneous structure Δ with a finite relational signature whose age is a Ramsey class and determined by finitely many forbidden substructures. Examples of structures Γ with this property are the order of the rationals, the random graph, the homogeneous universal poset, the random tournament, all homogeneous universal C-relations, and many more. We also obtain decidability of the problem when we replace primitive positive definability by existential positive, or existential definability. Our proof makes use of universal algebraic and model theoretic concepts, Ramsey theory, and a recent characterization of Ramsey classes in topological dynamics.

On second order intuitionistic propositional logic without a universal quantifier

2009 ◽  
Vol 74 (1) ◽  
pp. 157-167 ◽  
Author(s):  
Konrad Zdanowski
Keyword(s):  
Propositional Logic ◽  
Second Order ◽  
Universal Quantifier ◽  
Intuitionistic Propositional Logic ◽  
Glivenko’S Theorem ◽  
Free Variables ◽  
Universal Quantification

AbstractWe examine second order intuitionistic propositional logic, IPC2. Let ℱ∃ a be the set of formulas with no universal quantification. We prove Glivenko's theorem for formulas in ℱ∃ that is, for φ ∈ ℱ∃, φ is a classical tautology if and only if ┐┐φ is a tautology of IPC2. We show that for each sentence φ ∈ ℱ∃ (without free variables), φ is a classical tautology if and only if φ is an intuitionistic tautology. As a corollary we obtain a semantic argument that the quantifier ∀ is not definable in IPC2 from ⊥, ⋁, ⋀, →, ∃.

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 A refinement calculus for logic programs

2002 ◽  
Vol 2 (4-5) ◽  
pp. 425-460 ◽  
Author(s):  
IAN HAYES ◽  
ROBERT COLVIN ◽  
DAVID HEMER ◽  
PAUL STROOPER ◽  
RAY NICKSON
Keyword(s):  
Wide Spectrum ◽  
Tool Support ◽  
Logic Programs ◽  
Refinement Calculus ◽  
Partial Functions ◽  
Prototype Tool ◽  
Stepwise Development ◽  
Declarative Semantics ◽  
Universal Quantification ◽  
Existential Quantification

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

The completeness theorem for infinitary logic

1972 ◽  
Vol 37 (1) ◽  
pp. 31-34 ◽  
Author(s):  
Richard Mansfield
Keyword(s):  
Boolean Algebra ◽  
Completeness Theorem ◽  
Complete Boolean Algebra ◽  
Infinitary Logic ◽  
Constant Symbol ◽  
Truth Values ◽  
Truth Function ◽  
Universal Quantification ◽  
Image Position ◽  
Extended Notion

It will be proven that a set of sentences of infinitary logic is satisfiable iff it is proof theoretically consistent. Since this theorem is known to be false, it must be quickly added that an extended notion of model is being used; truth values may be taken from an arbitrary complete Boolean algebra. We shall give a Henkin style proof of this result which generalizes easily to Boolean valued sets of sentences.For each infinite candinal number κ the language Lκ is built up from a set of relation symbols together with a constant symbol cα and a variable υα for each α in κ. It contains atomic formulas and is closed under the following rules:(1) If Γ is a set of formulas of power < κ ∧ Γ is a set of formulas.(2) If φ is a formula, ¬ φ is also.(3) If φ is a formula and A Is a subset of κ of power < κ then Aφ is a formula.∧Γ is meant to be the conjunction of all the formulas in Γ, while Aφ is the universal quantification of all the variables υα for α in A. We let C denote the set of constant symbols in Lκ, the parameter κ must be discovered from the context.A model is identified with its truth function. Thus a model is a function mapping the sentences of Lκ into a complete Boolean algebra which satisfies the following conditions:

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.

Computable numberings of families of infinite sets

2019 ◽  
Vol 58 (3) ◽  
pp. 334-343
Author(s):  
M. V. Dorzhieva
Keyword(s):  
Computable Numberings ◽  
Infinite Sets

Indiscernibility

2018 ◽  
Author(s):  
Tim Button ◽  
Sean Walsh
Keyword(s):  
Model Theory ◽  
Infinitary Logic ◽  
Identity Of Indiscernibles ◽  
Sheer Number

This chapter explores Leibniz's principle of the Identity of Indiscernibles. Model theory supplies us with the resources to distinguish between many different notions of indiscernibility; we can vary: (a) the primitive ideology (b) the background logic and (c) the grade of discernibility. We use these distinctions to discuss the possibility of singling-out “indiscernibles”. And we then use these to distinctions to explicate Leibniz's famous principle. While model theory allows us to make this principle precise, the sheer number of different precise versions of this principle made available by model theory can serve to mitigate some of the initial excitement of this principle. We round out the chapter with two technical topics: indiscernibility in infinitary logic, and the relation between indiscernibility, orders, and stability.

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