"La conjonction est-elle un connecteur multiplicatif ou un connecteur additif ?" par Alain Prouté (6 janvier 2016)

Résumé

Traditionnellement, la conjonction (``et logique'') est vue comme un connecteur multiplicatif, ce qui, en langage catégorique revient à dire qu'elle est définie comme un adjoint à droite. Toutefois, cette conjonction ``ordinaire'' ne couvre pas toutes les situations qu'on peut rencontrer en mathématiques, même élémentaires. Par exemple, soit A une partie de l'ensemble N des entiers naturels, alors la conjonction ``A n'est pas vide et la borne inférieure de A est 0'' n'est pas modélisable par cette conjonction ordinaire, ne serait-ce que parce qu'elle n'est clairement pas commutative. Dans cet exposé, nous donnons une définition plus générale de la conjonction, qui couvre le cas de l'exemple, et qui, assez curieusement, la fait apparaître comme un adjoint à gauche et non plus à droite, et donc comme un connecteur additif. Ce sujet, qui fait partie du cryptofolklore de la théorie des types et de la théorie des topos, n'est pratiquement pas présent dans la littérature. Nous en donnons une version que nous espérons originale. (Travail en commun avec Matthieu Herrmann)

Un article en collaboration avec Matthieu Hermann

On the dependent conjunction and implication. sept. 2015

Connecteurs additifs et multiplicatifs

Un connecteur est dit multiplicatif s'il est un adjoint à droite d'une application structurelle (ex. : "et").

Un connecteur est dit additif s'il est un adjoint à gauche d'une application structurelle.

Un "et" non commutatif

Connecteurs définis par démontrabilité plutôt que par tables de vérité

Heyting, Kolmogorov...

Démontrabilité et foncteurs adjoints

Adjonctions entre ensembles pré-ordonnés

unité

counité

Applications équivalentes

Unicité de l'adjoint à équivalence près

Composition, commutation aux bornes sup (resp. inf)

Comme l'a dit Burroni, avec les préordonnés, c'est simple car tous les diagrammes sont commutatifs

Le "et" adjoint de la diagonale

Diagonale

Produit de deux ensembles pré-ordonnés

Ensemble des énoncés fermés

Le "et" adjoint de la diagonale

Implication

Le "et " (à gauche) est adjoint d'implique (à droite)

Le "et" devient le produit tensoriel dans certaines logiques...

Le modus ponens est la co-unité de cette adjonction

Les "et / implique" élargis : du calcul propositionnel au calcul des prédicats

Adjonction des quantificateurs existentiel et universel

Lawvere, dans un contexte topos

Image directe universelle et image directe existentielle

Ici, on ne fera pas appel aux topos mais à la notion logique de contexte

Notion de contexte

Notion ordonnée dans la pratique de tout mathématicien (alors que dans le langage interne d'un topos ça ne l'est pas)

Ensemble des énoncés ayant un sens dans un contexte donné

Quantificateurs comme adjoints de la déclaration (à la Lawvere)

Déclarations et suppositions

Discussion sur les notations

Contextes de déclarations et de supposition

"Le nom est une preuve !"

Les "et / implique" élargis aux suppositions : conjonction et implication usuelles

La Règle spéciale

Question de Paul-André Melliès (1)

Formalisation de l'implication usuelle

Le modus ponens est-il encore la co-unité de cette adjonction ?

Le modus ponens est "un peu une arnaque"

P.-A. Melliès : un écart apparent entre la curryfication dans les catégories cartésiennes fermées, et la situation habituelle léguée par Lawvere. Remarque : autre modus ponens, avec quatre foncteurs.

Mise en place de l'adjonction

La conjonction dépendante et l'implication dépendante sont définis comme les adjoints à gauche et à droite de l'opération de supposition :

Remarque : ne pas identifier des choses isomorphes même canoniquement

Paul-André Melliès : remarque (suite)

Un "et" multiplicatif.... et un "et" additif

Union disjointe des fibres d'un fibré...

Paul-André Melliès : remarque sur le modus ponens à 4 foncteurs (suite & fin)

L'union disjointe (additive) des fibres d'un fibré devient multiplicative si indépendance

2+2+2 = 3 x 2

Remarques épistémologiques : impact de l'informatique, crypto-floklore, etc...

Système W et la notion de garant

Élément global d'un fibré

Section comme garant de vérité

Association des théorèmes anonymes

Le garant d'un énoncé n'étant pas ambigu, il n'est pas nécessaire de lui donner un nom

Laxisme dans l'écriture des preuves

Considérations logiques & conclusion

Théorème de Diaconescu

Prouté, Alain, "Expressions indéterminées, constructivisme et axiome du choix". Cahiers de Topologie et Géométrie Différentielle Catégoriques, 33 no. 3 (1992), p. 279-288

Références

On the dependent conjunction and implication.

Dans cet article écrit en collaboration avec mon étudiant Matthieu Herrmann, nous donnons une explication des conjonctions 'E et F' et implications 'E implique F', dans lesquelles l'énoncé F n'est correctement formulé que quand E est vrai. Cette situation est très courante en mathématiques, même élémentaires. L'idée est que ces opérations jouent par rapport à la notion de supposition le même rôle que les quantificateurs par rapport à celle de déclaration. Nous expliquons également, et c'est là notre principale motivation, le lien entre ce phénomène, deux principes fondamentaux des mathématiques, et le langage vernaculaire des mathématiques.

400 KO (17 pages)

Table des matières détaillée