PHOX301 et PHOX501 : Initiation au raisonnement mathématique avec PhoX

Introduction

Que sont les mathématiques

Les mathématiques tentent de définir une réalité indépendante du monde réel et de trouver les énoncés qui y sont vrais. Comme on ne peut rien faire à partir de rien, Les mathématiques partent d'axiomes pour déduire la vérité d'autres énoncés.

Ensuite, les mathématiques sont utilisés dans le monde réel, car si les axiomes utilisés sont considérées comme vrais dans le monde réel, les déductions faites à partir de ces axiomes le seront aussi.

Le but de cette option est de comprendre comment lire et écrire des énoncés mathématiques ainsi que leur preuve. On utilisera l'outils PhoX sur machine, les raisons en sont expliquées plus loin.

Que sont les énoncés mathématiques

Les énoncés mathématiques sont des phrases qui sont vraies ou fausses. De plus, tous les mathématiciens comprennent les énoncés de la même manière (quand ils sont bien écrit). Les énoncés mathématiques ont donc un sens non amibiguë, indépendant du lecteur.

Toutefois, il y a plusieurs manière d'écrire un énoncé mathématiques :

• écriture symboliqe avec des symboles tels que $\forall ,\exists ,+,\times ,\Sigma ,...$,
• usage de la langue naturelle (le français),
• un mélange des deux,
• enfin, écriture purement formelle dans un système logique précis.

Cette dernière manière d'écrire les mathématiques n'est pratiquement jamais utilisé. Car, cela prendrait trop de temps. Mais c'est le fait que des chercheurs (Hilbert, Tarski, Gödel, ...) aient pris conscience au début du XXième siècle que l'on pouvait en principe formaliser les mathématiques complètement qui a permis d'établir la non ambiguïté des énoncés.

Un autre intérêt de l'approche purement formelle est que les machines peuvent alors analyser les énoncés mathématiques (et donc détecter des erreurs de syntaxe par exemple).

Que sont les preuves mathématiques.

Ce sont des textes qui établissent la vérité d'un énoncé mathématiques. La encore ces textes ont un sens précis et non ambiguë. De plus, et ceci peut paraître surprenant, on peut aussi complètement formaliser la notion de preuve. À tel point qu'une machine peut analyser une preuve et vérifier qu'elle est bien une preuve correcte d'un énoncé. Il existe de nombreux logiciels permettant de faire cela : PhoX (que l'on va utiliser), CoQ, Isabelle, ...

Là encore, on ne formalise pratiquement jamais les preuves et très peu de mathématiciens utilisent ces logiciels. Mais le fait de savoir que l'on peut le faire donne un critère précis de validiter des preuves écrites en langue naturelle : on doit en principe pouvoir les formaliser.

Retour sur le langage mathématique.

Donc l'usage en mathématiques est d'utiliser un mélange de langue naturelle, d'écriture symbolique en rendant le texte aussi agréable à lire que possible. Pour cela, on pratique souvent des ommissions, des abus de langages, etc ... Mais, on prend garde à rester intelligible pour un autre mathématicien connaissant le contexte.

En fait le langage mathématique est un dialecte du français et le problème pour l'étudiant est aussi d'apprendre ce langage. Pour se convaincre que le langage mathématiques est un dialecte dérivé du français, il suffit de constater que des locutions tels que si et seulement si ou soit un entier ne sont pratiquement jamais utilisé en français.

Déroulement de cette option

On prendra de petits exemples, on écrira les énoncés et les preuves à la fois en français et en PhoX en essayant de bien comprendre l'usage de la langue. Le but final n'est pas que vous appreniez le logiciel PhoX, mais que vous progressiez en mathématiques.

Utilisation de PhoX

• Redémarrer l'ordinateur sous linux
• Se logger
• Ouvrir un terminal : Menu applications => Accessoires => Terminal
• Taper : '/home/commun/phox/setup' puis la touche entrée.

Premier exemple en PhoX 301

Définition : le support d'une application $f$ de $E$ dans $E$ est l'ensemble des éléments de $E$ tel que $f(x)\neq x$

Théoreme : $f$ et $g$ deux injections à support disjoints de $E$ dans $E$, on a $f\circ g=g\circ f$

Premier exemple en PhoX 501

Les trois définitions suivantes de la continuité sont équivalentes :

• $f$ est continue sur $\mathbb {R}$ si et seulement si

$\forall x\in \mathbb {R} \,\forall \epsilon >0\,\exists \eta >0\,\forall y\in \mathbb {R} \,(|y-x|<\eta =>|f(y)-f(x)|<\epsilon )$

• $f$ est continue sur $\mathbb {R}$ si et seulement si L'image réciproque d'un ouvert par $f$

est un ouvert.

• $f$ est continue sur $\mathbb {R}$ si et seulement si pour toute suite réelle $u$

convergeante vers $l$, on a $f(u_{n})$ qui converge vers $f(l)$.