How can we formalize this procedure of converting first order logic formulas into propsitional formulas?

Question

Here is a procedure which shows us how to convert any FOL formula into a propositional formula:

I wonder how to formalize this rigurously in a simple way? by that I mean, give a precise definition which shouws a machine how to construct $\phi_p$ from $\phi$.

I tried doing this but I didn't find a simple rigurous formalization for this untill now (I have a very complicated formlization which may take about 1.5-2 page though! but this works only for countable languages)

Any good(simple) formalization?

Answer 1

See Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 114 for the "specification" of the process (it does not mean that it is easily translatable into a computer program ...) :

Divide the wffs into two groups:

1. The prime formulas are the atomic formulas and those of the form $∀x \alpha$ [for Enderton, only $\forall$ is primitive; $\exists$ is an abbreviation for $\lnot \forall \lnot$].

2. The nonprime formulas are the others, i.e., those of the form $¬ \alpha$ or $\alpha → \beta$ [again : $\lor, \land$ and $\leftrightarrow$ are abbreviations].

Thus any formula is built up from prime formulas by the operations $\mathcal E_¬$ and $\mathcal E_→$ [see page 17 for the formula-building operations].

Now go back to sentential logic, but take the sentence symbols to be the prime formulas of our first-order language.

---

The "procedure" must start from formula $\varphi$ and decompose it according to the main connective; if there is none, i.e. if the formula is $\forall x \psi$, then it is a prime and thus we are done: its "propositional transformation" is simply $p_1$.

If the main connective is $\rightarrow$, this means that $\varphi$ is $\psi_1 \rightarrow \psi_2$. Then we have to "search into" the two sub-formulae for their main connectives, if any; otherwise they are prime.