Classical logic has proved inadequate in various areas of computer science, artificial intelligence, mathematics, philosopy and linguistics. This is an introduction to extensions of first-order logic, based on the principle that many-sorted logic (MSL) provides a unifying framework in which to place, for example, second-order logic, type theory, modal and dynamic logics and MSL itself. The aim is two fold: only one theorem-prover is needed; proofs of the metaproperties of the different existing (...) calculi can be avoided by borrowing them from MSL. To make the book accessible to readers from different disciplines, whilst maintaining precision, the author has supplied detailed step-by-step proofs, avoiding difficult arguments, and continually motivating the material with examples. Consequently this can be used as a reference, for self-teaching or for first-year graduate courses. (shrink)

We prove an Omitting Types Theorem for certain algebraizable extensions of first order logic without equality studied in [SAI 00] and [SAY 04]. This is done by proving a representation theorem preserving given countable sets of infinite meets for certain reducts of ?- dimensional polyadic algebras, the so-called G polyadic algebras (Theorem 5). Here G is a special subsemigroup of (?, ? o) that specifies the signature of the algebras in question. We state and prove an (...) independence result connecting our representation theorem to Martin's axiom (Theorem 6). Also we show that the countable atomic G polyadic algebras are completely representable (Corollary 16) contrasting results on cylindric algebras. Several related results are surveyed. (shrink)

That every first-order theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently well-known nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. (...) It can be seen as a modification of Skolem’s argument from 1920 for his “Normal Form” theorem. “Geometric” being the infinitary version of “coherent”, it is further shown that every infinitary first-order theory, suitably restricted, has a geometric conservative extension, hence the title. The results are applied to simplify methods used in reasoning in and about modal and intermediate logics. We include also a new algorithm to generate special coherent implications from an axiom, designed to preserve the structure of formulae with relatively little use of normal forms. (shrink)

We prove a generalization of Maehara’s lemma to show that the extensions of classical and intuitionistic first-order logic with a special type of geometric axioms, called singular geometric axioms, have Craig’s interpolation property. As a corollary, we obtain a direct proof of interpolation for (classical and intuitionistic) first-order logic with identity, as well as interpolation for several mathematical theories, including the theory of equivalence relations, (strict) partial and linear orders, and various intuitionistic (...) class='Hi'>order theories such as apartness and positive partial and linear orders. (shrink)

Fix \. Let \ denote first order logic restricted to the first n variables. Using the machinery of algebraic logic, positive and negative results on omitting types are obtained for \ and for infinitary variants and extensions of \.

We show that, assuming the consistency of a supercompact cardinal, the first inaccessible cardinal can satisfy a strong form of a Löwenheim–Skolem–Tarski theorem for the equicardinality logic L, a logic introduced in [5] strictly between first order logic and second order logic. On the other hand we show that in the light of present day inner model technology, nothing short of a supercompact cardinal suffices for this result. In particular, we show that (...) the Löwenheim–Skolem–Tarski theorem for the equicardinality logic at κ implies the Singular Cardinals Hypothesis above κ as well as Projective Determinacy. (shrink)

It is shown by Parsons [2] that the first-order fragment of Frege's logical system in the Grundgesetze der Arithmetic is consistent. In this note we formulate and prove a stronger version of this result for arbitrary first-order theories. We also show that a natural attempt to further strengthen our result runs afoul of Tarski's theorem on the undefinability of truth.

There exist two known types of ultrafilter extensions of first-order models, both in a certain sense canonical. One of them comes from modal logic and universal algebra, and in fact goes back to Jónsson and Tarski :891–939, 1951; 74:127–162, 1952). Another one The infinity project proceeding, Barcelona, 2012) comes from model theory and algebra of ultrafilters, with ultrafilter extensions of semigroups as its main precursor. By a classical fact of general topology, the space of ultrafilters (...) over a discrete space is its largest compactification. The main result of Saveliev The infinity project proceeding, Barcelona, 2012), which confirms a canonicity of this extension, generalizes this fact to discrete spaces endowed with an arbitrary first-order structure. An analogous result for the former type of ultrafilter extensions was obtained in Saveliev. Results of such kind are referred to as extension theorems. After a brief introduction, we offer a uniform approach to both types of extensions based on the idea to extend the extension procedure itself. We propose a generalization of the standard concept of first-order interpretations in which functional and relational symbols are interpreted rather by ultrafilters over sets of functions and relations than by functions and relations themselves, and define ultrafilter models with an appropriate semantics for them. We provide two specific operations which turn ultrafilter models into ordinary models, establish necessary and sufficient conditions under which the latter are the two canonical ultrafilter extensions of some ordinary models, and obtain a topological characterization of ultrafilter models. We generalize a restricted version of the extension theorem to ultrafilter models. To formulate the full version, we propose a wider concept of ultrafilter models with their semantics based on limits of ultrafilters, and show that the former concept can be identified, in a certain way, with a particular case of the latter; moreover, the new concept absorbs the ordinary concept of models. We provide two more specific operations which turn ultrafilter models in the narrow sense into ones in the wide sense, and establish necessary and sufficient conditions under which ultrafilter models in the wide sense are the images of ones in the narrow sense under these operations, and also are two canonical ultrafilter extensions of some ordinary models. Finally, we establish three full versions of the extension theorem for ultrafilter models in the wide sense. The results of the first three sections of this paper were partially announced in Poliakov and Saveliev On two concepts of ultrafilter extensions of first-order models and their generalizations, Springer, Berlin, 2017). (shrink)

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)

Many authors have noted that there are types of English modal sentences cannot be formalized in the language of basic first-order modal logic. Some widely discussed examples include “There could have been things other than there actually are” and “Everyone who is actually rich could have been poor.” In response to this lack of expressive power, many authors have discussed extensions of first-order modal logic with two-dimensional operators. But claims about the relative expressive (...) power of these extensions are often justified only by example rather than by rigorous proof. In this paper, we provide proofs of many of these claims and present a more complete picture of the expressive landscape for such languages. (shrink)

We present the first-order logic of change, which is an extension of the propositional logic of change $\textsf {LC}\Box $ developed and axiomatized by Świętorzecka and Czermak. $\textsf {LC}\Box $ has two primitive operators: ${\mathcal {C}}$ to be read it changes whether and $\Box $ for constant unchangeability. It implements the philosophically grounded idea that with the help of the primary concept of change it is possible to define the concept of time. One of the characteristic (...) axioms for ${\mathcal {C}}$ is ${\mathcal {C}} A \to {\mathcal {C}}\neg A$ and one of the primitive rules is $\omega $-rule introducing $\Box $. It turns out that the next operator is definable in $\textsf {LC}\Box $. Logic $\textsf {LC}\Box $ with next is equivalent to certain fragment of $\textsf {LTL}$ extended by the appropriate definition of ${\mathcal {C}}$. Recently, $\textsf {LC}\Box $ has also been modified to the propositional logic of ‘branching’ changes $\textsf {BTC}$ by Łyczak and the logic of ‘parallel’ changes $\textsf {LC}\Box $ ↳ by Świętorzecka and Łyczak. Extended in an appropriate manner, $\textsf {BTC}$ is equivalent to a certain fragment of logic $\textsf {CTL}$ to which definitions of two kinds of changes have been added. Here we propose an extension of $\textsf {LC}\Box $ to first-order logic in which, again, the only primitive modal operators are ${\mathcal {C}}$ and $\Box $. We interpret our logic in the semantics of histories of changes. We give an axiomatic system $\textsf {LC}\Box Q$ for the considered logic, and we show selected theses about some relationships between ${\mathcal {C}}$, $\Box $ and $\forall $. Then we prove the completeness of $\textsf {LC}\Box Q$. Finally, we compare our logic with $\textsf {FOLT}$ and show the relation between $\textsf {LC}\Box Q$ and a certain fragment of the Kröger system $\varSigma $ to which the definition of ${\mathcal {C}}$ was added. (shrink)

We consider one aspect of the problem of specification and verification of reactive real-time systems which involve operations and constraints concerning time. Time is continuous what is motivated by specifications of hybrid systems. Our goal is to try to find a framework that is based on applied first order logic that permits to represent the verification problem directly, completely and conservatively , and that is apt to describe interesting decidable classes, maybe showing way to feasible algorithms. To (...) achieve this goal we use a first order timed logic that is an extension of a decidable theory of reals with timed functions. This logic permits, on the one hand, to rewrite directly and completely requirements and, on the other hand, to describe executions of various timed algorithms—here we consider block Gurevich abstract state machines because of their theoretical clarity and sufficient expressive power. Then we describe one decidable class of the verification problem that is based on notions reflecting finiteness properties of systems of control. These notions may be of independent interest, as, in particular, they give a way to describe a limited usage of arithmetics preserving decidability that is not covered by existing model-theoretic approaches. As an example we consider the generalized railroad crossing problem that we analyze in its entirety. (shrink)

This is part I of a two-part essay introducing case-intensional first order logic, an easy-to-use, uniform, powerful, and useful combination of first-order logic with modal logic resulting from philosophical and technical modifications of Bressan’s General interpreted modal calculus. CIFOL starts with a set of cases; each expression has an extension in each case and an intension, which is the function from the cases to the respective case-relative extensions. Predication is intensional; identity is (...) extensional. Definite descriptions are context-independent terms, and lambda-predicates and -operators can be introduced without constraints. These logical resources allow one to define, within CIFOL, important properties of properties, viz., extensionality and absoluteness, Bressan’s chief innovation that allows tracing an individual across cases without recourse to any notion of “rigid designation” or “trans-world identity.” Thereby CIFOL abstains from incorporating any metaphysical principles into the quantificational machinery, unlike extant frameworks of quantified modal logic. We claim that this neutrality makes CIFOL a useful tool for discussing both metaphysical and scientific arguments involving modality and quantification, and we illustrate by discussing in diagrammatic detail a number of such arguments involving the extensional identification of individuals via absolute properties, essential properties, de re vs. de dicto, and the results of possible tests. (shrink)

We prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, (...) GL.3, etc.). For many quantified modal logics, including those in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable. (shrink)

The logics of formal inconsistency (LFIs, for short) are paraconsistent logics (that is, logics containing contradictory but non-trivial theories) having a consistency connective which allows to recover the ex falso quodlibet principle in a controlled way. The aim of this paper is considering a novel semantical approach to first-order LFIs based on Tarskian structures defined over swap structures, a special class of multialgebras. The proposed semantical framework generalizes previous aproaches to quantified LFIs presented in the literature. The case (...) of QmbC, the simpler quantified LFI expanding classical logic, will be analyzed in detail. An axiomatic extension of QmbC called QLFI1o is also studied, which is equivalent to the quantified version of da Costa and D'Ottaviano 3-valued logic J3. The semantical structures for this logic turn out to be Tarkian structures based on twist structures. The expansion of QmbC and QLFI1o with a standard equality predicate is also considered. (shrink)

This is part I of a two-part essay introducing case-intensional first order logic, an easy-to-use, uniform, powerful, and useful combination of first-order logic with modal logic resulting from philosophical and technical modifications of Bressan’s General interpreted modal calculus. CIFOL starts with a set of cases; each expression has an extension in each case and an intension, which is the function from the cases to the respective case-relative extensions. Predication is intensional; identity is (...) extensional. Definite descriptions are context-independent terms, and lambda-predicates and -operators can be introduced without constraints. These logical resources allow one to define, within CIFOL, important properties of properties, viz., extensionality and absoluteness, Bressan’s chief innovation that allows tracing an individual across cases without recourse to any notion of “rigid designation” or “trans-world identity.” Thereby CIFOL abstains from incorporating any metaphysical principles into the quantificational machinery, unlike extant frameworks of quantified modal logic. We claim that this neutrality makes CIFOL a useful tool for discussing both metaphysical and scientific arguments involving modality and quantification, and we illustrate by discussing in diagrammatic detail a number of such arguments involving the extensional identification of individuals via absolute properties, essential properties, de re vs. de dicto, and the results of possible tests. (shrink)

This paper introduces the logic _Q__L__E__T_ _F_, a quantified extension of the logic of evidence and truth _L__E__T_ _F_, together with a corresponding sound and complete first-order non-deterministic valuation semantics. _L__E__T_ _F_ is a paraconsistent and paracomplete sentential logic that extends the logic of first-degree entailment (_FDE_) with a classicality operator ∘ and a non-classicality operator ∙, dual to each other: while ∘_A_ entails that _A_ behaves classically, ∙_A_ follows from _A_’s violating some (...) classically valid inferences. The semantics of _Q__L__E__T_ _F_ combines structures that interpret negated predicates in terms of anti-extensions with first-order non-deterministic valuations, and completeness is obtained through a generalization of Henkin’s method. By providing sound and complete semantics for first-order extensions of _FDE_, _K3_, and _LP_, we show how these tools, which we call here the method of _anti-extensions + valuations_, can be naturally applied to a number of non-classical logics. (shrink)

Certain extensions of Nelson's constructive logic N with strong negation have recently become important in arti.cial intelligence and nonmonotonic reasoning, since they yield a logical foundation for answer set programming (ASP). In this paper we look at some extensions of Nelson's .rst-order logic as a basis for de.ning nonmonotonic inference relations that underlie the answer set programming semantics. The extensions we consider are those based on 2-element, here-and-there Kripke frames. In particular, we prove completeness (...) for .rst-order here-and-there logics, and their minimal strong negation extensions, for both constant and varying domains. We choose the constant domain version, which we denote by QNc5, as a basis for de.ning a .rst-order nonmonotonic extension called equilibrium logic. We establish several metatheoretic properties of QNc5, including Skolem forms and Herbrand theorems and Interpolation, and show that the .rst-oder version of equilibrium logic can be used as a foundation for answer set inference. (shrink)

Inquisitive first order logic is an extension of first order classical logic, introducing questions and studying the logical relations between questions and quantifiers. It is not known whether is recursively axiomatizable, even though an axiomatization has been found for fragments of the logic. In this paper we define the \—classical antecedent—fragment, together with an axiomatization and a proof of its strong completeness. This result extends the ones presented in the literature and introduces a (...) new approach to study the axiomatization problem for fragments of the logic. (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 investigates the question of characterizing first-order LFIs (logics of formal inconsistency) by means of two-valued semantics. LFIs are powerful paraconsistent logics that encode classical logic and permit a finer distinction between contradictions and inconsistencies, with a deep involvement in philosophical and foundational questions. Although focused on just one particular case, namely, the quantified logic QmbC, the method proposed here is completely general for this kind of logics, and can be easily extended to a large (...) family of quantified paraconsistent logics, supplying a sound and complete semantical interpretation for such logics. However, certain subtleties involving term substitution and replacement, that are hidden in classical structures, have to be taken into account when one ventures into the realm of nonclassical reasoning. This paper shows how such difficulties can be overcome, and offers detailed proofs showing that a smooth treatment of semantical characterization can be given to all such logics. Although the paper is well-endowed in technical details and results, it has a significant philosophical aside: it shows how slight extensions of classical methods can be used to construct the basic model theory of logics that are weaker than traditional logic due to the absence of certain rules present in classical logic. Several such logics, however, as in the case of the LFIs treated here, are notorious for their wealth of models precisely because they do not make indiscriminate use of certain rules; these models thus require new methods. In the case of this paper, by just appealing to a refined version of the Principle of Explosion, or Pseudo-Scotus, some new constructions and crafty solutions to certain non-obvious subtleties are proposed. The result is that a richer extension of model theory can be inaugurated, with interest not only for paraconsistency, but hopefully to other enlargements of traditional logic. (shrink)

Classical first-order logic \ is commonly used to study logical connections between statements, that is sentences that in every context have an associated truth-value. Inquisitive first-order logic \ is a conservative extension of \ which captures not only connections between statements, but also between questions. In this paper we prove the disjunction and existence properties for \ relative to inquisitive disjunction Open image in new window and inquisitive existential quantifier \. Moreover we extend these (...) results to several families of theories, among which the one in the language of \. To this end, we initiate a model-theoretic approach to the study of \. In particular, we develop a toolkit of basic constructions in order to transform and combine models of \. (shrink)

Classical first-order logic \ is commonly used to study logical connections between statements, that is sentences that in every context have an associated truth-value. Inquisitive first-order logic \ is a conservative extension of \ which captures not only connections between statements, but also between questions. In this paper we prove the disjunction and existence properties for \ relative to inquisitive disjunction Open image in new window and inquisitive existential quantifier \. Moreover we extend these (...) results to several families of theories, among which the one in the language of \. To this end, we initiate a model-theoretic approach to the study of \. In particular, we develop a toolkit of basic constructions in order to transform and combine models of \. (shrink)

In this paper, an extension of first order logic is introduced. In such logics atomic formulas may have infinite lengths. An Omitting Types Theorem is proved.

Dynamic predicate logic (DPL), presented in [5] as a formalism for representing anaphoric linking in natural language, can be viewed as a fragment of a well known formalism for reasoning about imperative programming [6]. An interesting difference from other forms of dynamic logic is that the distinction between formulas and programs gets dropped: DPL formulas can be viewed as programs. In this paper we show that DPL is in fact the basis of a hierarchy of formulas-as-programs languages.

The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO 2 over ordered, respectively wellordered, domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision (...) problems is essentially the same as for plain unconstrained FO 2 , namely non-deterministic exponential time. In contrast FO 2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings, wellorderings, or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO 2 and computation tree logic CTL. (shrink)

We show how mereotopological notions can be expressed by extending intuitionistic propositional logic with propositional quantification and a strong modal operator. We first prove completeness for the logics wrt Kripke models; then we trace the correspondence between Kripke models and topological spaces that have been enhanced with an explicit notion of expressible region. We show how some qualitative spatial notions can be expressed in topological terms. We use the semantical and topological results in order to show how (...) in some extensions of the logics it is possible to express connectedness, non-emptiness and a set of jointly exhaustive, pairwise disjoint, binary relations that play a significant role in qualitative spatial reasoning. (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. Some extensions to the type theory are discussed, type polymorphism, and enriching the system with sufficient number theory to account for quantifiers of proportion, such as “most.”.

In 1950, B.A. Trakhtenbrot showed that the set of first-order tautologies associated to finite models is not recursively enumerable. In 1999, P. Hájek generalized this result to the first-order versions of Łukasiewicz, Gödel and Product logics, w.r.t. their standard algebras. In this paper we extend the analysis to the first-order versions of axiomatic extensions of MTL. Our main result is the following. Let \ be a class of MTL-chains. Then the set of all (...) first-order tautologies associated to the finite models over chains in \, fTAUT\, is \ -hard. Let TAUT\ be the set of propositional tautologies of \. If TAUT\ is decidable, we have that fTAUT\ is in \. We have similar results also if we expand the language with the Δ operator. (shrink)

W. V. Quine thinks logical truth can be defined in purely extensional terms, as follows: a logical truth is a true sentence that exemplifies a logical form all of whose instances are true. P. F. Strawson objects that one cannot say what it is for a particular use of a sentence to exemplify a logical form without appealing to intensional notions, and hence that Quine's efforts to define logical truth in purely extensional terms cannot succeed. Quine's reply to this criticism (...) is confused in ways that have not yet been noticed in the literature. This may seem to favour Strawson's side of the debate. In fact, however, a proper analysis of the difficulties that Quine's reply faces suggests a new way to clarify and defend the view that logical truth can be defined in purely extensional terms. (shrink)

In his preface, Hunter explains that this volume is intended to provide for non-mathematicians an introduction to the most important results of modern mathematical logic. The reader will find here the work of Post, Skolem, Gödel, Church, Henkin, and others, presented in a terse and closely-knit style. Though acknowledging the trend toward natural deduction systems, Hunter sticks to more classical axiomatic systems on the grounds that the proofs of metatheorems are simplified by that choice. He begins with a formal (...) system of propositional logic, for which he develops proofs of completeness, consistency, and decidability. Systems of first order predicate logic are then dealt with, and Church's and Gödel's results on undecidability and incompleteness are presented. There is a brief, useful discussion indicating what parts of first order predicate logic are decidable. It is assumed that the reader has some familiarity with elementary formal logic: Hunter develops the set-theoretical results he requires. The compactness of the presentation is facilitated by the use of earlier results for propositional logic to obtain certain results for predicate logic. Especially helpful is Hunter's technique of prefacing each of the longer and more difficult proofs with a section explaining the key ideas and the general method of proof; summaries are also often provided in conclusion. Because of the orientation of the book, a more extensive discussion of the significance of the results obtained and the philosophical issues which have been raised concerning some of them, would have been welcome. Nonetheless, this is a good, concise introduction for those who are not yet prepared to tackle the more technical literature. A bibliography is provided for those interested in pursuing the subject in greater detail.--E. M. F. (shrink)

I build a canonical model for constant domain basic first-order logic (BQLCD), the constant domain first-order extension of Visser’s basic propositional logic, and use the canonical model to verify that BQLCD satisfies the disjunction and existence properties.

Reference [12] introduced a novel formula to formula translation tool that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is unavailable. This paper applies the formulator approach to show the independence of (...) the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations. In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics. (shrink)

The previously introduced algorithm \sqema\ computes first-order frame equivalents for modal formulae and also proves their canonicity. Here we extend \sqema\ with an additional rule based on a recursive version of Ackermann's lemma, which enables the algorithm to compute local frame equivalents of modal formulae in the extension of first-order logic with monadic least fixed-points \mffo. This computation operates by transforming input formulae into locally frame equivalent ones in the pure fragment of the hybrid mu-calculus. (...) In particular, we prove that the recursive extension of \sqema\ succeeds on the class of `recursive formulae'. We also show that a certain version of this algorithm guarantees the canonicity of the formulae on which it succeeds. (shrink)

Via the formulas-as-types embedding certain extensions of Heyting Arithmetic can be represented in intuitionistic type theories. In this paper we discuss the embedding of ω-sorted Heyting Arithmetic HA ω into a type theory WL, that can be described as Troelstra's system ML 1 0 with so-called weak Σ-elimination rules. By syntactical means it is proved that a formula is derivable in HA ω if and only if its corresponding type in WL is inhabited. Analogous results are proved for Diller's (...) so-called restricted system and for a type theory based on predicate logic instead of arithmetic. (shrink)

We introduce a path-based cyclic proof system for first-order $\mu $-calculus, the extension of first-order logic by second-order quantifiers for least and greatest fixed points of definable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam and Sprenger. Furthermore, we establish cut-free completeness of our system for the fragment corresponding to the modal $\mu $-calculus.

Contrary to what is stated in Lemma 7.1 of [8], it is shown that some Boolean algebras of finitary logic admit finitely additive probabilities that are not σ-additive. Consequences of Lemma 7.1 are reconsidered. The concept of a C-σ-additive probability on B (where B and C are Boolean algebras, and $\mathscr{B} \subseteq \mathscr{C}$ ) is introduced, and a generalization of Hahn's extension theorem is proved. This and other results are employed to show that every S̄(L)-σ-additive probability on s̄(L) can (...) be extended (uniquely, under some conditions) to a σ-additive probability on S̄(L), where L belongs to a quite extensive family of first order languages, and S̄(L) and s̄(L) are, respectively, the Boolean algebras of sentences and quantifier free sentences of L. (shrink)

I present a sequent calculus that extends a nonmonotonic reflexive consequence relation as defined over an atomic first-order language without variables to one defined over a logically complex first-order language. The extension preserves reflexivity, is conservative (therefore nonmonotonic) and supraintuitionistic, and is conducted in a way that lets us codify, within the logically extended object language, important features of the base thus extended. In other words, the logical operators in this calculus play what Brandom (2008) calls (...) expressive roles. Expressivist logical systems have already been proposed for propositional logics (see Hlobil, 2016, and Kaplan, 2018) but not for first-order logics. An advantage of this calculus over standard first-order calculi (e.g., those in Gentzen, 1935/1964) is that universally quantified variables behave as they should even in the presence of arbitrary nonlogical axioms. I claim that because of this robust well-behavedness of variables, this calculus also provides logical inferentialists with a way to understand the meanings of variables in terms of the roles those variables play in a wide range of inferences that is not limited to purely logical ones (e.g, mathematical inferences). (shrink)

We consider second-order propositional modal logic (SOPML), an extension of the basic modal language with propositional quantifiers introduced by Kit Fine in 1970. We determine the precise expressive power of SOPML by giving analogues of the Van Benthem–Rosen theorem and the Goldblatt Thomason theorem. Furthermore, we show that the basic modal language is the bisimulation invariant fragment of SOPML, and we characterize the bounded fragment of first-order logic as being the intersection of first-order (...) logic and SOPML. (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)

A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (...) (if the rule is included as primitive; or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules. (shrink)

In this dissertation, we construct a consistent, complete quotational logic G$\sb1$. We first develop a semantics, and then show the undecidability of circular quotation and anaphorism . Next, a complete axiom system is presented, and completeness theorems are shown for G$\sb1$. We show that definable truth exists in G$\sb1$. ;Later, we replace equality in G$\sb1$ with an equivalence relation. An axiom system and completeness theorems are provided for this equality-free version of G$\sb1$, which is useful in program verification. (...) ;Interpolation and definability are discussed in intensional and extensional contexts. We show that G$\sb1$ contains the complete first order theory of arithmetic by implicit definitional extension. ;The last chapter deals with representability and fixed points. Derived induction schemata are produced, and G$\sb1$ is shown to be a recursion theory. We give an example of how G$\sb1$ may be used to solve domain equations of Scott. (shrink)