On deciding the provability of certain fixed point statements

1977 ◽  
Vol 42 (2) ◽  
pp. 191-193
Author(s):  
George Boolos
Keyword(s):  
Fixed Point ◽  
Fixed Points ◽  
Decision Procedure ◽  
Free Variable ◽  
Peano Arithmetic ◽  
First Order ◽  
Order Arithmetic ◽  
Functional Combination

Terminology. PA is Peano Arithmetic, classical first-order arithmetic with induction. ⌈A⌉ is the formal numeral in PA for the Gödel number of A. – A is the negation of A, (A&B) is the conjunction of A and B, and Bew(x) is the usual provability predicate for PA. neg(x), conj(x, y), bicond(x, y), and bew(x) are terms of PA such that for all sentences A and B of PA ⊢PA, neg(˹A˺) = ˹−A˺ ⊢PA Conj(˹A˺, ˹B˺)= ˹(A&B)˺ ⊢PA bicond(˹A˺, ˹B˺)= ˹(A ↔ B)˺, and ⊢PA bew(˹A˺) = ˹Bew(˹A˺)˺. T is the sentence ‘0 = 0’ and Con is the usual sentence expressing the consistency of PA. If A (x) is any formula of PA, then a fixed point of A(x) is a sentence S such that ⊢PAS ↔ A(˹S˺). (It is well known that every formula of PA with one free variable has a fixed point.) The P-terms are defined inductively by: the variable x is a P-term; if t(x) and u(x) are P-terms, so are neg(t(x)), conj(t(x), u(x)), and bew(t(x)). A basic P-formula is a formula Bew(t(x)), where t(x) is a P-term; and a P-formula is a truth-functional combination of basic P-formulas. An F-sentence is a member of the smallest class that contains Con and contains −A, (A&B), and −Bew(˹−A˺) whenever it contains A and B. In [B] we gave a decision procedure for the class of true F-sentences.−Bew(x), Bew(x), and Bew(neg(x)) are examples of P-formulas, and fixed points of these particular P-formulas have been studied by Gödel, Henkin [H] and Löb [L], and Jeroslow [J], respectively. In this note we show how to decide whether or not a fixed point of any given P-formula is provable in PA.

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

On deciding the truth of certain statements involving the notion of consistency

1976 ◽  
Vol 41 (4) ◽  
pp. 779-781 ◽  
Author(s):  
George Boolos
Keyword(s):  
Free Variable ◽  
Incompleteness Theorem ◽  
First Order ◽  
Order Arithmetic ◽  
Image Position

Friedman has posed (see [F, p. 117]) the following problem: “35. Define the set E of expressions by (i) Con is an expression; (ii) if A, B are expressions so are (~ A), (A&B), and Con(A). Each expression ϕ in E determines a sentence ϕ in PA [classical first-order arithmetic] by taking Con* to be “PA is consistent,” ( ~ A) * to be ~ (A*), (A&B)* to be A*&B*, and Con(A)* to be “PA + ‘A*’ is consistent.” The set of expressions ϕ ∈ E such that ϕ* is true is recursive.The formalized second incompleteness theorem readsIn order to simplify notation, we will reformulate Friedman's problem slightly. Let Con be the usual sentence of PA expressing the consistency of PA, ~ A the negation of A, (A&B) the conjunction of A and B, etc., and Bew(A) the result of substituting the numeral for the Gödel number of A for the free variable in the usual provability predicate for PA. Let Con(A) = ~ Bew(~ A). (Con(A) is equivalent in PA to the usual sentence expressing the consistency of PA + A.) And let the class of F-sentences be the smallest class which contains Con and which also contains ~ A, (A&B) and Con(A) whenever it contains A and B. Since ⊦PA Bew(A) ↔ Bew(B) if ⊦PAA ↔ B, Friedman's problem is then the question whether the class of true F-sentences is recursive.The answer is that it is recursive. To see why, we need a definition and a theorem.Definition. An atom is a sentence Conn for some n ≥ 1, where Cont = Con and Conn + 1 = Con(Conn).

scholarly journals Theory of finite or infinite trees revisited

2008 ◽  
Vol 8 (04) ◽  
pp. 431-489 ◽  
Author(s):  
KHALIL DJELLOUL ◽  
THI-BICH-HANH DAO ◽  
THOM FRÜHWIRTH
Keyword(s):  
Constraint Satisfaction ◽  
Decision Procedure ◽  
Constraint Satisfaction Problem ◽  
Free Variable ◽  
Constraint Solver ◽  
First Order ◽  
Infinite Trees ◽  
Order Constraint ◽  
Infinite Set ◽  
Rewriting Rules

AbstractWe present in this paper a first-order axiomatization of an extended theoryTof finite or infinite trees, built on a signature containing an infinite set of function symbols and a relationfinite(t), which enables to distinguish between finite and infinite trees. We show thatThas at least one model and prove its completeness by giving not only a decision procedure, but a full first-order constraint solver that gives clear and explicit solutions for any first-order constraint satisfaction problem inT. The solver is given in the form of 16 rewriting rules that transform any first-order constraintinto an equivalent disjunction φ of simple formulas such that φ is either the formulatrueor the formulafalseor a formula having at least one free variable, being equivalent neither totruenor tofalseand where the solutions of the free variables are expressed in a clear and explicit way. The correctness of our rules implies the completeness ofT. We also describe an implementation of our algorithm in CHR (Constraint Handling Rules) and compare the performance with an implementation in C++ and that of a recent decision procedure for decomposable theories.

Fixed point theorems for a pair of single-valued operators in a metric space endowed with a reflexive relation

2017 ◽  
Vol 33 (3) ◽  
pp. 301-310
Author(s):  
MELANIA-IULIA DOBRICAN ◽  
Keyword(s):  
Fixed Point ◽  
Fixed Points ◽  
Metric Space ◽  
Existence And Uniqueness ◽  
Fixed Point Theorems ◽  
Uniqueness Theorems ◽  
Mixed Monotone Property ◽  
First Order ◽  
System Equation ◽  
Coupled Fixed Points

In this paper we provide some existence and uniqueness theorems for coupled fixed points for a pair of contractive operators satisfying a mixed monotone property, in a metric space endowed with a reflexive relation. An application to a first-order differential system equation with PBV conditions is also given to illustrate the utility of our results.

On generalized quantifiers in arithmetic

1982 ◽  
Vol 47 (1) ◽  
pp. 187-190 ◽  
Author(s):  
Carl Morgenstern
Keyword(s):  
Axiom System ◽  
Peano Arithmetic ◽  
Order Logic ◽  
First Order Logic ◽  
Generalized Quantifiers ◽  
First Order ◽  
Order Language ◽  
Truth Definition ◽  
Order Arithmetic ◽  
Infinite Set

In this note we investigate an extension of Peano arithmetic which arises from adjoining generalized quantifiers to first-order logic. Markwald [2] first studied the definability properties of L1, the language of first-order arithmetic, L, with the additional quantifer Ux which denotes “there are infinitely many x such that…. Note that Ux is the same thing as the Keisler quantifier Qx in the ℵ0 interpretation.We consider L2, which is L together with the ℵ0 interpretation of the Magidor-Malitz quantifier Q2xy which denotes “there is an infinite set X such that for distinct x, y ∈ X …”. In [1] Magidor and Malitz presented an axiom system for languages which arise from adding Q2 to a first-order language. They proved that the axioms are valid in every regular interpretation, and, assuming ◊ω1, that the axioms are complete in the ℵ1 interpretation.If we let denote Peano arithmetic in L2 with induction for L2 formulas and the Magidor-Malitz axioms as logical axioms, we show that in we can give a truth definition for first-order Peano arithmetic, . Consequently we can prove in that is Πn sound for every n, thus in we can prove the Paris-Harrington combinatorial principle and the higher-order analogues due to Schlipf.

scholarly journals An Application of the Fixed Point Theory to the Study of Monotonic Solutions for Systems of Differential Equations

Mathematics ◽  
2020 ◽  
Vol 8 (7) ◽  
pp. 1183
Author(s):  
Adrian Nicolae Branga ◽  
Ion Marian Olaru
Keyword(s):  
Fixed Point ◽  
Differential Equations ◽  
Fixed Points ◽  
Existence And Uniqueness ◽  
Fixed Point Theory ◽  
Point Theory ◽  
Linear Differential Equations ◽  
First Order ◽  
Systems Of Differential Equations ◽  
Linear Differential

In this paper, we establish some conditions for the existence and uniqueness of the monotonic solutions for nonhomogeneous systems of first-order linear differential equations, by using a result of the fixed points theory for sequentially complete gauge spaces.

scholarly journals Fixed Points for Multivalued Suzuki Type (θ,R)-Contraction Mapping with Applications

2019 ◽  
Vol 2019 ◽  
pp. 1-13 ◽  
Author(s):  
Mujahid Abbas ◽  
Hira Iqbal ◽  
Adrian Petrusel
Keyword(s):  
Differential Equation ◽  
Fixed Point ◽  
Fixed Points ◽  
Metric Space ◽  
Contraction Mapping ◽  
Order Differential Equation ◽  
Existence Of A Solution ◽  
First Order ◽  
Fractional Differential ◽  
Homotopy Result

In this paper, we will introduce the concept of Suzuki type multivalued (θ,R)-contraction and we will prove some fixed point results in the setting of a metric space equipped with a binary relation. Our results generalize and extend various comparable results in the existing literature. Examples are provided to support the results proved here. As an application of our results, we obtain a homotopy result, proving the existence of a solution for a second-order differential equation and for a first-order fractional differential equation.

Tarski’s Theorem for Arithmetic

1992 ◽  
Author(s):  
Raymond M. Smullyan
Keyword(s):  
Peano Arithmetic ◽  
Finite Alphabet ◽  
Universal Quantifier ◽  
Natural Numbers ◽  
Successor Function ◽  
Material Implication ◽  
Second Order Arithmetic ◽  
First Order ◽  
Order Arithmetic ◽  
Concrete Language

In the last chapter, we dealt with mathematical languages in considerable generality. We shall now turn to some particular mathematical languages. One of our goals is to reach Gödel’s incompleteness theorem for the particular system known as Peano Arithmetic. We shall give several proofs of this important result; the simplest one is based partly on Tarski’s theorem, to which we first turn. The first concrete language that we will study is the language of first order arithmetic based on addition, multiplication and exponentiation. [We also take as primitive the successor function and the less than or equal to relation, but these are inessential.] We shall formulate the language using only a finite alphabet (mainly for purposes of a convenient Gödel numbering); specifically we use the following 13 symbols. . . . 0’ ( ) f, υ ∽ ⊃ ∀ = ≤ # . . . The expressions 0, 0′, 0″, 0‴, · · · are called numerals and will serve as formal names of the respective natural numbers 0, 1, 2, 3, · · ·. The accent symbol (also called the prime) is serving as a name of the successor function. We also need names for the operations of addition, multiplication and exponentiation; we use the expressions f′, f″, f‴ as respective names of these three functions. We abbreviate f′ by the familiar “+”; we abbreviate f’’ by the familiar dot and f‴ by the symbol “E”. The symbols ~ and ⊃ are the familiar symbols from prepositional logic, standing for negation and material implication, respectively. [For any reader not familiar with the use of the horseshoe symbol, for any propositions p and q, the propositions p ⊃ q is intended to mean nothing more nor less than that either p is false, or p and q are both true.] The symbol ∀ is the universal quantifier and means “for all.” We will be quantifying only over natural numbers not over sets or relations on the natural numbers. [Technically, we are working in first-order arithmetic, not second-order arithmetic.] The symbol “=” is used, as usual, to denote the identity relation, and “≤” is used, as usual, to denote the “less than or equal to” relation.

Regularity in models of arithmetic

1984 ◽  
Vol 49 (1) ◽  
pp. 272-280 ◽  
Author(s):  
George Mills ◽  
Jeff Paris
Keyword(s):  
Peano Arithmetic ◽  
Second Order ◽  
Axiom Schema ◽  
First Order ◽  
Nonstandard Models ◽  
Order Arithmetic ◽  
Bounded Sets ◽  
Models Of Arithmetic

AbstractThis paper investigates the quantifier “there exist unboundedly many” in the context of first-order arithmetic. An alternative axiomatization is found for Peano arithmetic based on an axiom schema of regularity: The union of boundedly many bounded sets is bounded. We also obtain combinatorial equivalents of certain second-order theories associated with cuts in nonstandard models of arithmetic.

Sign in / Sign up

Export Citation Format

Share Document