Infinite time computable model theory

Propositional temporal logic over the real number time flow is finitely axiomatisable, but its first-order counterpart is not recursively axiomatisable. We study the logic that combines the propositional axiomatisation with the usual axioms for first-order logic with identity, and develop an alternative ``admissible'' semantics for it, showing that it is strongly complete for admissible models over the reals. By contrast there is no recursive axiomatisation of the first-order...

We study the computational strength of resetting $\alpha$-register machines, a model of transfinite computability introduced by P. Koepke in \cite{K1}. Specifically, we prove the following strengthening of a result from \cite{C}: For an exponentially closed ordinal $\alpha$, we have $L_{\alpha}\models$ZF$^{-}$ if and only if COMP$^{\text{ITRM}}_{\alpha}=L_{\alpha+1}\cap\mathfrak{P}(\alpha)$, i.e. if and only if the set of $\alpha$-ITRM-computable subsets of $\alpha$ coincides...

Challenging the standard notion of totality in computable functions, one has that, given any sufficiently expressive formal axiomatic system, there are total functions that, although computable and "intuitively" understood as being total, cannot be proved to be total. In this article we show that this implies the existence of an infinite hierarchy of time complexity classes whose representative members are hidden from (or unknown by) the respective formal axiomatic systems. A...

This paper establishes model-theoretic properties of $\mathrm{FOE}^{\infty}$, a variation of monadic first-order logic that features the generalised quantifier $\exists^\infty$ (`there are infinitely many'). We provide syntactically defined fragments of $\mathrm{FOE}^{\infty}$ characterising four different semantic properties of $\mathrm{FOE}^{\infty}$-sentences: (1) being monotone and (2) (Scott) continuous in a given set of monadic predicates; (3) having truth preserved u...

We use fast-growing finite and infinite sequences of natural numbers and more complicated constructs to define models of hypercomputation and interpret non-arithmetic predicates, with the strongest extensions reaching full second order arithmetical truth and beyond. Since the predicates are interpreted using properties of certain natural finite structures, they are arguably finitistic.

The purpose of this paper is to clarify the relationship between various conditions implying essential undecidability: our main result is that there exists a theory $T$ in which all partially recursive functions are representable, yet $T$ does not interpret Robinson's theory $R$. To this end, we borrow tools from model theory--specifically, we investigate model-theoretic properties of the model completion of the empty theory in a language with function symbols. We obtain a ce...

We state a version of the P=?NP problem for infinite time Turing machines. It is observed that P not= NP for this version.

We describe various computational models based initially, but not exclusively, on that of the Turing machine, that are generalized to allow for transfinitely many computational steps. Variants of such machines are considered that have longer tapes than the standard model, or that work on ordinals rather than numbers. We outline the connections between such models and the older theories of recursion in higher types, generalized recursion theory, and recursion on ordinals such ...

We define Oracle-Type-2-Machine capable of writing infinite oracle queries. In contrast to finite oracle queries, this extends the realm of oracle-computable functions into the discontinuous realm. Our definition is conservative; access to a computable oracle does not increase the computational power. Other models of real hypercomputation such as Ziegler's (finitely) revising computation or Type-2-Nondeterminism are shown to be special cases of Oracle-Type-2-Machines. Our a...

In this paper we use infinitary Turing machines with tapes of length $\kappa$ and which run for time $\kappa$ as presented, e.g., by Koepke \& Seyfferth, to generalise the notion of type two computability to $2^{\kappa}$, where $\kappa$ is an uncountable cardinal with $\kappa^{<\kappa}=\kappa$. Then we start the study of the computational properties of $\mathbb{R}_\kappa$, a real closed field extension of $\mathbb{R}$ of cardinality $2^{\kappa}$, defined by the first author u...