Nous sommes arrivés, dans notre étude de la logique, à un point tournant, car c’est ici que nous commençons la révision des Systèmes Déductifs de la Logique Propositionnelle. C’est là que tout ce que nous avons vu commence à devenir opérationnel et où le véritable esprit de la logique se dévoile, car nous étudierons l’essence des démonstrations. À ce stade, on suppose que vous avez déjà vu comment écrire des expressions et que vous comprenez de quoi il s’agit en logique propositionnelle ; et si ce n’est pas totalement clair, il est recommandé de revoir les cours précédents.

Ceci fait, ce qui suit maintenant est de revoir la manière dont les expressions de la logique propositionnelle se rapportent entre elles pour former une déduction. Le mécanisme à travers lequel ces relations sont construites est le système déductif formel.

Qu’est-ce qu’un Système Déductif Formel ?

Les systèmes déductifs formels, ou systèmes de calcul déductif, ont trois composants élémentaires :

1. Un Langage Formel.
2. Un Schéma Axiomatique.
3. Règles d’Inférence Élémentaires.

Nous avons déjà examiné tout ce qui est lié aux langages formels. Maintenant, il est temps d’introduire les schémas axiomatiques et les règles d’inférence élémentaires.

Pour la construction du système déductif du calcul propositionnel, nous commencerons par assembler le système déductif à partir des Axiomes de Łukasiewicz, et comme règle d’inférence élémentaire, nous utiliserons le Modus Ponens.

Les Axiomes de Łukasiewicz pour la Logique Propositionnelle

Si \alpha, \beta et \gamma sont des expressions du calcul propositionnel, alors les suivants sont des axiomes du calcul propositionnel :

Le Modus Ponens : Le moteur déductif du calcul propositionnel

Si \alpha et \beta sont des expressions valides du calcul propositionnel, alors le modus ponens établit qu’à partir de \alpha et (\alpha \rightarrow \beta) on déduit \beta. Sous forme de raisonnement, cela s’écrit de la manière suivante :

Ici, le Modus Ponens est abrégé entre les étapes (1) et (2) par l’écriture « MP(1,2) », et la synthèse de tout cela se représente à travers la notation :

Par conséquent \{\alpha, (\alpha \rightarrow \beta)\}\vdash \beta

Nous verrons bientôt qu’à partir des axiomes de Łukasiewicz et du Modus Ponens, toutes les techniques de déduction du calcul propositionnel peuvent être construites, synthétisant les règles de base du raisonnement habituel et servant de base fondamentale pour la logique classique.

Raisonnements, théorèmes et prémisses

Dans les systèmes déductifs de la logique propositionnelle, on exécute des raisonnements (ou déductions), et ceux-ci sont toute succession d’expressions où chacune d’elles est, ou une prémisse ou une expression obtenue à partir des prémisses en utilisant seulement les axiomes de Łukasiewicz et le modus ponens. Un théorème est le résultat d’une déduction sans prémisse. Une prémisse peut être toute expression qui n’est ni un axiome ni déduite de ceux-ci. En général, quand nous avons un ensemble de prémisses \Gamma et une expression \alpha obtenue en utilisant un élément de \Gamma, les axiomes et le modus ponens, on écrit « \Gamma \vdash \alpha » et on dit que

de \Gamma se déduit \alpha

Si \Gamma est un ensemble vide, alors au lieu d’écrire « \emptyset\vdash \alpha« , on écrit «  \vdash \alpha .  » Cela se lit « \alpha est un théorème ». Cette façon de représenter les théorèmes peut être étendue à la représentation des axiomes de sorte que, si \alpha, \beta et \gamma sont des expressions, alors les axiomes de Łukasiewicz peuvent être écrits sous la forme

C’est à partir de cela que l’on dit que les axiomes sont des affirmations évidentes par elles-mêmes, ou que les théorèmes sont des expressions qui se déduisent à partir du vide, ou que axiomes et théorèmes sont des propriétés du calcul propositionnel.

Comment exécuter une démonstration en logique propositionnelle ?

À ce stade, nous cesserons de parler de théorie pour passer à la pratique. Il est vrai que beaucoup de choses peuvent être dites sur l’exécution d’une démonstration ; mais bien qu’on puisse dire des choses brillantes sur les systèmes déductifs et la logique propositionnelle, et toutes soient comprises, cela n’implique pas nécessairement le développement des compétences nécessaires pour exécuter une démonstration. Pour cette raison, afin d’enseigner comment se font les démonstrations, nous examinerons la démonstration d’un théorème simple.

Théorème

Si \alpha est une expression de la logique propositionnelle, alors il est vrai que

\vdash (\alpha\rightarrow \alpha)

Démonstration

Par conséquent \vdash (\alpha\rightarrow\alpha)

Fin de la démonstration.

Comme on peut le voir, dans les systèmes déductifs et la logique propositionnelle, les démonstrations ne sont pas triviales, mais une fois construites, elles sont faciles à reproduire.

Maintenant, avant de nous plonger tête première dans les déductions avec ces techniques, nous allons d’abord développer quelques propriétés et définitions qui seront extrêmement utiles pour cette tâche, car si nous raisonnons seulement avec cela, nous rencontrerons de terribles problèmes.

Le concept d’équivalence prouvée

Si \alpha et \beta sont des expressions quelconques et qu’il est simultanément vrai que \{\alpha\}\vdash \beta et \{\beta\} \vdash \alpha, alors on dit que \alpha et \beta sont prouvés équivalents et on l’écrira \alpha \dashv \vdash \beta. Cela se résume symboliquement comme suit :

\left(\{\alpha\}\vdash\beta \wedge \{\beta\}\vdash\alpha \right) \Leftrightarrow \left(\alpha\dashv\vdash\beta\right)

Cela se lit : de \alpha on déduit \beta, et de \beta on déduit \alpha si et seulement si \alpha et \beta sont prouvés équivalents.

Ceci est une méta-propriété de la logique propositionnelle

Le (méta)Théorème de Déduction

Si \alpha et \beta sont des expressions du calcul propositionnel, et \Gamma est un ensemble de prémisses ; alors il est vrai que si de \Gamma \cup \{\alpha\} on déduit \beta, alors à partir de \Gamma on déduit (\alpha \rightarrow \beta). Symboliquement cela s’exprime comme suit :

\left(\Gamma \cup \{\alpha\}\vdash \beta \right) \Rightarrow \left( \Gamma\vdash(\alpha\rightarrow\beta)\right)

Démonstration :

Pour que \Gamma \cup \{\alpha\}\vdash \beta soit vrai, il est nécessaire d’avoir une déduction de la forme

Par conséquent \Gamma\cup\{\alpha\} \vdash \beta

Pour que cela soit possible, il est nécessaire qu’au moins une des expressions \gamma_1, \cdots, \gamma_n, \overline{\gamma_1}, \cdots, \overline{\gamma_m} soit de la forme (\alpha\rightarrow \beta), mais toutes ces lignes n’impliquent que des éléments de \Gamma et les axiomes de Łukasiewicz dans leur déduction, donc il doit être vrai que \Gamma\vdash (\alpha \rightarrow \beta). Ainsi, le théorème est démontré

Fin de la démonstration.

Le Réciproque du Théorème de Déduction

Dans les mêmes conditions que le théorème de déduction, il s’ensuit que

\left(\Gamma\vdash(\alpha \rightarrow \beta)\right) \Rightarrow \left( \Gamma \cup \{\alpha\}\vdash \beta \right)

Démonstration :

Si \Gamma\vdash (\alpha\rightarrow \beta) est vrai, alors on a une déduction de la forme

Maintenant, si nous ajoutons \alpha comme prémisse à ce raisonnement, alors nous aurons les lignes suivantes

Par conséquent \Gamma \cup \{\alpha\} \vdash \beta

Ce qui était à démontrer.

Fin de la démonstration.

Déductions sur les Expressions et Déductions sur les Déductions

Des démonstrations comme celle faite précédemment pour arriver au résultat \vdash (\alpha\rightarrow \alpha) sont des cas de déductions basées sur des expressions, car chaque étape contient une expression spécifique. De manière analogue, il est possible de faire des déductions basées sur d’autres déductions, où chaque étape est une déduction en soi. En pratique, les deux sont faites de manière analogue, mais la seconde nous permet d’utiliser le théorème de déduction et son réciproque, donnant une grande flexibilité à la technique de raisonnement. Pour voir cela, démontrons à nouveau que \vdash (\alpha \rightarrow \alpha), mais cette fois en utilisant des déductions au lieu d’expressions. Une alternative à cela est la suivante :

Notons que ce raisonnement n’est pas plus court que celui que nous avions fait auparavant, mais il est beaucoup plus facile à réaliser, nous nous contentons du théorème de déduction, de son réciproque et du schéma axiomatique A1 pour construire la démonstration.

En apparence, dans le développement que nous venons de faire, nous utilisons un seul axiome de Łukasiewicz et nous oublions à la fois d’autres axiomes et le modus ponens. Cela implique-t-il que, en raisonnant de cette manière, nous oublions les autres axiomes et le modus ponens ? La réponse est oui et non. D’un côté, nous pouvons faire comme si nous oublions certains axiomes et le modus ponens simplement parce que nous ne les utilisons pas de manière explicite, cependant, il faut se rappeler que le théorème de déduction et son réciproque sont précisément la conséquence des axiomes de Łukasiewicz et du modus ponens, ce qui implique que, en les utilisant, comme nous l’avons fait dans le raisonnement que nous venons de voir, nous faisons un usage implicite d’eux.

Règle de Monotonie

Si \tau est un théorème, alors il sera vrai que, pour toute expression \beta, il s’ensuit que

\{\beta\}\vdash\tau

Ceci est en réalité une règle très facile à prouver, car étant \tau un théorème, il est vrai que \vdash \tau. C’est-à-dire qu’il existe un raisonnement qui, sans nécessiter l’ajout de prémisses, conduit à l’expression \tau, donc ajouter une expression supplémentaire aux prémisses (vide) ne fera aucune différence.

De manière similaire à cela, on peut énoncer le résultat suivant : si d’un ensemble de prémisses \Gamma on déduit \gamma, alors il s’ensuit que

\Gamma\cup\{\alpha\}\vdash\gamma

Où \alpha est une expression quelconque.

Synthèse et Réflexions sur les Systèmes Déductifs et la Logique Propositionnelle

Lorsque nous dotons le langage de la logique propositionnelle d’une règle d’inférence et d’expressions de base : Le Modus Ponens et les Axiomes de Łukasiewicz, ce que nous faisons est analogue à assembler une « machine déductive » et un « moteur qui lui fournit l’énergie pour se mettre en mouvement ». À partir de là, toutes les règles de base de la déduction commencent à émerger naturellement et nous commencerons à les examiner dans les livraisons immédiatement après celle-ci.

Un autre détail. Les expressions de la logique propositionnelle sont en réalité des méta-expressions du langage à deux symboles que nous avons vu précédemment. Rappelons que l’intérêt de ces méta-expressions est qu’elles nous permettent de remplacer leurs méta-variables par n’importe quelle expression du langage pour obtenir une nouvelle qui satisfait cette structure. Lorsque nous dotons le langage de logique propositionnelle de schémas axiomatiques et de règles d’inférences, nous construisons les Systèmes Déductifs de la logique propositionnelle qui permettent de générer des déductions reliant les expressions. En résultat, nous avons un schéma déductif capable d’englober une infinité de déductions : toutes celles que nous pouvons obtenir en remplaçant les méta-variables par les expressions que nous voulons. Le pouvoir de la logique se déchaîne, en réalité, lorsque nous réalisons qu’en plus de ces expressions du langage à deux symboles que nous avons utilisées au début, nous observons ce qui se passe lorsque nous remplaçons à la place des expressions de notre langue habituelle et, par conséquent, nous sommes émerveillés.