There are two well‐known ways of doing arithmetic with ordinal numbers: the “ordinary” addition, multiplication, and exponentiation, which are defined by transfinite iteration; and the “natural” (or “Hessenberg”) addition and multiplication (denoted ⊕ and ⊗), each satisfying its own set of algebraic laws. In 1909, Jacobsthal considered a third, intermediate way of multiplying ordinals (denoted × ), defined by transfinite iteration of natural addition, as well as the notion of exponentiation defined by transfinite iteration of his multiplication, which we denote. (...) (Jacobsthal's multiplication was later rediscovered by Conway.) Jacobsthal showed these operations too obeyed algebraic laws. In this paper, we pick up where Jacobsthal left off by considering the notion of exponentiation obtained by transfinitely iterating natural multiplication instead; we shall denote this. We show that and that ; note the use of Jacobsthal's multiplication in the latter. We also demonstrate the impossibility of defining a “natural exponentiation” satisfying reasonable algebraic laws. (shrink)

$$\mathbf {Z}$$ is a new type of non-finitist inference, i.e., an inference that involves treating some infinite collection as completed, designed for contraction free logic with unrestricted abstraction. It has been introduced in Petersen (Studia Logica 64:365–403, 2000) and shown to be consistent within a system $$\mathbf {{}L^iD{}}{}$$ $$_{\uplambda }$$ of contraction free logic with unrestricted abstraction. In Petersen (Arch Math Log 42(7):665–694, 2003) it was established that adding $$ \mathbf {Z}$$ to $$\mathbf {{}L^iD{}}{}$$ $$_{\uplambda }$$ is sufficient to prove (...) the totality of primitive recursive functions but it was also indicated that this would not extend to 2-recursive functions such as the Ackermann–Péter function, for instance. The purpose of the present paper is to expand the underlying idea in the construction of $$\mathbf {Z}$$ to gain a stronger notion, conveniently labeled $$\mathbf {Z}_2$$, which is sufficient to prove a form of nested double induction and thereby the totality of 2-recursive functions. (shrink)

This essay demonstrates proof-theoretically the consistency of a type-free theoryC with an unrestricted principle of comprehension and based on a predicate logic in which contraction (A (A B)) (A B), although it cannot holds in general, is provable for a wide range ofA's.C is presented as an axiomatic theoryCH (with a natural-deduction equivalentCS) as a finitary system, without formulas of infinite length. ThenCH is proved simply consistent by passing to a Gentzen-style natural-deduction systemCG that allows countably infinite conjunctions and in (...) which all theorems ofCH are provable.CG is seen to be a consistent by a normalization argument. It also shown that in a senseC is highly non-extensional. (shrink)

Z\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {Z}$$\end{document} is a new type of non-finitist inference, i.e., an inference that involves treating some infinite collection as completed, designed for contraction free logic with unrestricted abstraction. It has been introduced in Petersen and shown to be consistent within a system LiD\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {{}L^iD{}}{}$$\end{document}λ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$_{\uplambda }$$\end{document} of contraction free logic with unrestricted abstraction. In Petersen (...) :665–694, 2003) it was established that adding Z\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ \mathbf {Z}$$\end{document} to LiD\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {{}L^iD{}}{}$$\end{document}λ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$_{\uplambda }$$\end{document} is sufficient to prove the totality of primitive recursive functions but it was also indicated that this would not extend to 2-recursive functions such as the Ackermann–Péter function, for instance. The purpose of the present paper is to expand the underlying idea in the construction of Z\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {Z}$$\end{document} to gain a stronger notion, conveniently labeled Z2\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {Z}_2$$\end{document}, which is sufficient to prove a form of nested double induction and thereby the totality of 2-recursive functions. (shrink)

We present a decision procedure for the ∀∃ theory of the lattice of Σ1 sentences of Peano Arithmetic.