Ordinals connected with formal theories for transfinitely iterated inductive definitions

1978 ◽  
Vol 43 (2) ◽  
pp. 161-182 ◽  
Author(s):  
W. Pohlers
Keyword(s):  
Fixed Point ◽  
Number Theory ◽  
Formal Theory ◽  
Order Type ◽  
General Notion ◽  
Inductive Definitions ◽  
Primitive Recursive ◽  
Formal Theories

Let Th be a formal theory extending number theory. Call an ordinal ξ provable in Th if there is a primitive recursive ordering which can be proved in Th to be a wellordering and whose order type is > ξ. One may define the ordinal ∣ Th ∣ of Th to be the least ordinal which is not provable in Th. By [3] and [12] we get , where IDN is the formal theory for N-times iterated inductive definitions. We will generalize this result not only to the case of transfinite iterations but also to a more general notion of ‘the ordinal of a theory’.For an X-positive arithmetic formula [X,x] there is a natural norm ∣x∣: = μξ (x ∈ Iξ), where Iξ is defined as {x: [∪μ<ξIμ, x]} by recursion on ξ (cf. [7], [17]). By P we denote the least fixed point of [X,x]. Then P = ∪ξξ holds. If Th allows the formation of P, we get the canonical definitions ∥Th()∥ = sup{∣x∣ + 1: Th ⊢ x ∈ P} and ∥Th∥ = sup{∥Th()∥: P is definable in Th} (cf. [17]). If ≺ is any primitive recursive ordering define Q≺[X,x] as the formula ∀y(y ≺ x → y ∈ X) and ∣x∣≺:= ∣x∣O≺. Then ∣x∣≺ turns out to be the order type of the ≺ -predecessors of x and P is the accessible part of ≺. So Th ⊢ x ∈ P implies the provability of ∣x∣≺ in Th.

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

scholarly journals About the proof-theoretic ordinals of weak fixed point theories

1992 ◽  
Vol 57 (3) ◽  
pp. 1108-1119 ◽  
Author(s):  
Gerhard Jäger ◽  
Barbara Primo
Keyword(s):  
Fixed Point ◽  
Number Theory ◽  
Second Order ◽  
Order Number ◽  
Natural Numbers

AbstractThis paper presents several proof-theoretic results concerning weak fixed point theories over second order number theory with arithmetic comprehension and full or restricted induction on the natural numbers. It is also shown that there are natural second order theories which are proof-theoretically equivalent but have different proof-theoretic ordinals.

Certain predicates defined by induction schemata

1953 ◽  
Vol 18 (1) ◽  
pp. 49-59 ◽  
Author(s):  
Hao Wang
Keyword(s):  
Number Theory ◽  
Set Theory ◽  
Formal System ◽  
General Notion ◽  
Constant Number ◽  
Natural Numbers ◽  
System L ◽  
Truth Definition ◽  
Consistency Proofs ◽  
Special Case

It is known that we can introduce in number theory (for example, the system Z of Hilbert-Bernays) by induction schemata certain predicates of natural numbers which cannot be expressed explicitly within the framework of number theory. The question arises how we can define these predicates in some richer system, without employing induction schemata. In this paper a general notion of definability by induction (relative to number theory), which seems to apply to all the known predicates of this kind, is introduced; and it is proved that in a system L1 which forms an extension of number theory all predicates which are definable by induction (hereafter to be abbreviated d.i.) according to the definition are explicitly expressible.In order to define such predicates and prove theorems answering to their induction schemata, we have to allow certain impredicative classes in L1. However, if we want merely to prove that for each constant number the special case of the induction schema for a predicate d.i. is provable, we do not have to assume the existence of impredicative classes. A certain weaker system L2, in which only predicative classes of natural numbers are allowed, is sufficient for the purpose. It is noted that a truth definition for number theory can be obtained in L2. Consistency proofs for number theory do not seem to be formalizable in L2, although they can, it is observed, be formalized in L1.In general, given any ordinary formal system (say Zermelo set theory), it is possible to define by induction schemata, in the same manner as in number theory, certain predicates which are not explicitly definable in the system. Here again, by extending the system in an analogous fashion, these predicates become expressible in the resulting system. The crucial predicate instrumental to obtaining a truth definition for a given system is taken as an example.

Every recursive linear ordering has a copy in DTIME-SPACE(n,log(n))

1990 ◽  
Vol 55 (1) ◽  
pp. 260-276 ◽  
Author(s):  
Serge Grigorieff
Keyword(s):  
Complexity Theory ◽  
Order Type ◽  
Linear Ordering ◽  
Binary Representation ◽  
Relational Structures ◽  
Time Space ◽  
Representation Of Integers ◽  
Recursive Structures ◽  
Primitive Recursive ◽  
Recursive Relations

This paper is a contribution to the following natural problem in complexity theory:(*) Is there a complexity theory for isomorphism types of recursive countable relational structures? I.e. given a recursive relational structure ℛ over the set N of nonnegative integers, is there a nontrivial lower bound for the time-space complexity of recursive structures isomorphic (resp. recursively isomorphic) to ℛ?For unary recursive relations R, the answer is trivially negative: either R is finite or coinfinite or 〈N, R〉 is recursively isomorphic to 〈N, {x ϵ N: x is even}〉.The general problem for relations with arity 2 (or greater) is open.Related to this problem, a classical result (going back to S. C. Kleene [4], 1955) states that every recursive ordinal is in fact primitive recursive.In [3] Patrick Dehornoy, using methods relevant to computer science, improves this result, showing that every recursive ordinal can be represented by a recursive total ordering over N which has linear deterministic time complexity relative to the binary representation of integers. As he notices, his proof applies to every recursive total order type α such that the isomorphism type of α is not changed if points are replaced by arbitrary finite nonempty subsets of consecutive points.In this paper we extend Dehornoy's result to all recursive total orderings over N and get minimal complexity for both time and space simultaneously.

scholarly journals Fitness Conditions for fixed Point Iteration

1992 ◽  
Vol 21 (384) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Fixed Point ◽  
Abstract Interpretation ◽  
Flow Analysis ◽  
Worst Case ◽  
Fixed Point Iteration ◽  
Average Case ◽  
Data Flow Analysis ◽  
Tail Recursion ◽  
Carry Over ◽  
Primitive Recursive

This paper provides a link between the formulation of static program analyses using the framework of abstract interpretation (popular for functional languages) and using the more classical framework of data flow analysis (popular for imperative languages). In particular we show how the classical notions of fastness, rapidity and k-boundedness carry over to the abstract interpretation framework and how this may be used to bound the number of times a functional should be unfolded in order to yield the fixed point. This is supplemented with a number of results on how to calculate the bounds for iterative forms (as for tail recursion), for linear forms (as for one nested recursive call), and for primitive recursive forms. In some cases this improves the ''worst case'' results of H.R. Nielson and F. Nielson: Bounded Fixed Point Iteration, but more importantly it gives much better ''average case'' results.

scholarly journals An application of results by Hardy, Ramanujan and Karamata to Ackermannian functions

2003 ◽  
Vol Vol. 6 no. 1 ◽  
Author(s):  
Andreas Weiermann
Keyword(s):  
Fine Structure ◽  
Structure Analysis ◽  
Tauberian Theorem ◽  
Classical Result ◽  
Order Type ◽  
Recursive Functions ◽  
Fine Structure Analysis ◽  
International Audience ◽  
Primitive Recursive

International audience The Ackermann function is a fascinating and well studied paradigm for a function which eventually dominates all primitive recursive functions. By a classical result from the theory of recursive functions it is known that the Ackermann function can be defined by an unnested or descent recursion along the segment of ordinals below ω ^ω (or equivalently along the order type of the polynomials under eventual domination). In this article we give a fine structure analysis of such a Ackermann type descent recursion in the case that the ordinals below ω ^ω are represented via a Hardy Ramanujan style coding. This paper combines number-theoretic results by Hardy and Ramanujan, Karamata's celebrated Tauberian theorem and techniques from the theory of computability in a perhaps surprising way.

Toward a Formal Theory of Transactions and Transvections

1965 ◽  
Vol 2 (2) ◽  
pp. 117-127 ◽  
Author(s):  
Wroe Alderson ◽  
Miles W. Martin
Keyword(s):  
Formal Theory ◽  
Marketing Channels ◽  
System Behavior ◽  
Marketing System ◽  
Basic Concepts ◽  
Formal Theories

This article presents the initial steps in the formalization of a partial theory of marketing. The partial theory pertains to the movement of goods and information through marketing channels, and the theory utilizes two basic concepts of marketing system behavior, namely, transactions and transvections. Current approaches to the problem of constructing formal theories are compared and reasons are given for choosing the “molar” approach.

Sign in / Sign up

Export Citation Format

Share Document