No Arabic abstract
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.
An old theorem of Adamek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using inflationary iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylors constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of elementary topos.
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 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.
Let f be a computable function from finite sequences of 0s and 1s to real numbers. We prove that strong f-randomness implies strong f-randomness relative to a PA-degree. We also prove: if X is strongly f-random and Turing reducible to Y where Y is Martin-Lof random relative to Z, then X is strongly f-random relative to Z. In addition, we prove analogous propagation results for other notions of partial randomness, including non-K-triviality and autocomplexity. We prove that f-randomness relative to a PA-degree implies strong f-randomness, hence f-randomness does not imply f-randomness relative to a PA-degree.
We consider $omega^n$-automatic structures which are relational structures whose domain and relations are accepted by automata reading ordinal words of length $omega^n$ for some integer $ngeq 1$. We show that all these structures are $omega$-tree-automatic structures presentable by Muller or Rabin tree automata. We prove that the isomorphism relation for $omega^2$-automatic (resp. $omega^n$-automatic for $n>2$) boolean algebras (respectively, partial orders, rings, commutative rings, non commutative rings, non commutative groups) is not determined by the axiomatic system ZFC. We infer from the proof of the above result that the isomorphism problem for $omega^n$-automatic boolean algebras, $n > 1$, (respectively, rings, commutative rings, non commutative rings, non commutative groups) is neither a $Sigma_2^1$-set nor a $Pi_2^1$-set. We obtain that there exist infinitely many $omega^n$-automatic, hence also $omega$-tree-automatic, atomless boolean algebras $B_n$, $ngeq 1$, which are pairwise isomorphic under the continuum hypothesis CH and pairwise non isomorphic under an alternate axiom AT, strengthening a result of [FT10].