In this paper the language of first-order modal logic is enriched with an operator @ ('actually') such that, in any model, the evaluation of a formula @A at a possible world depends on the evaluation of A at the actual world. The models have world-variable domains. All the logics that are discussed extend the classical predicate calculus, with or without identity, and conform to the philosophical principle known as serious actualism. The basic logic relies on the system (...) K, whereas others correspond to various properties that the actual world may have. All the logics are axiomatized. (shrink)

Van Lambalgen (1990) proposed a translation from a language containing a generalized quantifierQ into a first-order language enriched with a family of predicatesR i, for every arityi (or an infinitary predicateR) which takesQxg(x, y1,..., yn) to x(R(x, y1,..., y1) (x,y1,...,yn)) (y 1,...,yn are precisely the free variables ofQx). The logic ofQ (without ordinary quantifiers) corresponds therefore to the fragment of first-order logic which contains only specially restricted quantification. We prove that it is decidable using (...) the method of analytic tableaux. Related results were obtained by Andréka and Németi (1994) using the methods of algebraic logic. (shrink)

This is a companion paper to Braüner where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom (...) system first-order hybrid logic. (shrink)

One well known problem regarding quantifiers, in particular the 1storder quantifiers, is connected with their syntactic categories and denotations. The unsatisfactory efforts to establish the syntactic and ontological categories of quantifiers in formalized first-order languages can be solved by means of the so called principle of categorial compatibility formulated by Roman Suszko, referring to some innovative ideas of Gottlob Frege and visible in syntactic and semantic compatibility of language expressions. In the paper the principle is introduced for (...) categorial languages generated by the Ajdukiewicz’s classical categorial grammar. The 1st-order quantifiers are typically ambiguous. Every 1st-order quantifier of the type k > 0 is treated as a two-argument functorfunction defined on the variable standing at this quantifier and its scope (the sentential function with exactly k free variables, including the variable bound by this quantifier); a binary function defined on denotations of its two arguments is its denotation. Denotations of sentential functions, and hence also quantifiers, are defined separately in Fregean and in situational semantics. They belong to the ontological categories that correspond to the syntactic categories of these sentential functions and the considered quantifiers. The main result of the paper is a solution of the problem of categories of the 1st-order quantifiers based on the principle of categorial compatibility. (shrink)

One well known problem regarding quantifiers, in particular the 1st order quantifiers, is connected with their syntactic categories and denotations.The unsatisfactory efforts to establish the syntactic and ontological categories of quantifiers in formalized first-order languages can be solved by means of the so called principle of categorial compatibility formulated by Roman Suszko, referring to some innovative ideas of Gottlob Frege and visible in syntactic and semantic compatibility of language expressions. In the paper the principle is introduced (...) for categorial languages generated by the Ajdukiewicz’s classical categorial grammar. The 1st-order quantifiers are typically ambiguous. Every 1st-order quantifier of the type k > 0 is treated as a two-argument functor-function defined on the variable standing at this quantifier and its scope (the sentential function with exactly k free variables, including the variable bound by this quantifier); a binary function defined on denotations of its two arguments is its denotation. Denotations of sentential functions, and hence also quantifiers, are defined separately in Fregean and in situational semantics. They belong to the ontological categories that correspond to the syntactic categories of these sentential functions and the considered quantifiers. The main result of the paper is a solution of the problem of categories of the 1st-order quantifiers based on the principle of categorial compatibility. (shrink)

We investigate how the sentence choice semantics for propositional superposition logic developed in Tzouvaras could be extended so as to successfully apply to first-order superposition logic. There are two options for such an extension. The apparently more natural one is the formula choice semantics based on choice functions for pairs of arbitrary formulas of the basis language. It is proved however that the universal instantiation scheme of first-order logic, $\varphi \rightarrow \varphi $, is false, as (...) a scheme of tautologies, with respect to FCS. This causes the total failure of FCS as a candidate semantics. Then we turn to the other option, which is a variant of SCS, since it uses again choice functions for pairs of sentences only. This semantics however presupposes that the applicability of the connective | is restricted to quantifier-free sentences, and thus the class of well-formed formulas and sentences of the language is restricted too. Granted these syntactic restrictions, the usual axiomatizations of FOLS turn out to be sound and conditionally complete with respect to this second semantics, just like the corresponding systems of PLS. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to (...) decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to (...) decide regular grammar logics with converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

This chapter offers an opinionated introduction to higher-order formal languages with an eye towards their applications in metaphysics. A simply relationally typed higher-order language is introduced in four stages: starting with first-order logic, adding first-order predicate abstraction, generalizing to higher-order predicate abstraction, and finally adding higher-order quantification. It is argued that both β-conversion and Universal Instantiation are valid on the intended interpretation of this language. Given these two principles, it is (...) then shown how we can use pure higher-order logic to ask, and begin to answer, metaphysical questions with non-trivial implications. In particular, while we must reject the popular idea that structural differences between sentences correspond to parallel distinctions in the logical structure of extra-linguistic reality, it may still be possible to give a purely logical characterization of objectual aboutness and related notions. (shrink)

Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting, the decision to trust a user may sensibly be based on that user’s past behaviour. We introduce a specification language based on linear temporal logic for expressing a policy for categorising the behaviour patterns of a user depending on its transaction history. We also present an algorithm for checking whether the (...) transaction history obeys the stated policy. To be useful in a real setting, such a language should allow one to express realistic policies which may involve parameter quantification and quantitative or statistical patterns. We introduce several extensions of linear temporal logic to cater for such needs: a restricted form of universal and existential quantification; arbitrary computable functions and relations in the term language; and a “counting” quantifier for counting how many times a formula holds in the past. We then show that model checking a transaction history against a policy, which we call the history-based transaction monitoring problem, is PSPACE-complete in the size of the policy formula and the length of the history, assuming that the underlying interpreted func-. (shrink)

Developed by Arthur Prior, Temporal Logic allows to represent temporal information on a logical system using modal operators such as P, F, H or G, whose intuitive meaning is “it was sometime in the Past...”, “it will be sometime in the Future...”, “it Has always been in the past...” and “it will always Going to be in the future...” respectively. Valuation of formulae built from these operators are carried out on Kripke semantics, so Modal Logic and Temporal Logic are consequently (...) related. In fact, Temporal Logic is an extension of Modal one. Even when both logics mechanisms are able to formalize modal-temporal information with some accuracy, they suffer from a lack of expressiveness which Hybrid Logic can solve. Indeed, one of the problems of Modal Logic consists in its incapacity of naming specific points inside a model. As Temporal Logic is based on it, it cannot make such a thing neither. But First-Order Logic does can by means of constants and equality relation. Hybrid Logic, which results from combining Modal Logic and First-Order Logic, may solve this shortcoming. The main aim of this paper is to explain how Hybrid Logic emanates from Modal and Temporal ones in order to show what it adds to both logics with regard to information representation, why it is more expressive than them and what relation it maintains with the First-Order Correspondence Language. (shrink)

Developed by Arthur Prior, Temporal Logic allows to represent temporal information on a logical system using modal operators such as P, F, H or G, whose intuitive meaning is “it was sometime in the Past...”, “it will be sometime in the Future...”, “it Has always been in the past...” and “it will always Going to be in the future...” respectively. Valuation of formulae built from these operators are carried out on Kripke semantics, so Modal Logic and Temporal Logic are consequently (...) related. In fact, Temporal Logic is an extension of Modal one. Even when both logics mechanisms are able to formalize modal-temporal information with some accuracy, they suffer from a lack of expressiveness which Hybrid Logic can solve. Indeed, one of the problems of Modal Logic consists in its incapacity of naming specific points inside a model. As Temporal Logic is based on it, it cannot make such a thing neither. But First-Order Logic does can by means of constants and equality relation. Hybrid Logic, which results from combining Modal Logic and First-Order Logic, may solve this shortcoming. The main aim of this paper is to explain how Hybrid Logic emanates from Modal and Temporal ones in order to show what it adds to both logics with regard to information representation, why it is more expressive than them and what relation it maintains with the First-Order Correspondence Language. (shrink)

Hybrid languages have both modal and first-order characteristics: a Kripke semantics, and explicit variable binding apparatus. This paper motivates the development of hybrid languages, sketches their history, and examines the expressive power of three hybrid binders. We show that all three binders give rise to languages strictly weaker than the corresponding first-order language, that full first-order expressivity can be gained by adding the universal modality, and that all three binders can force the existence (...) of infinite models and have undecidable satisfiability problems. (shrink)

In the present paper, we study the correspondence and canonicity theory of modal subordination algebras and their dual Stone space with two relations, generalizing correspondence results for subordination algebras in [13–15, 25]. Due to the fact that the language of modal subordination algebras involves a binary subordination relation, we will find it convenient to use the so-called quasi-inequalities and |$\varPi _{2}$|-statements. We use an algorithm to transform (restricted) inductive quasi-inequalities and (restricted) inductive |$\varPi _{2}$|-statements to equivalent (...) class='Hi'>first-order correspondents on the dual Stone spaces with two relations with respect to arbitrary (resp. admissible) valuations. (shrink)

The book is a collection of papers and aims to unify the questions of syntax and semantics of language, which are included in logic, philosophy and ontology of language. The leading motif of the presented selection of works is the differentiation between linguistic tokens (material, concrete objects) and linguistic types (ideal, abstract objects) following two philosophical trends: nominalism (concretism) and Platonizing version of realism. The opening article under the title “The Dual Ontological Nature of Language Signs and (...) the Problem of Their Mutual Relations” provides a broad introduction into the problem area connected with this differentiation, while the logic-formal characteristics of the distinction are framed in the work entitled “On the Type-Token Relationships” (Chapter 1). The basic part of the book deals with issues relating to syntax (Chapters 2-4) and semantics of language (Chapters 5-6), as well as pertaining to syntactic-semantic pragmatic questions (Chapters 7-13). Throughout the book, language, categorial language, is characterized syntactically as generated by classical categorial grammar (Chapter 2) and formalized on two opposing levels: as language of expression-tokens (level of tokens) and language of expression-types (level of types). The author’s considerations contained in Chapters 2 and 4 lead to the important philosophical conclusion that in formal-logical syntactic studies on language the assumption that expression-types constitute the primary language layer while expression-tokens make the secondary one, can be neglected; thus, this speaks in favour of the opposing standpoint—the concretistic one—in the ontology of language syntax. In the works “Meaning and Interpretations”, Parts I and II (Chapters 5 and 6), it is underlined, however, that such semantic concepts as: meaning, denotation and interpretation are defined on the types level, yet their formal definitions require making use of notions of the tokens level. The semantic notions introduced in the above-mentioned articles are also used in the following works of the present selection, under the titles: “Three Principles of Compositionality” and “On Metaknowledge and Truth” (Chapters 7 and 8). They formalize two principles of compositionality that are well known in the literature on the subject, deriving from Frege, i.e. those of meaning and of denotation; they are related to the syntactic principle of compositionality which was introduced by the author. All the three principles are, at the same time, three conditions of homomorphism of categorial language algebra into three kinds of non-standard models of language (one syntactic and two semantic ones: intensional and extensional), which allows introducing three definitions of truthfulness into these models. The next two works in the collection, entitled: “On Language Adequacy” and “What is the Sense in Logic and Philosophy of Language” (Chapters 9 and 10) concern adequacy of categorial language syntax along with its dual semantics: intensional and extensional, and categorial compatibility of any of its syntactic categories with two corresponding semantic categories: intensional and extensional, based on the compatibility the syntactic category of each language expression with the ontological category assigned to its denotatum. The well-known problem of categorial compatibility for first-order quantifiers finds its solution in the paper “Categories of First-Order Quantifiers” (Chapter 11). In the work “Logic and Ontology of Language” (Chapter 12), being in a sense a summary of the considerations presented in the preceding chapters of the book, language is treated as an ontological being, characterized in compliance with the logical conception of language proposed by Ajdukiewicz. Application—like throughout the book—of tools of classical logic and set theory has resulted in emergence of a general formal logical theory of syntax, semantics and pragmatics of language, which takes into account duality in the understanding of linguistic expressions as tokens (concretes) and types (abstract objects). In terms that take into account a functional approach to language itself, there comes out an ontological neutrality of logic with respect to existential assumptions relating to the ontological nature of linguistic expressions and their extra-linguistic ontological counterparts. The issues connected with applying logic while explaining the manner of using linguistic tokens and linguistic types to determine notions of language communication are raised and illustrated in the last chapter of the work, bearing the title “A Logical Conceptualization of Knowledge on the Notion of Language Communication”. (shrink)

The paper presents Property Theory with Curry Typing (PTCT) where the language of terms and well-formed formulæ are joined by a language of types. In addition to supporting fine-grained intensionality, the basic theory is essentially first-order, so that implementations using the theory can apply standard first-order theorem proving techniques. The paper sketches a system of tableau rules that implement the theory. Some extensions to the type theory are discussed, including type polymorphism, which provides a (...) useful analysis of conjunctive terms. Such terms can be given a single polymorphic type that expresses the fact that they can conjoin phrases of any one type, yielding an expression of the same type. (shrink)

In this paper we investigate some mathematical consequences of the Equivocation Principle, and the Maximum Entropy models arising from that, for first order languages. We study the existence of Maximum Entropy models for these theories in terms of the quantifier complexity of the theory and will investigate some invariance and structural properties of such models.

The paper presents Property Theory with Curry Typing where the language of terms and well-formed formulæ are joined by a language of types. In addition to supporting fine-grained intensionality, the basic theory is essentially first-order, so that implementations using the theory can apply standard first-order theorem proving techniques. The paper sketches a system of tableau rules that implement the theory. Some extensions to the type theory are discussed, including type polymorphism, which provides a useful (...) analysis of conjunctive terms. Such terms can be given a single polymorphic type that expresses the fact that they can conjoin phrases of any one type, yielding an expression of the same type. (shrink)

Standard models for model predicate logic consist of a Kripke frame whose worlds come equipped with relational structures. Both modal and two-sorted predicate logic are natural languages for speaking about such models. In this paper we compare their expressivity. We determine a fragment of the two-sorted language for which the modal language is expressively complete on S5-models. Decidable criteria for modal definability are presented.

The Language of First-Order Logic is a complete introduction to first-order symbolic logic, consisting of a computer program and a text. The program, an aid to learning and using symbolic notation, allows one to construct symbolic sentences and possible worlds, and verify that a sentence is well formed. The truth or falsity of a sentence can be determined by playing a deductive game with the computer.

We investigate an approach for drawing logical inference from inconsistent premisses. The main idea in this approach is that the inconsistencies in the premisses should be interpreted as uncertainty of the information. We propose a mechanism, based on Kinght’s [14] study of inconsistency, for revising an inconsistent set of premisses to a minimally uncertain, probabilistically consistent one. We will then generalise the probabilistic entailment relation introduced in [15] for propositional languages to the first order case to draw logical (...) inference from a probabilistic set of premisses. We will show how this combination can allow us to limit the effect of uncertainty introduced by inconsistent premisses to only the reasoning on the part of the premise set that is relevant to the inconsistency. (shrink)

We present Property Theory with Curry Typing (PTCT), an intensional first-order logic for natural language semantics. PTCT permits fine-grained specifications of meaning. It also supports polymorphic types and separation types. We develop an intensional number theory within PTCT in order to represent proportional generalized quantifiers like “most.” We use the type system and our treatment of generalized quantifiers in natural language to construct a type-theoretic approach to pronominal anaphora that avoids some of the difficulties that (...) undermine previous type-theoretic analyses of this phenomenon. (shrink)

This book is intended, along with the computer program, to introduce the user to some of the most important concepts and tools of logic, including learning a new computer language.

Ignacio Jane has argued that second-order logic presupposes some amount of set theory and hence cannot legitimately be used in axiomatizing set theory. I focus here on his claim that the second-order formulation of the Axiom of Separation presupposes the character of the power set operation, thereby preventing a thorough study of the power set of infinite sets, a central part of set theory. In reply I argue that substantive issues often cannot be separated from a logic, but (...) rather must be presupposed. I call this the logic-metalogic link. There are two facets to the logic-metalogic link. First, when a logic is entangled with a substantive issue, the same position on that issue should be taken at the meta- level as at the object level; and second, if an expression has a clear meaning in natural language, then the corresponding concept can equally well be deployed in a formal language. The determinate nature of the power set operation is one such substantive issue in set theory. Whether there is a determinate power set of an infinite set can only be presupposed in set theory, not proved, so the use of second-order logic cannot be ruled out by virtue of presupposing one answer to this question. Moreover, the legitimacy of presupposing in the background logic that the power set of an infinite set is determinate is guaranteed by the clarity and definiteness of the notions of all and of subset. This is also exactly what is required for the same presupposition to be legitimately made in an axiomatic set theory, so the use of second-order logic in set theory rather than first-order logic does not require any new metatheoretic commitments. (shrink)

We provide first-order axioms for the theories of finite trees with bounded branching and finite trees with arbitrary (finite) branching. The signature is chosen to express, in a natural way, those properties of trees most relevant to linguistic theories. These axioms provide a foundation for results in linguistics that are based on reasoning formally about such properties. We include some observations on the expressive power of these theories relative to traditional language complexity classes.

This paper introduces two languages and associated logics designed to afford perspicuous representations of a range of natural language arguments involving adverbs and the like: first-order logic with basic adverbs (FOL-BA) and first-order logic with scoped adverbs (FOL-SA). The guiding logical idea is that an adverb can come between a term and the rest of the statement it is a part of, resulting in a logically stronger statement. I explain various interesting challenges that arise in (...) the attempt to implement the guiding idea, and provide solutions for some but not all of them. I conclude by outlining some directions for further research. (shrink)

If are structures for a first-order language , is said to be algebraically closed in just in case every positive existential -sentence true in is true in . In 1976 Elliott showed that unital AF algebras are classified up to isomorphism by corresponding dimension groups with order unit. This paper shows that one dimension group with order unit is algebraically closed in another just in case the corresponding AF algebras, viewed as metric structures, fall in (...) the same relation. (shrink)

In several areas of Mathematical Logic and Computer Science one would ideally like to use the set F orm(L) of all formulas of some first-order language L for some goal, but this cannot be done safely. In such a case it is necessary to select a subset of F orm(L) that can safely be used. Three main examples of this phenomenon are: • The main principle of naive set theory is the comprehension schema: ∃Z(∀x.x ∈ Z ⇔ (...) A). (shrink)

This paper is about a special version of PDL, proposed by Marcus Kracht, for reasoning about sibling ordered trees. It has four basic programs corresponding to the child, parent, left- and right-sibling relations in such trees. The original motivation for this language is rooted in the field of model-theoretic syntax. Motivated by recent developments in the area of semi-structured data, and, especially, in the field of query languages for XML (eXtensible Markup Language) documents, we revisit the language. (...) This renewed interest comes with a special focus on complexity and expressivity aspects of the language, aspects that have so far largely been ignored. We survey and derive complexity results, and spend most of the paper on the most important open question concerning the language: what is its expressive power? We approach this question from two angles: Which first-order properties can be expressed? And which second-order properties? While we are still some way from definitive answers to these questions, we discuss two first-order fragments of the PDL language for ordered trees, and show how the language can be used to express some typical (second-order) problems, like the boolean circuit and the frontier problem. (shrink)

This text/courseware package presents a new approach to teaching first-order logic. Taking advantage of Tarski's World 4.0, the text skilfully balances the semantic conception of logic with methods of proof. The book contains eleven chapters, in four parts. Part I is about propositional logic, Part II about quantifier logic. Part III contains chapters on set theory and inductive definitions. Part IV contains advanced topics in logic, including topics of importance in applications of logic in computer science. The (...) class='Hi'>Language of First-order Logic contains hundreds of problems and exercises for the user to work through. (shrink)

A first-order language with a defined identity predicate is proposed whose apparatus for atomic predication is sensitive to grammatical categories of natural language. Subatomic natural deduction systems are defined for this naturalistic first-order language. These systems contain subatomic systems which govern the inferential relations which obtain between naturalistic atomic sentences and between their possibly composite components. As a main result it is shown that normal derivations in the defined systems enjoy the subexpression property (...) which subsumes the subformula property with respect to atomic and identity formulae as a special case. The systems admit a proof-theoretic semantics which does not only apply to logically compound but also to atomic and identity formulae—as well as to their components. The potential of the defined systems for a meticulous first-order analysis of natural inferences whose validity crucially depends on expressions of some of the aforementioned categories is demonstrated. (shrink)

In preference aggregation a set of individuals express preferences over a set of alternatives, and these preferences have to be aggregated into a collective preference. When preferences are represented as orders, aggregation procedures are called social welfare functions. Classical results in social choice theory state that it is impossible to aggregate the preferences of a set of individuals under different natural sets of axiomatic conditions. We define a first-order language for social welfare functions and we give a (...) complete axiomatisation for this class, without having the number of individuals or alternatives specified in the language. We are able to express classical axiomatic requirements in our first-order language, giving formal axioms for three classical theorems of preference aggregation by Arrow, by Sen, and by Kirman and Sondermann. We explore to what extent such theorems can be formally derived from our axiomatisations, obtaining positive results for Sen’s Theorem and the Kirman-Sondermann Theorem. For the case of Arrow’s Theorem, which does not apply in the case of infinite societies, we have to resort to fixing the number of individuals with an additional axiom. In the long run, we hope that our approach to formalisation can serve as the basis for a fully automated proof of classical and new theorems in social choice theory. (shrink)

The paper studies first order extensions of classical systems of modal logic (see (Chellas, 1980, part III)). We focus on the role of the Barcan formulas. It is shown that these formulas correspond to fundamental properties of neighborhood frames. The results have interesting applications in epistemic logic. In particular we suggest that the proposed models can be used in order to study monadic operators of probability (Kyburg, 1990) and likelihood (Halpern-Rabin, 1987).

This paper provides finitary jointly necessary and sufficient acceptance and rejection conditions for the logical constants of a first order quantificational language. By introducing the notion of making an assignment as a distinct object level practice—something you do with a sentence—(as opposed to a meta-level semantic notion) and combining this with the practice of (hypothetical and categorical) acceptance and rejection and the practice of making suppositions one gains a structure that is sufficiently rich to fully characterize the (...) class of classical first order theories. The analysis thus provides a way of characterizing classical first order quantification by expressivist means. (shrink)

The main aim of this paper is to introduce first-order versions of logics of evidence and truth, together with corresponding sound and complete Kripke semantics with variable and constant domains. According to the intuitive interpretation proposed here, these logics intend to represent possibly inconsistent and incomplete information bases over time. The paper also discusses the connections between Belnap-Dunn’s and da Costa’s approaches to paraconsistency, and argues that the logics of evidence and truth combine them in a very natural (...) way. (shrink)