Formules du premier ordre

1) soit $A$ un ensemble donné, on considère
$A':=\bigcup \{ Hom_{\mathcal E ns}(n,A)\mid n\in \mathbb N \}$
Et on considère $*:A'^2\to A'$ qui à $(u,v)\in A'^2$ associe l'application $w:(dom(u)+dom(v))\to A$ telle que pour tout $z\in dom(u)$, on a $w(z)=u(z)$ et pout tout $z\in (dom(u)+dom(v))\backslash(dom(u))$, on a $w(z)=v(z-(dom(u)))$.
Alors $(A',*,(0;A;0))$ est le monoïde libre de base $A$.

Édit.  J'avais oublié le $\bigcup$ dans la définition de $A'$.
Edit2. Un symbole est sorti lors d'une modification automatique (ou peut-être une modification de la modération), j'avais mal écris le symbole. (C'est $\backslash$)

@Math Coss tes remarques sont très pertinentes, cependant j'ai corrigé mon erreur 3 minutes avant ta remarque, mais je te remercie quand même d'avoir observé l'erreur et d'avoir tenté de le signaler.

Notation. Pour tout ensemble $A$, on note $Mon(A)$ le monoïde libre de base $A$, et on note $\Pi _A$ la généralisation de la loi du monoïde $Mon(A)$.

2) Ici, par langage fonctionnel, j'entends tout couple $(A,a)$ tel que $a$ est une application de $A$ dans $\mathbb N$ et l'image réciproque de $\{0\}$ par $a$  est non vide.
(En gros je considère les éléments de $A$ comme des symboles de fonction dont l'arité est donnée par $a$)

3) On se donne un langage fonctionnel $(A,a)$, soient $A',*$ tels que $Mon(A)=(A',*,(0;A;0))$, soit $B$ l'ensemble des $z\in \mathcal P (A')$ tels que pour tout $ f\in A$, pour tout $u\in Hom_{\mathcal Ens} (a(f),A')$, si $im(u)\subseteq z$ alors $*((1;A;\{(0;f)\}),\Pi _A (u))\in z$.
On a $A'\in B$, donc on a $B\not = \emptyset$, donc $\bigcap B$ est défini.
On dit que  $\bigcap B$ est l'ensemble des termes du langage fonctionnel $(A,a)$.
(ici j'ai donné une définition par le haut 🙂)
Édit. Pour éviter une possible ambiguïté, j'ai remplacé $A'^{a(f)}$ par $Hom_{\mathcal Ens} (a(f),A')$ et j'ai amélioré la rédaction.

4) Ici, j'ai une approche très personnelle, commençons par une petite remarque: "pour toute variable $x$, $\forall x$ est un quantificateur".

a) on se donne un ensemble
$c:=\{ \to, \wedge, \vee, \lnot, \leftrightarrow \}$ à 5 éléments. On suppose qu'aucun de ces éléments n'est une application.
(On verra pourquoi après)
b) on se donne une bijection $v$ de domaine $\mathbb N$
(ici l'image de $v$ sera notre ensemble de variables)

c) on se donne deux bijections $e$ et $u$ de domaine $\mathbb N$. 
On suppose qu'aucun élément de $\bigcup \{im(e),im(u)\}$ n'est une application.
(Ici les images respectifs de $e$ et $u$ sont respectivement les quantificateurs existentiels et universels)

d) on se donne un objet mathématique $\sim$ 
(Ici, $\sim$ jouera le rôle du symbole d'égalité)

d') on se donne deux ensembles $F$ et $R$, on suppose que $\sim \in R$.
(Ici $F$ et $R$ sont respectivement les ensembles des symboles de fonction et de relation)

e) on se donne deux applications $a_F$ et $a_R$ respectivement de domaines $F$ et $R$ et chacun de but $\mathbb N$. On suppose que $a_R (\sim)= 2$.
(Ici, les deux fonctions sont les fonctions arité)

f) on suppose $\emptyset =\bigcap \{F,im(v)\}$ et on suppose $\emptyset =\bigcup \{ \bigcap \{a,b\} \vert a,b\in \{im(e),im(u),c\} \}$

g) On dit que $(c,v,e,u,\sim,(F,a_F),(R,a_R))$ est un langage du premier ordre.

5) On se donne un langage du premier ordre $L$, soient $c,v,e,u,\sim,F,a_F,R,a_R$ tels que $L=(c,v,e,u,\sim,(F,a_F),(R,a_R))$. On définit $F':=\bigcup \{F,im(v)\}$, on note $a_{F'}$ l'application de domaine $F'$ et de but $\mathbb N$ qui à tout élément $z\in F$ associe $a_F (z)$ et qui à tout élément de $im(v)$ associe $0$.
$(F',a_{F'})$ est un langage fonctionnel.
On appelle terme de $L$ tout élément de l'ensemble des termes du langage fonctionnel $(F',a_{F'})$, et on notera $\tau (L)$ l'ensemble des termes du langage fonctionnel $(F',a_{F'})$.

Édit. J'ai modifié la remarque du début pour la rendre plus pédante. 🙂