Qu'est-ce qu'une «preuve de rond-point» dans Propositions en tant que Types par P. Wadler?

Question

En Propositions as Types, il est écrit:

En 1935, à l'âge de 25 ans, Gentzen15 introduit non pas un mais deux nouvelles formulations de déduction logique naturelle et calcul des séquents qui est devenu établi comme les deux principaux systèmes pour formuler une logique et de rester ainsi à ce jour. Il a montré comment normaliser les preuves afin de s'assurer qu'ils n'étaient pas "rond-point", ce qui donne une nouvelle preuve de la cohérence du système de Hilbert . Et, pour couronner le tout, pour correspondre à l'utilisation du symbole ∃ pour la quantification existentielle introduite par Peano, Gentzen a introduit le symbole ∀ pour désigner la quantification universelle. Il a écrit implication comme A ⊃ B (si A tient, puis B tient), conjonction comme A & B (A et B tiennent), et disjonction comme A ∨ B (au moins un de A ou B tient).

Qu'est-ce qu'un rond-point? Pourriez-vous donner un exemple simple? Pourquoi est-ce un problème?

Answer 1

Considérons par exemple: A ∧ B.

Si nous savons A et B, on peut déduire A ∧ B:

A B 
------- I 
A ∧ B 

Ceci est connu comme règle d'introduction.

Dualement, si nous savons A ∧ B nous pouvons en déduire A, ou B:

A ∧ B   A ∧ B 
------- E1  ------- E2 
    A    B 

Ce sont des règles d'élimination.

Ensuite, si nous savons A nous pouvons prouverA en tant que premier déduisant A ∧ A en utilisant la règle d'introduction, et destructives ensuite dans A (et un autre A) en utilisant la règle d'élimination:

A A 
------- I 
A ∧ A 
-------- E1 
    A  

Et ce genre de les ronds-points peuvent se produire dans des épreuves plus grandes.

Il n'y a aucune raison de faire ce tour: nous avons terminé là où nous avons commencé!

Le calcul séquentiel «interdit» les règles d'introduction après les règles d'élimination. Le résultat de Gentzen dit que la logique avec cette propriété est aussi forte que celle où les règles d'élimination après les règles d'introduction sont permises. De nos jours c'est important, car l'espace des preuves est beaucoup plus petit: d'abord nous éliminons (en faisant de petites formules comme nous pouvons/avons besoin), ensuite nous introduisons (pour construire le but). Cela est pratiquement utile, par exemple, pour la recherche automatique de preuves ou la synthèse de programmes.

EDIT la première version de cette réponse avait la preuve de A ∧ B:

A ∧ B   A ∧ B 
------- E1 ------- E2 
    A    B 
    ----------------- I 
     A ∧ B 

Pourtant, à l'exception de la preuve directe:

A ∧ B 

------- Id A ∧ B

il semble être la seule autre "preuve simple". Dans la syntaxe Haskell on écrirait:

proof :: (a, b) -> (a, b) 
proof (x, y) = (x, y) 
-- or 
proof x = x 
proof = id 

Quelles sont (à l'exception des propriétés de strictness, dont la logique ne l'intéresse pas) les mêmes, et les seules définitions raisonnables. Par exemple:

proof :: (a, b) -> (a, b) 
proof x = fst (x, x) 

Est également valide, n'est plus intelligent.