Logique et topos

Vincent Semeria · July 2015

Bonjour à tous !

Je me demande si l'existence de modèles ensemblistes se généralise à tout topos. Dans les ensembles, toute théorie du premier ordre consistante a un modèle (dont la taille est fixée par la taille de la signature). Dans ce cas la consistance utilise la logique usuelle, notamment le principe du tiers exclu.

Si je me place dans un topos élémentaire quelconque, son classificateur de sous-objets est une algèbre de Heyting, c'est-à-dire représente des valeurs de vérité avec interprétation des connecteurs logiques $\lnot,\land,\lor,\Rightarrow$. J'ai donc une logique propositionnelle, qui inclut la logique intuitionniste et ajoute toutes les tautologies de cette algèbre de Heyting. Avec cette logique, garde-t-on l'existence de modèles de toute théorie du premier ordre consistante ?

Si oui qu'appèle-t-on modèle dans un topos ? Dans un modèle ensembliste $M$, on interprète facilement $\exists x$ par $\exists x\in M$, mais ceci n'a pas de sens dans un topos.

Par hasard connaissez-vous d'autres topos, avec des exemples de tautologies qu'ils introduisent ?

Merci,
Vincent

GaBuZoMeu · July 2015

Un texte que j'ai déjà plusieurs fois l'occasion de donner sur ce forum. C'est centré sur les topos de faisceaux sur un espace topologique et topos de Grothendieck, mais ça permet de donner des exemples concrets.

christophe c · July 2015

@Vincent d'après un rumeur persistante un topos de Grothendieck est essentiellement un modèle de la théorie intuitionniste des ensembles.

Tu peux donc essayer de prouver le théorème de complétude de manière intuitionniste et voir ce qui bloque. Ce sera une activité enrichissante

Vincent Semeria · July 2015

Effectivement ce PDF explique comment modéliser un langage du premier ordre dans un topos, merci.

Au passage j'ai répondu à ma question sur les tautologies. Toute algèbre de Heyting contient $\{0,1\}$ et les connecteurs logiques y ont leurs valeurs habituelles. Ainsi une tautologie dans une algèbre de Heyting est une tautologie binaire, prouvable en ajoutant le tiers exclu.
À travailler dans des algèbres de Heyting, on peut seulement espérer des preuves plus constructives, quoique plus longues et de moins de formules propositionnelles. Cela a-t-il vraiment un intérêt, à part nous apprendre qu'on gagne à éviter le tiers exclu autant que possible ?

Enfin je me rends compte que ma question de complétude était mal posée. Si on met toutes les tautologies dans les règles de déduction, il n'y a plus rien à prouver. Le théorème de complétude isole un (petit) sous-ensemble de tautologies qui suffisent à prouver toutes les autres. Il faudrait dire quel sous-ensemble de tautologies on utilise dans chaque topos.

@Christophe : un topos a un objet terminal, donc une relation $\in$ via les morphismes qui en partent. Un topos a aussi tous les objets exponentiels, qui donnent des espèces de fonctions ensemblistes. Également les produits qui donnent les couples. Ça ne m'étonnerait pas que ta rumeur soit fondée

LR est dans C · July 2015

Vincent Semeria a écrit:

Le théorème de complétude isole un (petit) sous-ensemble de tautologies qui suffisent à prouver toutes les autres. Il faudrait dire quel sous-ensemble de tautologies on utilise dans chaque topos.

La structure des topos serait algébrique sur celle des graphes même s'il est validé manifestement qu'elle n'est pas encore bien définie ce jour.X:-(