1.4. Termes et formules; connecteurs

Pour toute théorie, on appelle terme un assemblage fini d'occurrences de symboles, visant à désigner un objet (sa valeur) une fois fixés le modèle et les valeurs des variables libres. (Une occurrence d'un symbole est un lieu où on le place, par exemple le terme «x+x» comporte 2 occurrences de x et une de +). On appelle formule un système semblable à un terme mais à valeurs booléennes. Nous appellerons expression un terme ou une formule.
Les expressions se construisent successivement, chacune comme donnée (occurrence) d'un symbole appelé son symbole principal , et d'une liste d'expressions précédemment construites (et éventuellement de symboles de variables). Ce symbole principal détermine le type de ses valeurs (et donc distingue si c'est un terme ou une formule) et le format de cette liste (le nombre d'entrées et le type de chacune). Pour un symbole de para-opérateur, ce format est donné par la liste de ses arguments.
Les premiers et plus simples termes sont ceux réduits à l'occurence d'un symbole de constante ou de variable, ce qu'on appelle un terme atomique. Les constantes booléennes «vrai» et «faux» (connecteurs d'arité 0) forment les premières formules.
Les autres symboles, demandant une liste non vide, nécessitent une convention de présentation de cette liste. La plupart des symboles de para-opérateurs binaires ont la forme d'un caractère séparant les deux arguments (l'addition est notée x+y au lieu du format initial +(x,y) des opérations); d'autres (multiplication, puissance) se présentent implicitement, sans caractère.
D'autres symboles sont notés par plusieurs caractères délimitant les entrées. Les parenthèses peuvent soit composer la notation de symboles comme l'évaluateur de fonction, soit servir à distinguer les sous-expressions et leurs symboles principaux respectifs, comme dans (x+y)n.

Connecteurs
Voici les connecteurs les plus utiles par ordre d'arité n > 0, avec leurs propriétés vraies pour toutes valeurs des variables booléennes (remplaçables par des formules) A, B, C.
n=1 : le «non» échange les booléens: non(vrai) ⇔  faux, non(faux) ⇔  vrai, non(nonA)) ⇔ A. Parfois abrégé en barrant le symbole principal de son argument, formant un autre symbole de même format: (x ≠ y) ⇔ non(x=y) («x est différent de y»); x ∉ E ⇔ non(x ∈ E) («x n'appartient pas à E»).
n=2 :
et : vaut vrai uniquement lorsque ses deux arguments valent vrai;
ou : vaut vrai sauf lorsque ses deux arguments valent faux;
 ⇒  : A ⇒ B peut se lire «A implique B», «A est une condition suffisante à B», ou «B est une condition nécessaire à A», et signifie ((nonA)  ou B). Etant vrai sauf quand A est vrai et B est faux, il exprime que si A est vrai alors B aussi, mais sinon il ne nous renseigne pas (étant vrai).
La formule (nonB ⇒ nonA) est appelée la contraposée de (A ⇒ B), et lui est équivalente.
 ⇔  (équivaut), égalité entre booléens: (A ⇔ B) ⇔ ((A ⇒ B) et (B ⇒ A)). Une preuve de A ⇔ B peut se former d'une preuve de l'implication (A ⇒ B), puis de l'autre (B ⇒ A) appelée sa réciproque.
Sa négation ⇎ , autant lisible en exerçant le «non» sur un argument: (A ⇎ B) ⇔ ((nonA) ⇔ B). Aussi appelé «ou exclusif» car traduisible par ((A ou B) et non(A et B)).
Les négations échangent divers connecteurs:

(A ou B)
⇎ (( non
 A)  et ( non
 B))


(A et B)
⇎ (( non
 A) ou ( non
 B))


(A ⇒ B)
⇎ (A et  non
 B)
Cela transforme les propriétés d'associativité et de distributivité en diverses formules:

((A et B) et C)
 ⇔ (A et (B et C))


((A ou B) ou C)
 ⇔ (A ou (B ou C))


(A ⇒ (B ⇒ C))
 ⇔ ((A et B) ⇒ C)


(A ⇒ (B ou C))
 ⇔ ((A ⇒ B) ou C)


(A et (B ou C))
 ⇔ ((A et B) ou (A et C))


(A ou (B et C))
 ⇔ ((A ou B) et (A ou C))


(A ⇒ (B et C))
 ⇔ ((A ⇒ B) et (A ⇒ C))


((A ou B) ⇒ C)
 ⇔ ((A ⇒ C) et (B ⇒ C))


((A ⇒ B) ⇒ C)
 ⇔ ((A ou C) et (B ⇒ C))


(A et (B ⇒ C))
 ⇔ ((A ⇒ B) ⇒ (A  et C))
n ≥ 3 : les chaînes de «et» (A et B et C) et celles de «ou» (A ou B ou C) s'obtiennent en effaçant les parenthèses grâce à l'associativité. L'affirmation d'une chaîne de «et» revient à affirmer séparément ses constituants. Par ailleurs toute chaîne de formules reliées par des  ⇔  et des  ⇒  abrégera la succession d'affirmations (lien par des «et») de chaque lien entre formules voisines:

faux
 ⇒ A ⇒ A ⇒ vrai


( non
 A)
 ⇔ (A ⇒ faux) ⇔ (A ⇔ faux)


(A ⇒ B ⇒ C)
 ⇔ ((A ⇒ B) et (B ⇒ C)) ⇒ (A ⇒ C)


(A ⇔ B ⇔ C)
 ⇔ ((A ⇔ B) et (B ⇔ C)) ⇒ (A ⇔ C)


(A et A) ⇔ (A et vrai)
 ⇔ A ⇔ (A ou A) ⇔ (A ou faux) ⇔ (vrai ⇒ A) ⇔ (A ⇔ vrai)


(B et A) ⇔ (A et B)
 ⇔ (A et (A ⇒ B)) ⇒ B ⇒ (A ou B) ⇔ (B ou A)
Structures définies par des expressions
En théorie du modèle, on appellera structure (opérateur ou prédicat) toute opération entre types définie par une expression (terme ou formule) et une liste de ses variables libres qu'on choisit de lier dans le rôle d'arguments. Cette structure dépend des autres variables restant libres, appelées ses paramètres (tandis que les variables liées dans l'expression, étant invisibles de l'extérieur, sont ici oubliées).
Des symboles de structure annexes peuvent être introduits au-delà du langage de la théorie, généralisant en arité non nulle le cas des variables libres à distinguer des constantes. Un tel symbole peut servir à abréger l'expression qui définit une structure voulue; ou s'employer sans définition de manière applicable à toute structure et même plus (opération indéfinissable). Mais la théorie ne peut lier la variation d'un tel symbole qu'en liant les paramètres de l'expression (ou le nombre fini d'expressions) définissant ses valeurs (structures) voulues. Elle ne peut donc pas englober d'un coup toutes les structures d'arité donnée.
Une structure sera dite invariante si elle est définie sans paramètre. Toute structure désignée par un symbole du langage est invariante. Tout ajout d'une structure invariante au langage (et de sa définition comme axiome), constitue un développement interne de la théorie, qui en préserve les méta-notions utiles (structure, structure invariante, prouvabilité).

Axiomes de l'égalité
Pour tout foncteur T et tous objets x,y (pouvant abréger des termes avec des paramètres), on a x=y ⇒ T(x)=T(y). De même pour tout prédicat unaire A on a x=y ⇒ A(x) ⇔ A(y). Ainsi une égalité entre termes x=y permet de remplacer une ou toute occurence de x par y dans toute expression sans en affecter le résultat. Cela s'applique notamment lorsqu'un symbole est défini par un terme: les deux sont égaux, et interchangeables dans chaque expression. Aussi les axiomes et autres lois s'expriment à l'aide de symboles de variables remplaçables par des termes dans leur utilisation.

1.3.  <—
Structure des théories

 Sommaire
—>     1.5.
Classes en théorie des ensembles