Past exam of the mathematics course of the University of Cambridge / 2013 / iii / Paper 20 / 2

If $M$ halts on every input, simulate $M$ on input $n$ while counting its steps, and output that count when it halts. The resulting function $t_M(n)$ is a total computable function. Consequently yes: one may take the exact running time,This construction does not promise a simple closed expression or a bound of any particular complexity class; it uses the promised totality of this particular machine.

For a machine computing a partial computable function, its exact halting-time function is still a partial computable function, with the same domain. A finite bound cannot cover a genuinely infinite computation. Even restricting attention to inputs on which $M$ halts, a total computable function bounding all halting times need not exist. In fact the precise characterization is the computable bound on halting time criterion:For the forward implication, compute $f(n)$ and simulate $M(n)$ for that many steps. If it has not halted, the proposed bound ensures that it never will. This decides the domain. Conversely, first decide whether $n$ is in the domain; return zero outside it and the simulated halting time inside it. This defines a total computable function satisfying the bound. The time needed to compute the bound itself is irrelevant to this argument.

A universal halting recognizer has undecidable domain by the halting problem, so it has no such total bound. On the other hand, a machine that immediately halts on even inputs and loops on odd inputs computes a nontotal partial computable function but has a constant bound on its halting times. Thus nontotality alone does not decide whether a total bound exists.

A propositional type is a set $\Sigma$ of propositional formulas; a Boolean valuation realizes it if every member is true, and omits it if at least one member is false. A consistent propositional theory $T$ locally omits $\Sigma$ if every formula $\theta$ which implies all members of $\Sigma$ modulo $T$ is refutable modulo $T$. Equivalently, whenever $T\cup \{\theta \}$ is consistent, there is a $\sigma \in \Sigma$ for which $T\cup \{\theta ,\neg \sigma \}$ is consistent. For a consistent propositional type, this says that it is a nonprincipal propositional type.

The extended omitting types theorem for propositional logic says that if a consistent $T$ locally omits each of a countable family ${\Sigma }_0,{\Sigma }_1,\dots$, there is one Boolean valuation satisfying $T$ and omitting them all. It also works inside any prescribed finite condition consistent with $T$.

To prove it, start with such a condition ${\theta }_0$, taking $\top$ when none is prescribed. At stage $i$, choose ${\sigma }_i\in {\Sigma }_i$ such thatSuch a choice exists by local omission. More explicitly, failure would imply $T⊢{\theta }_i\to \sigma$ for every $\sigma \in {\Sigma }_i$, hence $T⊢\neg {\theta }_i$, contradicting the stage invariant. Every finite subset of $T\cup \{{\theta }_0\}\cup \{\neg {\sigma }_i:i\in \mathbb{N}\}$ lies inside a consistent stage. By the propositional compactness theorem and the completeness theorem for propositional logic, it has a Boolean valuation. That Boolean valuation satisfies $T$ and makes the selected member ${\sigma }_i$ of every type false. All types are therefore omitted simultaneously. No effective test for consistency is assumed, and the argument does not require the ambient propositional language to be countable. Only the family of omission requirements is countable.