اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCombinatorial principles equivalent to weak induction
62
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We consider two combinatorial principles, ${sf{ERT}}$ and ${sf{ECT}}$. Both are easily proved in ${sf{RCA}}_0$ plus ${Sigma^0_2}$ induction. We give two proofs of ${sf{ERT}}$ in ${sf{RCA}}_0$, using different methods to eliminate the use of ${Sigma^0_2}$ induction. Working in the weakened base system ${sf{RCA}}_0^*$, we prove that ${sf{ERT}}$ is equivalent to ${Sigma^0_1}$ induction and ${sf{ECT}}$ is equivalent to ${Sigma^0_2}$ induction. We conclude with a Weihrauch analysis of the principles, showing ${sf{ERT}} {equiv_{rm W}} {sf{LPO}}^* {<_{rm W}}{{sf{TC}}_{mathbb N}}^* {equiv_{rm W}} {sf{ECT}}$.
قيم البحث
اقرأ أيضاً
We study the reverse mathematics and computability-the-o-re-tic strength of (stable) Ramseys Theorem for pairs and the related principles COH and DNR. We show that SRT$^2_2$ implies DNR over RCA$_0$ but COH does not, and answer a question of Mileti b
y showing that every computable stable $2$-coloring of pairs has an incomplete $Delta^0_2$ infinite homogeneous set. We also give some extensions of the latter result, and relate it to potential approaches to showing that SRT$^2_2$ does not imply RT$^2_2$.
We prove that, for every theory $T$ which is given by an ${mathcal L}_{omega_1,omega}$ sentence, $T$ has less than $2^{aleph_0}$ many countable models if and only if we have that, for every $Xin 2^omega$ on a cone of Turing degrees, every $X$-hyperar
ithmetic model of $T$ has an $X$-computable copy. We also find a concrete description, relative to some oracle, of the Turing-degree spectra of all the models of a counterexample to Vaughts conjecture.
User defined recursive types are a fundamental feature of modern functional programming languages like Haskell, Clean, and the ML family of languages. Properties of programs defined by recursion on the structure of recursive types are generally prove
d by structural induction on the type. It is well known in the theorem proving community how to generate structural induction principles from data type declarations. These methods deserve to be better know in the functional programming community. Existing functional programming textbooks gloss over this material. And yet, if functional programmers do not know how to write down the structural induction principle for a new type - how are they supposed to reason about it? In this paper we describe an algorithm to generate structural induction principles from data type declarations. We also discuss how these methods are taught in the functional programming course at the University of Wyoming. A Haskell implementation of the algorithm is included in an appendix.
We identify principles characterizing Solomonoff Induction by demands on an agents external behaviour. Key concepts are rationality, computability, indifference and time consistency. Furthermore, we discuss extensions to the full AI case to derive AIXI.
We present three ordinal notation systems representing ordinals below $varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic c
an be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
