Modus Ponens, Théorie de la démonstration

[EternalApprentice]

Bonjour,

Ces derniers temps j’ai essayé de vérifier la conformité de ma conception des maths avec la théorie et je me suis aperçu que ma façon de voir et d’appréhender les maths comporte des problèmes.
Pour y voir plus clair, je me suis penché sur la logique fondamentale, les systèmes de déduction et la théorie de la démonstration, et j’ai besoin d’aide pour appréhender ces concepts.

Par exemple je ne comprends pas la différence entre



et le modus ponens.

Pour commencer pouvez-vous me donner un exemple d'une démonstration simple et concrète écrite dans le langage du système de déduction naturelle (celui-ci car d’après ce que j’ai lu il est le plus facile à comprendre) ?
Merci de vos éclaircissements.

[Skullkid]

Bonsoir, la différence est du même ordre que celle entre l'implication et la déduction.

est une proposition logique dont la valeur de vérité dépend a priori de celles de A et B (les connecteurs logiques tels que et ne sont ni plus ni moins que des fonctions qui prennent des valeurs de vérité en argument et qui produisent une nouvelle valeur de vérité), et il se trouve qu'elle vaut "vrai" quelles que soient les valeurs de vérité de A et B.

Le modus ponens est une règle d'inférence, c'est-à-dire une recette qui te permet de faire des preuves. C'est la règle qui te dit qu'en prouvant A et tu obtiens une preuve de B. Formellement, on peut l'écrire , où la virgule et le symbole de déduction ne sont pas des connecteurs logiques.

Un exemple de démonstration est donné dans cet article Wikipédia ("notion d'arbre de preuve").

[mathelot]

Bonjour,
on peut considérer un programme d'intelligence artificielle. Il agit sur deux bases de données:
la BASE DES FAITS et la BASE DES REGLES.
On écrit la propriété A dans la base des faits. (A est vraie). On écrit B dans la base des règles.L Le modus ponens est réalisé par le programme d'I.A en lisant A dans la base des faits , dans la base des régles et en écrivant B dans la base des faits.
La règle est une tautologie (toujours Vraie). Sans doute, qu'on peut l'écrire de manière provisoire dans la base des règles pour les besoins d'une démonstration ou l'écrire dans le code du programme d'inférence.

[EternalApprentice]

Je pense y voir un peu plus clair grâce à vos réponses. L’exemple de Wikipédia est facile à comprendre.

Par contre, dans les cas qui me viennent à l’esprit n’est pas un théorème que l’on peut utiliser directement, c’est ce que l’on veut montrer. Est-il juste de dire que l'on décompose la démonstration de en plusieurs déductions (au sens des systèmes de déduction) successives,

où des théorèmes faisant intervenir des connecteurs logiques comme par exemple , etc...
sont propres à l'axiomatique du domaine des maths que l'on étudie ?

Par exemple, je veux montrer que (ne vous moquez pas de moi).

Quand je dis « Soit tel que » ; constitue mon premier théorème.
Ensuite est un théorème ;
est un théorème (d’après un axiome sur la transitivité de la relation binaire « ») ;
Les implications ci-dessus sont bien données par des axiomes de calcul, et le modus ponens permet d’en déduire que : .

Je pense que ce raisonnement est correct ?
J’aimerais quand même décrire l’entièreté du processus dans le système de déduction naturelle ; la première étape serait :
.

Comment décrire la suite, qui fait intervenir une conjonction ?

[GaBuZoMeu]

Il te faut aussi écrire les axiomes dont tu pars (axiomes des corps ordonnés, par exemple ?). La déduction naturelle à elle seule ne dit rien sur la multiplication ni sur la relation d'ordre et sa compatibilité avec la multiplication

[mathelot]

.

Comment décrire la suite, qui fait intervenir une conjonction ?

cette écriture est de la logique de 1er ordre -elle fait intervenir des prédicats avec une ou plusieurs variables-

j'aurai écrit
.

Les variables peuvent être liées comme x ou libres comme y.