Systematization of finite many-valued logics through the method of tableaux

1987 ◽  
Vol 52 (2) ◽  
pp. 473-493 ◽  
Author(s):  
Walter A. Carnielli
Keyword(s):  
Model Theory ◽  
Proof Theory ◽  
Completeness Theorem ◽  
First Order ◽  
Formal Systems ◽  
Skolem Theorem ◽  
Consistency Properties ◽  
Model Existence ◽  
Model Existence Theorem ◽  
Theory And Model

AbstractThis paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way.We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Löwenheim-Skolem theorem.The paper is completely self-contained and includes examples of application to particular many-valued formal systems.

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.

Ranked partial structures

2003 ◽  
Vol 68 (4) ◽  
pp. 1109-1144
Author(s):  
Timothy J. Carlson
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Order Logic ◽  
Basic Theory ◽  
First Order Logic ◽  
Theoretic Method ◽  
First Order ◽  
Partial Structures ◽  
Skolem Theorem

AbstractThe theory of ranked partial structures allows a reinterpretation of several of the standard results of model theory and first-order logic and is intended to provide a proof-theoretic method which allows for the intuitions of model theory. A version of the downward Löwenheim-Skolem theorem is central to our development. In this paper we will present the basic theory of ranked partial structures and their logic including an appropriate version of the completeness theorem.

Fragments of first order logic, I: universal Horn logic

1977 ◽  
Vol 42 (2) ◽  
pp. 221-237 ◽  
Author(s):  
George F. McNulty
Keyword(s):  
Existence Theorem ◽  
Predicate Logic ◽  
Logical Consequence ◽  
Horn Logic ◽  
First Order ◽  
Consistency Properties ◽  
Model Existence ◽  
Model Existence Theorem ◽  
Sharp Version ◽  
Horn Sentences

Let L be any finitary language. By restricting our attention to the universal Horn sentences of L and appealing to a semantical notion of logical consequence, we can formulate the universal Horn logic of L. The present paper provides some theorems about universal Horn logic that serve to distinguish it from the full first order predicate logic. Universal Horn equivalence between structures is characterized in two ways, one resembling Kochen's ultralimit theorem. A sharp version of Beth's definability theorem is established for universal Horn logic by means of a reduced product construction. The notion of a consistency property is relativized to universal Horn logic and the corresponding model existence theorem is proven. Using the model existence theorem another proof of the definability result is presented. The relativized consistency properties also suggest a syntactical notion of proof that lies entirely within the universal Horn logic. Finally, a decision problem in universal Horn logic is discussed. It is shown that the set of universal Horn sentences preserved under the formation of homomorphic images (or direct factors) is not recursive, provided the language has at least two unary function symbols or at least one function symbol of rank more than one.This paper begins with a discussion of how algebraic relations between structures can be used to obtain fragments of a given logic. Only two such fragments seem to be under current investigation: equational logic and universal Horn logic. Other fragments which seem interesting are pointed out.

Some model theory for game logics

1979 ◽  
Vol 44 (2) ◽  
pp. 147-152
Author(s):  
Judy Green
Keyword(s):  
Model Theory ◽  
Existence Theorems ◽  
Semantic Interpretation ◽  
Rule Based ◽  
Game Logic ◽  
Important Method ◽  
Consistency Property ◽  
Consistency Properties ◽  
Model Existence

Consistency properties and their model existence theorems have provided an important method of constructing models for fragments of L∞ω. In [E] Ellentuck extended this construction to Suslin logic. One of his extensions, the Borel consistency property, has its extra rule based not on the semantic interpretation of the extra symbols but rather on a theorem of Sierpinski about the classical operation . In this paper we extend that consistency property to the game logic LG and use it to show how one can extend results about and its countable fragments to LG and certain of its countable fragments. The particular formation of LG which we use will allow in the game quantifier infinite alternation of countable conjunctions and disjunctions as well as infinite alternation of quantifiers. In this way LG can be viewed as an extension of Suslin logic.

Barwise: Abstract Model Theory and Generalized Quantifiers

2004 ◽  
Vol 10 (1) ◽  
pp. 37-53 ◽  
Author(s):  
Jouko Väänänen
Keyword(s):  
Model Theory ◽  
Interpolation Property ◽  
Order Logic ◽  
First Order Logic ◽  
Generalized Quantifiers ◽  
Abstract Model ◽  
Famous Theorem ◽  
Abstract Model Theory ◽  
First Order ◽  
Skolem Theorem

§1. Introduction. After the pioneering work of Mostowski [29] and Lindström [23] it was Jon Barwise's papers [2] and [3] that brought abstract model theory and generalized quantifiers to the attention of logicians in the early seventies. These papers were greeted with enthusiasm at the prospect that model theory could be developed by introducing a multitude of extensions of first order logic, and by proving abstract results about relationships holding between properties of these logics. Examples of such properties areκ-compactness. Any set of sentences of cardinality ≤ κ, every finite subset of which has a model, has itself a model. Löwenheim-Skolem Theorem down to κ. If a sentence of the logic has a model, it has a model of cardinality at most κ. Interpolation Property. If ϕ and ψ are sentences such that ⊨ ϕ → Ψ, then there is θ such that ⊨ ϕ → θ, ⊨ θ → Ψ and the vocabulary of θ is the intersection of the vocabularies of ϕ and Ψ.Lindstrom's famous theorem characterized first order logic as the maximal ℵ0-compact logic with Downward Löwenheim-Skolem Theorem down to ℵ0. With his new concept of absolute logics Barwise was able to get similar characterizations of infinitary languages Lκω. But hopes were quickly frustrated by difficulties arising left and right, and other areas of model theory came into focus, mainly stability theory. No new characterizations of logics comparable to the early characterization of first order logic given by Lindström and of infinitary logic by Barwise emerged. What was first called soft model theory turned out to be as hard as hard model theory.

On theories and models in fuzzy predicate logics

2006 ◽  
Vol 71 (3) ◽  
pp. 863-880 ◽  
Author(s):  
Petr Hájek ◽  
Petr Cintula
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Fuzzy Logics ◽  
Formal Systems ◽  
Conservative Extensions

AbstractIn the last few decades many formal systems of fuzzy logics have been developed. Since the main differences between fuzzy and classical logics lie at the propositional level, the fuzzy predicate logics have developed more slowly (compared to the propositional ones). In this text we aim to promote interest in fuzzy predicate logics by contributing to the model theory of fuzzy predicate logics. First, we generalize the completeness theorem, then we use it to get results on conservative extensions of theories and on witnessed models.

Introduction and Overview

2017 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Scientific Method ◽  
Proof Theory ◽  
Valid Argument ◽  
First Order ◽  
Proof Systems ◽  
Formal Systems ◽  
Deductive Logic ◽  
Order Language ◽  
Foundational Work ◽  
The Right

This is a foundational work, written not just for philosophers of logic, but for logicians and foundationalists generally. Like Frege we seek to deal with the formal first-order language of mathematics. We revisit Gentzen’s proof theory in order to build relevance into proofs, while leaving intact all the logical power one is entitled to expect of a deductive logic for mathematics and for scientific method generally. Proof systems are constituted by particular choices of rules of inference. We raise the issue of the reflexive stability of any argument for a particular choice of logic as the ‘right’ logic. We examine the question of pluralism v. absolutism in choice of logic, and suggest that the informal notion of valid argument is stable and robust enough for us to be able to ‘get it right’ with our formal systems of proof for both constructive and non-constructive reasoning.

A First Course in Logic

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Propositional Logic ◽  
Proof Theory ◽  
Order Logic ◽  
First Order Logic ◽  
University Of Maryland ◽  
First Order ◽  
Science Philosophy ◽  
The University ◽  
Second Order Logic ◽  
Theory And Model

The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as proof theory, computability theory, and model theory, the text also contains numerous carefully graded exercises and is ideal for a first or refresher course.

Logic in the 1930s: Type Theory and Model Theory

2013 ◽  
Vol 19 (4) ◽  
pp. 433-472 ◽  
Author(s):  
Georg Schiemer ◽  
Erich H. Reck
Keyword(s):  
Twentieth Century ◽  
Model Theory ◽  
Type Theory ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Gradual Transformation ◽  
Standard Framework ◽  
Theory And Model ◽  
Made In

AbstractIn historical discussions of twentieth-century logic, it is typically assumed that model theory emerged within the tradition that adopted first-order logic as the standard framework. Work within the type-theoretic tradition, in the style of Principia Mathematica, tends to be downplayed or ignored in this connection. Indeed, the shift from type theory to first-order logic is sometimes seen as involving a radical break that first made possible the rise of modern model theory. While comparing several early attempts to develop the semantics of axiomatic theories in the 1930s, by two proponents of the type-theoretic tradition (Carnap and Tarski) and two proponents of the first-order tradition (Gödel and Hilbert), we argue that, instead, the move from type theory to first-order logic is better understood as a gradual transformation, and further, that the contributions to semantics made in the type-theoretic tradition should be seen as central to the evolution of model theory.

Sign in / Sign up

Export Citation Format

Share Document