AeriesGuard Le Refuge des Créateurs Minecraftiens !

Toi, à priori, ce qui t'intéresse c'est plutôt l'informatique. Dans ce cas la vidéo d'Alain Prouté est l'introduction la plus accessible (voir expéditive) aux topoi dans la programmation.

Je ne comprends déjà pas les sujets des conférences

Comme c'est un sujet qui a le vent en poupe, il y a justement un cycle de conférences inter-disciplinaire sur les topos (topoi), au programme :

• topoi en mathématiques et logique
• topoi en sciences physiques
• topoi en philosophie

Version française , inscription gratuite.

Jme demande si tu devrai pas te pencher du coté de la logique plutôt que des maths.
Pour ce qui est abstrait c'est assez puissant en général.

mais arrétez, je comprend rien et ça me stress :'(

Je ne suis pas certain de comprendre la nature exacte de tes interrogations. Je vais me contenter de faire quelques remarques :

• par définition 1 = succ zero c'est-à-dire que un est le successeur de zéro
• oui, les définitions que je donne (en Coq) des entiers naturels sont purement behavioristes, elles ne sont pas initialement basées sur la notion intuitive de quantité
• toutefois les définitions que je donne ne sont pas arbitraires, n'importe quelle opération que je peux définir à l'aide de ces "nombres" va immanquablement te renvoyer à une notion de quantité

Par exemple :

Fixpoint add m n {struct m} :=
  match m with
  | zero => n
  | succ p => succ (add p n)
  end.

Definition two := succ (succ zero).

Eval compute in add two two.
  = succ (succ (succ (succ zero)))
  : nat1 

C'est-à-dire que 2 + 2 = 4.

Mes définitions sont peut-être (trop?) abstraites cela n'enlève rien quant à leurs capacités computationnelles.

Luminox a écrit :

Quoi de plus humain que ma définition ? Tu peux prouver que 2 + 2 = 4, en comptant sur tes doigts. Pour le faire tu bascules 2 doigts puis les 2 doigts suivants. En clair tu utilises la fonction doigt-successeur. Le support est biologique mais le principe reste le même.

Si j'avais codé l'addition en base 2 le principe serait similaire à celui d'un circuit intégré. En fait, quelque soit la façon dont tu comptes tu ne peux le faire qu'en appliquant un principe mathématique que Coq peut valider. Il n'existe pas d'autre moyen.

Là j'ai du mal à suivre. Autant je peux comprendre que tu me dises que 1 n'est pas une quantité mais un opérateur, au sens où c'est un concept purement abstrait. Cependant j'avais demandé ce qu'était 1 sans dire qu'en mathématiques, c'était une quantité; alors oui, la définition de nombre que je donne est "objet abstrait représentant une quantité précise de certain élément", mais c'est plus pour expliquer d'où vient l'idée du nombre; je n'ai pas la prétention de donner une définition mathématique pure(en tout cas pas à mon niveau de compréhension). Et ce n'est pas non plus tout à fait contradictoire, étant donné que j'admet qu'il s'agit d'un objet abstrait (le fait de dire opérateur peut aider, mais qu'est-ce qu'un opérateur à proprement parler? Est-ce qu'être un nombre implique être un opérateur ou opérateur=>nombre?), et que la définition de nombre que tu me donnes est une définition purement mathématique et donc qui ne cherche pas d'où vient l'idée de nombre.

Je pense que le fait que les nombres sont des constructions humaines a son importance dans la définition du nombre.

Par contre, ce qui me pose problème, c'est de dire "si coq le dit, alors c'est mathématique". Il me semble que Coq a été créé selon certains principes et que ce sont ces principes qui font qu'il sait ce qui est mathématique ou non. Or ce sont ces principes qui m'importent. Mais je ne demande pas la partie codée, parce que je n'y comprendrais rien: je demande la partie écrite en français, ou du moins dans une langue que je peux comprendre, et qui me dirait ce qui fait qu'une proposition est mathématique.

(Alors j'essaie de comprendre un peu comment marche cette théorie des Topoï mais j'ai un peu de mal à m'imaginer des ensembles sans élément. Il y a également des concepts que je ne connais pas -> "préfaisceau d'ensemble" par exemple, qui peuvent être plus ou moins complexe (je crois avoir compris celui-là, du moins à moitié, parce que j'ai encore du mal à me l'expliquer en mots). Par contre je n'y ait pas trouvé de quoi vérifier qu'une proposition est mathématique ou non)

Enfin, les phrases "la route est violette" ou "dieu existe/n'existe pas" dans l'absolu sont des propositions qui peuvent être soit vraies, soit fausses, soit indécidables. L'une peut consister en un fait, l'autre peut consister en une profession de foi, mais ça ne les empêche pas d'être des propositions et donc de devoir être différenciées des propositions mathématiques. (Mais je chipote)

Je vais te répondre à l'aide de code source Coq , c'est plus simple, plus pragmatique, et ça va plus vite.

Question n°1: c'est quoi cette quantité 1 ?
Réponse: Il n'y a pas de quantité 1, il y a un opérateur qu'on a arbitrairement appelé 1 + ...
Cet opérateur on va désormais l'appeler succ (pour successeur).

En Coq on défini les entiers naturel unaires à l'aide de zéro et succ :

• zéro est un entier naturel unaire (nat1)
• succ est une fonction de nat1 vers nat1

Inductive nat1 : Set :=
  | zero: nat1
  | succ: nat1 → nat1. 

Coq génère alors automatiquement le principe de récurrence correspondant :

nat1_ind :
  forall P : nat1 → Prop,
  P zero →
  (forall n : nat1, P n → P (succ n)) → forall n : nat1, P n 

Il n'y a pas qu'une seule façon de définir les entiers naturels. 

On peut tout aussi bien définir les entiers naturels en base 2, c'est pratique par exemple pour prouver la correction d'un algorithme d'exponentiation rapide:

• null vaut zéro
• one vaut un
• double double la valeur d'un entier en base 2
• double_succ double la valeur d'un entier en base 2 puis renvoie son successeur

Inductive nat2 : Set :=
  | null: nat2
  | one: nat2
  | double: nat2 → nat2
  | double_succ: nat2 → nat2. 

Coq génère alors automatiquement le principe de récurrence correspondant à cette nouvelle définition:

nat2_ind :
  forall P : nat2 → Prop,
  P null →
  P one →
  (forall n : nat2, P n -> P (double n)) →
  (forall n : nat2, P n → P (double_succ n)) -> forall n : nat2, P n 

Question n°2: comment distinguer un fait ( "la route est violette" ) ou une profession de foi ( "Dieu existe", "Dieu n'existe pas" ) d'une proposition mathématique ?
Réponse idiote: si Coq ne veut pas de ta déclaration alors ça n'est pas une proposition mathématique (valide).
Réponse sibylline: c'est la théorie des Topos qui défini l'ensemble Ω.

Ce que j'appelle ici "principe de récurrence" est un cas particulier de ce que j'appelle "récurseur" dans mon langage Moonscript. Content de voir qu'il y a au moins un membre du refuge qui voit à peu près de quoi je parle

Si j'ai bien compris ce que tu veux dire c'est que grâce au principe de récurrence tu peux produire n'importe quel entier naturel en prenant 0 comme base et en ajoutant 1 pour chaque "rang" d'entier qu'on veut obtenir (rang 1 = 1, rang 2 = 2, rang 3 = 3, rang n = n, avec n un entier naturel quelconque).

C'est donc comme ça qu'on définit un nombre en mathématique, du moins un entier naturel. D'accord.

Donc comment définis-tu 1? N'est-ce pas une unité abstraite et arbitraire?

Ensuite, si ça me permet de comprendre comment sont définis les nombres de façon mathématique,  ces nombres restent en apparence des objets tout à fait abstraits qui représentent une quantité. Ici, du moins pour les entiers naturels, il s'agit d'une quantité de l'unité abstraite "1", si j'ai bien compris.

Enfin, si je comprends ce que tu veux dire, l'objet des mathématiques est l'étude des propositions. Mais je pense qu'il faudrait encore préciser ces propositions: je ne crois pas qu'une étude mathématique aide beaucoup sur la proposition "la route est violette" ou "Dieu n'existe pas".

D'un autre côté, si on définit les mathématiques comme la science qui étudie les propositions mathématiques, j'ai pas l'impression qu'on va loin (pourtant ç'aurait été plus simple). Donc il faut trouver ce qui fait qu'une proposition est "mathématique".

EDIT: ah, et pour Cynder: le sujet ici c'est beaucoup de philosophie au sujet de mathématiques, mais sur des questions assez simples: "Les mathématiques, c'est quoi" "Les nombres, c'est quoi" et puis un peu de réflexion pas forcément profonde sur le sujet des idées innées et qu'il en existe au moins une d'après moi, et que ça veut dire qu'il en existe beaucoup d'autres pour les hommes. Voilà, ça a l'air énorme et j'utilise des mots compliqués, je suis d'accord, mais c'est lisible (j'espère )

RE-EDIT: Ca m'intéresse beaucoup cette histoire de théorie intuitionniste. Je verrais aussi pour Per Martin-Löf merci encore pour ta réponse!

Tu connais sans doute le principe d'induction suivant :

Citation :

Deux remarques mathématiques :

• Ce principe est dérivé d'une définition unaire des entiers, par exemple 3 = 1 + 1 + 1 + 0 (et non pas 3 = 1 + 1 + 1, sinon ça ne serait que de l'arithmétique, pas des mathématiques). En lui-même ce principe est une bonne définition des entiers. Il dit comment construire de nouveaux entiers, à partir de zéro.
• L'important dans ce principe c'est P, il s'agit d'une proposition, c'est un élément de Ω (oméga et non pas Ω, ohm qui est l'unité standard de la résistance électrique), Ω est l'ensemble des propositions, c'est l'objet dont s'occupent les mathématiques. En lui-même ce principe est une assez bonne définition des propositions. Il dit comment construire une nouvelle proposition, à partir des deux propositions P(0) et P(n) ⇒ P(n+1) on construit la nouvelle proposition ∀n∈ℕ, P(n), et vive-versa.

En généralisant ce principe d'induction on obtient plusieurs choses plus ou moins identiques :

• la logique intuitionniste qui est une logique constructive
• la programmation fonctionnelle
• les types (en programmation) et les propositions (mathématiques) sont des notions plus ou moins identiques

Remarque: Per Martin-Löf , l'inventeur de la théorie intuitionniste , est à la fois mathématicien et philosophe !