Some results in modal model theory

1974 ◽  
Vol 39 (3) ◽  
pp. 496-508 ◽  
Author(s):  
Michael Mortimer
Keyword(s):  
Modal Logic ◽  
Model Theory ◽  
Classical Logic ◽  
Classical Model ◽  
Completeness Theorem ◽  
Strong Completeness ◽  
Barcan Formula ◽  
Weak Completeness ◽  
Modal Model ◽  
Omitting Types

This paper is concerned with extending some basic results from classical model theory to modal logic.In §1, we define the majority of terms used in the paper, and explain our notation. A full catalogue would be excessive, and we cite [3] and [7] as general references.Many papers on modal logic that have appeared are concerned with (i) introducing a new modal logic, and (ii) proving a weak completeness theorem for it. Theorem 1, in §2, in many cases allows us to conclude immediately that a strong completeness theorem holds for such a logic in languages of arbitrary cardinality. In particular, this is true of S4 with the Barcan formula.In §3 we strengthen Theorem 1 for a number of modal logics to deal with the satisfaction of several sets of sentences, and so obtain a realizing types theorem. Finally, an omitting types theorem, generalizing the result for classical logic (see [5]) is proved in §4.Several consequences of Theorem 1 are already to be found in the literature. [2] gives a proof of strong completeness in languages of arbitrary cardinality of various logics without the Barcan formula, and [8] for some logics in countable languages with it. In the latter case, the result for uncountable languages is cited, without proof, in [1], and there credited to Montague. Our proof was found independently.

Well-behaved modal logics

1984 ◽  
Vol 49 (4) ◽  
pp. 1393-1402
Author(s):  
Harold T. Hodes
Keyword(s):  
Modal Logic ◽  
Model Theory ◽  
Classical Model ◽  
Classical Case ◽  
Recursion Theory ◽  
Modal Logics ◽  
Modal Model ◽  
The Right ◽  
Domain Property ◽  
The Way

Much of the literature on the model theory of modal logics suffers from two weaknesses. Firstly, there is a lack of generality; theorems are proved piecemeal about this or that modal logic, or at best small classes of logics. Much of the literature, e.g. [1], [2], and [3], confines attention to structures with the expanding domain property (i.e., if wRu then Ā(w) ⊆ Ā(u)); the syntactic counterpart of this restriction is assumption of the converse Barcan scheme, a move which offers (in Russell's phrase) “all the advantages of theft over honest toil”. Secondly, I think there has been a failure to hit on the best ways of extending classical model theoretic notions to modal contexts. This weakness makes the literature boring, since a large part of the interest of modal model theory resides in the way in which classical model theoretic notions extend, and in some cases divide, in the modal setting. (The relation between α-recursion theory and classical recursion theory is analogous to that between modal model theory and classical model theory. Much of the work in α-recursion theory involved finding the right definitions (e.g., of recursive-in) and separating concepts which collapse in the classical case (e.g. of finiteness and boundedness).)The notion of a well-behaved modal logic is introduced in §3 to make possible rather general results; of course our attention will not be restricted to structures with the expanding domain property. Rather than prove piecemeal that familiar modal logics are well-behaved, in §4 we shall consider a class of “special” modal logics, which obviously includes many familiar logics and which is included in the class of well-behaved modal logics.

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.

An embedding of classical logic in S4

1970 ◽  
Vol 35 (4) ◽  
pp. 529-534 ◽  
Author(s):  
Melvin Fitting
Keyword(s):  
Intuitionistic Logic ◽  
Model Theory ◽  
Classical Logic ◽  
First Order ◽  
Barcan Formula ◽  
Complete Sequences

There are well-known embeddings of intuitionistic logic into S4 and of classical logic into S5. In this paper we give a related embedding of (first order) classical logic directly into (first order) S4, with or without the Barcan formula. If one reads the necessity operator of S4 as ‘provable’, the translation may be roughly stated as: truth may be replaced by provable consistency. A proper statement will be found below. The proof is based ultimately on the notion of complete sequences used in Cohen's technique of forcing [1], and is given in terms of Kripke's model theory [3], [4].

A proof-theoretic study of the correspondence of classical logic and modal logic

2003 ◽  
Vol 68 (4) ◽  
pp. 1403-1414 ◽  
Author(s):  
H. Kushida ◽  
M. Okada
Keyword(s):  
Modal Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Transformation Method ◽  
Modal Operator ◽  
Theoretic Method ◽  
Barcan Formula ◽  
Theoretic Proof ◽  
Classical Predicate

AbstractIt is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg [10] proved this fact in a syntactic way. Mints [7] extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints' result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 (with and without the Barcan formula) and the classical predicate logic (with one-sorted variable). We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.

scholarly journals Weak Completeness Theorem for Propositional Linear Time Temporal Logic

2012 ◽  
Vol 20 (3) ◽  
pp. 227-234
Author(s):  
Mariusz Giero
Keyword(s):  
Temporal Logic ◽  
Classical Logic ◽  
Linear Time ◽  
Completeness Theorem ◽  
Weak Completeness ◽  
Finite Set ◽  
Temporal Model ◽  
Linear Time Temporal Logic

Summary We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads to derivability of every valid formula. We build a tree of consistent and complete PNPs which is used to construct the model.

A unified completeness theorem for quantified modal logics

2002 ◽  
Vol 67 (4) ◽  
pp. 1483-1510 ◽  
Author(s):  
Giovanna Corsi
Keyword(s):  
Modal Logic ◽  
Completeness Theorem ◽  
Modal Logics ◽  
General Strategy ◽  
Quantified Modal Logic ◽  
Barcan Formula ◽  
Completeness Theorems

AbstractA general strategy for proving completeness theorems for quantified modal logics is provided. Starting from free quantified modal logic K. with or without identity, extensions obtained either by adding the principle of universal instantiation or the converse of the Barcan formula or the Barcan formula are considered and proved complete in a uniform way. Completeness theorems are also shown for systems with the extended Barcan rule as well as for some quantified extensions of the modal logic B. The incompleteness of Q°.B + BF is also proved.

κ-Suslin logic

1978 ◽  
Vol 43 (4) ◽  
pp. 659-666
Author(s):  
Judy Green
Keyword(s):  
Model Theory ◽  
Upper Bound ◽  
Completeness Theorem ◽  
Infinitary Logic ◽  
Complete Axiomatization ◽  
Standard Notation ◽  
Weak Completeness

An analogue of a theorem of Sierpinski about the classical operation () provides the motivation for studying κ-Suslin logic, an extension of Lκ+ω which is closed under a propositional connective based on (). This theorem is used to obtain a complete axiomatization for κ-Suslin logic and an upper bound on the κ-Suslin accessible ordinals (for κ = ω these results are due to Ellentuck [E]). It also yields a weak completeness theorem which we use to generalize a result of Barwise and Kunen [B-K] and show that the least ordinal not H(κ+) recursive is the least ordinal not κ-Suslin accessible.We assume familiarity with lectures 3, 4 and 10 of Keisler's Model theory for infinitary logic [Ke]. We use standard notation and terminology including the following.Lκ+ω is the logic closed under negation, finite quantification, and conjunction and disjunction over sets of formulas of cardinality at most κ. For κ singular, conjunctions and disjunctions over sets of cardinality κ can be replaced by conjunctions and disjunctions over sets of cardinality less than κ so that we can (and will in §2) assume the formation rules of Lκ+ω allow conjunctions and disjunctions only over sets of cardinality strictly less than κ whenever κ is singular.

scholarly journals A proof of completeness for continuous first-order logic

2010 ◽  
Vol 75 (1) ◽  
pp. 168-190 ◽  
Author(s):  
Itaï Ben Yaacov ◽  
Arthur Paul Pedersen
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Order Logic ◽  
First Order Logic ◽  
Complete Theory ◽  
Strong Completeness ◽  
First Order ◽  
Completeness Result ◽  
Metric Structures ◽  
Natural Classes

AbstractContinuous first-order logic has found interest among model theorists who wish to extend the classical analysis of “algebraic” structures (such as fields, group, and graphs) to various natural classes of complete metric structures (such as probability algebras, Hilbert spaces, and Banach spaces). With research in continuous first-order logic preoccupied with studying the model theory of this framework, we find a natural question calls for attention. Is there an interesting set of axioms yielding a completeness result?The primary purpose of this article is to show that a certain, interesting set of axioms does indeed yield a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies anapproximatedform of strong completeness, whereby Σ⊧φ(if and) only if Σ⊢φ∸2−nfor alln < ω. This approximated form of strong completeness asserts that if Σ⊧φ, then proofs from Σ, being finite, can provide arbitrarily better approximations of the truth ofφ.Additionally, we consider a different kind of question traditionally arising in model theory—that of decidability. When is the set of all consequences of a theory (in a countable, recursive language) recursive? Say that a complete theoryTisdecidableif for every sentenceφ, the valueφTis a recursive real, and moreover, uniformly computable fromφ. IfTis incomplete, we say it is decidable if for every sentenceφthe real numberφTois uniformly recursive fromφ, whereφTois the maximal value ofφconsistent withT. As in classical first-order logic, it follows from the completeness theorem of continuous first-order logic that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable.

Omitting types: application to recursion theory

1972 ◽  
Vol 37 (1) ◽  
pp. 81-89 ◽  
Author(s):  
Thomas J. Grilliot
Keyword(s):  
Set Theory ◽  
Model Theory ◽  
Significant Contribution ◽  
Hard Core ◽  
Completeness Theorem ◽  
Recursion Theory ◽  
Omitting Types ◽  
Admissible Ordinals ◽  
Models Of Set Theory

Omitting-types theorems have been useful in model theory to construct models with special characteristics. For instance, one method of proving the ω-completeness theorem of Henkin [10] and Orey [20] involves constructing a model that omits the type {x ≠ 0, x ≠ 1, x ≠ 2,···} (i.e., {x ≠ 0, x ≠ 1, x ≠ 2,···} is not satisfiable in the model). Our purpose in this paper is to illustrate uses of omitting-types theorems in recursion theory. The Gandy-Kreisel-Tait Theorem [7] is the most well-known example. This theorem characterizes the class of hyperarithmetical sets as the intersection of all ω-models of analysis (the so-called hard core of analysis). The usual way to prove that a nonhyperarithmetical set does not belong to the hard core is to construct an ω-model of analysis that omits the type representing the set (Application 1). We will find basis results for and s — sets that are stronger than results previously known (Applications 2 and 3). The question of how far the natural hierarchy of hyperjumps extends was first settled by a forcing argument (Sacks) and subsequently by a compactness argument (Kripke, Richter). Another problem solved by a forcing argument (Sacks) and then by a compactness argument (Friedman-Jensen) was the characterization of the countable admissible ordinals as the relativized ω1's. Using omitting-types technique, we will supply a third kind of proof of these results (Applications 4 and 5). S. Simpson made a significant contribution in simplifying the proof of the latter result, with the interesting side effect that Friedman's result on ordinals in models of set theory is immediate (Application 6). One approach to abstract recursiveness and hyperarithmeticity on a countable set is to tenuously identify the set with the natural numbers. This approach is equivalent to other approaches to abstract recursion (Application 7). This last result may also be proved by a forcing method.

Sign in / Sign up

Export Citation Format

Share Document