Discussion:Système F
- Admissibilité
- Neutralité
- Droit d'auteur
- Article de qualité
- Bon article
- Lumière sur
- À faire
- Archives
- Commons
Cet article est indexé par le projet Mathématiques.
Les projets ont pour but d’enrichir le contenu de Wikipédia en aidant à la coordination du travail des contributeurs. Vous pouvez modifier directement cet article ou visiter les pages de projets pour prendre conseil ou consulter la liste des tâches et des objectifs.
| Avancement | Importance | pour le projet | |
|---|---|---|---|
| Bon début | À évaluer |  | Mathématiques (discussion • critères • liste • stats • hist. • comité • stats vues) |
Cet article ne comporte pas de liste de tâches suggérées. Vous pouvez saisir une liste de tâches à accomplir (par exemple sous forme d'une liste à puces), puis sauvegarder. Vous pouvez aussi consulter la page d'aide.
Qu'entend -on par logique minimale intuitionniste ?
[modifier le code]L'article dit que "le système F correspond très exactement à la logique minimale intuitionniste du second ordre", mais qu'entend -on par logique minimale intuitionniste ? A ce que je connais 1/ log classique moins raisonnement par l'absurde = logique intuitionniste 2/ et logique intuitionniste moins la règle subsistante pour la négation = logique minimale ... donc parle t-on ici de la logique minimale du second ordre ou parle t-on d'une autre logique ... qu'il faudrait alors définir ? --Epsilon0 (discuter) 20 juin 2017 à 11:16 (CEST)
Je regarde plus précisément, on parle dans l'article de logique minimale intuitionniste du second ordre, bon en clair c'est le calcul propositionnel sans la négation et avec les quantificateurs, pas ? Je compte faire la modif. --Epsilon0 (discuter) 8 juillet 2017 à 13:03 (CEST)
Indécidabilité du typage
[modifier le code]Je pense qu'il manque, dans la correspondance entre les deux présentations du système F, le fait que le typage est indécidable (https://www.sciencedirect.com/science/article/pii/S0168007298000475). Je préfèrerais toutefois que ce soit un spécialiste du typage qui rédige. David.Monniaux (discuter) 10 septembre 2022 à 10:27 (CEST)
- En effet, tu as raison. Je vais rédiger une première version. --Pierre de Lyon (discuter) 11 septembre 2022 à 08:51 (CEST)
- J'ai créé la section "indécidabilité". --Pierre de Lyon (discuter) 11 septembre 2022 à 10:03 (CEST)