I've been taking a lecture course on Logic and Verification which has been focussing on automation of logical proofs of tautologies and similar such things. Recently, we discussed an algorithm for converting any formula in propositional logic into Conjunctive Normal Form (CNF). The algorithm is rather simple to describe.
If we are given a propositional formula $X$, write it as $\langle[X]\rangle$ where $\langle X_1,X_2,..., X_n\rangle$ represents the conjunction of the formulae $X_1,..., X_n$ and where $[X_1,..., X_n]$ is the disjunction of these formulae. Then given a current stage of the expansion $\langle D_1,..., D_n\rangle$ select one of the disjunctions $D_i$ that is not a disjunction of literals and select a non-literal $N$ from $D_i$ and:
- If $N = \neg \top, \neg \bot$ replace it by $\bot, \top$ respectively.
- If $N = \neg\neg Z$ then replace it by $Z$.
- If it is a beta-formula (i.e. a disjunction of two formulae $B_1,B_2$) then replace it by the two formula squence $B_1, B_2$ in the disjunction (e.g. $[X\vee Y, Z, W]$ would become $[X,Y,Z,W]$).
- If it is an alpha-formula (i.e. it contains a conjunction $\alpha_1\wedge \alpha_2$), then replace $N$ with a sequence of two disjunctions where one has the conjunction replaced with $\alpha_1$ and another where it is replaced with $\alpha_2$ (e.g. $[X\wedge Y, Z]$ would become $[X,Z],[Y,Z]$).
If no such disjunction exists, terminate.
Anyway, the point is that the lecturer wanted to know that this algorithm always terminated (as correctness is very easy to establish) and ended up using Kőnig's Lemma. However, as you can see on that page this lemma's proof requires a weak form of choice and it seems utterly bizarre to me that this algorithm's termination would depend on Choice.
I thus suspect there's a proof of termination without using Choice and in particular wondered if we might be able to do a slick proof using some powerful results from Logic. Can we use an absoluteness theorem somehow, such as the famous one due to Schoenfield, to show that we can remove choice from the proof of termination of the algorithm?
I suspect that the analytical complexity of the statement that this algorithm terminates is fairly low but I don't quite know enough about logic and these kinds of results to say much about this with complete certainty.