"Trouver le bon langage de présentation du problème résoud déjà la moitié du problème". En appliquant cette adage, on cherche un langage formel plus pertinant pour exposer les propositions logiques du premier ordre. Il nous faut une formalisation la plus simple tout en étant la plus expressive sémantiquement.
La présentation d'un langage logique passe par la déclaration de prédicat dits générateurs. On procède à trois simplifications :
`P(x,y,z,t) = P(x,y)`
Dans ces expressions, chaque argument "point" ou manquant représente une nouvelle variable libre (c-à-d non quantifiées ni ne faisant partie du langage). La currification ainsi que la non prise en compte des arguments surnuméraires, ramène la déclaration d'existence d'un prédicat dans le langage, d'un point de vue informationnel, à celle d'un unique prédicat d'arité déterminée, `n` ou `oo`. Dans le cas d'une arité infinie, le prédicat ne donne jamais de réponse, c'est pourquoi on exclus par principe ce cas.
Délors, chaque prédicat possède une arité entière. Et celle-ci doit être déclaré dans la présentation du langage. On le fait en adjoignant en suffixe une liste de "point" correspondant au nombre d'arguments attendus.
L'argument "point" joue alors le rôle d'une nouvelle variable muette s'insérant dans la liste des variables libres lues de gauche à droite. Considérons par exemple un prédicat binaire `P(".,.")` et considérons la formule:
`AAx, P(x,y) => EEz, P(z,".") => P(".",x)`
Cette formule nommé `varphi` possède 3 variables libres que l'on peut explicité comme suit:
`varphi = (y,x_1,x_2 |-> AAx, P(x,y) => EEz, P(z,x_1) => P(x_2,x))`
Chaque formule possède ainsi une arité qui est le nombre de variables libres, d'arguments "point" ou d'arguments manquants aux différents prédicats générateurs présents dans la formule. L'ordre des variables arguments d'une formule est celui de l'ordre d'apparition des variables libres et des arguments "point" ou des arguments manquants dans la formule lue de gauche à droite.
La grammaire énumère toutes les formules qui, regroupées, forment donc un ensemble énumérable noté `sfF`. Un programme rudimentaire calcul l'arité de la formule. Ainsi toutes les formules d'arité `n` sont énumérées par un procédé effectif et forment donc un ensemble énumérable noté `sfF_n`. Ainsi :
Cette première étape où l'on semble être revenu au point de départ, est importante pour nous libérer d'une syntaxe un peu trop corsetée. Elle va nous permetrre d'entrevoir des formes syntaxiquement plus simple du langage logique du premier ordre, et de satisfaire l'adage: « Dans tout problème, le choix du bon langage, et donc de sa bonne formulation, constitue la moitier de sa résolution ».
Le langage de la théorie des ensembles est `{"∈"(".,.")}`. On ne mentionne pas le prédicat d'égalité ni l'élément "point" qui sont spéciaux et propres au langage du premier ordre. La théorie `sfT` est un ensemble de propositions engendré par la grammaire suivante :
Grammaire de la théorie des ensembles : `sfQ ← {AA, EE}` # Quantificateurs `sfV← {x_1,x_2,x_3,...}` # Variables élémentaires `sfB← {sfV, "."}` # Variables élémentaires plus le "point" `sfL← {"⊤", sfB"="sfB, sfB"∈"sfB }` # Littéraux affirmatifs `sfF← {sfL,"¬"sfF, sfQsfV & sfF, sfF"⇔" sfF, sfF"⇒" sfF, sfF"∧" sfF, sfF"∨"sfF}` # Formules `sfT← {`
`AA A AA B&(AAx & x"∈"A<=> x "∈"B) <=> A"="B,`
`AAaAAbEEpAAx & x "∈"p<=> (x"="a ∨ x"="b),`
`AAE EE R AAx & x"∈"R<=> (EE p & x"∈"p ∧ p"∈"E"),`
`AAE EEP AA A & A"∈"P <=> (AAx & x"∈"A => x"∈"E),`
`AAE EE S AAx & x"∈"S<=> (x"∈"E ∧ sfF_1(x))`
`}`# Théorie des ensembles
Où `sfF_1` est le sous-ensemble énumérable des formules unaire de `sfF`.
Pour parfaire la présentation, il faut définir ce qu'est une démonstration formelle en logique des prédicats. Il faut décrire le langage des démonstrations. C'est l'objet de la discussion Logique du premier ordre.
Zermelo pose ici les premiers axiomes dans la logique du premier ordre, d'une théorie des ensembles, qui ouvre de multiple voix de développements et nous amène à de nombreuses interrogations.
La formalisation proposée a quelques défauts. Le choix d'omettre les arguments surnuméraires nuit à la puissance d'expression sémantique du langage. C'est une perte d'information qui peut être enlevée en adoptant un point de vue un peu plus générale sur les varibales élémentaires. Cela se fait en manipulant non pas des variables élémentaires mais des vecteurs de variables élémentaires. Cela est rendu possible en appliquant la logique polonaise, et en répétant autant de fois que nécessaire le prédicat pour produire des vecteurs de variables booléennes. Ainsi considérons un prédicat binaire `P(".,.")` et un vecteur de variables élémentaitres `vecx = (a,b,c,d,e)`. La composition va transmettre les arguments surnuméraires tels quels dans l'ordre comme arguments du même prédicat répété plusieurs fois de suite, assurant ainsi potentiellement sous l'arbitraire de `P` aucune perte d'information.
`vecx = (a,b,c,d,e)` #vecteur élémentaire `P(vecx) = (P(a,b),P(c,d), P(e,"."))` #vecteur booléen
Et la logique polonaise s'applique aussi pour les connecteurs logiques mais sans répéter le connecteur car il n'y a plus nécessité, les arguments surnuméraires sont simplement transmis tels quels dans l'ordre assurant ainsi aucune perte d'information. Faisant que par exemple `"⇒"(vecx)` s'interprète comme suit:
`"⇒"(vecx) = "⇒"(a,b,c,d) = (a"⇒"b, c,d,e)`
Les formes de langage logique ayant une grande liberté syntaxique sans perte d'information potentiel comme celui-ci sont rares, ce qui dénote leur pertinence.
Les opérations booléennes fondamentales ont été choisies parmi celles opérant sur deux arguments booléens au plus. Dans la nouvelle optique où nous opérons non pas sur deux booléens mais sur une liste de taille variable de booléens, les opérations logiques de base sont apriori différentes. Passons les candidats en revue, Le "et" et le "ou" ensembliste, l'équivalence ensembliste, la disjonction exclusive, l'implication successive, la négation:
`"¬"(x,y,z) = "¬"x "et" "¬"y "et" "¬"z` # Négation. `"¬"()="⊤"` `"∧"(x,y,z) = x "et" y "et" z` # Et ensembliste. `"∧"()="⊤"` `"∨"(x,y,z) = x "ou" y "ou" z` # Ou ensembliste. `"∨"() ="⊥"` `"⇔"(x,y,z) = (x"⇔"y) "et" (y"⇔"z)` # Équivalence ensembliste. `"⇔"()="⊤"` `"⊕"(x,y,z) = (x "et" "¬"y "et" "¬"z) "ou"`
`("¬"x "et" y "et" "¬"z) "ou"`
` ("¬"x "et" "¬"y "et" z) `# Disjonction exclusive. `"⊕"() ="⊥"` `"⇒"(x,y,z) = (x"⇒"y) "et" (y"⇒"z)` # Implication successive. `"⇒"()="⊤"`
---- 27 décembre 2025 ----