computable "completion" of ZFC Let $f : \omega \to \{\text{wffs of set theory}\}$ be a function.  Let $\leq_f$ be a total order on $\omega$.

Definition: $\langle f,\leq_f \rangle$ is a computable quasi-completion of ZFC if and only if

1.  $f$ and $\leq_f$ are both computable

and

2.  for all $m,n$ in $\omega$, if $m \leq_f \; n$, then all theorems of $ZFC+f(m)$ are theorems of $ZFC+f(n)$

and

3.  for all sentences $s$ in the language of set theory, there exists a member $n$ of $\omega$ such that $ZFC+f(n)$ is consistent and one of $\{s,\lnot s\}$ is a theorem of $ZFC+f(n)$


Is it known that there is no computable quasi-completion of ZFC?


Basically, has the goal of Ultimate L been shown to be impossible?
 A: Here is something very close which might be adaptable to get a suitable $f$ and ${\leq_f}$.
Outline
Since there is nothing very special about ZFC in the construction, I will instead work with a consistent computably axiomatizable theory $T$ for which Goedel's First Incompleteness Theorem applies. Let $\phi_0,\phi_1,\ldots$ be a computable enumeration of all sentences in the language of $T$. I will assume that $\phi_0$ is your favorite contradiction, which I will also denote $\perp$.
I will define a computable function $f:\omega\to\omega$ and computable linear ordering ${\preceq}$ of $\omega$ by stages. At each stage $s$, I will decide the restrictions of $f$ and ${\preceq}$ on the set $\{0,1,\dots,t_s\}$. I will also keep track of a marker $m_s$ which will mark the ${\preceq}$-first element of $\{0,1,\dots,t_s\}$ for which it is known by stage $s$ that $T + \{\phi_{f(i)} : i \leq t_s \land i \preceq m_s\}$ is inconsistent. By the phrase known by stage $s$ I mean that $\perp$ appears by stage $s$ in the standard computable enumeration of the consequences of $T + \{\phi_{f(i)} : i \leq t_s \land i \preceq m_s\}$. This standard computable enumeration is allowed to enumerate finitely many consequences at each stage. I will also assume that this standard computable enumeration is such that:


*

*If $F$ is a finite set of sentences in the language of $T$, then all elements of $F$ appear at stage $0$ of the enumeration of the consequences of $T + F$.

*If $F \subseteq G$ are finite sets of sentences in the language of $T$, then all elements which appear by stage $s$ of the enumeration of the consequences of $T + F$ also appear by stage $s$ of the enumeration of the consequences of $T + G$.
The function $f:\omega\to\omega$ and the linear ordering ${\preceq}$ will have the following properties.


*

*Every $n \in \omega$ has either finitely many ${\preceq}$-predecessors or finitely many ${\preceq}$-successors. The dividing line is whether or not the theory $T + \{\phi_{f(i)} : i \preceq n\}$ is consistent.

*If $I$ is the set of all $n \in \omega$ which have finitely many ${\preceq}$-predecessors, then $T_I = T + \{\phi_{f(i)} : i \in I\}$ is a complete theory.
So the only missing requirement is that $i \prec j$ implies that $T \vdash \phi_{f(j)} \rightarrow \phi_{f(i)}$.
Construction
Stage $s = 0$ is trivial: $t_s = 0$, $f(0) = 0$, $0 \preceq 0$. (Note that $m_0 = 0$ since $\phi_0 = \perp$.) 
At stage $s+1$, let $\ell_s$ be the ${\preceq}$-first element of the set $\{i \leq t_s : i \preceq m_s\}$ such that $T + \{\phi_{f(i)} : i \leq t_s \land i \preceq \ell_s\}$ is known to be inconsistent by stage $s+1$. Note that $\ell_s$ necessarily exists since $m_s$ is in the set being searched.
Case $\ell_s \neq m_s$: Then simply let $t_{s+1} = t_s$. (Note that $m_{s+1} = \ell_s$.)
Case $\ell_s = m_s$: Then consider the first element $n$ of the set
$$\{0,1,\ldots,s+1\}\setminus\{f(i): i \leq t_s \land i \prec m_s\}$$
such that
$$T + \phi_n + \{\phi_{f(i)} : i \leq t_s \land f(i) < n \land i \prec m_s\}$$
is not known to be inconsistent by stage $s+1$.


*

*If there is no such $n$, then simply let $t_{s+1} = t_s$. (Note that $m_{s+1} = m_s$.)

*Otherwise, set $t_{s+1} = t_s + 1$ and $f(t_{s+1}) = n$. Place $t_{s+1}$ immediately after the maximum element of $\{i \leq t_s : f(i) < n \land i \prec m_s\}$ in the ${\preceq}$-ordering.
Note that we always have that if $i \prec j \prec m_s$ and $i, j \leq t_s$ then $f(i) < f(j)$.
Verifications
First, observe that $\sup_{s<\omega} t_s = \omega$. Thus $f:\omega\to\omega$ is well-defined and ${\preceq}$ is a linear ordering of $\omega$.
Proof. Suppose, for the sake of contradiction, that $t_s = t_{s_0}$ for all $s \geq s_0$. Note that there are only finitely many stages $s \geq s_0$ such that $\ell_s \neq m_s$. So we can find a stage $s_1 \geq s_0$ such that $\ell_s = m_s$ for all $s \geq s_1$. Let $t = t_{s_0}$ and $m = m_{s_1}$. Note that $T' = T + \{\phi_{f(i)} : i \leq t \land i \prec m\}$ is necessarily consistent. Moreover, for every $n \notin \{f(i) : i \leq t \land i \prec m\}$, we must have that $T' + \phi_n$ is inconsistent and hence $T' \vdash \lnot\phi_n$. Since $\phi_0,\phi_1,\ldots$ enumerates all sentences of the language of $T$, it follows that $T'$ is a complete extension of $T$. However, $T'$ is computably axiomatizable and hence cannot be complete. QED
Next, observe that every $n \in \omega$ has either finitely many ${\preceq}$-predecessors or finitely many ${\preceq}$-successors. The dividing line is whether the theory $T + \{\phi_{f(i)} : i \preceq n\}$ is consistent or not.
Proof. First, suppose that $T + \{\phi_{f(i)} : i \preceq n\}$ is inconsistent. Then, there is some stage $s$ such that $n \leq t_s$ and $T + \{\phi_{f(i)} : i \leq t_s \land i \preceq n\}$ is inconsistent and this is known by stage $s$. It follows that $m_s \preceq n$ and after this stage no new elements will appear after $n$ in the ${\preceq}$-ordering.
Next, suppose that $T + \{\phi_{f(i)} : i \preceq n\}$ is consistent. For any stage $s$ such that $n \leq t_s$, the theory $T + \{\phi_{f(i)} : i \leq t_s \land i \preceq n\}$ is consistent and hence not known to be inconsistent by stage $s$. It follows that $n \prec m_s$ and hence that $f(i) < f(j) < f(n)$ for all $i \prec j \prec n$ such that $i,j \leq t_s$. Therefore, $n$ has no more than $f(n)$ predecessors in the ${\preceq}$-ordering by stage $s$. Since the bound $f(n)$ is independent of $s$, it follows that $n$ has no more than $f(n)$ predecessors in the ${\preceq}$-ordering. QED
Now let $I$ be the set of all $n \in \omega$ which have only finitely many ${\preceq}$-predecessors. I claim that $T_I = T + \{\phi_{f(i)}:i \in I\}$ is complete.
Proof. Let $n_0 \in \omega$ be minimal such that $n_0 \notin \{f(i) : i \in I\}$ and $T_I + \phi_{n_0}$ is consistent. Find $i_0 \in I$ such that $n_0 < f(i_0)$ and let $s_0 \geq n_0$ be such that $\max\{i : i \preceq i_0\} \leq t_{s_0}$. If $s \geq s_0$, then 
$$\{i : i \prec i_0\} = \{i \leq t_s : f(i) < f(i_0) \land i \prec m_s\}$$ 
because $i \prec i_0$ iff $f(i) < f(i_0)$ for all $i \prec m_s$.
Since $T_I + \phi_{n_0}$ is consistent, it follows that if $s \geq s_0$ then 
$$T + \phi_{n_0} + \{\phi_{f(i)} : i \leq t_s \land f(i) < n_0 \land i \prec m_s\}$$
is not known to be inconsistent by stage $s+1$. Indeed, 
$$\{\phi_{f(i)} : i \leq t_s \land f(i) < n_0 \land i \prec m_s\} \subseteq \{\phi_{f(i)} : i \leq t_s \land f(i) < f(i_0) \land i \prec m_s\}$$ 
and 
$$\{i \leq t_s : f(i) < f(i_0) \land i \prec m_s\} = \{i : i \prec i_0\} \subseteq I.$$
If $s \geq s_0$ and $\ell_s = m_s$, then $n_0$ belongs to the set of all 
$$n \in \{0,1,\ldots,s+1\} \setminus \{f(i) : i \leq t_s \land i \prec m_s\}$$
such that
$$T + \phi_n + \{\phi_{f(i)} : i \leq t_s \land f(i) < n \land i \prec m_s\}$$
is not known to be inconsistent by stage $s+1$. Let $n_1 \leq n_0$ be the minimal such $n$. Then, by the construction, we have $f(t_s+1) = n_1$ and $t_s+1$ comes immediately after the ${\preceq}$-maximal element of 
$$\{i \leq t_s : f(i) < n_1 \land i \prec m_s\}.$$
Since $n_1 \leq n_0 < f(i_0)$ it follows that $t_s+1 \prec i_0$, which contradicts the fact that $\max\{i : i \preceq i_0\} \leq t_{s_0}$.
It follows that $n_0$ does not exist and hence that $n \notin \{f(i) : i \in I\}$ entails that $T_I + \phi_n$ is inconsistent (i.e., $T_I \vdash \lnot\phi_n$). Since $\phi_0,\phi_1,\ldots$ enumerates all sentences in the language of $T$, it follows that $T_I$ is complete. QED 
