Des articles

2.3 : Les axiomes logiques


Soit un langage de premier ordre (mathcal{L}) donné. De plus, nous pourrions, en principe, concevoir un programme informatique qui serait capable de décider de l'appartenance à (Lambda) dans un laps de temps fini.

Après avoir établi l'ensemble d'axiomes logiques (Lambda) et nous voulons commencer à faire des mathématiques, nous voudrons ajouter des axiomes supplémentaires qui sont conçus pour nous permettre de déduire des déclarations sur n'importe quel système mathématique que nous pouvons avoir à l'esprit. Ceux-ci constitueront la collection d'axiomes non logiques, (Sigma). Par exemple, si nous travaillons en théorie des nombres, en utilisant le langage (mathcal{L}_{NT}), avec les axiomes logiques (Lambda) nous voudrons également utiliser d'autres axiomes qui concernent le propriétés d'addition et la relation d'ordre dénotée par le symbole (<). Ces axiomes supplémentaires sont les formules que nous placerons dans (Sigma). Ensuite, à partir de cet ensemble étendu d'axiomes (Lambda cup Sigma), nous tenterons d'écrire des déductions de formules qui font des déclarations d'intérêt pour la théorie des nombres. Pour rappel : (Lambda), l'ensemble des axiomes logiques, sera fixe, de même que l'ensemble des règles d'inférence. Mais l'ensemble des axiomes non logiques doit être spécifié pour chaque déduction. Dans la présente section, nous ne présentons que les axiomes logiques, en traitant des règles d'inférence dans la section 2.4, et en reportant notre discussion sur les axiomes non logiques à la section 2.8.

Axiomes d'égalité

Nous avons pris le chemin de supposer que le symbole d'égalité, (=), fait partie du langage (mathcal{L}). Il existe trois groupes d'axiomes qui sont conçus pour ce symbole. Le premier dit simplement que tout objet est égal à lui-même :

[x = x : ext{pour chaque variable} : x. ag{E1}]

Pour le deuxième groupe d'axiomes, supposons que (x_1, x_2, ldots, x_n) sont des variables, (y_1, y_2, ldots, y_n) sont des variables et (f) est un (n )-aire symbole de fonction.

[left[ left( x_1 = y_1 ight) land left( x_2 = y_2 ight) land cdots land left( x_n = y_n ight) ight] ightarrow left( f left( x_1, x_2, ldots, x_n ight) = f left( y_1, y_2, ldots, y_n ight) ight). ag{E2}]

Les hypothèses pour le troisième groupe d'axiomes sont les mêmes que pour le deuxième groupe, sauf que (R) est supposé être un symbole de relation (n)-aire ((R) pourrait être le symbole d'égalité, qui est considéré comme un symbole de relation binaire).

[left[ left( x_1 = y_1 ight) land left( x_2 = y_2 ight) land cdots land left( x_n = y_n ight) ight] ightarrow left( R left( x_1, x_2, ldots, x_n ight) ightarrow R ightarrow R left( y_1, y_2, ldots, y_n ight) ight). ag{E3}]

Les axiomes (E2) et (E3) sont des axiomes conçus pour permettre la substitution d'égal à égal. Rien de plus chic que ça.

Axiomes quantificateurs

Les axiomes quantificateurs sont conçus pour permettre une entrée très raisonnable dans une déduction. Supposons que l'on connaisse (forall x P left( x ight)). Alors, si (t) est un terme quelconque du langage, nous devrions pouvoir énoncer (P left( t ight)). Pour éviter les problèmes du genre évoqué au début de la section 1.8, nous exigerons que le terme (t) soit substituable à la variable (x).

[left( forall x phi ight) ightarrow phi_t^x, : ext{if} : t : ext{est substituable à} : x : ext{in} : phi. ag{Q1}]

[phi_t^x ightarrow left( exists x phi ight), : ext{if} : t : ext{est substituable à} : x : ext{in} : phi. ag{Q2}]

Dans de nombreux textes logiques, l'axiome (Q1) serait appelé instanciation universelle, tandis que (Q2) serait appelé généralisation existentielle. Nous éviterons ce langage impressionnant et nous en tiendrons aux plus banals (Q1) et (Q2).

Résumer

Juste pour rassembler tous les axiomes logiques en un seul endroit, reprenons-les. L'ensemble (Lambda) des axiomes logiques est la collection de toutes les formules qui entrent dans l'une des catégories suivantes :

[x = x : ext{pour chaque variable} : x. ag{E1}]

[left[ left( x_1 = y_1 ight) land left( x_2 = y_2 ight) land cdots land left( x_n = y_n ight) ight] ightarrow left( f left( x_1, x_2, ldots, x_n ight) = f left( y_1, y_2, ldots, y_n ight) ight). ag{E2}]

[left[ left( x_1 = y_1 ight) land left( x_2 = y_2 ight) land cdots land left( x_n = y_n ight) ight] ightarrow left( R left( x_1, x_2, ldots, x_n ight) ightarrow R left( y_1, y_2, ldots, y_n ight) ight). ag{E3}]

[left( forall x phi ight) ightarrow phi_t^x, : ext{if} : t : ext{est substituable à} : x : ext{in} : phi. ag{Q2}]

Notez que (Lambda) est décidable. Nous pourrions écrire un programme de calcul qui, étant donné une formule (phi), peut décider en un temps fini si (phi) est ou non un élément de (Lambda).


Voir la vidéo: séance 3: les axiomes de rationalité partie 1 (Octobre 2021).