1: \begin{definition}

2: \label{d:univ_trans}

3: We start by defining the translations for sentences in basic normal forms. 

4: 

5: For  $\ofo$-sentences in basic form we first set

6: \[

7:           \Big(  \dbnfofo{\Sigma}  \Big)^{\tuniv} 

8:          \isdef 

9:    \forall z \bigvee_{S \in \Sigma} \tau_{S}(z)

10: \]

11: Second, we define $(\bigvee_{i} \alpha_{i})^{\tuniv} \isdef \bigvee 

12: \alpha_{i}^{\tuniv}$. 

13: Finally, we extend the translation $(-)^{\tuniv}$ to the collection of all 

14: $\ofo$-sentences by defining $\phi^{\tmoda} \isdef (\tbas{\phi})^{\tuniv}$, 

15: where $\tbas{\phi}$

16: is the basic normal form of $\phi$ as given by Fact~\ref{fact:ofonormalform}.

17: 

18: Similarly, for $\ofoe$-sentences we first define

19: \[

20:         \Big(  \dbnfofoe{\vlist{T}}{\Pi}  \Big)^{\tuniv} 

21:          \isdef 

22:    \forall z \bigvee_{S \in \vlist{T}\cup \Pi} \tau_{S}(z)

23: \]

24: and then we extend it to the full language by distributing over disjunction and applying Theorem~\ref{thm:bnfofoe} to convert an arbitrary $\ofoe$ sentence into an equivalent sentence in basic normal form.

25: 

26: Finally, for simple basic formulas of $\ofoei$, the translation $(-)^\tuniv$ is given as follows:

27: \[

28: (\dbnfofoei{\vlist{T}}{\Pi}{\Sigma})^{\tuniv} \isdef 

29:    \forall z \bigvee_{S \in \vlist{T}\cup \Pi\cup\Sigma} \tau_{S}(z) 

30:    \land \dqu z \bigvee_{S \in \Sigma} \tau_{S}(z).

31: \]

32: The definition is thus extended to the full language $\ofoei$ as expected: 

33: given a $\ofoei$-sentence $\phi$, by Theorem~\ref{thm:bfofoei} and

34: Proposition~\ref{prop:bfofoei-sigmapi} we compute an equivalent

35: basic form $\bigvee \dbnfofoei{\vlist{T}}{\Pi}{\Sigma}$, with 

36: $\Sigma \subseteq \Pi \subseteq \vlist{T}$, and therefore we set

37: $\phi^{\tuniv}\isdef \bigvee (\dbnfofoei{\vlist{T}}{\Pi}{\Sigma})^{\tuniv}$.

38: \end{definition}

39: