Résolution d’équations et déduction naturelle

De nombreux élèves rencontrent des difficultés dans l’acquisition des compétences logiques nécessaires à l’activité mathématique. Ces compétences se situent bien souvent en filigrane de l’activité mathématique, ce qui les rend difficilement identifiables. Notre exposé a pour objectif de mettre en exergue quelques-unes des compétences logiques mobilisées dans le cadre de la résolution d’équations. Pour ce faire, nous proposons une analyse de quelques exemples de résolution d’équation à la lumière de la déduction naturelle. La déduction naturelle est une approche formelle élaborée par G. Gentzen (1909-1945) visant à refléter le plus adéquatement possible les raisonnements logiques qui sont à l’œuvre dans les démonstrations mathématiques. En raison de sa précision conceptuelle et de sa proximité avec la pratique mathématique, elle constitue un cadre particulièrement commode pour la mise en lumière de l’arrière-plan logique à partir duquel sont enseignées les mathématiques.