Style de Fitch pour la déduction naturelle - Définition

Exemples

Nous donnons ci-dessous quelques exemples d'utilisation de la déduction naturelle. Dans la première partie, nous n'utiliserons pas la règle d'élimination de la double négation. Dans la deuxième partie, nous utiliserons cette règle. Les formules déduites dans cette deuxième partie ne sont pas reconnues valides par les mathématiciens intuitionnistes. Nous utiliserons les symboles suivants : pour si ... alors ..., pour ou, pour et, pour non. Le symbole désigne une contradiction, c'est-à-dire une proposition fausse.

Exemples n'utilisant pas l'élimination de la double négation

Exemple 1 :

(hypothèse provisoire)

(élimination de la conjonction 01)

(élimination de la conjonction 01)

(hypothèse provisoire)

(hypothèse provisoire)

contradiction entre 02 et 05

(introduction de l'implication entre 05 et 06)

(hypothèse provisoire)

contradiction entre 03 et 08

(introduction de l'implication entre 08 et 09)

(élimination de la disjonction entre 04, 07, 10)

(introduction de la négation entre 04 et 11)

(introduction de l'implication entre 01 et 12 et fin de la déduction)

On montre que la réciproque est également valide. On montre également que , mais pour la réciproque de cette dernière propriété, on utilise l'élimination de la double négation.

Exemple 2 :

(hypothèse provisoire)

(hypothèse provisoire)

(élimination de la négation entre 01 et 02)

(introduction de la négation entre 02 et 03)

(introduction de l'implication entre 01 et 04, fin de la déduction)

La réciproque découle directement de l'élimination de la double négation et est rejetée par les intuitionnistes. Mais curieusement, il n'en est pas de même de qui se prouve sans cette hypothèse, et qui, elle, est acceptée par les intuitionnistes.

Exemple 3 :

(hypothèse provisoire)

(hypothèse provisoire)

(théorème de l'exemple 2)

(élimination de l'implication ou modus ponens entre 02 et 03)

(élimination de la négation entre 01 et 04)

(introduction de la négation entre 02 et 05)

(introduction de l'implication entre 01 et 06, fin de la déduction)

Exemples utilisant l'élimination de la double négation

Les exemples qui suivent utilisent l'élimination de la double négation. On peut montrer que cette utilisation est nécessaire. Ils ne sont donc pas acceptés en logique intuitionniste.

Exemple 4 :

(hypothèse provisoire [raisonnement par l'absurde])

(hypothèse provisoire)

(théorème, réciproque de l'exemple 1)

(élimination de l'implication ou modus ponens entre 02 et 03)

(élimination de la double négation dans 04)

(élimination de la négation entre 01 et 05)

(introduction de la négation entre 02 et 06)

(élimination de la double négation dans 07)

(introduction de l'implication entre 01 et 08)

Exemple 5 : si ne nécessite pas l'élimination de la double négation, celle-ci est nécessaire pour prouver la réciproque .

Exemple 6: On peut démontrer que . En effet si on et A, on a (faux) et donc on a B.

Exemple 7 : de même la démonstration de la validité du tiers exclu utilise l'élimination de la double négation. En supposant que , on en déduit (réciproque de l'exemple 1), d'où une contradiction et la validité de .

Si les intuitionnistes rejettent le tiers exclu, ils acceptent bien sûr le principe de non contradiction : . En effet, la supposition est une contradiction. On a donc par introduction de la négation.

Exemple 7 connu sous le nom de loi de Peirce : . Curieusement, bien que ne contenant pas de négation, la déduction de cette loi nécessite l'élimination de la double négation, par exemple par l'intermédiaire de l'utilisation du tiers exclu. On suppose que l'on a . D'après le tiers exclu:

.ou bien on a A,

.ou bien on a et donc on a (exemple 6) et puisqu'on a avec le modus ponens, on a A.