La logique IF (Independence-Friendly), littéralement « respectueuse de l'indépendance » est une extension de la logique standart du premier ordre, qui a été conçue en 1989 par Jaakko Hintikka, logicien et philosophe finlandais (1929 Vantaa - 2015 Porvoo) et Gabriel Sandu, logicien et philosophe finlandais, professeur de philosophie théorétique à l'université de Helsinki.
Considérons un prédicat binaire `P"(.,.)"`. Et considérons la propriété suivante :
`AAx EEy, P(x,y)`
Cette propriété signifie littéralement : « quelques soit l'élément `x`, il existe un élément `y` tel que `P(x,y)` »
Et si pour chaque valeur de `x` on choisie une valeur `y` telle que `P(x,y)`, comme cela est possible d'après la proposition, en passant en revue tous les éléments, ce qui demandera un temps infini, on finira par construire un opérateur unaire que l'on note également `y"(.)"` satisfaisant la propriété suivante :
`AAx, P(x,y(x))`
Par ce raisonnement, nous obtenons l'équivalence de Skolem qui porte le nom de son auteur Thoralf Skolem (1887-1963) mathématicien et logicien norvégien. Cette équivalence s'écrit dans la logique du second ordre comme suit :
`AAx EEy, P(x,y) <=> EEy"(.)" AAx, P(x,y(x))`
La formule `EEy"(.)" AAx, P(x,y(x))` s'appelle la skolémisée de `AAx EEy, P(x,y)`. Elle est du second ordre car il y a deux types de variables, des éléments variables tel que `x` et des opérateurs variables tel que `y"(.)"`.
D'après la loi De Morgan généralisée aux ensembles infnis et à la logique du second ordre, la négation d'une formule n'utilisant que les quantificateurs `EE, AA` et les connecteurs `¬,^^,vv`, s'obtient toujours très facilement en inversant les quantificateurs `EE` et `AA`, en inversant les connecteurs `^^` et `vv` et en négativant chaque littéraux.
La contraposé de l'équivalence de Skolem produit l'équivalence de Herbrand, du nom de son concepteur, Jacques Herbrand (1908 Paris - 1931 La Bérarde), mathématicien et logicien français.
Considérons un prédicat binaire `Q"(.,.)"`. L'équivalence de Herbrand est :
`EEx AAy, Q(x,y) <=> AAy"(.)" EEx, Q(x,y(x))`
La formule `AAy"(.)" EEx, Q(x,y(x))` s'appelle la herbrandisée de `AAx EEy, Q(x,y)`. Elle est du second ordre car il y a deux types de variables, des éléments variables tel que `x` et des opérateurs variables tel que `y"(.)"`.
Considérons un prédicat quaternaire `P"(.,.,.,.)"`. Et considérons la propriété suivante :
`AAx EEu AAy EEv, P(x,u,y,v)`
Le choix de `u` dépend de `x` et le choix de `v` dépent de `(x,y)`. La skolemisée est :
`EEu"(.)" EEv"(.,.)" AAx AAy, P(x,u(x),y,v(x,y))`
Parcontre si nous prenons comme hypothèse que le choix de `v` peut ne dépendre que de `y` alors il faut enrichir la notation pour pouvoir l'exprimer au premier ordre. On utilise à cet effet les quantificateurs de Henkin, ou bien on explicite les dépendances :
`AAx EEu AAy (EEv"/"AAx), P(x,u,y,v)` `AAx EEu{x} AAy EEv{y}, P(x,u,y,v)`
Cette propriété signifie littéralement : « Quelques soit `x`, il existe `u`, quelque soit `y`, il existe `v` indépendament de `x` tel que `P(x,u,y,v)` ». La skolemisée est :
`EEu"(.)" EEv"(.)" AAx AAy, P(x,u(x),y,v(y))`
Considérons deux prédicats unaires `P"(.)"` et `Q"(.)"`. Et considérons la propriété suivante :
`AAx, P(x) ("∨/"AAx) Q(x)`
L'expression `("∨/"AAx)` désigne un connecteur "ou", notée `vv`, qui est indépendant de `x`. C'est à dire qu'il faut choisire l'un ou l'autre des arguments du connecteur mais de façon indépendante de la valeur de `x`. La formule skolemisée est :
`EE B() AAx, (P(x)"∧"B()) vv (Q(x)"∧¬"B())`
où `B"()"` est un prédicat zéro-aire, autrement dit une variable booléenne. La formule s'avère être équivalente à :
`(AAx P(x)) vv (AAx, Q(x))`
Considérons maintenant deux prédicats quaternaires `P"(.,.,.,.)"` et `Q"(.,.,.,.)"`. Et considérons la propriété suivante :
`AAxEEaAAyAAz, P(x,a,y,z) ("∨/"AAx) Q(x,a,y,z)`
La formule skolemisée est :
`EE B"(.,.)" EE a"(.)" AAx AAy, (P(x,a(x),y,z)"∧"B(y,z)) vv (Q(x,a(x),y,z)"∧¬"B(y,z))`
La négation d'une formule utilisant les quantificateurs `EE, AA` avec la notation de Henkin ainsi que les connecteurs `¬,^^,vv` avec la notation de Henkin, s'obtient toujours facilement en inversant les quantificateurs `EE` et `AA`, en inversant les connecteurs `^^` et `vv` et en négativant chaque littéraux.
D'après le chapitre 4, nous avons :
`AAx EEu AAy EEv, P(x,u,y,v) <=> EEu"(.)" EEv"(.,.)" AAx AAy, P(x,u(x),y,v(x,y))`
`AAx EEu AAy (EEv"/"AAx), P(x,u,y,v) <=> EEu"(.)" EEv"(.)" AAx AAy, P(x,u(x),y,v(y))`
Par contraposé et en notant la négation `Q"(.,.,.,.)" = "¬"P"(.,.,.,.)"`, on obtient :
`EEx AAu EEy AAv, Q(x,u,y,v) <=> AAu"(.)" AAv"(.,.)" EEx EEy, Q(x,u(x),y,v(x,y))`
`EEx AAu EEy (AAv"/"EEx), Q(x,u,y,v) <=> AAu"(.)" AAv"(.)" EEx EEy, Q(x,u(x),y,v(y))`
Les mêmes propositions s'écrivent en notation dépendance explicite comme suit :
`AAx EEu{x} AAy EEv{x,y}, P(x,u,y,v) <=> EEu"(.)" EEv"(.,.)" AAx{u,v} AAy{u,v}, P(x,u(x),y,v(x,y))`
`AAx EEu{x}AAy EEv{y}, P(x,u,y,v) <=> EEu"(.)" EEv"(.)" AAx{u,v} AAy{u,v}, P(x,u(x),y,v(y))`
`EEx AAu{x}EEy AAv{x,y}, Q(x,u,y,v) <=> AAu"(.)" AAv"(.,.)" EEx{u,v} EEy{u,v}, Q(x,u(x),y,v(x,y))`
`EEx AAu{x}EEy AAv{y}, Q(x,u,y,v) <=> AAu"(.)" AAv"(.)" EEx{u,v} EEy{u,v}, Q(x,u(x),y,v(y))`
D'après le chapitre 5, nous avons :
`AAx, P(x) ("∨/"AAx) Q(x) <=> EE B"()" AAx, (P(x)"∧"B()) vv (Q(x)"∧¬"B()) <=> (AAx P(x)) vv (AAx, Q(x))`
Par contraposé et en notant les négations `R"(.)" = "¬"P"(.)"` et `S"(.)" = ¬Q"(.)"`, on obtient :
`EEx, R(x) ("∧/"EEx) S(x) <=> AA B"()" EEx, (R(x)"∨¬"B() ^^ (S(x)"∨"B()) <=> (EEx R(x)) ^^ (EEx, S(x))`
D'après le chapitre 5, nous avons :
`AAx EEu AAyAAz, P(x,u,y,z) ("∨/"AAx) Q(x,u,y,z) <=> EE B"(.,.)" EE u"(.)" AAx AAy, (P(x,u(x),y)"∧"B(y,z)) vv (Q(x,u(x),y)"∧¬"B(y,z))`
Par contraposé et en notant les négations `R"(.,.,.)" = "¬"P"(.,.,.)"` et `S"(.,.,.)" = ¬Q"(.,.,.)"`, on obtient :
`EEx AAu EEy EEz, R(x,u,y,z) ("∧/"EEx) Q(x,u,y,z) <=> AA B"(.,.)" AA u"(.)" EEx EEy, (R(x,u(x),y)"∨¬"B(y,z)) ^^ (S(x,u(x),y)"∨"B(y,z))`
Etant donné la proposition suivante :
`AAx EEy, P(x,y)`
Sa forme skolémisée est :
`EEy"(.)" AAx, P(x,y(x))`
Si on herbranise, on obtient :
`AAx"(.)", EEy"(.)" , P(x(y),y(x(y)))`
On note `Omega` la catégorie des éléments. Nous avons :
`y "∈" (Omega"→"Omega)`
`x "∈" ((Omega"→"Omega)"→"Omega)`
Il convient de trouver une notation plus explicite pour ne pas confondre les différents types. Voici la succession des skolémisations-herbranisations
`AAx "∈" Omega EEy "∈" Omega, P(x,y)`
`EEy "∈" (Omega"→"Omega), AAx "∈" Omega , P(x,y(x))`
`AAx "∈" ((Omega"→"Omega)"→"Omega), EEy "∈" (Omega"→"Omega), P(x(y),y(x(y)))`
`EEy "∈" (((Omega"→"Omega)"→"Omega)"→"(Omega"→"Omega))AAx "∈" ((Omega"→"Omega)"→"Omega), P(x(y(x)),y(x)(x(y(x))))`
Noter le terme `y(x)(x(y(x)))` qui signifie que `y` s'applique à `x` pour produire un résultat intermédiaire qui est en suite appliqué à `x(y(x))`.
---- 16 septembre 2018 ----
Puisque on ne veut pas s'investire de toute la mathématique mais de la seul logique. On construit la structure sur laquelle reposera le raisonnement, à partir du seul langage logique et de ses constructions syntaxiques appelées règles de déduction. Ou autrement dit, on construit la sémantique à partir de la seul syntaxe. On construit le modèle censé satisfaire la théorie à partir de la théorie elle-même.
Une théorie sans quantificateur telle que décrite précédement comprend implicitement un langage, le langage dont la présentation est constituée des opérateurs et prédicats qui sont mentionnés au moins une fois dans la théorie. En cela, il y a bien dans la théorie, une partie déclarative qui déclare les opérateurs et prédicats utilisés, et donc qui déclare un langage.
Une structure est l'association d'un langage `L` et d'une théorie `T` écrite dans ce langage, et on la représente sous forme d'un quotient
`L"/"T`
Il est toujours possible d'ajouter au langage placé au numérateur de nouveaux opérateurs et de nouveaux prédicats. Et il est toujours possible d'ajouter à la théorie placée au dénominateur des propositions supplémentaires écrites dans le langage placé au numérateur.
La structure `L"/"T` est l'ensemble des éléments engendrés par `L`, muni des opérateurs et prédicats de la présentation du langage `L`, et satisfaisant la théorie `T`.
`"<"L">"` représente l'ensemble des éléments engendrés par `L`
`"<"T">"` représente l'ensemble des théories engendrées par `T`
Pour toutes théories `A`, `B` écrites dans le langage `L`, on note `A|--B` pour signifier que la théorie `B` se déduit de la théorie `A` à l'aide des règles de déduction que nous allons décrire, et cela signifie que `B` est engendrée par `A`, c'est à dire que `B in "<"A">"`, ou encore que `"<"B">" sube "<"A">"`.
L'engendrement se fait par un procédé calculatoire, et donc n'engendre par principe que des ensembles énumérables. Il existe un procédé de calcul qui énumère tous les éléments de `"<"L">"` et toutes les théories de `"<"T">"`. Les règles de déduction forment un énumérateur qui appliqué à une théorie `A` va énumérer toutes les déductions possibles exprimables dans le langage `L`. Ainsi, si une théorie se déduit de `A` alors l'énumérateur produira en un temps fini cette théorie. Par contre si la théorie n'est pas déduisible de `A` nous n'avons aucun procédé qui nous assure de pouvoir le découvrir en un temps fini. Autrement dit, le complément de `"<"T">"` dans l'ensemble de toutes les théories exprimables dans le langage `L` peut ne pas être énumérable.
La théorie vide qui correspond à la conjonction vide, notée `"⊤"` (ou notée `{}`, ou notée true, ou notée `1`) est toujours vrai. Elle engendre l'ensemble `"<⊤>"` qui est l'ensemble de toutes les totologies écrivables dans le langage `L`.
La théorie incohérente, notée `"⊥"` (ou notée false, ou notée `0`) est toujours fausse. Elle engendre l'ensemble `"<⊥>"` qui est l'ensemble de toutes les théories écrivables dans le langage `L`.
Une telle structure `L"/"T` peut être floue, et ainsi en quelque sorte, être dans plusieurs états à la fois.... Par analogie à la mécanique quantique, la structure se comporte comme un système physique pouvant se trouvant dans plusieurs états quantiques à la fois. On considère que son état est déterminé si et seulement si la théorie `T` est complète pour l'égalité c'est à dire que pour tout couple de termes `u` et `v` appartenant à `L^•`, la théorie doit toujours trancher la question en temps fini, si `u` est égal ou non à `v` en tant qu'élément. Autrement dit, la théorie `T` doit satisfaire la propriété suivante :
`AAu"∈"L^•, AAv"∈"L^•, (T|--u"="v) vv (T|--u"≠"v)`
La relation d'égalité définie dans `T` forme une relation d'équivalence sur la structure libre `L^•`, et les classes d'équivalences de termes forment les éléments. La notation `L"/"T` pour désigner la structure, prend alors tout sont sens comme étant la division de l'ensemble `L^•` par la relation d'équivalence qu'est l'égalité `"=(.,.)"` définie par `T`, une division en des parties de taille non nécessairement égale que sont les classes d'équivalences de termes. Les éléments de la structure `L"/"T` sont exactement les classes d'équivalences de termes de `L^•`.
La complétude de `T` pour l'égalité entraine que chaque élément de la structure est un sous-ensemble énumérable de `L^•` dont le complément dans `L^•` est également énumérable.
Mais la plus part du temps la théorie `T` n'est pas complète pour l'égalité. Dans ce cas, selon l'adage des intuitionnistes comme quoi il n'y a rien au delà de l'infini, l'incomplétude de la théorie sur l'égalité entres deux termes `u` et `v`, ne s'interprète alors que de trois façons possibles qui sont les trois sens que l'on peut donner à l'assertion suivante :
`(T"⊬"u"="v) ^^ (T"⊬"u"≠"v")`
Cela signifie que `T` ne tranche pas la théorie `{u=v}`, ou dit autrement que `T` est indépendant de la théorie `{u=v}`. Et donc que :
T ^^u=v est cohérent
Soit on considère que les éléments `u` et `v` sont distincts mais d'une distinction non déclarée. Soit on considère qu'il sont égaux mais d'une égalité non déclarée. Soit on considère un troisième état logique ni distinct ni égaux, qui entre alors dans le cadre d'une logique ternaire.
On dira que `u` et `v` sont indiscernable si et seulement si `T"⊬"u"≠"v"`
Les deux premier cas définissent deux relations d'équivalences, la relation dite d'indiscernablité noté `~_T`, et une relation plus étroite dite d'égalité déclaré notée `=_T`.
`u~_Tv <=> (T"⊬"u"≠"v)`
`=_T`<=> (T"⊢"u"≠"v)`
-----------
On note u=v si et seulement si T|-u=v. L'égalité ainsi définie forment une relation d'équivalence sur `L^•` :
Reflexive : `Ax, x"="x`
Symétrique : `AxAy, x"="y => y"="x`
Transitive : `AxAyAz, (x"="y ^^ y="z) =>x"="z`
Une variable est désignée par toute nouvelle lettre minuscule ne figurant pas dans la présentation du langage. La variable est un nouvel opérateur et possède une arité. La variable enrichie le langage. On parlera de l'univers de Herbrand étendu, du langage étendu. Le procédé consistant à ajouter ces nouveaux opérateurs s'appelle une extension.
L'extension est dite élémentaire si le nouvel opérateur `x` ajouté est d'arité nulle. L'opérateur est ajouté dans le langage `L`, c'est à dire dans sa présentation, et on obtient un nouveau langage que l'on note `L[x]` :
`L = {a,f"(.)",g"(.,.)"}`
`L[x] = {a,x,f"(.)",g"(.,.)"}`
Et on obtient une nouvelle structure que l'on note `S[x]` :
`S = L"/"T`
`S[x] = L[x]"/"T`
L'extension est dite intérieure si on ajoute à la théorie la condition `x"∈"L`. Et l'extension est dite extérieure si on ajoute à la théorie la condition inverse `x"∉"L`.
Il est possible de procéder à plusieurs extensions élémentaires à la suite. Par exemple on note `S[x][y][z]` simplement `S[x,y,z]`, une extension de la structure `S` par trois nouveaux opérateurs d'arité nulle `x,y,z`.
L'extension est dite unaire si le nouvel opérateur `h` ajouté est d'arité un. L'opérateur est ajouté dans le langage `L`, c'est à dire dans sa présentation, et on obtient un nouveau langage que l'on note `L[h"(.)"]` :
`L = {a,f"(.)",g"(.,.)"}`
`L[h"(.)"] = {a,f"(.)",h"(.)",g"(.,.)"}`
Et on obtient une nouvelle structure que l'on note `S[h"(.)"]` :
`S = L"/"T`
`S[h"(.)"] = L[h"(.)"]"/"T`
L'extension est dite intérieure si on ajoute à la théorie la condition `AAx, h(x)"∈"L`. L'extension est dite extérieure si on ajoute à la théorie la condition inverse `EEx, h(x)"∉"L`.
Il est possible de procéder à plusieurs extensions à la suite, et par exemple on note `S[x][h"(.)"]` simplement `S[x,h"(.)"]`.
(à simplifier)
Un morphisme est une application entre deux structures de même patronage qui respecte la forme. Mais pour comprendre cette phrase, il faut définir ce qu'est un patronage. Comme reconnait-on deux structures de même patronage ?. Il faut pouvoir définir un langage commun aux deux structures. Il faut pouvoir associer de façon biunivoque, en respectant les arités, les opérateurs générateurs d'une structure avec les opérateurs générateurs de l'autre structures. La signature de leur langage doit donc être identique.
La signature d'un langage d'opérateurs est la liste des nombres d'opérateurs pour chaque arité. Par exemple la signature de `L` est `(1,1,1)` car la présentation de `L` contient exactement `1` opérateur d'arité nulle, `1` opérateur unaire et `1` opérateur binaire.
Mais une même signature de langage ne suffit pas, il convient en plus de disposer les opérateurs de même arités selon un ordre précis. Le patronage de la structure ou de son langage, c'est la signature du langage, mais dans lequel on ajoute en plus, un ordre total dans chaque groupe d'opérateurs ayants la même arité.
Un patronage est donc quelque chose d'un peu plus riche que la présentation anonymisée d'un langage. Il incorpore ces ordres. Par convention, le patronage se présente sous forme d'une liste sachant que l'ordre n'a d'importance que dans les groupes d'opérateurs de même arité. Par exemple considérons les deux patronages de signature `(1,2)` suivants :
`L_1 = (a,f"(.)",h"(.)")`
`L_2 = (a,h"(.)",f"(.)")`
L'ordre d'apparition de `f"(.)"` par rapport à `h"(.)"` joue un rôle. Les patronages `L_1` et `L_2`, sont distincts. Le patronage `L_1` admet comme premier opérateurs unaire, l'opérateur `f"(.)"`, et comme second opérater unaire, l'opérateur `h"(.)`. Parcontre, en terme de langage d'opérateurs, ce sont deux mêmes langages, mais celui-ci ne sera pas le langage commun.
Etant donné un patronage utilisant des opérateurs non prédéfinie, l'arité d'un opérateur et sa position au sein du groupe de même arité suffit à détermine l'opérateur. C'est pourquoi deux structures de même patronage possède un langage commun, le langage obtenu en renomant les opérateurs par leur caractéristiques comprenant leur arité et l'ordre s'il y en a plusieurs de même arité.
Le patronage permet d'anonymiser tout langage d'opérateurs.
Un morphisme est relatif à un patronage. Le morphisme doit respecter chaque opérateur du patronage qui constitue un langage commun à plusieurs structures. Par exemple considérons deux structures de même patronage :
`S_1 = (a_1, f_1"(.)", g_1"(.,.)") "/" T_1`
`S_2 = (a_2, f_2"(.)", g_2"(.,.)") "/" T_2`
Il y a une correspondance biunivoque des opérateurs entre les deux structures comme suit :
`((a_1|->a_2), (f_1|->f_2), (g_1|->g_2))`
Cette correspondance fait qu'il est possible de parler d'un unique langage qui peut être interprété dans l'une ou l'autre structure.
Une application `varphi` de `S_1 -> S_2` est un morphisme si et seulement si quelques soient `x` et `y` appartenant à `S_1` nous avons :
`varphi(a_1)=a_2`
`varphi(f_1(x))=f_2(varphi(x))`
`varphi(g_1(x,y))=g_2(varphi(x),varphi(y))`
Si de plus le morphisme est injectif alors c'est un plongement et la structure `S_1` est abstraitement inclus dans `S_2`, ce qui se note `S_1"↪"S_2` ou plus précisement `S_1"↪"_varphi S_2`
Si de plus le morphisme est bijectif alors c'est un isomorphisme, et les deux structures sont dite isomorphes, ce qui se note `S_1 ~= S_2` ou plus précisement `S_1 ~=_varphi S_2`
--- 14 octobre 2017 ---
Considérons une variable `x` appartenant à `L`. Cela constitue une extension interieur de la structure `L`. Puis considérons la proposition `AAx B(x)`. Le quantificateur `AA` appliqué à la variable `x` correspond à un `"et"` logique intégré sur l'ensemble des valeurs possibles de `x` c'est à dire sur l'ensemble des éléments de la structure `L`
L'opérateur `"et"` est représenté par le symbole `^^` similaire à l'intersection. Nous avons :
`(AAx B(x)) <=> ^^^_(x in L) B(x)`
L'ensemble des valeurs possible de `x`, qui est l'ensemble sous-jacent de la structure `L`, est par principe énumérable. Cela entraine que la proposition `AA x, P(x)` est réfutable en un temps fini dans le cas où celle-ci serait fausse. Et il s'agit là d'une périssologie car on définie justement la valeur logique fausse de cette proposition par le fait qu'elle doit être réfutée en un temps fini. Parcontre dans le cas où elle ne serait pas fausse, on remarquera qu'elle n'est pas assurement affirmable en un temps fini. Et en effet, on verra que l'affirmation d'une telle proposition peut dans certain cas constituer un oracle.
En tant qu'idée mathématique sans contrainte matériel ni temporelle d'aucune sorte, on peut se placer à l'infini des temps et ainsi connaître l'oracle. Mais il faut en quelque sorte, être immortel dans un monde immortel et de surcroit régit par une mécanique classique, somme-toute, des présupposés assurement faux, mais qui à notre échelle sont approximativement vrai. Si on adopte ce principe qui correspond au présuposé des mathématiques, à savoir que le monde dans le quel est développé cette mathématique perdure éternellement et est régis par une mécanique abstraite mais classique, et que nous pouvons nous placer abstraitement à l'infini des temps et ainsi connaitre la valeur logique de la proposition, alors toutes les propositions exprimables dans notre langage ont une valeur logique bien définie.
La négation de cette propostion s'obtient simplement en inversant les quantificateurs et en négativant les combinaisons selon une loi de Morgane étendu aux suites énumérables.
`¬(AAx B(x)) <=> (EEx ¬B(x))`
`¬(EEx B(x)) <=> (AAx ¬B(x))`
Le quantificateur `EE` appliqué à la variable `x` correspond à un `"ou"` intégré sur l'ensemble des valeurs possible de `x`. L'opérateur `"ou"` est représenté par le symbole `vv` similaire à l'union. Nous avons :
`(EEx B(x)) <=> vvv_(x in L) B(x)`
Même remarque que précédement, cette proposition, dans le cas où elle ne serait pas vrai, n'est pas assurement réfutable en un temps fini. La réfutation d'une telle proposition peut dans certain cas constituer un oracle.
Le `AA x` constituant un `"et"` logique intégré sur `L`, et le `EE y` constituant un `"ou"` logique intégré sur `L`, nous pouvons conclure un certain nombre de règles sur les quantificateurs.
--- 25 septembre 2017 ---
On considère considère la variables booléennes `A`, les prédicats `B(.), C(.)` et le prédicat `R(.,.)`, qui peuvent être définis librement dans la théorie de la structure. Nous avons :
Distributivité du `"ou"` par rapport au `"et"` :
`(AAx B(x)) "ou" (AAy C(y)) `
`(^^^_(x in L) B(x)) "ou" (^^^_(y in L) C(y))`
`(B(1) "et" B(2) "et" B(3) "et" ...) "ou" (C(1) "et" C(2) "et" C(3) "et" ...)`
`^^^_((x,y) in L^2) B(x) "ou" C(y))`
`AA(x,y) B(x) "ou" C(y)`
Distributivité du `"ou"` par rapport au `"et"` :
`(AAx B(x)) "ou" (EEy C(y)) `
`(^^^_(x in L) B(x)) "ou" (vvv_(y in L) C(y))`
`(B(1) "et" B(2) "et" B(3) "et" ...) "ou" (C(1) "ou" C(2) "ou" C(3) "ou" ...)`
`^^^_((x,y) in L^2) B(x) "ou" C(y))`
`AA(x,y) B(x) "ou" C(y)`
Associativité du `"et"` : Associativité du `"ou"` : Indépendance de `y` par rapport à `x`
<=>
=><=>
<=>
brouillon : theorie3
Et pour les élémentariens, cet ensemble est un ensemble d'éléments énumérable quelconque. Et cela revient à dire que l'on se place dans l'ensemble des entiers naturels `bbbN`. Et ce n'est pas un infini immanent puisqu'il se construit par un processus récurcif. Le seul postulat est notre capacité d'abstraction à nous projeter aussi loin que l'on veut dans le temps, et à concevoir l'oracle, c'est à dire à se placer à la fin des temps pour le vérifier.