First-order logic based on inclusion and abstraction

1982 ◽  
Vol 47 (4) ◽  
pp. 793-808
Author(s):  
John Bacon
Keyword(s):  
Order Logic ◽  
Boolean Logic ◽  
First Order Logic ◽  
Order Restriction ◽  
First Order ◽  
Unit Classes ◽  
Definition Of ◽  
The Universe ◽  
Primitive Notion ◽  
Universe Of Discourse

Quine has shown that set theory may be based on inclusion and abstraction [1937], [1953]. He quantifies over (or abstracts upon) sets of all kinds, of course, including sets of sets. Here I confine Quine's approach to quantification over (abstraction upon) individuals alone, or at any rate their unit classes. Forsaking quantification over sets undercuts Quine's definition of negation, however. Smullyan sketches a first-order restriction of Quine's approach with no bound class variables for which inclusion and abstraction alone are adequate logical primitives [1957, n. 10]. However, the definition of negation requires more than one element in the universe of discourse. This requirement is met for Smullyan because he is doing arithmetic. Here, on the other hand, I presuppose only that the universe is nonempty. Accordingly, I assume a third primitive notion, the empty class. I will show that this threefold basis suffices both for classical first-order logic and for a version of “free” many-sorted logic. The monadic fragment, which I call Boolean logic with abstraction, is intermediate in strength between Boolean class logic and Lesniewski's Ontology. It affords a novel perspective on descriptions, particularly in their generic use.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

μ-definable sets of integers

1993 ◽  
Vol 58 (1) ◽  
pp. 291-313 ◽  
Author(s):  
Robert S. Lubarsky
Keyword(s):  
Fixed Point ◽  
Free Variable ◽  
Order Logic ◽  
First Order Logic ◽  
Inductive Definition ◽  
Natural Class ◽  
First Order ◽  
Inductive Definitions ◽  
Definable Sets ◽  
The Universe

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.

Church’s theorem and the decision problem

2018 ◽  
Author(s):  
Rohit Parikh
Keyword(s):  
Decision Problem ◽  
Combinatorial Problem ◽  
Order Logic ◽  
First Order Logic ◽  
Negative Solution ◽  
Great Contribution ◽  
Solvable Problem ◽  
First Order ◽  
Mathematical Definition ◽  
Definition Of

Church’s theorem, published in 1936, states that the set of valid formulas of first-order logic is not effectively decidable: there is no method or algorithm for deciding which formulas of first-order logic are valid. Church’s paper exhibited an undecidable combinatorial problem P and showed that P was representable in first-order logic. If first-order logic were decidable, P would also be decidable. Since P is undecidable, first-order logic must also be undecidable. Church’s theorem is a negative solution to the decision problem (Entscheidungsproblem), the problem of finding a method for deciding whether a given formula of first-order logic is valid, or satisfiable, or neither. The great contribution of Church (and, independently, Turing) was not merely to prove that there is no method but also to propose a mathematical definition of the notion of ‘effectively solvable problem’, that is, a problem solvable by means of a method or algorithm.

scholarly journals Semantics for Hyperclassical Logic and the Problem of Negation in the Formal Language

2018 ◽  
Vol 16 (3) ◽  
pp. 5-15
Author(s):  
V. V. Tselishchev
Keyword(s):  
Theoretical Model ◽  
Formal Language ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Order Language ◽  
Winning Strategies ◽  
Game Theoretic ◽  
Definition Of ◽  
Game Theoretic Semantics

The application of game-theoretic semantics for first-order logic is based on a certain kind of semantic assumptions, directly related to the asymmetry of the definition of truth and lies as the winning strategies of the Verifier (Abelard) and the Counterfeiter (Eloise). This asymmetry becomes apparent when applying GTS to IFL. The legitimacy of applying GTS when it is transferred to IFL is based on the adequacy of GTS for FOL. But this circumstance is not a reason to believe that one can hope for the same adequacy in the case of IFL. Then the question arises if GTS is a natural semantics for IFL. Apparently, the intuitive understanding of negation in natural language can be explicated in formal languages in various ways, and the result of an incomplete grasp of the concept in these languages can be considered a certain kind of anomalies, in view of the apparent simplicity of the explicated concept. Comparison of the theoretical-model and game theoretic semantics in application to two kinds of language – the first-order language and friendly-independent logic – allows to discover the causes of the anomaly and outline ways to overcome it.

The measure quantifier

1979 ◽  
Vol 44 (1) ◽  
pp. 103-108 ◽  
Author(s):  
Carl F. Morgenstern
Keyword(s):  
Measurable Cardinal ◽  
Order Logic ◽  
First Order Logic ◽  
Order Structure ◽  
Proper Class ◽  
First Order ◽  
Recursive Enumerability ◽  
Almost All ◽  
Measurable Cardinals ◽  
The Universe

Originally generalized quantifiers were introduced to specify that a given formula was true for “many x's” e.g. ⊨ Qxφ(x) iff card{x ∈ ∣∣ ∣ ⊨ φ[x]} ≥ ℵ0, ℵ1, or some fixed cardinal κ. In this paper we formalize the notion that φ{x) is true “for almost all x”. This is accomplished by referring to structures = (′, μ) where ′ is a first-order structure and μ is a measure of a suitable type on the universe of ′. We will prove that the language Lμ obtained from first-order logic by adjoining a quantifier Qμ, which ranges over the measure μ, is fully compact if we assume the existence of a proper class of measurable cardinals. As a corollary to the compactness theorem we obtain the recursive enumerability of the validities of Lμ. Finally, the Magidor-Malitz quantifiers Qkn (n ∈ ω) will be added to Lμ together with analogous quantifiers Qμm (m ∈ ω) to form Lκμ<ω,<ω, which is compact for sets of sentences of cardinality < κ, where κ is a measurable cardinal > ℵ0.An alternate approach to formalizing “for almost all” has been recently developed by Barwise, Kaufmann and Makkai [1] who follow a suggestion of Shelah [5].

Second- and higher-order logics

2018 ◽  
Author(s):  
Shaughan Lavine
Keyword(s):  
Predicate Logic ◽  
Higher Order ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Third Order ◽  
First Order ◽  
Proof Systems ◽  
The Universe ◽  
Second Order Logic

In first-order predicate logic there are symbols for fixed individuals, relations and functions on a given universe of individuals and there are variables ranging over the individuals, with associated quantifiers. Second-order logic adds variables ranging over relations and functions on the universe of individuals, and associated quantifiers, which are called second-order variables and quantifiers. Sometimes one also adds symbols for fixed higher-order relations and functions among and on the relations, functions and individuals of the original universe. One can add third-order variables ranging over relations and functions among and on the relations, functions and individuals on the universe, with associated quantifiers, and so on, to yield logics of even higher order. It is usual to use proof systems for higher-order logics (that is, logics beyond first-order) that include analogues of the first-order quantifier rules for all quantifiers. An extensional n-ary relation variable in effect ranges over arbitrary sets of n-tuples of members of the universe. (Functions are omitted here for simplicity: remarks about them parallel those for relations.) If the set of sets of n-tuples of members of a universe is fully determined once the universe itself is given, then the truth-values of sentences involving second-order quantifiers are determined in a structure like the ones used for first-order logic. However, if the notion of the set of all sets of n-tuples of members of a universe is specified in terms of some theory about sets or relations, then the universe of a structure must be supplemented by specifications of the domains of the various higher-order variables. No matter what theory one adopts, there are infinitely many choices for such domains compatible with the theory over any infinite universe. This casts doubt on the apparent clarity of the notion of ‘all n-ary relations on a domain’: since the notion cannot be defined categorically in terms of the domain using any theory whatsoever, how could it be well-determined?

Beth’s theorem and Craig’s theorem

2018 ◽  
Author(s):  
Zeno Swijtink
Keyword(s):  
Sufficient Conditions ◽  
Predicate Symbol ◽  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
Infinite Length ◽  
First Order ◽  
Explicit Definition ◽  
Central Result ◽  
Definition Of

Beth’s theorem is a central result about definability of non-logical symbols in classical first-order theories. It states that a symbol P is implicitly defined by a theory T if and only if an explicit definition of P in terms of some other expressions of the theory T can be deduced from the theory T. Intuitively, the symbol P is implicitly defined by T if, given the extension of these other symbols, T fixes the extension of the symbol P uniquely. In a precise statement of Beth’s theorem this will be replaced by a condition on the models of T. An explicit definition of a predicate symbol states necessary and sufficient conditions: for example, if P is a one-place predicate symbol, an explicit definition is a sentence of the form (x) (Px ≡φ(x)), where φ(x) is a formula with free variable x in which P does not occur. Thus, Beth’s theorem says something about the expressive power of first-order logic: there is a balance between the syntax (the deducibility of an explicit definition) and the semantics (across models of T the extension of P is uniquely determined by the extension of other symbols). Beth’s definability theorem follows immediately from Craig’s interpolation theorem. For first-order logic with identity, Craig’s theorem says that if φ is deducible from ψ, there is an interpolant θ, a sentence whose non-logical symbols are common to φ and ψ, such that θ is deducible from ψ, while φ is deducible from θ. Craig’s theorem and Beth’s theorem also hold for a number of non-classical logics, such as intuitionistic first-order logic and classical second-order logic, but fail for other logics, such as logics with expressions of infinite length.

scholarly journals A FORMALIZATION OF KANT’S TRANSCENDENTAL LOGIC

2011 ◽  
Vol 4 (2) ◽  
pp. 254-289 ◽  
Author(s):  
T. ACHOURIOTI ◽  
M. VAN LAMBALGEN
Keyword(s):  
Formal Proof ◽  
Order Logic ◽  
First Order Logic ◽  
Pure Reason ◽  
Critique Of Pure Reason ◽  
Technical Application ◽  
First Order ◽  
Transcendental Logic ◽  
Definition Of ◽  
Argumentative Structure

Although Kant (1998) envisaged a prominent role for logic in the argumentative structure of his Critique of Pure Reason, logicians and philosophers have generally judged Kant’s logic negatively. What Kant called ‘general’ or ‘formal’ logic has been dismissed as a fairly arbitrary subsystem of first-order logic, and what he called ‘transcendental logic’ is considered to be not a logic at all: no syntax, no semantics, no definition of validity. Against this, we argue that Kant’s ‘transcendental logic’ is a logic in the strict formal sense, albeit with a semantics and a definition of validity that are vastly more complex than that of first-order logic. The main technical application of the formalism developed here is a formal proof that Kant’s Table of Judgements in Section 9 of the Critique of Pure Reason, is indeed, as Kant claimed, complete for the kind of semantics he had in mind. This result implies that Kant’s ‘general’ logic is after all a distinguished subsystem of first-order logic, namely what is known as geometric logic.

Sign in / Sign up

Export Citation Format

Share Document