Retour
Cours précédent
Cours suivant

Incomplétude de la logique minimale

Logique minimale

• Assez “pauvre” : seulement deux connecteurs (implication et négation)
• Propriété de cohérence : tout séquent prouvable est valide
• Pas de propriété de complétude : réciproque tout séquent valide est prouvable : impossible en logique minimale

Arbre de preuves

Les preuves sont sous forme d’arbres, sans règles dérivées.
Chaque nœud porte un séquent.
Les nœuds sont :

• “hyp” pour les feuilles
• ”\(\to _i\)” ou “\(\bot _e\)” pour les nœuds unaires
• “mp” pour les nœuds binaires

Formule de Peirce

\[((P\to Q)\to P)\to P\]

C’est une tautologie donc ce séquent est valide.
Mais il n’admet pas de preuve en logique minimale.

Préservation locale des hypothèses

Dans tout arbre de preuve correct, dans le séquent de chaque nœud autre que la racine, on trouve au moins toutes les hypothèses du séquent du parent de ce nœud.

Coupures

Dans un arbre de preuve, on appelle coupure la configuration de deux nœuds suivante :

• un nœud s : \(\Gamma \vdash B\) utilisant la règle du modus ponens
• un nœud t : \(\Gamma \vdash A\to B\), fils de gauche de s, utilisant la règle d’introduction de l’implication

Élimination de la coupure

\[\frac{\Gamma\vdash A,\Delta\qquad\Gamma',A\vdash\Delta'}{\Gamma,\Gamma'\vdash\Delta,\Delta'}\]

Ou en plus simple :

\[\frac{\Gamma\vdash A\qquad\Pi,A\vdash B}{\Gamma,\Pi\vdash B}\]

Sous-formules

Une formule est un arbre. Une sous-formule est sous-arbre.

Exemple : \((P\to Q)\to R\to S\)
Les sous-formules sont :

• \[P, Q, R, S\]
• \[P\to Q\]
• \[R\to S\]
• \[(P\to Q)\to R\to S\]

Attention : \((P\to Q)\to R\) n’est pas une sous-formule de \((P\to Q)\to R\to S\).

Retour
Cours précédent
Cours suivant