μ-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.

Strong extension axioms and Shelah's zero-one law for choiceless polynomial time

2003 ◽  
Vol 68 (1) ◽  
pp. 65-131 ◽  
Author(s):  
Andreas Blass ◽  
Yuri Gurevich
Keyword(s):  
Fixed Point ◽  
Polynomial Time ◽  
Order Logic ◽  
Complexity Class ◽  
First Order Logic ◽  
Infinitary Logic ◽  
Extensive Discussion ◽  
First Order ◽  
Detailed Proof ◽  
Strong Extension

AbstractThis paper developed from Shelah's proof of a zero-one law for the complexity class “choiceless polynomial time,” defined by Shelah and the authors. We present a detailed proof of Shelah's result for graphs, and describe the extent of its generalizability to other sorts of structures. The extension axioms, which form the basis for earlier zero-one laws (for first-order logic, fixed-point logic, and finite-variable infinitary logic) are inadequate in the case of choiceless polynomial time; they must be replaced by what we call the strong extension axioms. We present an extensive discussion of these axioms and their role both in the zero-one law and in general.

The ground-negative fragment of first-order logic is -complete

1999 ◽  
Vol 64 (3) ◽  
pp. 984-990 ◽  
Author(s):  
Andrei Voronkov
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Natural Class ◽  
First Order

AbstractWe prove that for a natural class of first-order formulas the validity problem is -complete.

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?

Locally cartesian closed categories and type theory

1984 ◽  
Vol 95 (1) ◽  
pp. 33-48 ◽  
Author(s):  
R. A. G. Seely
Keyword(s):  
Type Theory ◽  
Free Variable ◽  
Order Logic ◽  
First Order Logic ◽  
Topos Theory ◽  
First Order ◽  
Cartesian Closed Categories ◽  
Cartesian Closed ◽  
Indexed Category

It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/A are cartesian closed. In such a category, the notion of a ‘generalized set’, for example an ‘A-indexed set’, is represented by a morphism B → A of C, i.e. by an object of C/A. The point about such a category C is that C is a C-indexed category, and more, is a hyper-doctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A, the predicates with a free variable of type A are morphisms into A, and ‘proofs’ are morphisms over A. We see here a certain ‘ambiguity’ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A, which is a predicate over A; a morphism 1 → A can be viewed either as an object of type A or as a proof of the proposition A.

Sign in / Sign up

Export Citation Format

Share Document