Formules du premier ordre
Vu les questions récurrentes dans le sous-forum logique, je propose qu'on donne ici au moins deux constructions de l'ensemble des formules d'un langage du premier ordre $L$ donné.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
En gros, je pars de 0. N'hésitez pas à proposer vos propres solutions pour chaque étape, j'ai une foule de choses à faire dont plusieurs projets en suspension là, donc je ne suis pas sûr d'écrire ceci en un temps raisonnable sans ressentir trop de culpabilité.
$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$)
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.
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. 🙂
Soient $A',*$ tels que $Mon(\bigcup \{R,\tau (L)\})=(A',*,(0;\bigcup \{R,\tau (L)\});0))$.
On définit $At(L):=\{*(( 1;\bigcup \{R,\tau (L)\};\{(0;u')\}),\Pi _{\bigcup \{R,\tau (L)\}} (v'))\vert u'\in R \bigwedge v'\in Hom_{\mathcal E ns} (a_R (u'),A')\bigwedge im(v')\subseteq \{ (1; \bigcup \{R,\tau (L)\}; \{(0;t)\})\vert t\in \tau (L) \} \}$
7) On se donne l'application $a_c$ de source $\bigcup \{c,im(e),im(u),At(L)\}$ et de but $\mathbb N$ qui à tout élément de $\bigcup \{ im(e),im(u)\}$ associe $1$ et à $\lnot$ associe $1$ et à tout élément de $c\backslash \{ \lnot \}$ associe $2$, et à tout élément de $At(L)$ associe $0$.
$(\bigcup \{c,im(e),im(u),At(L)\},a_c)$ est un langage fonctionnel, on note $Formule(L)$ l'ensemble des termes du langage fonctionnel $(\bigcup \{c,im(e),im(u),At(L)\},a_c)$.
Notation. Pour tout $i\in \mathbb N$, on note $\forall v(i):=u(i)$ et on note $\exists v(i):=e(i)$
Remarque. La raison pour laquelle j'ai demandé que certains symboles ne soient pas des applications était pour m'assurer qu'aucun d'entre eux ne puisse appartenir à l'ensemble des formules atomiques.
Édit. J'avais oublié $\bigcup$ à deux instances de $(\bigcup \{c,im(e),im(u),At(L)\},a_c)$, c'est corrigé. Si vous voyez une erreur, signalez le s'il vous plaît.
Édit2. Encore un $\bigcup$ oublié, cette fois ci, c'était dans $\bigcup \{ im(e),im(u) \}$, c'est corrigé.