Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userThree Equivalent Ordinal Notation Systems in Cubical Agda
121
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
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 can 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.
rate research
Read More
As the field of recommender systems has developed, authors have used a myriad of notations for describing the mathematical workings of recommendation algorithms. These notations ap-pear in research papers, books, lecture notes, blog posts, and software documentation. The dis-ciplinary diversity of the field has not contributed to consistency in notation; scholars whose home base is in information retrieval have different habits and expectations than those in ma-chine learning or human-computer interaction. In the course of years of teaching and research on recommender systems, we have seen the val-ue in adopting a consistent notation across our work. This has been particularly highlighted in our development of the Recommender Systems MOOC on Coursera (Konstan et al. 2015), as we need to explain a wide variety of algorithms and our learners are not well-served by changing notation between algorithms. In this paper, we describe the notation we have adopted in our work, along with its justification and some discussion of considered alternatives. We present this in hope that it will be useful to others writing and teaching about recommender systems. This notation has served us well for some time now, in research, online education, and traditional classroom instruction. We feel it is ready for broad use.
For every partial combinatory algebra (pca), we define a hierarchy of extensionality relations using ordinals. We investigate the closure ordinals of pcas, i.e. the smallest ordinals where these relations become equal. We show that the closure ordinal of Kleenes first model is $omega_1^textit{CK}$ and that the closure ordinal of Kleenes second model is $omega_1$. We calculate the exact complexities of the extensionality relations in Kleenes first model, showing that they exhaust the hyperarithmetical hierarchy. We also discuss embeddings of pcas.
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
These are the lecture notes of an introductory course on ordinal analysis. Our selection of topics is guided by the aim to give a complete and direct proof of a mathematical independence result: Kruskals theorem for binary trees is unprovable in conservative extensions of Peano arithmetic (note that much stronger results of this type are due to Harvey Friedman). Concerning prerequisites, we assume a solid introduction to mathematical logic but no specialized knowledge of proof theory. The material in these notes is intended for 14 lectures and 7 exercise sessions of 90 minutes each.
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}}$.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
