questions pour les logiciens

[karlp]

Bonjour

Au hasard de mes lectures, je suis tombé sur une formalisation (?) du raisonnement par l'absurde, dans le langage de la logique propositionnelle, et qui s'écrit ainsi (veuillez m'excuser si j'emploie le langage courant, je ne maîtrise pas le TEX et ai perdu ma fiche avec les codes):

((( non P implique (Q et non Q)) implique non non P)implique P

1) Cette formule est-elle une bonne formalisation du raisonnement par l'absurde (au moins dans certaines de ses formes) ?

2) Cette formule n'est pas une tautologie du calcul propositionnel: cela constitue t'il un argument valable en faveur du rejet (par certains intuitionnistes) de ce type d'argumentation.

Merci infiniment pour la patience de ceux qui voudront bien m'éclairer
-----

[Médiat]

Bonjour cher karlp,

N'étant pas spécialiste de l'intuitionnisme, je ne suis pas sûr de ce qui suit :

1) Il me semble que la formulation par séquent est une formulation plus simple.
2) Le rejet du tiers exclu est plus lié, me semble-t-il à une vision constructive des mathématiques, qu'à une répulsion face à ce principe.

A noter que et ne posent pas de problèmes aux intuitionnistes.

Médiat

[karlp]

Bonjour cher karlp,

N'étant pas spécialiste de l'intuitionnisme, je ne suis pas sûr de ce qui suit :

1) Il me semble que la formulation par séquent est une formulation plus simple.
2) Le rejet du tiers exclu est plus lié, me semble-t-il à une vision constructive des mathématiques, qu'à une répulsion face à ce principe.

A noter que et ne posent pas de problèmes aux intuitionnistes.

Médiat

Bonjour cher Médiat !
Je savais que je pouvais compter sur vous.
1) Cette écriture est en effet plus simple et plus "parlante" (même si ce n'est pas vraiment un critère logique)
2) Ces deux écritures n'impliquent pas l'équivalence entre P et non non P, contrairement à celle que j'ai rencontrée: c'est pourquoi je me demandais si le fait qu'elle ne soit pas une tautologie pouvait être tenu pour un argument valable (je n'aime pas beaucoup l'intuitionnisme, mais je me dois de me faire violence si un des arguments en sa faveur est fondé).

Vous venez, au passage de m'instruire de ce symbole que je ne connaissais pas (celui qui exprime P et nonP).

[invite9dcc7bec]

Au hasard de mes lectures, je suis tombé sur une formalisation (?) du raisonnement par l'absurde, dans le langage de la logique propositionnelle, et qui s'écrit ainsi ((( non P implique (Q et non Q)) implique non non P)implique P

Vraiment ? Pourtant cela n'en est pas une formule équivalente !

Ce que tu nous montre c'est une formule dont le grand membre de gauche ((( non P implique (Q et non Q)) implique non non P) est une tautologie, mais l'ensemble n'en est effectivement pas une.

Par ailleurs, le raisonnement par l'absurde n'est pas un quelconque théorème formel valide dans la logique propositionnelle (ou tautologie sur le plan sématique). C'est une preuve simple. On ne peut pas en donner une formulation plus simple que si non-p mène à une antinomie alors p, c'est à dire que l'on ne peut pas la dériver d'autres preuves/règles d'inférence (en particulier on ne peut pas la dériver de la règle d'introduction de la négation, si p implique une antinomie alors non-p).

Comme le dit Médiat, l'intuitionnisme n'est pas là pour démontrer une erreur de la logique standard. Si Brouwer l'a introduit c'est sur la base d'arguments philosophiques, résumés par la formule « il n'y a pas de vérité sans expérience de la vérité ». Après l'intuitionnisme a connu du succès pour son utilité en mathématiques et informatique théorique, mais je n'en connais pas les détails. La meilleure manière de concevoir la pléthore de logiques différentes actuellement disponibles (une logique étant un ensemble syntaxe-sémantique-règles d'inférence) n'est pas de les penser comme des théories rivales sur ce qu'est le vrai mais comme des outils pour modéliser des problèmes/raisonnements différents. (Pour avoir une idée de l'aspect pléthorique, une liste non-exhaustive : logique intuitionniste, logique modale, logique déontique, logique libre, logique floue, logique temporelle, logique défaisable,...)

[A voir en vidéo sur Futura]