Discussion:Système F

Le contenu de la page n’est pas pris en charge dans d’autres langues.
Une page de Wikipédia, l'encyclopédie libre.
Autres discussions [liste]
  • Admissibilité
  • Neutralité
  • Droit d'auteur
  • Article de qualité
  • Bon article
  • Lumière sur
  • À faire
  • Archives
  • Commons

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)[répondre]

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)[répondre]

✔️ Avec l'impression de soliloquer ;-) --Epsilon0 (discuter) 8 juillet 2017 à 14:40 (CEST)[répondre]

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)[répondre]

En effet, tu as raison. Je vais rédiger une première version. --Pierre de Lyon (discuter) 11 septembre 2022 à 08:51 (CEST)[répondre]
J'ai créé la section "indécidabilité". --Pierre de Lyon (discuter) 11 septembre 2022 à 10:03 (CEST)[répondre]