Fonction valeur de vérité

Congru

Je propose ici de définir la fonction valeur de vérité. Je crois que ma méthode est plus naturelle que la méthode classique exposée dans le livre de Monsieur Dehornoy.

Plan:

1. Interprétation des termes clos

2. Substitution dans un terme

3. Substitution dans une formule

4. Fonction valeur de vérité

Congru

1. Interprétation des termes clos.

Soit $L$ un langage du premier ordre ayant des symboles de constante. Soit $J$ le langage obtenu en retirant à $L$ tout symbole de relation de $L$. Soit $(M;\iota )$ une $L$-structure. Soit $\tau _c L$ l'ensemble des termes clos de $L$.

Alors $\tau _c L$ a une structure canonique qui fait de lui une $J$-structure, notons $(\tau _c L; j)$ cette structure.

$(\tau _c L;j)$ est la $J$-structure libre de base $\emptyset $. Il existe donc un seul morphisme $(f;(\tau _c L; j);(M;\iota \restriction _J))$ de $J$-structures de source $(\tau _c L; j)$ et de but $(M;\iota \restriction _J)$.

Pour tout terme clos $t$ de $L$, on note $\overline t ^{(M;\iota)}:= ft$.

Edit. Si quelqu'un voulait bien m'aider à faire au moins un des chapitres, ça irait plus vite. Sinon je le ferais mais ça me prendra plus de temps.

Congru

2. Substitution dans les termes.

Contexte: Soit $L$ un langage du premier ordre.

Notations: 

a. On note $\tau L$ l'ensemble des termes de $L$. 

b. Notons $V$ l'ensemble des variables de $L$. 

c. Notons $\pi _1$ un prédicat fonctionnel unaire qui à tout couple associe sa première projection et notons $\pi _2$ un prédicat fonctionnel unaire qui à tout couple associe sa deuxième projection. 

d. On notera $[arity]f$ l'arité d'un symbole de fonction ou de relation de $L$. On note $[dom]$ un prédicat fonctionnel qui à toute application associe son domaine.

e. On notera $Mon$ monoïde libre de base "l'ensemble des symboles de fonction de $L$ union avec l'ensemble des symboles de variable de $L$".  

f. On notera (en préfixe) $\square $ le produit de $Mon$. 

g. On note $\square _{gen}$ le produit généralisé $Mon$

Construction du bienfondé ensembliste de travail: soit $A$ l'ensemble des triplets $(x;y;z)$ tels que $x\in \tau L$ et $y$ est une bijection de source un ordinal fini et de but une partie de $V$, et $z$ une application surjective de source la source de $y$ et de but inclus dans $\tau L$. Soit $B:=(A;\{z \vert \exists x\exists y((z=(x;y))\wedge (x\in A)\wedge (y\in A)\wedge ([profondeur]\pi _1\pi _1 x\in [profondeur]\pi _1\pi _1 y))\} )$.

Proposition: $B$ est une relation bienfondée.

Corollaire: Il existe une unique application surjctive $f$ de source $A$ telle que pour tous $x;y;z$ tels que $(x;y;z)\in A$:

a) si $x$ est de profondeur $0$ alors pour tout $j\in [dom]y$ tel que $x(0)=y(j)$ on a $f(x;y;z)=z(j)$

b) si $x$ est de profondeur $0$ et que $x(0)\notin [but]y$ on a $f(x;y;z)=x$

c) Pour tout symbole $g$ de fonction de $L$ et toute application $u$ de domaine $[arity]g$ et de but $\tau L$ tel que $x=\square \{ (0;g)\}  \square _{gen}\{ (k;u(k))\vert k\in [arity]g \} \} $, on a $f(x;y;z)= \square\{ (0;g)\}  \square _{gen}\{ (k;f(u(k);y;z)) \vert k\in [arity]g \} \}$

Preuve: $B$ est une relation bienfondée et $A=\pi _1B$, donc ceci est un cas d'application du théorème de récursion transfinie.

Définition: on note $[subst;L;\tau L]$ la fonction $f$.

Congru

Notation. Notons $[couple]$ le prédicat fonctionnel binaire qui à tous $a;b$ associe le couple $(a;b)$

Par définition, pour tous $x;y;z$, on a $(x;y;z)=[couple][couple]xyz$.

Donc, pour tous $x;y;z$, on a $\pi _1 (x;y;z)= \pi _1[couple][couple]xyz=[couple]xy$ et on a $\pi _2 (x;y;z)= \pi _2[couple][couple]xyz=z$ et on a $\pi _1\pi _1 (x;y;z)= \pi _1\pi _1[couple][couple]xyz=\pi _1[couple]xy=x$ et on a $\pi _2\pi _1 (x;y;z)= \pi _2\pi _1[couple][couple]xyz=\pi _2[couple]xy=y$

Congru

3. Substitution sur les formules.

Disclaimer: Je ne suis pas aussi formel que d'habitude ici car je manque de temps.

Contexte: On se donne un langage $L$ du premier ordre.

Notations: En plus des notations précédentes, on notera $[Rel]$ l'ensemble des symboles de relation de $L$ et on notera $\mathcal F L$ l'ensemble des formules de $L$.

Construction du bienfondé ensembliste de travail: soit $A'$ l'ensemble des triplets $(x;y;z)$ tels que $x\in  \mathcal FL$ et $y$ est une bijection de source un ordinal fini et de but une partie de $V$, et $z$ une application surjective de source la source de $y$ et de but inclus dans $\tau L$. Soit $B':=(A';\{z \vert \exists x\exists y((z=(x;y))\wedge (x\in A')\wedge (y\in A')\wedge ([profondeur]\pi _1\pi _1 x\in [profondeur]\pi _1\pi _1 y))\} )$.

Proposition: $B'$ est une relation bienfondée.

Définition: On définit

$F:=\left(\left(\bigvee\left\{ \begin{array}{c} \exists A\exists B\exists\alpha\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L\\ B\in\mathcal{F}L\\ \alpha\in\left\{ \wedge,\vee,\to,\leftrightarrow\right\} \\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\alpha AB\\ C_{_{2}}=\alpha\left(C_{_{1}}\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\left(C_{_{1}}\left(B,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right) \end{array}\right\} \right)\\ \exists A\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\lnot A\\ C_{_{2}}=\lnot\left(C_{_{1}}\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right) \end{array}\right\} \right)\\ \exists i\exists A\exists x\exists Q\left(\bigwedge\left\{ \begin{array}{c} x\in V\\ Q\in\left\{ \exists,\forall\right\} \\ i\in\left[dom\right]\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\\ x=\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(i\right)\\ A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=QxA\\ C_{_{2}}=Qx\left(C_{_{1}}\left(\begin{array}{c} A\\ \begin{cases} \begin{array}{ccc} \left(\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)-1 & \to & \left(\left[but\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\backslash\left\{ \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(i\right)\right\} \\ k<i & \mapsto & \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(k\right)\\ k\geq i & \mapsto & \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(k+1\right) \end{array}\end{cases}\\ \begin{cases} \begin{array}{ccc} \left(\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)-1 & \to & \left\{ \left(\pi_{_{2}}C_{_{0}}\right)\left(k\right)\vert\left(\bigwedge\left\{ \begin{array}{c} k\in\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\\ \left(\bigvee\left\{ \begin{array}{c} k\in i\\ i\in k \end{array}\right\} \right) \end{array}\right\} \right)\right\} \\ k<i & \mapsto & \left(\pi_{_{2}}C_{_{0}}\right)\left(k\right)\\ k\geq i & \mapsto & \left(\pi_{_{2}}C_{_{0}}\right)\left(k+1\right) \end{array}\end{cases} \end{array}\right)\right) \end{array}\right\} \right)\\ \exists A\exists x\exists Q\left(\bigwedge\left\{ \begin{array}{c} x\in V\\ \lnot\left(x\in\left[but\right]\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\right)\\ Q\in\left\{ \exists,\forall\right\} \\ A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=QxA\\ C_{_{2}}=Qx\left(C_{_{1}}\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right) \end{array}\right\} \right)\\ \exists R\exists h\left(\bigwedge\left\{ \begin{array}{c} R\in\left[Rel\right]\\ h\in\left(\tau L\right)^{\left[arity\right]R}\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;h\left(k\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \\ C_{_{2}}=\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;\left[subst;L;\tau L\right]\left(h\left(k\right);\pi_{_{2}}\pi_{_{1}}C_{_{0}};\pi_{_{2}}C_{_{0}}\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \end{array}\right\} \right)\\ \left(\pi_{_{1}}\pi_{_{1}}C_{_{0}}\notin\mathcal{F}L\right)\wedge\left(C_{_{2}}=\perp\right) \end{array}\right\} \right);\left(\begin{array}{c} C_{_{0}}\\ C_{_{1}}\\ C_{_{2}} \end{array}\right)\right) $

Preuve: $B'$ est une relation bienfondée ensembliste et $\pi _1B'=A'$ donc on est dans un cas d'application du théorème de récursion transfinie.

Définition: On note $[subst;L;\mathcal F L]$ la fonction $f$.

Edit. Je viens de revoir le poly, il y avait une coquille, c'est corrigé.

Congru

Ainsi, j'ai presque tous les outils pour définir la fonction "Valeur de vérité". Je vais juste rajouter quelques définitions minimes avant d'attaquer. (A suivre)

Congru

Définition: on définit

 $\Theta:=\begin{cases} \begin{array}{ccc} \left\{ \forall;\exists;\to;\leftrightarrow;\wedge;\vee;\lnot\right\} & \to & \bigcup\left\{ \begin{array}{c} Hom_{_{\mathcal{E}ns}}\left(2;2\right)\\ Hom_{_{\mathcal{E}ns}}\left(\left(2\right)\times\left(2\right);2\right)\\ Hom_{_{\mathcal{E}ns}}\left(\left(\mathcal{P}2\right)\backslash1;2\right)\\ Hom_{_{\mathcal{E}ns}}\left(\mathcal{P}2;2\right) \end{array}\right\} \\ \forall & \mapsto & \begin{cases} \begin{array}{ccc} \left(\mathcal{P}2\right)\backslash1 & \to & 2\\ a & \mapsto & \bigcap a \end{array}\end{cases}\\ \exists & \mapsto & \begin{cases} \begin{array}{ccc} \mathcal{P}2 & \to & 2\\ a & \mapsto & \bigcup a \end{array}\end{cases}\\ \to & \mapsto & \begin{cases} \begin{array}{ccc} \left(2\right)\times\left(2\right) & \to & 2\\ \left(a;b\right) & \mapsto & \bigcup\left\{ \begin{array}{c} 1-a\\ b \end{array}\right\} \end{array}\end{cases}\\ \leftrightarrow & \mapsto & \begin{cases} \begin{array}{ccc} \left(2\right)\times\left(2\right) & \to & 2\\ \left(a;b\right) & \mapsto & \bigcap\left\{ \begin{array}{c} \bigcup\left\{ \begin{array}{c} 1-a\\ b \end{array}\right\} \\ \bigcup\left\{ \begin{array}{c} 1-b\\ a \end{array}\right\} \end{array}\right\} \end{array}\end{cases}\\ \wedge & \mapsto & \begin{cases} \begin{array}{ccc} \left(2\right)\times\left(2\right) & \to & 2\\ \left(a;b\right) & \mapsto & \bigcap\left\{ \begin{array}{c} a\\ b \end{array}\right\} \end{array}\end{cases}\\ \vee & \mapsto & \begin{cases} \begin{array}{ccc} \left(2\right)\times\left(2\right) & \to & 2\\ \left(a;b\right) & \mapsto & \bigcup\left\{ \begin{array}{c} a\\ b \end{array}\right\} \end{array}\end{cases}\\ \lnot & \mapsto & \begin{cases} \begin{array}{ccc} 2 & \to & 2\\ a & \mapsto & 1-a \end{array}\end{cases} \end{array}\end{cases} $

raoul.S

Pourquoi cacher ta métaformule $F$ dans un poly ? il faut l'afficher fièrement

Congru

4. Fonction valeur de vérité.

Contexte: On se donne un langage du premier ordre $L$ et on se donne une $L$-structure $(M;\iota )$.

Notations: a. On se donne $j$ tel que $(M;j)$ est l'enrichissement de $(M;\iota)$ en $L_{(M;\iota )}$-structure. 

b. On notera $\mathcal F _c L_{(M;\iota )} $ l'ensemble des formules closes de $L_{(M;\iota )}$. 

c. On notera $[Rel]$ l'ensemble des symboles de ralation de $L$

d. Je rappelle que $V$ est l'ensemble des variables.

e. Pour tout ensemble A, on notera $\chi _A$ la fonction caractéristique de $A$

Construction du bienfondé de travail: Soit $A':=  \mathcal F _c L_{(M;\iota )} $. Soit $B':=(A';\{z \vert \exists x\exists y((z=(x;y))\wedge (x\in A')\wedge (y\in A')\wedge ([profondeur] x\in [profondeur] y))\} )$.

Proposition: $B'$ est une relation bienfondée.

On définit

$G':=\left(\bigvee\left\{ \begin{array}{c} \exists A\exists B\exists\alpha\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ B\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ \alpha\in\left\{ \wedge,\vee,\to,\leftrightarrow\right\} \\ C_{_{0}}=\alpha AB\\ C_{_{2}}=\left(\Theta\alpha\right)\left(C_{_{1}}\left(A\right);C_{_{1}}\left(B\right)\right) \end{array}\right\} \right)\\ \exists A\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ C_{_{0}}=\lnot A\\ C_{_{2}}=\left(\Theta\lnot\right)\left(C_{_{1}}\left(A\right)\right) \end{array}\right\} \right)\\ \exists A\exists x\exists Q\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ x\in V\\ Q\in\left\{ \exists,\forall\right\} \\ C_{_{0}}=QxA\\ C_{_{2}}=\left(\Theta Q\right)\left(\left\{ C_{_{1}}\left(\left[subst;L_{_{\left(M;\iota\right)}};\mathcal{F}L_{_{\left(M;\iota\right)}}\right]\left(A;\left\{ \left(0;x\right)\right\} ;\left\{ \left(0;a\right)\right\} \right)\right)\vert a\in M\right\} \right) \end{array}\right\} \right)\\ \exists R\exists h\left(\bigwedge\left\{ \begin{array}{c} R\in {\left[Rel\right]}\\ h\in\left(\tau L_{_{\left(M;\iota\right)}}\right)^{^{\left[arity\right]R}}\\ C_{_{0}}=\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;h\left(k\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \\ C_{_{2}}=\chi_{_{\iota\left(R\right)}}\left(\left\{ \left(k;\overline{h\left(k\right)}^{^{\left(M;j\right)}}\right)\vert k\in\left[arity\right]R\right\} \right) \end{array}\right\} \right)\\ \left(C_{_{0}}\notin\mathcal{F}L_{_{\left(M;\iota\right)}}\right)\wedge\left(C_{_{2}}=0\right) \end{array}\right\} \right)$ 

et on définit $G:=\left(G';\left(\begin{array}{c} C_{_{0}}\\ C_{_{1}}\\ C_{_{2}} \end{array}\right)\right) $

Proposition. Il existe une unique fonction surjective $f$ de domaine $A'$ telle que $\forall x(x\in A'\implies G(x;f\restriction _{_{{B'}^{-1}x}};f(x)))$

Preuve: $B'$ est une relation bienfondée ensembliste et $\pi _1B'=A'$ donc on est dans un cas d'application du théorème de récursion transfinie.

Définition: On note $\mathcal V _{(M;\iota )}$ la fonction $f$.

Edit. Je viens de me rendre compte que j'avais oublié de poster le poly, c'est corrigé.

Congru

@raoul.S les formules que je laisse dans les polis y sont parce que je n'arrive pas à les écrire sur le format du forum. Je ne maitrise pas assez le code pour cela.

Congru

Exemple d'application:

On considère le langage $L:=\{(+;2);(1;0)\}$ (les symboles sont $+$ et $1$, les autres informations sont les arités respectifs). On considère $\iota $ tel que   $(\mathbb Z;\iota )$ est la $L$ structure jouant le rôle de $(\mathbb Z ;+;1)$. Calculer $\mathcal V _{(\mathbb Z;\iota ) }(\forall x\exists yx=+y1)$.

Exercice piqué à ce fil: https://les-mathematiques.net/vanilla/discussion/2337920/dehornoy-logique-du-premier-ordre

Congru

Réponse: On a $\mathcal V _{(\mathbb Z;\iota ) }(\forall x\exists yx=+y1)=\bigcap \{ \mathcal V _{(\mathbb Z;\iota ) }(\exists ya=+y1)\vert a\in \mathbb Z \}=\bigcap \{  \bigcup \{ \mathcal V _{(\mathbb Z;\iota )}(a=+b1)\vert b\in \mathbb Z\} \vert a\in \mathbb Z \} \geq \bigcap \{  \mathcal V _{(\mathbb Z;\iota )}(a=+(a-1)1) \vert a\in \mathbb Z \} = \bigcap \{  1 \vert a\in \mathbb Z \} =1$

Congru

Edit. J'ai corrigé quelques coquilles dans les polys du "4." et du "3." et j'ai fait du renommage pour éviter un problème de capture. Normalement il n'y a plus aucune coquille.

Demande: Si quelqu'un a connaissance d'un texte où la fonction" valeur de vérité" est construite avec la même méthode que moi (c.à.d avec le même plan que moi), ce serait sympa de partager.

Georges Abitbol

Mmmmh, j'y pense, Congru, est-ce qu'il n'y a pas un langage de programmation qui dans lequel tu puisses compiler/vérifier ce que tu écris ?

Ou alors, au contraire, est-ce que tu écris toutes tes formules à la main ? Ou alors est-ce qu'elles sont générées par ordinateur (autre que toi ) ?

Congru

@Georges Abitbol au fait là j'ai adapté des formules que j'ai écrites il y a longtemps dans un cadre plus large. La difficulté a été d'adapter ces formules au contexte du fil et de faire moins formel, car j'avais peur de perdre tout lecteur potentiel. C'est un peu formel, mais l'original est beaucoup plus formel.

J'ai fait plusieurs preuves détaillées portant sur les formules de base (que j'ai adapté ici). En gros, j'applique beaucoup le même processus: créer une relation bienfondée, définir une formule fonctionnelle sur la classe des couples dont la première projection est un élément de la base que bienfondé et le second élément est une application, ensuite j'appliquer le théorème de récursion transfinie. Ma façon de définir la formule est basée sur un même modèle, c'est toujours une disjonction où dans les clauses respectives, je m'intéresse à tous les différents appels récursifs/inductifs.

J'ajoute que les coquilles que j'ai dû corriger ne sont pas présents dans les formules originales, elles sont seulement apparues lors de la transformation des formules originales pour les adapter au contexte et aussi faire moins formel.

Vassillia

Congru a dit :

La difficulté a été d'adapter ces formules au contexte du fil et de faire moins formel, car j'avais peur de perdre tout lecteur potentiel.

Bonjour,

Bon objectif @Congru, je te soutiens dans cette démarche, mais j'ai peur qu'il ne soit pas encore tout à fait atteint.

C'est encore beaucoup trop formel donc beaucoup trop illisible pour la quasi totalité des gens, même qui comprennent les maths, et qui savent ce qu'est une valeur de vérité. Ceci explique que les gens ne répondent pas ou ironisent, je te le précise comme tu m'as dit avoir du mal à comprendre les blagues.

Quant à la prétention de faire plus naturel que Dehornoy ou autres spécialistes en logique, tu aurais peut-être mieux fait de t'abstenir et te contenter de le présenter comme une définition alternative mais ce n'est que mon avis.

Congru

Vassillia a dit :

Quant à la prétention de faire plus naturel que Dehornoy ou autres spécialistes en logique, tu aurais peut-être mieux fait de t'abstenir et te contenter de le présenter comme une définition alternative mais ce n'est que mon avis.

Tout à fait d'accord avec toi, mais mon but n'était pas d'être prétentieux. Je ne me compares pas à Monsieur Dehornoy loin de là, d'ailleurs je vais enfin pouvoir lire son livre dont j'ai déjà lu quelques extraits qui m'ont appris beaucoup de choses.

Il me semble que la façon de définir cette fonction exposée dans l'extrait du livre de Monsieur Dehornoy est plutôt classique et non spécifique à Monsieur Dehornoy lui même (si je fais erreur, j'en suis désolé). Ma mention de Monsieur Dehornoy n'est dû que au fait que je citais en quelque sorte l'autre fil et de mon point de vue c'est plus naturel de définir cette fonction comme cela. Je ne dis pas que c'est "mieux", la comparaison "mieux" n'aurait aucun sens. Ma définition est plus longue et utilise d'autres notions (c'est pourquoi il a fallut 4 étapes), donc c'est moins efficace que la méthode classique. Et je n'aurais jamais trouvé tout seul et naturellement la méthode classique contrairement à celle que j'expose ici. Il n'y a absolument aucune tentative de "faire la grosse tête" ici.

Edit. J'ai failli modifier le titre suite à ton commentaire, mais en relecture, je vois que j'ai bien précisé "méthode classique". Donc ce que tu dis ne ma parait pas objectif, mais il est probable que d'autres partagent ton interprétation de ce que j'ai écrit...En espérant que tout se soit éclaircit.

Congru

Vassillia a dit :

Bonjour,

....et qui savent ce qu'est une valeur de vérité...

C'est assez difficile de "savoir ce qu'est une valeur de vérité", tu vois ce n'est pas un groupe, ce n'est pas un polynôme. Là ce que je définis est une fonction qui a une formule close paramétrée quelconque (langage et modèle donné) associe $0$ ou $1$, et je l'appelle "fonction valeur de vérité".

Vassillia

Et bien voilà, tu vois que tu peux faire du non formel, ton explication en une ligne me va tout à fait.

Foys

Ces constructions sont en fait informatiques. Je recommande pour s'autoformer et être à l'aise d'écrire une classe "formule de logique du premier ordre" dans votre langage préféré, idéalement un assistant de preuve pour établir au fur et à mesure la correction des constructions.
J'avais écrit ce code il y a quelques temps: https://pastebin.com/KfCCrVhd
Il compile avec la version de js coq disponible sur leur site (pas besoin de télécharger quoi que ce soit du coup): https://coq.vercel.app/

L'idée que le formel est un ajout artificiel sur les maths qui empêcherait leur compréhension est aussi aberrante que l'idée que le langage machine et l'assembleur seraient des ajouts artificiels sur javascript et python. Les maths ont un contenu bas niveau et celui-ci devrait être diffusé le plus largement possible.

Vassillia

Perso, pour un code ayant la même finalité, je trouve la version python plus lisible que la version assembleur et donc j'ai appris directement à coder en python. Je ne nie pas qu'il est transformé en langage machine derrière (transformation nécessaire pour l'assembleur ou le code de Foys aussi d'ailleurs qui doit être compilé) mais ce n'est pas mon problème. Je n'en ai aucun besoin. J'affirme en revanche que rendre la programmation obligatoire en assembleur nuirait à la compréhension du code et je doute que n'importe qui ayant vraiment codé une seule fois dans sa vie me contredise.

Foys a dit :

Les maths ont un contenu bas niveau et celui-ci devrait être diffusé le plus largement possible.

La première partie de la phrase est vraie, la seconde est une opinion mais rien ne t’empêche de diffuser. Si tu n'as pas de récepteur à ta diffusion, c'est ton problème mais comme @Congru parlait d'avoir des lecteurs, je lui suggère de ne pas faire la même erreur et il fera ce qu'il veut de cette suggestion.

Médiat_Suprème

@Vassilia, je parle ici d'expérience : comprendre les pointeurs en C, est considéré comme un pont-aux-ânes de la programmation, ceux qui ont fait un peu d'assembleur avant, ne se rendent même pas compte qu'il y a peut-être une difficulté pour d'autres. Il y a d'autres façons de gommer cette "difficulté", mais à titre pédagogique, c'est démonstratif.

PS : je ne pense pas que Foys dise qu'il faut tout écrire en assembleur (langage formel), mais que sa connaissance facilite la suite et stimule la créativité.

Vassillia

Je connais les pointeurs car j'ai eu un prof à la fac qui m'a fait faire du C à une époque, à posteriori, je pense que c'était une perte de temps. Je ne m'en sers plus du tout donc ... pas convaincue par la démonstration, il n'y en a pas en python, java... des langages haut niveau où les objets sont passés par valeur.

Médiat_Suprème

Je pense que vous n'avez pas compris mon allégorie (ni la deuxième phrase du premier paragraphe)

Vassillia

Possible mais je pense que vous avez, et c'est bien normal, envie de défendre votre discipline de prédilection sans vraiment vous occuper de l’intérêt réel dans une formation mais on ne va pas revenir sur l’intérêt, cette histoire est sans fin.

Je n'ai rien contre la logique, surtout sa présentation par les informaticiens,  je pense aussi qu'elle peut apporter beaucoup, mais j'ai quelque chose contre les gens qui disent qu'il faut absolument faire comme eux ils disent car sinon point de salut.

Médiat_Suprème

Je suis en train de vous dire que les gens qui savent (en gros) ce qu'est un embrayage et une boite de vitesse apprennent plus vite que les autres (c'est un fait) et vous me répondez "je m'en fous, j'ai une automatique", c'est votre droit, mais cela n'invalide pas le constat.

Ni Foys (à en juger par ses interventions) ni moi ne sommes concernés, par votre deuxième phrase, limite insultante.

PS : je ne sais pas comment vous savez de quoi je me préoccupe ou pas.

Autant en rester là

gerard0

Voila le débat entre ceux qui ont appris à programmer dans les temps héroïques des "micro-ordinateurs" et les programmeurs de maintenant. D'ailleurs, à l'époque, certains trouvaient que l'assembleur était déjà une facilité, et qu'on ne pouvait programmer en assembleur correctement que si on avait une formation en électronique afin d'être capable de programmer "en dur".

Mais considérer que connaître la programmation en assembleur (lequel, d'ailleurs ? Certains assembleurs actuels sont plus évolués que le basic du Z81) est nécessaire à la programmation en langage de haut niveau est une vieille idée inutile.

NB : J'ai programmé en assembleur un langage de haut niveau dans mes jeunes années.

Cordialement.

Médiat_Suprème

Bien évidemment, tout le monde aura compris que là n'est pas le débat, poser la question "lequel d'ailleurs" est la preuve patente de la non-compréhension de ce débat !

Pour enfoncer le dernier clou : cela n'a que peu d'intérêt, aujourd'hui, de programmer en assembleur, par contre savoir comment marche un processeur, cela aide (et l'assembleur permet de bien comprendre ce point, même si ce n'est pas la seule solution).

gerard0

Si ce n'est pas le débat, pourquoi Foys en a-t-il parlé ?

Ou comment un contre argument se détruit de lui-même ... jusqu'à être retiré ("même si ce n'est pas la seule solution").

Et toujours des réponses hautaines, désagréables ("preuve patente de la non-compréhension") et bien évidemment fausse.

Médiat_Suprème

Oui Miss Teschmacher

gerard0

Voilà, on passe aux insultes ... pensée pauvre.

Karnaj

Bonjour, concernant le « il n'y en a pas en python, java... des langages haut niveau où les objets sont passés par valeur ». Non, les objets sont passés par référence dans beaucoup de langages (dont les deux cités), pas par valeur, ce qui cause d'ailleurs de nombreuses incompréhensions lorsqu'on enseigne le langage (par exemple des modifications de tableaux non attendues).

Vassillia

Mouais disons que tu peux modifier les attributs de l'objet mais pas l'objet lui-même. Pour moi, l'objet est passé par valeur et l'accès aux attributs de l'objet se fait par référence ce qui peut effectivement causer des surprises.

Karnaj

Oui, c'est vrai que dans certains langages, on considère la modification de l'objet par affectation pour dire qu'on fait des passages par référence. Mais il y en a d'autres où avec x = t on n'essaie pas de modifier un objet, mais une variable. Avec ça en tête, ça n'a pas vraiment de sens de parler de modifier les attributs de l'objet ou de modifier l'objet lui-même. Modifier l'objet lui-même, c'est modifier ses attributs.
Mais en tout cas, je veux pouvoir dire que les objets sont passés par valeur en C. Tout ce qu'on passe est copié, et la modification dans la fonction n'affectera que la copie. Passer un pointeur, c'est passer une adresse par valeur (la valeur de l'adresse passée en paramètre est copiée), et la modification du pointeur (pas de la valeur pointée) dans la fonction n'a aucun effet sur le pointeur qui a été passé par valeur. Et ça m'embêterait de dire qu'en C comme en Python, les objets sont passés par valeur.

Foys

Les tableaux 100 x 100, on n'a pas envie de les passer par valeur ...

Foys

@gerard0 a écrit:
Si ce n'est pas le débat, pourquoi Foys en a-t-il parlé ?

Le sujet du débat, c'est-à-dire du fil lui-même, est la définition de la valeur de vérité d'une formule (quantifiée notamment), autrement dit d'une notion qui exploite directement et incontournablement la nature syntaxique des objets concernés. Autant dire que l'antiformalisme militant rampant qu'on voit parfois sur le forum est largement hors-sujet ici.

Quand à la digression sur la programmation bas niveau, même s'il ne met pas tout le monde d'accord, le choix pédagogique de faire faire de l'assembleur (sans parler du C) aux étudiants de formations en informatique existe encore aujourd'hui, par exemple à l'école 42. Même s'ils n'écriront jamais dans de tels langages dans leur vie professionnelle cela leur apporte une conscience des mécanismes sous-jacents qui est irremplaçable.

Karnaj

Foys a dit :

Les tableaux 100 x 100, on n'a pas envie de les passer par valeur ...

Merci au C (non, pas merci), une expression de type tableau de <type> est convertie en expression pointeur sur <type> (qui pointe sur le premier élément du tableau), sauf quand elle est l'opérande de sizeof, de &, ou une chaîne littérale pour initialiser un tableau. Voir la section 6.3.2 des différents brouillons de la norme (pas sûr de la section pour C11). Donc quand on écrit f(t) où t est un tableau, c'est un pointeur qui est passé par valeur. On ne peut juste pas passer un tableau en paramètre. Enfin, si on veut être chafouin, on peut déclarer une structure dans laquelle on place un gros tableau, et là on passera un gros objet par valeur. Mais effectivement, on a pas vraiment envie de faire ça...
Mais bon, c'est pas trop le sujet, on peut la continuer dans une autre discussion si ça intéresse des gens.

Vassillia

 Autant dire que l'antiformalisme militant rampant qu'on voit parfois sur le forum est largement hors-sujet ici.

Euh, c'est @Congru lui même qui a parlé d'être trop formel, tu sais l'auteur de ce fil auquel tu n'as pas répondu et tu te goures si tu crois que c'est mon genre de ramper

Congru

Je l'ai déjà dit, le formalisme est l'avenir des mathématiques, et les informaticiens (je ne parle même pas des mathématiciens-informaticiens comme notre ami Heuristique ) maitrisent en général cette partie des mathématiques bien mieux que la plupart des mathématiciens. Je ne suis pas en train de devenir anti-formaliste, au contraire, je suis en train de ramener les anti-formalistes vers le formalisme à petites goutes

Edit. Je viens de me relire, je n'ai jamais dit "trop formel".

Congru

Foys a dit :

Ces constructions sont en fait informatiques. Je recommande pour s'autoformer et être à l'aise d'écrire une classe "formule de logique du premier ordre" dans votre langage préféré, idéalement un assistant de preuve pour établir au fur et à mesure la correction des constructions.
J'avais écrit ce code il y a quelques temps: https://pastebin.com/KfCCrVhd
Il compile avec la version de js coq disponible sur leur site (pas besoin de télécharger quoi que ce soit du coup): https://coq.vercel.app/

L'idée que le formel est un ajout artificiel sur les maths qui empêcherait leur compréhension est aussi aberrante que l'idée que le langage machine et l'assembleur seraient des ajouts artificiels sur javascript et python. Les maths ont un contenu bas niveau et celui-ci devrait être diffusé le plus largement possible.

Merci @Foys

Vassillia

@Congru Tu as dit que la difficulté a été d'être moins formel, de là à penser que sinon tu es trop formel.

Mais admettons, c'est une interprétation, c'est toute la puissance et la faiblesse du langage humain, il y a souvent plusieurs interprétations. En tout cas, je plussoie ton idée, pour ramener les anti-formalistes dans ton camp, il faut faire un pas vers eux et donner des versions non formalisées tout en proposant par la suite une version plus formelle pour plus de précisions si besoin. Plusieurs niveaux de lecture pour contenter tout le monde, c'est sûrement le mieux.

Je sais pour l'avenir mais ce sera aidé par des assistants de preuves nouvelle génération qui seront largement plus efficace exactement comme les langages de programmation évoluent, comme l'IA évolue...

Georges Abitbol

@Congru : Ce que je voulais dire c'est que, si je n'ai aucun doute que quand tu écris ces formules, elles sont claires pour toi, elles le sont moins pour d'autres (qui n'ont pas ton "intention" en tête). Le travail de "compréhension" de tes formules étant peu ou prou équivalent à un calcul que ferait un ordinateur, je me disais qu'il devrait y avoir un format plus adapté à donner à tes productions, afin qu'elles soient compréhensibles et testables par d'autres.

Congru

D'accord @Georges Abitbol, je vais reformuler le "3." et le "4."

Congru

3'. Substitution dans les formules

Contexte: On se donne un langage $L$ du premier ordre.

Notations: On reprend les notations du "3.", on notera $[Rel]$ l'ensemble des symboles de relation de $L$ et on notera $\mathcal F L$ l'ensemble des formules de $L$. Je rappelle que $V$ est l'ensemble des variables.

Construction du bienfondé ensembliste de travail: soit $A'$ l'ensemble des triplets $(x;y;z)$ tels que $x\in  \mathcal FL$ et $y$ est une bijection de source un ordinal fini et de but une partie de $V$, et $z$ une application surjective de source la source de $y$ et de but inclus dans $\tau L$. Soit $B':=(A';\{z \vert \exists x\exists y((z=(x;y))\wedge (x\in A')\wedge (y\in A')\wedge ([profondeur]\pi _1\pi _1 x\in [profondeur]\pi _1\pi _1 y))\} )$.

Proposition. $B'$ est une relation bienfondée.

Proposition. Il existe une unique application surjective $f$ de domaine $A'$ telle que pour tout $C_0 \in A'$ la conjonction des énoncés suivants est vérifiée:

a. $\forall A\forall B\forall\alpha\left(\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L\\ B\in\mathcal{F}L\\ \alpha\in\left\{ \wedge,\vee,\to,\leftrightarrow\right\} \\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\alpha AB \end{array}\right\} \right)\implies f\left(C_{_{0}}\right)=\alpha\left(f\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\left(f\left(B,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\right)$

b. $\forall A\left(\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\lnot A \end{array}\right\} \right)\implies\left(f\left(C_{_{0}}\right)=\lnot\left(f\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\right)\right) $

c. $\forall i\forall A\forall x\forall Q\left(\left(\bigwedge\left\{ \begin{array}{c} x\in V\\ Q\in\left\{ \exists,\forall\right\} \\ i\in\left[dom\right]\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\\ x=\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(i\right)\\ A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=QxA \end{array}\right\} \right)\implies\left(f\left(C_{_{0}}\right)=Qx\left(f\left(\begin{array}{c} A\\ \begin{cases} \begin{array}{ccc} \left(\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)-1 & \to & \left(\left[but\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\backslash\left\{ \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(i\right)\right\} \\ k<i & \mapsto & \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(k\right)\\ k\geq i & \mapsto & \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(k+1\right) \end{array}\end{cases}\\ \begin{cases} \begin{array}{ccc} \left(\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)-1 & \to & \left\{ \left(\pi_{_{2}}C_{_{0}}\right)\left(k\right)\vert\left(\bigwedge\left\{ \begin{array}{c} k\in\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\\ \left(\bigvee\left\{ \begin{array}{c} k\in i\\ i\in k \end{array}\right\} \right) \end{array}\right\} \right)\right\} \\ k<i & \mapsto & \left(\pi_{_{2}}C_{_{0}}\right)\left(k\right)\\ k\geq i & \mapsto & \left(\pi_{_{2}}C_{_{0}}\right)\left(k+1\right) \end{array}\end{cases} \end{array}\right)\right)\right)\right) $

d. $\forall A\forall x\forall Q\left(\left(\bigwedge\left\{ \begin{array}{c} x\in V\\ \lnot\left(x\in\left[but\right]\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\right)\\ Q\in\left\{ \exists,\forall\right\} \\ A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=QxA \end{array}\right\} \right)\implies f\left(C_{_{0}}\right)=Qx\left(f\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\right)$

e. $\forall R\forall h\left(\left(\bigwedge\left\{ \begin{array}{c} R\in\left[Rel\right]\\ h\in\left(\tau L\right)^{\left[arity\right]R}\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;h\left(k\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \end{array}\right\} \right)\implies\left(f\left(C_{_{0}}\right)=\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;\left[subst;L;\tau L\right]\left(h\left(k\right);\pi_{_{2}}\pi_{_{1}}C_{_{0}};\pi_{_{2}}C_{_{0}}\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \right)\right) $

Preuve. $B'$ est une relation bienfondée ensembliste et $\pi _1B'=A'$ donc on est dans un cas d'application du théorème de récursion transfinie.

Définition. On note $[subst;L;\mathcal F L]$ la fonction $f$.

Edit. La conjonction des énoncés, je la note ainsi $\left(\bigwedge\left\{ \begin{array}{c} \forall A\forall B\forall\alpha\left(\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L\\ B\in\mathcal{F}L\\ \alpha\in\left\{ \wedge,\vee,\to,\leftrightarrow\right\} \\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\alpha AB \end{array}\right\} \right)\implies f\left(C_{_{0}}\right)=\alpha\left(f\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\left(f\left(B,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\right)\\ \forall A\left(\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\lnot A \end{array}\right\} \right)\implies\left(f\left(C_{_{0}}\right)=\lnot\left(f\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\right)\right)\\ \forall i\forall A\forall x\forall Q\left(\left(\bigwedge\left\{ \begin{array}{c} x\in V\\ Q\in\left\{ \exists,\forall\right\} \\ i\in\left[dom\right]\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\\ x=\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(i\right)\\ A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=QxA \end{array}\right\} \right)\implies\left(f\left(C_{_{0}}\right)=Qx\left(f\left(\begin{array}{c} A\\ \begin{cases} \begin{array}{ccc} \left(\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)-1 & \to & \left(\left[but\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\backslash\left\{ \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(i\right)\right\} \\ k<i & \mapsto & \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(k\right)\\ k\geq i & \mapsto & \left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\left(k+1\right) \end{array}\end{cases}\\ \begin{cases} \begin{array}{ccc} \left(\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)-1 & \to & \left\{ \left(\pi_{_{2}}C_{_{0}}\right)\left(k\right)\vert\left(\bigwedge\left\{ \begin{array}{c} k\in\left[dom\right]\pi_{_{2}}\pi_{_{1}}C_{_{0}}\\ \left(\bigvee\left\{ \begin{array}{c} k\in i\\ i\in k \end{array}\right\} \right) \end{array}\right\} \right)\right\} \\ k<i & \mapsto & \left(\pi_{_{2}}C_{_{0}}\right)\left(k\right)\\ k\geq i & \mapsto & \left(\pi_{_{2}}C_{_{0}}\right)\left(k+1\right) \end{array}\end{cases} \end{array}\right)\right)\right)\right)\\ \forall A\forall x\forall Q\left(\left(\bigwedge\left\{ \begin{array}{c} x\in V\\ \lnot\left(x\in\left[but\right]\left(\pi_{_{2}}\pi_{_{1}}C_{_{0}}\right)\right)\\ Q\in\left\{ \exists,\forall\right\} \\ A\in\mathcal{F}L\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=QxA \end{array}\right\} \right)\implies f\left(C_{_{0}}\right)=Qx\left(f\left(A,\pi_{_{2}}\pi_{_{1}}C_{_{0}},\pi_{_{2}}C_{_{0}}\right)\right)\right)\\ \forall R\forall h\left(\left(\bigwedge\left\{ \begin{array}{c} R\in\left[Rel\right]\\ h\in\left(\tau L\right)^{\left[arity\right]R}\\ \pi_{_{1}}\pi_{_{1}}C_{_{0}}=\left\{ \left(0;\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;h\left(k\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \right)\right\} \end{array}\right\} \right)\implies f\left(C_{_{0}}\right)=\left\{ \left(0;\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;\left[subst;L;\tau L\right]\left(h\left(k\right);\pi_{_{2}}\pi_{_{1}}C_{_{0}};\pi_{_{2}}C_{_{0}}\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \right)\right\} \right) \end{array}\right\} \right) $

Congru

Avant de poursuivre, est-ce que le "3'." est assez clair ? @Georges Abitbol

Congru

4'. Fonction valeur de vérité

Contexte: On se donne un langage du premier ordre $L$ et on se donne une $L$-structure $(M;\iota )$.

Notations: a. On se donne $j$ tel que $(M;j)$ est l'enrichissement de $(M;\iota)$ en $L_{(M;\iota )}$-structure. 

b. On notera $\mathcal F _c L_{(M;\iota )} $ l'ensemble des formules closes de $L_{(M;\iota )}$. 

c. On notera $[Rel]$ l'ensemble des symboles de ralation de $L$

d. Je rappelle que $V$ est l'ensemble des variables.

e. Pour tout ensemble A, on notera $\chi _A$ la fonction caractéristique de $A$

Construction du bienfondé de travail: Soit $A':=  \mathcal F _c L_{(M;\iota )} $. Soit $B':=(A';\{z \vert \exists x\exists y((z=(x;y))\wedge (x\in A')\wedge (y\in A')\wedge ([profondeur] x\in [profondeur] y))\} )$.

Proposition: $B'$ est une relation bienfondée.

Proposition: il existe une unique application surjective $f$ de domaine $A'$ telle que pour tout $C_0 \in A'$ la formule suivante est vérifiée:

$\left(\bigvee\left\{ \begin{array}{c} \exists A\exists B\exists\alpha\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ B\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ \alpha\in\left\{ \wedge,\vee,\to,\leftrightarrow\right\} \\ C_{_{0}}=\alpha AB\\ f\left(C_{_{0}}\right)=\left(\Theta\alpha\right)\left(f\left(A\right);f\left(B\right)\right) \end{array}\right\} \right)\\ \exists A\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ C_{_{0}}=\lnot A\\ f\left(C_{_{0}}\right)=\left(\Theta\lnot\right)\left(f\left(A\right)\right) \end{array}\right\} \right)\\ \exists A\exists x\exists Q\left(\bigwedge\left\{ \begin{array}{c} A\in\mathcal{F}L_{_{\left(M;\iota\right)}}\\ x\in V\\ Q\in\left\{ \exists,\forall\right\} \\ C_{_{0}}=QxA\\ f\left(C_{_{0}}\right)=\left(\Theta Q\right)\left(\left\{ f\left(\left[subst;L_{_{\left(M;\iota\right)}};\mathcal{F}L_{_{\left(M;\iota\right)}}\right]\left(A;\left\{ \left(0;x\right)\right\} ;\left\{ \left(0;a\right)\right\} \right)\right)\vert a\in M\right\} \right) \end{array}\right\} \right)\\ \exists R\exists h\left(\bigwedge\left\{ \begin{array}{c} R\in {\left[Rel\right]}\\ h\in\left(\tau L_{_{\left(M;\iota\right)}}\right)^{^{\left[arity\right]R}}\\ C_{_{0}}=\bigcup\left\{ \begin{array}{c} \left\{ \left(0;R\right)\right\} \\ \left\{ \left(k+1;h\left(k\right)\right)\vert k\in\left[arity\right]R\right\} \end{array}\right\} \\ f\left(C_{_{0}}\right)=\chi_{_{\iota\left(R\right)}}\left(\left\{ \left(k;\overline{h\left(k\right)}^{^{\left(M;j\right)}}\right)\vert k\in\left[arity\right]R\right\} \right) \end{array}\right\} \right) \end{array}\right\} \right) $

Preuve: $B'$ est une relation bienfondée ensembliste et $\pi _1B'=A'$ donc on est dans un cas d'application du théorème de récursion transfinie.

Définition: On note $\mathcal V _{(M;\iota )}$ la fonction $f$.

Congru

Vassillia a dit :

@Congru Tu as dit que la difficulté a été d'être moins formel, de là à penser que sinon tu es trop formel.

Mais admettons, c'est une interprétation, c'est toute la puissance et la faiblesse du langage humain, il y a souvent plusieurs interprétations. En tout cas, je plussoie ton idée, pour ramener les anti-formalistes dans ton camp, il faut faire un pas vers eux et donner des versions non formalisées tout en proposant par la suite une version plus formelle pour plus de précisions si besoin. Plusieurs niveaux de lecture pour contenter tout le monde, c'est sûrement le mieux.

Je sais pour l'avenir mais ce sera aidé par des assistants de preuves nouvelle génération qui seront largement plus efficace exactement comme les langages de programmation évoluent, comme l'IA évolue...

Très bonne suggestion, je vais tenter cela.

Congru

J'avais déjà programmé la fonction substitution dans le cas du lambda calcul dans mon fil d’implémentation du lambda calcul. Je pourrais à la rigueur implémenter un langage du premier ordre assez simple ainsi qu'une de ses structures, ensuite je pourrait transformer ces formules en programmes récursifs pour le langage et la structure donnés.

Sinon, je ne vois pas trop où sont les difficultés à comprendre, je suis ouvert aux questions, mais personne n'en pose.

raoul.S

Sinon, je ne vois pas trop où sont les difficultés à comprendre, je suis ouvert aux questions, mais personne n'en pose.

Je réponds pour moi : la logique mathématique m'a toujours intéressé. Mais ce qui m'intéresse vraiment en logique, comme partout en math, c'est en gros des résultats avec du contenu : genre théorèmes de complétude et d'incomplétude (je ne suis pas allé beaucoup plus loin).

À mon avis tu te focalise sur "des détails" qui à moi personnellement ne m'intéressent pas. Alors oui ce sont des détails utiles, mais pour accéder à des choses plus intéressantes. Pour moi le formalisme n'est pas une fin en soi.

Par exemple, je ne vais pas passer des heures à formaliser le fait que les deux formules $\forall x (x=x)$ et $\forall y (y=y)$ sont "équivalentes". Ce sont des détails qui en logique ne m'intéressent pas.

Petite anecdote : lorsque j'étais à l'université, mon prof de géométrie devait vérifier la commutativité de je ne sais plus quoi, mais ça impliquait un calcul très fastidieux bien que simple. Alors après l'avoir fait il a dit quelque chose dans le genre : ce calcul vous le faites une fois dans votre vie pour vérifier et puis c'est tout.

Ce que tu fais avec ta fonction valeur de vérité a déjà été fait (fastidieusement) dans les bouquins de logique. C'est une partie fastidieuse, pourquoi revenir dessus ? Enfin ça c'est mon avis en tout cas.

Congru

@raoul.S Je ne partage pas ton point de vue, quand j'étudie un domaine mathématique, il faut que je me l'approprie. Je refais tout de A à Z. Par exemple, en logique j'ai mes propres construction des termes d'un langage, des formules...

Il n'y a aucune zone d'ombre que je me permets. Peu importe si ça a été fait un million de fois de façon fastidieuse.

J'ai d'ailleurs ma propre construction des polynômes avec des choses purement formelles. Le théorème de Complétude est d'ailleur un théorème qui vise à faire une équivalence (sous conditions) entre sémantique et syntaxique/formel.

raoul.S

Je ne partage pas ton point de vue

Je sais. C'est pour ça que tu ouvres des fils auxquels quasiment personne ne participe...