Some model theory for game logics

1979 ◽  
Vol 44 (2) ◽  
pp. 147-152
Author(s):  
Judy Green

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.

1973 ◽  
Vol 38 (4) ◽  
pp. 613-627 ◽  
Author(s):  
Melvin Fitting

In classical logic a collection of sets of statements (or equivalently, a property of sets of statements) is called a consistency property if it meets certain simple closure conditions (a definition is given in §2). The simplest example of a consistency property is the collection of all consistent sets in some formal system for classical logic. The Model Existence Theorem then says that any member of a consistency property is satisfiable in a countable domain. From this theorem many basic results of classical logic follow rather simply: completeness theorems, the compactness theorem, the Lowenheim-Skolem theorem, and the Craig interpolation lemma among others. The central position of the theorem in classical logic is obvious. For the infinitary logic the Model Existence Theorem is even more basic as the compactness theorem is not available; [8] is largely based on it.In this paper we define appropriate notions of consistency properties for the first-order modal logics S4, T and K (without the Barcan formula) and for intuitionistic logic. Indeed we define two versions for intuitionistic logic, one deriving from the work of Gentzen, one from Beth; both have their uses. Model Existence Theorems are proved, from which the usual known basic results follow. We remark that Craig interpolation lemmas have been proved model theoretically for these logics by Gabbay ([5], [6]) using ultraproducts. The existence of both ultra-product and consistency property proofs of the same result is a common phenomena in classical and infinitary logic. We also present extremely simple tableau proof systems for S4, T, K and intuitionistic logics, systems whose completeness is an easy consequence of the Model Existence Theorems.


1987 ◽  
Vol 52 (2) ◽  
pp. 473-493 ◽  
Author(s):  
Walter A. Carnielli

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.


2002 ◽  
Vol 25 (3) ◽  
pp. 330-331
Author(s):  
Pierre Barrouillet ◽  
Henry Markovits

As stressed by Perruchet & Vinter, the SOC model echoes Johnson-Laird's mental model theory. Indeed, the latter rejects rule-based processing and assumes that reasoning is achieved through the manipulation of conscious representations. However, the mental model theory as well as its modified versions resorts to the abstraction of complex schemas and some form of implicit logic that seems incompatible with the SOC approach.


2004 ◽  
Vol 69 (4) ◽  
pp. 1027-1088 ◽  
Author(s):  
Christoph Benzmüller ◽  
Chad E. Brown ◽  
Michael Kohlhase

Abstract.In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes.


1977 ◽  
Vol 42 (2) ◽  
pp. 221-237 ◽  
Author(s):  
George F. McNulty

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.


Author(s):  
John R Taylor

After a brief account of the salient characteristics of Langacker’s Cognitive Grammar, this chapter highlights the distinctive perspective which this approach offers on traditional topics in the description of English, including the question of word classes, the nature of syntactic relations, and the status of constructions as an alternative to rule-based accounts of linguistic knowledge. It presents three case studies illustrating the role of background cognition, not only as a factor in semantic interpretation but also for its grammatical effects. These concern (i) the role of grounding in nominal and verbal systems, (ii) some of the manifestations of cognitive reference points in such diverse areas as possessive expressions and constraints on the use of participles, and (iii) processes of subjectification, as exemplified in such areas as modals, fictive motion, and causal relations.


2020 ◽  
pp. 182-197
Author(s):  
M.S. Nikitchenko ◽  
◽  
О.S. Shkilniak ◽  
S.S. Shkilniak ◽  
◽  
...  

We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi.


Sign in / Sign up

Export Citation Format

Share Document