scholarly journals Foundational and Mathematical Uses of Higher Types

1999 ◽  
Vol 6 (31) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Reverse Mathematics ◽  
Continuous Functions ◽  
Higher Order ◽  
Second Order ◽  
Polish Spaces ◽  
Primitive Recursive Arithmetic ◽  
Higher Types ◽  
A Priority ◽  
Primitive Recursive

In this paper we develop mathematically strong systems of analysis in<br />higher types which, nevertheless, are proof-theoretically weak, i.e. conservative<br />over elementary resp. primitive recursive arithmetic. These systems<br />are based on non-collapsing hierarchies (Phi_n-WKL+, Psi_n-WKL+) of principles<br />which generalize (and for n = 0 coincide with) the so-called `weak' K¨onig's<br />lemma WKL (which has been studied extensively in the context of second order<br />arithmetic) to logically more complex tree predicates. Whereas the second<br />order context used in the program of reverse mathematics requires an encoding<br />of higher analytical concepts like continuous functions F : X -> Y between<br />Polish spaces X, Y , the more flexible language of our systems allows to treat<br />such objects directly. This is of relevance as the encoding of F used in reverse<br />mathematics tacitly yields a constructively enriched notion of continuous functions<br />which e.g. for F : N^N -> N can be seen (in our higher order context) to be equivalent<br /> to the existence of a continuous modulus of pointwise continuity.<br />For the direct representation of F the existence of such a modulus is<br />independent even of full arithmetic in all finite types E-PA^omega plus quantifier-free<br />choice, as we show using a priority construction due to L. Harrington.<br />The usual WKL-based proofs of properties of F given in reverse mathematics<br />make use of the enrichment provided by codes of F, and WKL does not seem<br />to be sufficient to obtain similar results for the direct representation of F in<br />our setting. However, it turns out that   Psi_1-WKL+ is sufficient.<br />Our conservation results for (Phi_n-WKL+,  Psi_n-WKL+) are proved via a new<br />elimination result for a strong non-standard principle of uniform Sigma^0_1-<br />boundedness<br />which we introduced in 1996 and which implies the WKL-extensions studied<br />in this paper.

scholarly journals Higher Order Reverse Mathematics

2000 ◽  
Vol 7 (49) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Finite Type ◽  
Recursion Theory ◽  
Reverse Mathematics ◽  
Higher Order ◽  
Second Order ◽  
Base System ◽  
Frame Work

In this paper we argue for an extension of the second order frame-work currently used in the program of reverse mathematics to finite types. In particular we propose a conservative finite type extension RCA^omega_0 of the second order base system RCA_0. By this conservation nothing is lost for second order statements if we reason in RCA^omega_0 in stead of RCA_0. However, the presence of finite types allows to treat various analytical notions in a rather direct way, compared to the encodings needed in RCA_0 which are not always provably faithful in RCA_0. Moreover, the language of finite types allows to treat many more principles and gives rise to interesting extensions of the existing scheme of reverse mathematics. We indicate this by showing that the class of principles equivalent (over RCA^omega_0 ) to Feferman's nonconstructive mu-operator forms a mathematically rich and very robust class. This is closely related to a phenomenon in higher type recursion theory known as Grilliot's trick.

scholarly journals TRANSFINITE RECURSION IN HIGHER REVERSE MATHEMATICS

2015 ◽  
Vol 80 (3) ◽  
pp. 940-969 ◽  
Author(s):  
NOAH SCHWEBER
Keyword(s):  
Reverse Mathematics ◽  
Higher Order ◽  
Steel Type ◽  
Base Theory ◽  
Higher Types ◽  
Flexible Framework ◽  
Image Position ◽  
Transfinite Recursion

AbstractIn this paper we investigate the reverse mathematics of higher-order analogues of the theory $$ATR_0$$ within the framework of higher order reverse mathematics developed by Kohlenbach [11]. We define a theory $$RCA_0^3$$, a close higher-type analogue of the classical base theory $$RCA_0$$ which is essentially a conservative subtheory of Kohlenbach’s base theory $$RCA_{\rm{0}}^\omega$$. Working over $$RCA_0^3$$, we study higher-type analogues of statements classically equivalent to $$ATR_0$$, including open and clopen determinacy, and examine the extent to which $$ATR_0$$ remains robust at higher types. Our main result is the separation of open and clopen determinacy for reals, using a variant of Steel’s tagged tree forcing; in the presentation of this result, we develop a new, more flexible framework for Steel-type forcing.

scholarly journals On the Uniform Weak König’s Lemma

1999 ◽  
Vol 6 (11) ◽  
Author(s):  
Ulrich Kohlenbach
Keyword(s):  
Finite Type ◽  
Binary Tree ◽  
Higher Order ◽  
Elimination Process ◽  
Primitive Recursive Arithmetic ◽  
Classical Mathematics ◽  
Order Arithmetic ◽  
Primitive Recursive ◽  
Weak König’S Lemma ◽  
König’S Lemma

The so-called weak K¨onig's lemma WKL asserts the existence of an infinite<br />path b in any infinite binary tree (given by a representing function f). Based on<br />this principle one can formulate subsystems of higher-order arithmetic which<br />allow to carry out very substantial parts of classical mathematics but are PI^0_2-conservative<br />over primitive recursive arithmetic PRA (and even weaker fragments of arithmetic). In [10] we established such conservation results relative to finite type extensions PRA^omega of PRA (together with a quantifier-free axiom of choice schema). In this setting one can consider also a uniform version UWKL of WKL which asserts the existence of a functional Phi which selects uniformly in a given infinite binary tree f an infinite path Phi f of that tree.<br />This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in [10] actually can be used to eliminate even this uniform weak K¨onig's lemma provided that PRA^omega only has a quantifier-free rule of extensionality QF-ER instead of the full axioms (E) of extensionality for all finite types. In this paper we show that in the presence of (E), UWKL is much stronger than WKL: whereas WKL remains to be Pi^0_2 -conservative over PRA, PRA^omega +(E)+UWKL contains (and is conservative over) full Peano arithmetic PA.

scholarly journals Countable sets versus sets that are countable in reverse mathematics

Computability ◽  
2021 ◽  
pp. 1-31
Author(s):  
Sam Sanders
Keyword(s):  
Reverse Mathematics ◽  
Higher Order ◽  
Second Order ◽  
Major Theme ◽  
Original Formulation ◽  
Second Order Arithmetic ◽  
First Order ◽  
Order Arithmetic ◽  
Definition Of

The program Reverse Mathematics (RM for short) seeks to identify the axioms necessary to prove theorems of ordinary mathematics, usually working in the language of second-order arithmetic L 2 . A major theme in RM is therefore the study of structures that are countable or can be approximated by countable sets. Now, countable sets must be represented by sequences here, because the higher-order definition of ‘countable set’ involving injections/bijections to N cannot be directly expressed in L 2 . Working in Kohlenbach’s higher-order RM, we investigate various central theorems, e.g. those due to König, Ramsey, Bolzano, Weierstrass, and Borel, in their (often original) formulation involving the definition of ‘countable set’ based on injections/bijections to N. This study turns out to be closely related to the logical properties of the uncountably of R, recently developed by the author and Dag Normann. Now, ‘being countable’ can be expressed by the existence of an injection to N (Kunen) or the existence of a bijection to N (Hrbacek–Jech). The former (and not the latter) choice yields ‘explosive’ theorems, i.e. relatively weak statements that become much stronger when combined with discontinuous functionals, even up to Π 2 1 - CA 0 . Nonetheless, replacing ‘sequence’ by ‘countable set’ seriously reduces the first-order strength of these theorems, whatever the notion of ‘set’ used. Finally, we obtain ‘splittings’ involving e.g. lemmas by König and theorems from the RM zoo, showing that the latter are ‘a lot more tame’ when formulated with countable sets.

scholarly journals On mathematical instrumentalism

2005 ◽  
Vol 70 (3) ◽  
pp. 778-794 ◽  
Author(s):  
Patrick Caldon ◽  
Aleksandar Ignjatović
Keyword(s):  
Equational Theory ◽  
Reverse Mathematics ◽  
The Other ◽  
Conservative Extension ◽  
Philosophical View ◽  
Other Hand ◽  
Primitive Recursive Arithmetic ◽  
Speed Up ◽  
Primitive Recursive

AbstractIn this paper we devise some technical tools for dealing with problems connected with the philosophical view usually called mathematical instrumentalism. These tools are interesting in their own right, independently of their philosophical consequences. For example, we show that even though the fragment of Peanos Arithmetic known as IΣ1 is a conservative extension of the equational theory of Primitive Recursive Arithmetic (PRA). IΣ1 has a super-exponential speed-up over PRA. On the other hand, theories studied in the Program of Reverse Mathematics that formalize powerful mathematical principles have only polynomial speed-up over IΣ1.

Optimal control of higher order differential inclusions with functional constraints

2020 ◽  
Vol 26 ◽  
pp. 37 ◽  
Author(s):  
Elimhan N. Mahmudov
Keyword(s):  
Optimal Control ◽  
Optimality Conditions ◽  
Differential Inclusion ◽  
Differential Inclusions ◽  
Higher Order ◽  
Second Order ◽  
Sufficient Optimality Conditions ◽  
Functional Constraints ◽  
Complementary Slackness ◽  
Complementary Slackness Conditions

The present paper studies the Mayer problem with higher order evolution differential inclusions and functional constraints of optimal control theory (PFC); to this end first we use an interesting auxiliary problem with second order discrete-time and discrete approximate inclusions (PFD). Are proved necessary and sufficient conditions incorporating the Euler–Lagrange inclusion, the Hamiltonian inclusion, the transversality and complementary slackness conditions. The basic concept of obtaining optimal conditions is locally adjoint mappings and equivalence results. Then combining these results and passing to the limit in the discrete approximations we establish new sufficient optimality conditions for second order continuous-time evolution inclusions. This approach and results make a bridge between optimal control problem with higher order differential inclusion (PFC) and constrained mathematical programming problems in finite-dimensional spaces. Formulation of the transversality and complementary slackness conditions for second order differential inclusions play a substantial role in the next investigations without which it is hardly ever possible to get any optimality conditions; consequently, these results are generalized to the problem with an arbitrary higher order differential inclusion. Furthermore, application of these results is demonstrated by solving some semilinear problem with second and third order differential inclusions.

scholarly journals Preserving the Shape of Functions by Applying Multidimensional Schoenberg-Type Operators

Symmetry ◽  
2021 ◽  
Vol 13 (6) ◽  
pp. 1016
Author(s):  
Camelia Liliana Moldovan ◽  
Radu Păltănea
Keyword(s):  
Applied Sciences ◽  
Degree Of Approximation ◽  
Higher Order ◽  
Second Order ◽  
Dimensional Case ◽  
Moduli Of Continuity ◽  
One Dimensional ◽  
Multidimensional Generalization ◽  
The One

The paper presents a multidimensional generalization of the Schoenberg operators of higher order. The new operators are powerful tools that can be used for approximation processes in many fields of applied sciences. The construction of these operators uses a symmetry regarding the domain of definition. The degree of approximation by sequences of such operators is given in terms of the first and the second order moduli of continuity. Extending certain results obtained by Marsden in the one-dimensional case, the property of preservation of monotonicity and convexity is proved.

scholarly journals Higher order Hamiltonian Monte Carlo sampling for cosmological large-scale structure analysis

2021 ◽  
Vol 502 (3) ◽  
pp. 3976-3992
Author(s):  
Mónica Hernández-Sánchez ◽  
Francisco-Shu Kitaura ◽  
Metin Ata ◽  
Claudio Dalla Vecchia
Keyword(s):  
Fourth Order ◽  
Large Scale ◽  
Equations Of Motion ◽  
Large Scale Structure ◽  
Real Space ◽  
Higher Order ◽  
Second Order ◽  
Scale Structure ◽  
Integration Schemes ◽  
Reconstruction Methods

ABSTRACT We investigate higher order symplectic integration strategies within Bayesian cosmic density field reconstruction methods. In particular, we study the fourth-order discretization of Hamiltonian equations of motion (EoM). This is achieved by recursively applying the basic second-order leap-frog scheme (considering the single evaluation of the EoM) in a combination of even numbers of forward time integration steps with a single intermediate backward step. This largely reduces the number of evaluations and random gradient computations, as required in the usual second-order case for high-dimensional cases. We restrict this study to the lognormal-Poisson model, applied to a full volume halo catalogue in real space on a cubical mesh of 1250 h−1 Mpc side and 2563 cells. Hence, we neglect selection effects, redshift space distortions, and displacements. We note that those observational and cosmic evolution effects can be accounted for in subsequent Gibbs-sampling steps within the COSMIC BIRTH algorithm. We find that going from the usual second to fourth order in the leap-frog scheme shortens the burn-in phase by a factor of at least ∼30. This implies that 75–90 independent samples are obtained while the fastest second-order method converges. After convergence, the correlation lengths indicate an improvement factor of about 3.0 fewer gradient computations for meshes of 2563 cells. In the considered cosmological scenario, the traditional leap-frog scheme turns out to outperform higher order integration schemes only when considering lower dimensional problems, e.g. meshes with 643 cells. This gain in computational efficiency can help to go towards a full Bayesian analysis of the cosmological large-scale structure for upcoming galaxy surveys.

scholarly journals Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

2021 ◽  
Vol 22 (2) ◽  
pp. 1-37
Author(s):  
Christopher H. Broadbent ◽  
Arnaud Carayol ◽  
C.-H. Luke Ong ◽  
Olivier Serre
Keyword(s):  
Model Checking ◽  
Free Variable ◽  
Higher Order ◽  
Second Order ◽  
Effective Solution ◽  
Parity Games ◽  
Transition Graphs ◽  
Second Order Logic ◽  
Pushdown Automata ◽  
Monadic Second Order Logic

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

Sign in / Sign up

Export Citation Format

Share Document