Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
256 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Logique et topos

Envoyé par Vincent Semeria 
Logique et topos
il y a quatre années
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
Re: Logique et topos
il y a quatre années
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.
Pièces jointes:
ouvrir | télécharger - faisceaux.pdf (1.17 MB)
Re: Logique et topos
il y a quatre années
@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

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Logique et topos
il y a quatre années
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 :)
L'R est dans C
Re: Logique et topos
il y a quatre années
Citation
Vincent Semeria
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.hot smiley
Re: Logique et topos
il y a quatre années
Dans un topos, les flèches de $1$ dans $X$ ne fournissent pas une bonne notion d'"éléments" de $X$.
Seuls les utilisateurs enregistrés peuvent poster des messages dans ce forum.

Cliquer ici pour vous connecter

Liste des forums - Statistiques du forum

Total
Discussions: 137 357, Messages: 1 329 655, Utilisateurs: 24 406.
Notre dernier utilisateur inscrit Louragli.


Ce forum
Discussions: 2 115, Messages: 41 168.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page