Lazi

Tiers exclu dans une logique de niveau 1

Contexte

Dans les raisonnements, on peut être amené à vouloir utiliser le tiers exclu pour des propriétés de niveau 1 comme "le calcul est infini".

Question

Peut-on avoir un théorème du tiers exclu en logique de niveau 1 ?

Étude

Essai 2

Contrairement à l'essai 1, on ne définit pas les autres symboles logiques de niveau 1 à partir de l'implication. Ainsi on a nos propres règles pour définir "∨". Le but est d'éviter des horreurs comme "∀ x ;; x ∨ ¬ x".

Dans ce cas le "or" de niveau 1 fournit déjà la règle du tiers exclu de niveau 1.

Essai 1 (abandonné)

L'implication (logique niveau 1) est définie par une règle. À partir de imply, on peut définir les autres opérations logique de niveau 1.

x ∨ y = ¬ x ⇒ y = (x ⇒ ⊥) ⇒ y

Donc il faut montrer que si on a les hypothèses:

  • (x ⇒ ⊥) ⇒ y
  • x ⇒ z
  • y ⇒ z
alors on peut déduire :
  • z

Idée de preuve n°1

Pour démontrer (x ⇒ ⊥) ⇒ y, soit l'hypothèse x ⇒ ⊥ est utilisée, soit elle ne l'est pas.
Si x ⇒ ⊥ n'est pas utilisé, alors y est vrai, donc par y ⇒ z on déduit z.
Si x ⇒ ⊥ est utilisé, en traduisant la preuve, on aboutit à l'application de x ⇒ ⊥ et donc à ce que x soit prouvé (faux), donc on peut utiliser x ⇒ z et démontrer z.

Donc pour ajouter le tiers exclu de niveau 1, il faudrait passer par une extension car la preuve ci-dessus est celle de la validité d'une extension.

Problème ?

Pour x quelconque, on a (x ⇒ ⊥) ⇒ (x ⇒ ⊥) , donc on a x ∨ ¬ x. Le raisonnement ci-dessus est faux car x ⇒ ⊥est utilisé sans pour autant appliquer x ⇒ ⊥ et avoir x prouvé.

Tiers exclu de niveau 1 et traduction

Prenons l'exemple simple de "calculable". Si on arrivait à utiliser le tiers exclu de niveau 1 sur la calculabilité d'une formule x, pour démontrer une chose y. Comment pourrait-on traduire cette preuve ?

Supposons que la preuve ne comporte pas de conditions ou variable, on peut donc la traduire.
Mais si on calcul x pour savoir si il est calculable, cela ne fonctionne que si x est calculable. Comment alors pourrait-on savoir quelle est la preuve du tiers exclu à utiliser ?

On peut prouver par récurrence que pour chaque étape du calcul par "calculable", les valeurs utilisées dans le calcul vérifient les propriétés voulues (comme "être une formule").

Changer les règles sur if ?

Traduire par une recherche de preuve ?

Réponse

Oui (voir essai 2), par les règles de déduction pour l'utilisation du "or" de niveau 1.

@todo