Introduction : Formalisation du raisonnement | les logiques
1 Systemes formels : exemples introductifs
1.1 Exemple 1 : generation de theoremes de l’arithmetique
1.2 Exemple 2 : calcul d’integrales
1.3 Exemple 3 : arithmetique de Peano
2 Calcul des propositions
2.1 Introduction
2.1.1 Les formules atomiques
2.1.2 Les formules composees
2.1.3 Le substrat de la logique
2.1.4 But du calcul des propositions
2.2 Syntaxe
2.3 Verite d’une formule
2.3.1 Introduction
2.3.2 Algebres de Boole
2.3.3 Interpretation des formules dans une algebre de Boole
2.3.4 Tautologies et equivalences
2.3.5 Tables de verite
2.4 Equivalences classiques
2.5 Systemes axiomatiques
2.5.1 Emploi d’un systeme axiomatique pour deriver des formules valides
2.5.2 Preuve a partir d’hypotheses
2.6 Calcul des sequents
2.6.1 Presentation
2.6.2 Reversibilite des regles
2.6.3 Recapitulation des regles
2.6.4 Validite d’un sequent
2.6.5 Theoreme de correction (ou consistance)
2.6.6 Theoreme de completude
2.6.7 Exemples de preuves
2.6.8 Exercices
3 Calcul des predicats : exemples introductifs
3.1 Le syllogisme ou les categories d’Aristote
3.2 Diagrammes de Venn
3.3 Limites du calcul des propositions
3.4 Limites des diagrammes de Venn
4 Calcul des predicats (logique du premier ordre)
4.1 Introduction
4.2 Syntaxe
4.2.1 Lexique
4.2.2 Grammaire
4.3 Interpretation des formules
4.3.1 Limites de l’interpretation, necessite d’un systeme de preuve
4.4 Equivalences classiques
4.5 Systemes axiomatiques
4.6 Calcul des sequents
4.6.1 Presentation
4.6.2 Recapitulation des regles
4.6.3 Theoremes de correction et de completude
4.6.4 Exemple de preuve
Glossaire et diffenitions
Bibliographie

Introduction : Formalisation du raisonnement | les logiques

< Logique > est un mot provenant du grec logos qui signie < science de la raison >. La logique etudie le discours, et plus particulierement le(s) raisonnement(s).De tous temps, les hommes se sont disputes et la force a souvent triomphe sur la raison.Les discours eussent souvent pu eviter des drames, pourvu qu’ils aient ete bien compris.Malheureusement, on s’est apercu il y a bien longtemps de la difficulte qu’il y avait a exprimer des choses s^ures et vraies dans notre langue. Celle-ci est source de malentendus.Pour convaincre ou pour se laisser convaincre, il parait indispensable de supprimer les ambigutes de la langue parlee ou ecrite. Nous souhaitons pouvoir comprendre sans equivoque une phrase. En somme, nous aimerions que la semantique d’une phrase soit clairement determinee.
Plus encore, m^eme si chaque phrase a un sens bien precis, il parait necessaire de codier les enchanements de phrases, tout comme dans un jeu ou certains coups ne sont pas autorises. Cette codication, ces regles, ces restrictions, creent une nouvelle langue, beaucoup plus rigide que la < vraie > langue, mais cette rigidite est ce qui nous interesse, car c’est elle qui va nous permettre de decouvrir des proprietes nouvelles.

Chapitre 1 Systemes formels : exemples introductifs

Nous donnons dans cette partie quelques exemples pouvant servir d’introduction aux systemes formels. Tous ces exemples font appel a certaines notions qui ne seront vues que dans les chapitres ulterieurs. Nous suggerons au lecteur de se faire une premiere idee des theories exposees ici, sans pour autant vouloir tout comprendre, puis d’y revenir apres avoir lu le chapitre consacre au calcul des predicats.

Exemple 1 : generation de theoremes de l’arithmetique
Voici un premier exemple repris a Quine
Admettons comme axiomes les deux equations :
et comme regles d’inference :
{ substitution d’une expression quelconque pour toutes les occurences d’une variable
(substitution );
{ si  =  , remplacement de  par  n’importe ou (remplacement des egaux par les egaux ).

Exemple 2 : calcul d’integrales
Exemple 3 : arithmetique de Peano
L’arithmetique de Peano (du nom du mathematicien italien qui l’a introduite) est une des grandes theories etudiees par les logiciens, et utilisee tant par les mathematiciens que par les informaticiens.
Il s’agit d’un systeme pour l’arithmetique usuelle sur les entiers naturels. Les axiomes de ce systeme comportent les symboles < et = pour representer les relations < plus petit > et < egal >. Ils comprennent d’autre part les symboles 0 pour le nombre zero et les symboles s,+ et
pour les operations < successeur >, < addition > et < multiplication >. Dans ce systeme,1 est note s(0) (< successeur de zero >), 2 est note s(s(0)) et ainsi de suite.Ce systeme admet les axiomes suivants :

Calcul des propositions

Introduction
On s’interesse a des armations concernant des choses particulieres, ces armations pouvant etre vraies ou fausses. Ces armations sont des formules et celles que nous considerons sont de deux sortes :
1. Les formules dites atomiques, ou encore propositions, sont des expressions que l’on considere indecomposables; certaines de ces propositions sont vraies, certaines sont fausses; quelquefois la verite (ou la faussete) d’une proposition nous est donnee, quelquefois nous devons la determiner.
2. Les formules composees, ou non atomiques, sont des formules obtenues a partir d’autres formules plus petites en appliquant des operations < logiques >. Dans la pratique, ces operations sont la negation (< non >), la conjonction (< et >), la disjonction (< ou >) et le conditionnel
(< si : : : alors >). On verra par la suite que l’ensemble des operations peut ^etre dierent, car certaines operations sont equivalentes a l’emploi combine de plusieurs autres operations.

Les formules atomiques
On peut decider que les phrases qui suivent sont des propositions (formules atomiques) :
{ < le tableau est propre >;
{ < j’ai ecrit sur le tableau >;
{ < personne ne vient d’eacer le tableau >;
Qu’est-ce qui fait qu’une formule est atomique et qu’une autre ne l’est pas?
La seule chose qui caracterise une formule atomique, c’est le fait que nous nous interdisons de la decomposer ou d’emettre | au sein du langage formel | des considerations relatives..

Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)
Cours logique formelle (516 KO) (Cours PDF)