Wolfram Pohlers. Subsystems of set theory and second-order number theory. Handbook of proof theory, edited by Samuel R. Buss, Studies in logic and the foundations of mathematics, vol. 137, Elsevier, Amsterdam etc. 1998, pp. 209–335.

2000 ◽  
Vol 6 (4) ◽  
pp. 467-469 ◽  
Author(s):  
Toshiyasu Arai
Keyword(s):  
Number Theory ◽  
Set Theory ◽  
Proof Theory ◽  
Second Order ◽  
Foundations Of Mathematics ◽  
Order Number

scholarly journals RELATIVE PREDICATIVITY AND DEPENDENT RECURSION IN SECOND-ORDER SET THEORY AND HIGHER-ORDER THEORIES

2014 ◽  
Vol 79 (3) ◽  
pp. 712-732 ◽  
Author(s):  
SATO KENTARO
Keyword(s):  
Number Theory ◽  
Set Theory ◽  
Higher Order ◽  
Second Order ◽  
Order Number ◽  
Recursion Scheme ◽  
Transfinite Recursion ◽  
The Given ◽  
The Universe ◽  
Order Set

AbstractThis article reports that some robustness of the notions of predicativity and of autonomous progression is broken down if as the given infinite total entity we choose some mathematical entities other than the traditional ω. Namely, the equivalence between normal transfinite recursion scheme and new dependent transfinite recursion scheme, which does hold in the context of subsystems of second order number theory, does not hold in the context of subsystems of second order set theory where the universe V of sets is treated as the given totality (nor in the contexts of those of n+3-th order number or set theories, where the class of all n+2-th order objects is treated as the given totality).

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.

Proof theory

2018 ◽  
Author(s):  
Wilfried Sieg
Keyword(s):  
Finite Type ◽  
Set Theory ◽  
Proof Theory ◽  
Second Order ◽  
Von Neumann ◽  
Second Order Arithmetic ◽  
First Order ◽  
David Hilbert ◽  
Heyting Arithmetic ◽  
Order Arithmetic

Proof theory is a branch of mathematical logic founded by David Hilbert around 1920 to pursue Hilbert’s programme. The problems addressed by the programme had already been formulated, in some sense, at the turn of the century, for example, in Hilbert’s famous address to the First International Congress of Mathematicians in Paris. They were closely connected to the set-theoretic foundations for analysis investigated by Cantor and Dedekind – in particular, to difficulties with the unrestricted notion of system or set; they were also related to the philosophical conflict with Kronecker on the very nature of mathematics. At that time, the central issue for Hilbert was the ‘consistency of sets’ in Cantor’s sense. Hilbert suggested that the existence of consistent sets, for example, the set of real numbers, could be secured by proving the consistency of a suitable, characterizing axiom system, but indicated only vaguely how to give such proofs model-theoretically. Four years later, Hilbert departed radically from these indications and proposed a novel way of attacking the consistency problem for theories. This approach required, first of all, a strict formalization of mathematics together with logic; then, the syntactic configurations of the joint formalism would be considered as mathematical objects; finally, mathematical arguments would be used to show that contradictory formulas cannot be derived by the logical rules. This two-pronged approach of developing substantial parts of mathematics in formal theories (set theory, second-order arithmetic, finite type theory and still others) and of proving their consistency (or the consistency of significant sub-theories) was sharpened in lectures beginning in 1917 and then pursued systematically in the 1920s by Hilbert and a group of collaborators including Paul Bernays, Wilhelm Ackermann and John von Neumann. In particular, the formalizability of analysis in a second-order theory was verified by Hilbert in those very early lectures. So it was possible to focus on the second prong, namely to establish the consistency of ‘arithmetic’ (second-order number theory and set theory) by elementary mathematical, ‘finitist’ means. This part of the task proved to be much more recalcitrant than expected, and only limited results were obtained. That the limitation was inevitable was explained in 1931 by Gödel’s theorems; indeed, they refuted the attempt to establish consistency on a finitist basis – as soon as it was realized that finitist considerations could be carried out in a small fragment of first-order arithmetic. This led to the formulation of a general reductive programme. Gentzen and Gödel made the first contributions to this programme by establishing the consistency of classical first-order arithmetic – Peano arithmetic (PA) – relative to intuitionistic arithmetic – Heyting arithmetic. In 1936 Gentzen proved the consistency of PA relative to a quantifier-free theory of arithmetic that included transfinite recursion up to the first epsilon number, ε0; in his 1941 Yale lectures, Gödel proved the consistency of the same theory relative to a theory of computable functionals of finite type. These two fundamental theorems turned out to be most important for subsequent proof-theoretic work. Currently it is known how to analyse, in Gentzen’s style, strong subsystems of second-order arithmetic and set theory. The first prong of proof-theoretic investigations, the actual formal development of parts of mathematics, has also been pursued – with a surprising result: the bulk of classical analysis can be developed in theories that are conservative over (fragments of) first-order arithmetic.

scholarly journals ULTIMATE TRUTH VIS-À-VIS STABLE TRUTH

2008 ◽  
Vol 1 (1) ◽  
pp. 126-142 ◽  
Author(s):  
P. D. WELCH
Keyword(s):  
Number Theory ◽  
Null Hypothesis ◽  
Second Order ◽  
Solution Model ◽  
Ground Model ◽  
Order Number ◽  
Consistency Proof ◽  
Ultimate Truth ◽  
Semantic Paradoxes ◽  
Semantic Values

We show that the set of ultimately true sentences in Hartry Field's Revenge-immune solution model to the semantic paradoxes is recursively isomorphic to the set of stably true sentences obtained in Hans Herzberger's revision sequence starting from the null hypothesis. We further remark that this shows that a substantial subsystem of second-order number theory is needed to establish the semantic values of sentences in Field's relative consistency proof of his theory over the ground model of the standard natural numbers: \Delta _3^1-CA0 (second-order number theory with a \Delta _3^1-comprehension axiom scheme) is insufficient. We briefly consider his claim to have produced a ‘revenge-immune’ solution to the semantic paradoxes by introducing this conditional. We remark that the notion of a ‘determinately true’ operator can be introduced in other settings.

A reflection principle and its applications to nonstandard models

1995 ◽  
Vol 60 (4) ◽  
pp. 1137-1152
Author(s):  
James H. Schmerl
Keyword(s):  
Number Theory ◽  
Reflection Principle ◽  
Peano Arithmetic ◽  
Second Order ◽  
Order Number ◽  
Nonstandard Models ◽  
Consistent Extension ◽  
Weak Theories

Some methods of constructing nonstandard models work only for particular theories, such as ZFC, or CA + AC (which is second order number theory with the choice scheme). The examples of this which motivated the results of this paper occur in the main theorems of [5], which state that if T is any consistent extension of either ZFC0 (which is ZFC but with only countable replacement) or CA + AC and if κ and λ are suitably chosen cardinals, then T has a model which is κ-saturated and has the λ-Bolzano-Weierstrass property. (Compare with Theorem 3.5.) Another example is a result from [12] which states that if T is any consistent extension of CA + AC and cf (λ) > ℵ0, then T has a natural λ-Archimedean model. (Compare with Theorem 3.1 and the comments following it.) Still another example is a result in [6] in which it is shown that if a model of Peano arithmetic is expandable to a model of ZF or of CA, then so is any cofinal extension of . (Compare with Theorem 3.10.) Related types of constructions can also be found in [10] and [11].A reflection principle will be proved here, allowing these constructions to be extended to models of many other theories, among which are some exceedingly weak theories and also all of their completions.

scholarly journals Second-Order Logic and Foundations of Mathematics

2001 ◽  
Vol 7 (4) ◽  
pp. 504-520 ◽  
Author(s):  
Jouko Väänänen
Keyword(s):  
Set Theory ◽  
Second Order ◽  
Order Logic ◽  
The Other ◽  
Foundations Of Mathematics ◽  
Mathematical Concepts ◽  
Informal Reasoning ◽  
First Order ◽  
Second Order Logic ◽  
Order Set

AbstractWe discuss the differences between first-order set theory and second-order logic as a foundation for mathematics. We analyse these languages in terms of two levels of formalization. The analysis shows that if second-order logic is understood in its full semantics capable of characterizing categorically central mathematical concepts, it relies entirely on informal reasoning. On the other hand, if it is given a weak semantics, it loses its power in expressing concepts categorically. First-order set theory and second-order logic are not radically different: the latter is a major fragment of the former.

Sign in / Sign up

Export Citation Format

Share Document