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)

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.”. (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 propose a formalization of a realist ontology using first order logic with identity and allowing quantification over terms representing both individuals and universals. In addition to identity, the ontology includes also relational predicates such as subtype, instantiation, parthood, location, and inherence. Inspired in part by Davidson’s treatment of events, the ontology includes also various relations linking events to their participants and to the times at which they occur.

J. D. Monk has shown that for first order languages with finitely many variables there is no finite set of schema which axiomatizes the universally valid formulas. There are such finite sets of schema which axiomatize the formulas valid in all structures of some fixed finite size.

We introduce a typed version of the intuitionistic epsilon calculus. We give a categorical semantics of it introducing a class of categories which we call \-categories. We compare our results with earlier ones of Bell :323–337, 1993).

From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as presentations of Boolean algebras, and the collections of models can be topologized in such a way that the theory can be recovered from its space of models. The situation can be cast as a formal duality relating two categories of syntax and semantics, mediated by homming into a common dualizing object, in (...) this case 2.In the present work, we generalize the entire arrangement from propositional to first-order logic, using a representation result of Butz and Moerdijk. Boolean algebras are replaced by Boolean categories presented by theories in first-order logic, and spaces of models are replaced by topological groupoids of models and their isomorphisms. A duality between the resulting categories of syntax and semantics, expressed primarily in the form of a contravariant adjunction, is established by homming into a common dualizing object, now Sets, regarded once as a boolean category, and once as a groupoid equipped with an intrinsic topology.The overall framework of our investigation is provided by topos theory. Direct proofs of the main results are given, but the specialist will recognize toposophical ideas in the background. Indeed, the duality between syntax and semantics is really a manifestation of that between algebra and geometry in the two directions of the geometric morphisms that lurk behind our formal theory. Along the way, we give an elementary proof of Butz and Moerdijkʼs result in logical terms. (shrink)

This paper contains an axiomatic theory of first order modal logic with operations, identity, and descriptions together with a formal semantics which interprets the theory in such a manner that empty universes of discourse and denotationless terms are allowed for at each possible world. The intuitive basis of the theory is discussed in preliminary sections, the syntax and semantics of theory are then characterized, its semantical adequacy is demonstrated, and certain important axioms and theorems (...) are discussed in detail in later sections. (shrink)

The aim of this paper is to give a new proof for the decidability and finite model property of first-order logic with two variables (without function symbols), using a combinatorial theorem due to Herwig. The results are proved in the framework of polyadic equality set algebras of dimension two (Pse 2 ). The new proof also shows the known results that the universal theory of Pse 2 is decidable and that every finite Pse 2 can (...) be represented on a finite base. Since the class Cs 2 of cylindric set algebras of dimension 2 forms a reduct of Pse 2 , these results extend to Cs 2 as well. (shrink)

The aim of this paper is to give a new proof for the decidability and finite model property of first-order logic with two variables, using a combinatorial theorem due to Herwig. The results are proved in the framework of polyadic equality set algebras of dimension two. The new proof also shows the known results that the universal theory of Pse$_2$ is decidable and that every finite Pse$_2$ can be represented on a finite base. Since the (...) class Cs$_2$ of cylindric set algebras of dimension 2 forms a reduct of Pse$_2$, these results extend to Cs$_2$ as well. (shrink)

In theTractatus, Wittgenstein advocates two major notational innovations in logic. First, identity is to be expressed by identity of the sign only, not by a sign for identity. Secondly, only one logical operator, called “N” by Wittgenstein, should be employed in the construction of compound formulas. We show that, despite claims to the contrary in the literature, both of these proposals can be realized, severally and jointly, in expressively complete systems of first-order logic. Building on (...) early work of Hintikka’s, we identify three ways in which the first notational convention can be implemented, show that two of these are compatible with the text of theTractatus, and argue on systematic and historical grounds, adducing posthumous work of Ramsey’s, for one of these as Wittgenstein’s envisaged method. With respect to the second Tractarian proposal, we discuss how Wittgenstein distinguished between general and non-general propositions and argue that, claims to the contrary notwithstanding, an expressively adequate N-operator notation is implicit in theTractatuswhen taken in its intellectual environment. We finally introduce a variety of sound and complete tableau calculi for first-order logics formulated in a Wittgensteinian notation. The first of these is based on the contemporary notion of logical truth as truth in all structures. The others take into account the Tractarian notion of logical truth as truth in all structures over one fixed universe of objects. Here the appropriate tableau rules depend on whether this universe is infinite or finite in size, and in the latter case on its exact finite cardinality.As it is obviously easy to express how propositions can be constructed by means of this operation and how propositions are not to be constructed by means of it, this must be capable of exact expression.5.503. (shrink)

"In his introduction to this most welcome republication (and second edition) of his logic text, Heil clarifies his aim in writing and revising this book: 'I believe that anyone unfamiliar with the subject who set out to learn formal logic could do so relying solely on [this] book. That, in any case, is what I set out to create in writing An Introduction to First-Order Logic.' Heil has certainly accomplished this with perhaps the (...) most explanatorily thorough and pedagogically rich text I've personally come across. "Heil's text stands out as being remarkably careful in its presentation and illuminating in its explanations--especially given its relatively short length when compared to the average logic textbook. It hits all of the necessary material that must be covered in an introductory deductive logic course, and then some. It also takes occasional excursions into side topics, successfully whetting the reader's appetite for more advanced studies in logic. "The book is clearly written by an expert who has put in the effort for his readers, bothering at every step to see the point and then explain it clearly to his readers. Heil has found some very clever, original ways to introduce, motivate, and otherwise teach this material. The author's own special expertise and perspective--especially when it comes to tying philosophy of mind, linguistics, and philosophy of language into the lessons of logic--make for a creative and fresh take on basic logic. With its unique presentation and illuminating explanations, this book comes about as close as a text can come to imitating the learning environment of an actual classroom. Indeed, working through its presentations carefully, the reader feels as though he or she has just attended an illuminating lecture on the relevant topics!" --Jonah Schupbach, University of Utah. (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)

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)

The paper focuses on extending to the first order case the semantical program for modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer in the first part of the paper a series of new completeness results for salient classical systems of first order modal logic. Among other results we show that it is possible to prove strong completeness results (...) for normal systems without the Barcan Formula (like FOL + K)in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. Models of this type are either difficult of impossible to build in terms of relational Kripkean semantics [40].We conclude by introducing general first order neighborhood frames with constant domains and we offer a general completeness result for the entire family of classical first order modal systems in terms of them, circumventing some well-known problems of propositional and first order neighborhood semantics (mainly the fact that many classical modal logics are incomplete with respect to an unmodified version of either neighborhood or relational frames). We argue that the semantical program that thus arises offers the first complete semantic unification of the family of classical first order modal logics. (shrink)

Provided here is an account, both syntactic and semantic, of first-order and monadic second-order quantification theory for domains that may be non-atomic. Although the rules of inference largely parallel those of classical logic, there are important differences in connection with the identification of argument places and the significance of the identity relation.

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)

The 3-valued paraconsistent logic Ciore was developed by Carnielli, Marcos and de Amo under the name LFI2, in the study of inconsistent databases from the point of view of logics of formal inconsistency (LFIs). They also considered a first-order version of Ciore called LFI2*. The logic Ciore enjoys extreme features concerning propagation and retropropagation of the consistency operator: a formula is consistent if and only if some of its subformulas is consistent. In addition, Ciore is algebraizable (...) in the sense of Blok and Pigozzi. On the other hand, the logic LFI2* satisfies a somewhat counter-intuitive property: the universal and the existential quantifier are inter-definable by means of the paraconsistent negation, as it happens in classical first-order logic with respect to the classical negation. This feature seems to be unnatural, given that both quantifiers have the classical meaning in LFI2*, and that this logic does not satisfy the De Morgan laws with respect to its paraconsistent negation. The first goal of the present article is to introduce a first-order version of Ciore (which we call QCiore) preserving the spirit of Ciore, that is, without introducing unexpected relationships between the quantifiers. The second goal of the article is to adapt to QCiore the partial structures semantics for the first-order paraconsistent logic LPT1 introduced by Coniglio and Silvestrini, which generalizes the semantic notion of quasi-truth considered by Mikeberg, da Costa and Chuaqui. Finally, some important results of classical Model Theory are obtained for this logic, such as Robinson’s joint consistency theorem, amalgamation and interpolation. Although we focus on QCiore, this framework can be adapted to other 3-valued first-order LFIs. (shrink)

The paper focuses on extending to the first order case the semantical program for modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer in the first part of the paper a series of new completeness results for salient classical systems of first order modal logic. Among other results we show that it is possible to prove strong completeness results (...) for normal systems without the Barcan Formula (like FOL + K)in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. Models of this type are either difficult of impossible to build in terms of relational Kripkean semantics [40].We conclude by introducing general first order neighborhood frames with constant domains and we offer a general completeness result for the entire family of classical first order modal systems in terms of them, circumventing some well-known problems of propositional and first order neighborhood semantics (mainly the fact that many classical modal logics are incomplete with respect to an unmodified version of either neighborhood or relational frames). We argue that the semantical program that thus arises offers the first complete semantic unification of the family of classical first order modal logics. (shrink)

DEALING INITIALLY WITH QC, THE STANDARD QUANTIFICATIONAL CALCULUS OF ORDER ONE, THE AUTHOR COMMENTS ON A SHORTCOMING, REPORTED IN 1956 BY MONTAGUE AND HENKIN, IN CHURCH'S ACCOUNT OF A PROOF FROM HYPOTHESES, AND SKETCHES THREE WAYS OF RIGHTING THINGS. THE THIRD, WHICH EXPLOITS A TRICK OF FITCH'S, IS THE SIMPLEST OF THE THREE. THE AUTHOR INVESTIGATES IT SOME, SUPPLYING FRESH PROOF OF UGT, THE UNIVERSAL GENERALIZATION THEOREM. THE PROOF HOLDS GOOD AS ONE PASSES FROM QC TO QC (...) asterisk , THE PRESUPPOSITION-FREE VARIANT OF QC. TURNING NEXT TO QC subscript = , THE STANDARD QUANTIFICATIONAL CALCULUS OF ORDER ONE WITH '=', AND TO THE PRESUPPOSITION-FREE VARIANT QC subscript = OF QC subscript = , THE AUTHOR NEXT ESTABLISHES THE LEMMAS NEEDED THERE TO PROVE UGT. THAT, GIVEN FITCH'S ACCOUNT OF A PROOF FROM HYPOTHESES, UGT HOLDS FOR QC subscript = WAS ARGUED IN LEBLANC'S "TRUTH-VALUE SEMANTICS", BUT THE PROOF WAS IN ERROR. (shrink)

We refine the constructions of Ferrante-Rackoff and Solovay on iterated definitions in first-order logic and their expressibility with polynomial size formulas. These constructions introduce additional quantifiers; however, we show that these extra quantifiers range over only finite sets and can be eliminated. We prove optimal upper and lower bounds on the quantifier complexity of polynomial size formulas obtained from the iterated definitions. In the quantifier-free case and in the case of purely existential or universal quantifiers, (...) we show that Ω quantifiers are necessary and sufficient. The last lower bounds are obtained with the aid of the Yao-Håstad switching lemma. (shrink)

I consider the well-known criticism of Quine's characterization of first-order logical truth that it expands the class of logical truths beyond what is sanctioned by the model-theoretic account. Briefly, I argue that at best the criticism is shallow and can be answered with slight alterations in Quine's account. At worse the criticism is defective because, in part, it is based on a misrepresentation of Quine. This serves not only to clarify Quine's position, but also to crystallize what (...) is and what is not at issue in choosing the model-theoretic account of first-order logical truth over one in terms of substitutions. I conclude by highlighting the need for justifying the belief that the definition of first-order logical truth in terms of models is superior to its definition in terms of substitutions. (shrink)

We introduce a new typed combinatory calculus with a type constructor that, to each type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}, associates the star type σ∗\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma ^*$$\end{document} of the nonempty finite subsets of elements of type σ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\sigma $$\end{document}. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this (...) star combinatory calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements. (shrink)

For first order languages with no individual constants, empty structures and truth values (for sentences) in them are defined. The first order theories of the empty structures and of all structures (the empty ones included) are axiomatized with modus ponens as the only rule of inference. Compactness is proved and decidability is discussed. Furthermore, some well known theorems of model theory are reconsidered under this new situation. Finally, a word is said on other approaches (...) to the whole problem. (shrink)

The paper focuses on extending to the first order case the semantical program for modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer in the first part of the paper a series of new completeness results for salient classical systems of first order modal logic. Among other results we show that it is possible to prove strong completeness results (...) for normal systems without the Barcan Formula (like FOL + K)in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. Models of this type are either difficult of impossible to build in terms of relational Kripkean semantics [40].We conclude by introducing general first order neighborhood frames with constant domains and we offer a general completeness result for the entire family of classical first order modal systems in terms of them, circumventing some well-known problems of propositional and first order neighborhood semantics (mainly the fact that many classical modal logics are incomplete with respect to an unmodified version of either neighborhood or relational frames). We argue that the semantical program that thus arises offers the first complete semantic unification of the family of classical first order modal logics. (shrink)

Intuitionistic epistemic logic by Artemov and Protopopescu (Rev Symb Log 9:266–298, 2016) accepts the axiom “if A, then A is known” (written $$A \supset K A$$ ) in terms of the Brouwer–Heyting–Kolmogorov interpretation. There are two variants of intuitionistic epistemic logic: one with the axiom “ $$KA \supset \lnot \lnot A$$ ” and one without it. The former is called $$\textbf{IEL}$$, and the latter is called $$\textbf{IEL}^{-}$$. The aim of this paper is to study first- (...) class='Hi'>order expansions (with equality and function symbols) of these two intuitionistic epistemic logics. We define Hilbert systems with additional axioms called geometric axioms and sequent calculi with the corresponding rules to geometric axioms and prove that they are sound and complete for the intended semantics. We also prove the cut-elimination theorems for both sequent calculi. As a consequence, the disjunction property and existence property are established for the sequent calculi without geometric implications. Finally, we establish that our sequent calculi can also be formulated with admissible structural rules (i.e., in terms of a G3-style sequent calculus). (shrink)

There are properties of finite structures that are expressible with the use of Hilbert's ε-operator in a manner that does not depend on the actual interpretation for ε-terms, but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly (...) enhance the expressive power of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu. (shrink)

After observing that the truth conditions of connectives of non–classical logics are generally defined in terms of formulas of first–order logic, we introduce ‘protologics’, a class of logics whose connectives are defined by arbitrary first–order formulas. Then, we introduce atomic and molecular logics, which are two subclasses of protologics that generalize our gaggle logics and which behave particularly well from a theoretical point of view. We also study and introduce a notion of equi-expressivity between (...) two logics based on different classes of models. We prove that, according to that notion, every pure predicate logic with \ variables and constants is as expressive as a predicate atomic logic, some sort of atomic logic. Then, we prove that the class of protologics is equally expressive as the class of molecular logics. That formally supports our claim that atomic and molecular logics are somehow ‘universal’. Finally, we identify a subclass of molecular logics that we call predicate molecular logics and which constitutes its representative core: every molecular logic is as expressive as a predicate molecular logic. (shrink)

We consider the decision problem for cases of first-order temporal logic with function symbols and without equality. The monadic monodic fragment with flexible functions can be decided with EXPSPACE-complete complexity. A single rigid function is sufficient to make the logic not recursively enumerable. However, the monadic monodic fragment with rigid functions, where no two distinct terms have variables bound by the same quantifier, is decidable and EXPSPACE-complete.

Features are unary operators used to build record-like expressions. The resulting term algebras are encountered in linguistic computation and knowledge representation. We present a general description of feature logic and of a slightly restricted version, called record logic. It is shown that every first-order theory can be faithfully interpreted in a record logic with various additional axioms. This fact is used elsewhere [15] to extend a result of Tarski and Givant [14] on expressing (...) class='Hi'>first order theories in relation algebra. (shrink)

Features are unary operators used to build record-like expressions. The resulting term algebras are encountered in linguistic computation and knowledge representation. We present a general description of feature logic and of a slightly restricted version, called record logic. It is shown that every first-order theory can be faithfully interpreted in a record logic with various additional axioms. This fact is used elsewhere [15] to extend a result of Tarski and Givant [14] on expressing (...) class='Hi'>first order theories in relation algebra. (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)

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)

An interpolation Theorem is proved for first order logic with infinitary predicates. Our proof is algebraic via cylindric algebras.1.

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)

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)

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and (...) DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle. (shrink)

In this paper we prove that $\forall \textrm{FO}$, the universal fragment of first-order logic, is superfluous in $\varSigma _2^p$ and $\varPi _2^p$. As an example, we show that this yields a syntactic proof of the $\varSigma _2^p$-completeness of value-cost satisfiability. The superfluity method is interesting since it gives a way to prove completeness of problems involving numerical data such as lengths, weights and costs and it also adds to the programme started by Immerman and Medina about (...) the syntactic approach in the study of completeness. (shrink)

The typical rules for truth-trees for first-order logic without functions can fail to generate finite branches for formulas that have finite models–the rule set fails to have the finite tree property. In 1984 Boolos showed that a new rule set proposed by Burgess does have this property. In this paper we address a similar problem with the typical rule set for first-order logic with identity and functions, proposing a new rule set that (...) does have the finite tree property. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:First Order Relationality and Its Implications:A Response to David ElsteinRoger T. Ames (bio)David Elstein has asked a series of important questions about Human Becomings that provide me with an opportunity to try to bring the argument of the book into clearer focus. Let me begin by thanking David for his always generous and intelligent reflection on not only my new monograph [End Page 181] but also (...) on Henry Rosemont's and my best efforts to expand upon the idea of "role ethics" as a productive way to read Confucian ethics.David asks: Is relationality truly a part of original Confucian thought? Does relationality rule out any notion of essential human nature, and does it necessarily imply or entail role ethics? Is relationality true or merely a useful way of thinking (if these can be distinguished)? Do we know that it's useful?I think the answer to these questions turns on two very different ways of understanding relationality, namely the doctrines of first and second order relationality. The term 'ontology' as "the science of being per se or in itself" gives us a doctrine of external, second order relations. Ontology was introduced into our philosophical vocabulary as a new term for an old way of thinking at the beginning of the seventeenth century by two German philosophers.1 For the classical Greeks, "the science of being per se" (to on he on) was posited as their "first philosophy" with all of its implications for metaphysics, epistemology, logic, ethics, philosophy of religion, and so on. Ontology is that branch of metaphysics that seeks to classify and explain the things that exist, with its underlying assumption that there are unchanging substances or essences internal to things that are available to us to classify them as this and not that. Ontology privileges "being per se" with its categorical language and its "substance" and "attribute" dualism, giving us a grammar of substances as property-bearers and properties that are borne, respectively.Such ontological thinking animates Plato's pursuit of formal, "real" definitions in his quest for certainty (that is, definitions not of words but of what really is), and underlies Aristotle's taxonomical science of knowing "what is what." For these classical Greek philosophers, only what is real and is thus true can be the proper object of knowledge, giving us a logic of the changeless. Corollary to ontology is causal thinking, formal definitions, and, important for David's question, a doctrine of external, second order relationality in which relations conjoin discrete and self-sufficient things, such as human "beings." As the contemporary philosopher Zhao Tingyang 趙汀陽 avers, this kind of substance ontology defining the real things that constitute the content of an orderly and structured cosmosprovides a "dictionary" kind of explanation of the world, seeking to set up an accurate understanding of the limits of all things. In simple terms, it determines "what is what," and all concepts are footnotes to "being" or "is."2In the Book of Changes, we find a vocabulary making explicit cosmological assumptions that stand in stark contrast to this substance ontology and that brings with it a doctrine of first order, constitutive relations. This alternative "first philosophy" has prompted me to create the neologism "zoetology," with the Greek zoe- "life" and -logia "discourse," as my own new term for an old way of thinking that we might translate into modern Chinese as shengshenglun 生生論: "the art of living." The starting point in this zoetological cosmology, then, is that nothing does anything by [End Page 182] itself; association is a fact. Since the very nature of life is associative and transactional, the vocabulary appealed to in defining Confucian cosmology is irreducibly dyadic and collateral: always multiple, never one.And further, it is the nature of life itself that it seeks to optimize the available conditions for its continuing growth, where such growth has a persistent existential and thus intentional aspect. "Life" is the productive correlation between organism and environment that gives rise to correlative, relational, ecological thinking that many of our best sinologists (Marcel Granet, David Keightley, Tang Junyi, K. C. Chang, A. C. Graham, and many others) would ascribe to the earliest semblances of Chinese... (shrink)

Girard introduced phase semantics as a complete set-theoretic semantics of linear logic, and Okada modified phase-semantic completeness proofs to obtain normal-form theorems. On the basis of these works, Okada and Takemura reformulated Girard’s phase semantics so that it became phase semantics for proof-terms, i.e., lambda-terms. They formulated phase semantics for proof-terms of Laird’s dual affine/intuitionistic lambda-calculus and proved the normal-form theorem for Laird’s calculus via a completeness theorem. Their semantics was obtained by an application of computability (...) predicates. In this paper, we first formulate phase semantics for proof-terms of second-order intuitionistic propositional logic by modifying Tait-Girard’s saturated sets method. Next, we prove the completeness theorem with respect to this semantics, which implies a strong normalization theorem. (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)

In order to introduce the text description of this class will show seven keywords, they represent In order to understand the general process for the seven. Need to mention is that the author published in Chinese script - title "Gadamer's philosophy of the seven key" - and this content is not the same. In fact, only one in that the use of key words in this speech mentioned the four key words will be used the next article. 1 (...) Linguistics as high as the United States in the "real management and methods," a book in the last third of the contents of the specified language is "the universal medium of interpretation of experience." It is in this medium, things are understood, understanding and interpretation to occur. It is the fundamental and the first thing on a switch, it makes things possible, without it, understanding must not occur. It is in this medium, the real management there, although in terms of the real incidence of management and is not limited to this medium. Sprachlichkeit is up to the universal language of the United States to name the first of of a proper noun. history of as language, history is a popular media, and history is also rising to become "a hermeneutical principle." To understand history, which must be traced back to Heidegger, "and there is time," the first six parts, entitled "Timing and historical nature." This title has been out of correct revelation, history is the study of this structure there is some a result of this there is the same as in the past and the present one there, it was possible there through his plans and will itself which extend to the future. Dilthey on Heidegger benefit of this term and its historical significance, but that裡Dilthey, the basic processes of life, and in Heidegger, the basic process is still alive there in the past and future Among the visual field. It is a learning process rather than the life there is a process, there is a process rather than the life philosophy of life regardless of the process. Dilthey and Gadamer and Heidegger places of historical analysis for the premise. 3 by the historical role of awareness up to the United States, this keyword has not appeared in from Schleiermacher, Dilthey, or Heidegger that裡. But Heidegger once spoke to the author, the concept represented by the word directly from Dilthey and future. Indeed, the word and the "fusion of" two persons都benefit from Hegel and Dilthey, Heidegger than In order to impact. At the same time, for the resumption of encounter with the text of the history of this effort directly, the recall In order to Heidegger and Qike fruit. Up to the United States shows that it is essential that "the existence of the structure." That is to say, it is usually associated with the text coming from a tradition, crushed In order to present before the sight. 4 hermeneutics into the cycle and see in understanding the structure and the first cycle between hermeneutics, there is a close link. Hermeneutics and the cycle regardless of such a concept, not only from a part of the overall future understanding, understanding from the part of the overall future. This is a logical contradiction, but it depicts In order to understand the kind of work does not have the way to recovery. This is to see What are the relationship? Up with the United States use this word in the former understanding of the meaning of a person he can understand any part of the text and context before, must have a pre-understanding. When Schleiermacher hermeneutics for the cycle to take a more formalistic point of view, he also participate in an objective and subjective look for. In order to reject the United States is up for the subjective, and he describes, in understanding the text, our understanding of a person but a different meaning, and this sense of ownership in a situation with a theme of the event . Heidegger the hermeneutic circle and put the world on their own understanding of the context in which the world is time and the existence of the world, in order to In order to reinvent the meaning of hermeneutic circle. It exists in the time being and is expected to forward to the future, it is a person exists in the world of all possibilities of a personal meaning. Gadamer Heidegger and then one more step beyond, he is defined as the cycle of hermeneutics and the interpretation of the traditional sports were a correlation between the movement. Heidegger's masterpiece裡tradition and not important, but those for the traditional and the interpretation of the relationship between text, up to the U.S. In order to play an important role in the analysis. Up to the United States, brought into the discussion In order to "complete expectation" that the key concept, it is subject to the historical role of awareness of the operation of the core. In this part of the contents of the directory for the present review is to show to some of the major associated. 5 authority and tradition up to the United States on the authority of the traditional view is that from his understanding and the hermeneutic circle before the concept developed in the future. Enlightenment for the suspect an effort made ​​to switch the authority of the United States to see coming up is one-sided, because the authority is naturally found in the leading field in a PhD, the referee, professors and experts. Recognize these people for a topic you know even in the natural and appropriate. So regardless of up to his brother's wife is not a legitimate authority and legitimate authority, and authority as a concept to see the future is appropriate. Similarly, our traditional understanding among the living, and we should explore a more deeper with our traditional relationship. Traditional German text is Űberlieferung, incurs passed along . Once again, as a fair decision without dialogue and is not legal to see, up to the United States against this anti-traditional views of the Enlightenment. 6 Depending on the domain of integration sight philosophy of integration is another sign up to the United States is not to find elsewhere. Basically, the text of the encounter with a sight In order to involve the integration of text and interpreter of the visual field of sight. And a man's own awareness is a fusion of traditional with the product. "That is convenient to get a sight of their own, but also requires a fusion of traditional with." In order for each dialogue also involves a fusion of sight. It is a wildcard description of the terminology. 7 Dialogue dialogue leading up to the U.S. interpretation of the theme of philosophy, relying on a life of his ideal, he as such a show of openness. Schleiermacher as high as the United States in general, is a talented rapper. However, the need for a fruitful dialogue open to others point of view, and the need to recognize that he or she may be right. In a true dialogue, both sides都want to talk more close to the truth regardless of management topics, which are more important than winning. Finally, the dialogue is a basic hermeneutical tool, a means to understand, so we coming close to the theme of the issue, but ready to change our point of view. An introductory section explains that the lecture will present seven key terms, representing seven aspects of the universal process of understanding. It is noted that a published lecture in Chinese by this author under the title "Seven Key Terms in the Philosophy of Hans-Georg Gadamer "is not the same as this, and indeed only one of the terms in that lecture is used in this one, although four of them are used in tomorrow's lecture. An introductory section explains that the lecture will present seven key terms, representing seven aspects of the universal process of understanding. It is noted that a published lecture in Chinese by this author under the title "Seven Key Terms in the Philosophy of Hans-Georg Gadamer" is not the same as this, and indeed only one of the terms in that lecture is used in this one, although four of them are used in tomorrow's lecture. 1. Sprachlichkeit-Linguisticality As Gadamer notes in the final third of Truth and Method, language is the "universal medium of hermeneutical experience." It is the medium in which things are understood, the medium in which understanding and interpretation take place. It is fundamental and prior to everything. It makes things possible, and without it understanding cannot take place at all. It is the medium in which truth happens, although there is more than this to the happening of truth. Sprachlichkeit is the term Gadamer uses to name the "universal priority" of language. 2. Geschichtlichkeit-Historicity Like language, history is a universal medium, and historicity is raised to the status of "a hermeneutical principle. "To understand historicity, one has to go back to the six sections of Heidegger's Being and Time that carry the heading" Temporality and Historicity. "Already this title correctly suggests that historicity is a consequence of the ontological structure of Dasein as a being that lives with a past and a present, and also extends itself into the future through projecting possible being. Heidegger is indebted to Dilthey for the term and sense of historicity, but in Dilthey the basic process is life, whereas in Heidegger, the basic process is being-in-the-world in horizons of past and future. It is an ontological process rather than a life process, a process of being rather than the vitalism of life in life-philosophy. Gadamer presupposes Dilthey's and Heidegger's analysis of Geschichtlichkeit . 3. das wirkungsgeschichtliche Bewusstsein-the Historically Effected Consciousness This is a key term in Gadamer that does not appear in Schleiermacher, Dilthey, or Heidegger. Heidegger once remarked to the author that the idea that this term represents is straight out of Dilthey. Certainly it and the "fusion of horizons" are more indebted to Hegel and Dilthey than to Heidegger. At the same time, the effort to restore the historical immediacy of encounter with a text recalls Heidegger and Kierkegaard. Gadamer argues that the essence of it is " the structure of experience. "That is to say, it shatters the present horizon, usually with a text from tradition. 4. Hermeneutische Zirkel and Vorurteil-Prejudice and the Hermeneutical Circle There is an intimate connection between the fore-structure of understanding and the hermeneutical circle. The hermeneutical circle refers to the idea that one understands the part from the whole, but also the whole from the parts. This is a logical contradiction, but it describes the back and forth way that understanding works. What has this to do with prejudices ? Gadamer uses this word as synonymous with pre-understanding, and one has to have a prior understanding before one can understand any part of a text or situation. While Schleiermacher took a more formalistic view of the hermeneutical circle, he also looked at the objective and subjective sides. Gadamer rejects the subjective side and explains that in understanding a text we are not understanding a person but a meaning that resides in a situation and a subject-matter. Heidegger revolutionized the meaning of the hermeneutical circle by placing it in the context of an understanding of self and world that is temporal and existential. It exists in time and anticipates a future, and it is the personal sense of one's possibilities for being in the world. Gadamer took a step beyond Heidegger by defining the hermeneutical circle as the interplay between the movement of tradition and that of the interpreter. Tradition plays little role in Heidegger's masterwork, but it and the interpreter's relation to the text loom large in Gadamer's analysis. The discussion brings in the key concept in Gadamer of the "anticipation of completion" which is central to the working of historically effected consciousness. A review of the table of contents for the section is presented to show some of the major relationships. 5. Autorität und Tradition-Authority and Tradition Gadamer's views with regard to authority and tradition grow out of his concepts of preunderstanding and the hermeneutical circle. The effort by the Enlightenment to discredit all authority seemed one-sided to Gadamer because authority is naturally accorded to doctors, judges, professors, and other experts in a field. To acknowledge that they know more about a subject than you do is natural and appropriate. So Gadamer speaks of legitimate authority and illegitimate authority, but authority as a concept seems appropriate. Likewise, tradition inhabits our understanding, and we should seek an ever deeper relationship to our tradition. The German word for tradition is Űberlieferung, that which is handed down. Again, Gadamer takes up arms against the Enlightenment prejudice against tradition as illegitimate without dialogue or a fair trial. 6. Horizontverschmelzung-Fusion of Horizons The "fusion of horizons "is another trademark of Gadamerian philosophy. It is not found elsewhere. Basically, the encounter with the text involves a fusion of horizons, that of the text and that of the interpreter. Also one's own consciousness is a product of a fusion of horizons with the tradition. "Even to acquire one's own horizon requires a fusion of horizons with the tradition." Every conversation, too, involves a fusion of horizons. It is an all-purpose term. 7. Conversation Conversation is a leitmotif of Gadamer's hermeneutical philosophy, an ideal he lived by, an openness he exemplified. Schleiermacher was a gifted conversationalist, as was Gadamer. But a fruitful conversation requires openness to the viewpoint of the other person, and the acknowledgement that he or she could be right. In a true conversation both partners want to come closer to the truth about a matter, and that is more important than winning. Ultimately, conversation is a basic hermeneutical tool, a means of reaching understanding, so we approach a subject with questions, but ready to change our point of view. (shrink)

The paper is inspired by and explicitly presupposes the readers’ knowledge of the Kürbis normalization procedure for the Milne tree-like natural deduction system _C_ for classical propositional logic. The novelty of _C_ is that for each conventional connective, it has only _general_ introduction and elimination rules, whose paradigm is the rule of proof by cases. The present paper deals with the Milne–Kürbis troublemaker—adding universal quantifier—caused by extending the normalization procedure to \(\mathbf {C^{\exists }_{\forall }} \), the (...) class='Hi'>first-order variant of _C_. For both quantifiers, \( \mathbf {C^{\exists }_{\forall }}\) has only general quantifier rules, whose paradigm is the indirect rule of existential elimination. We propose the classical first-order tree-like natural deduction system \( \mathbf {NC^{\exists }_{\forall }}\) such that it contains all the propositional and half the quantifier rules of \(\mathbf {C^{\exists }_{\forall }}\) and differs from it with respect to the other half of the quantifier rules and the notion of a deduction. We show that in the case of \(\mathbf {NC^{\exists }_{\forall }} \), whose specifics is based on the Quine treatment of _flagged_ variables in the linear-style natural deduction system as well as on the Aguilera-Baaz treatment of _characteristic_ and _side_ variables for sequent-style calculi, the troublemaker doesn’t occur. In order to handle another specifics of \(\mathbf {NC^{\exists }_{\forall }}\) —an auxiliary notion of a _finished_ deduction that makes deductions _nonhereditary_—we show soundness and completeness of \( \mathbf {NC^{\exists }_{\forall }} \). While emphasizing the former with the help of the Smirnov technique, we additionally indicate a fixable gap in the Quine soundness argument. At last, the philosophical significance of the main result of this paper is developed in more detail. (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)