Lazi

Représenter la théorie des ensembles dans Lazi

Contexte

Pour la documentation sur Lazi, j'aimerais montrer que Lazi permet de représenter la théorie de l'ensemble et d'ajouter la notion de catégorie.

Mon argument de fond est l'adéquation entre Lazi et la réalité plus la souplesse de Lazi qui a pour objets toute chose. Mais Il me semble nécessaire d'apporter des arguments plus concrets.

Question

Quelle est la représentation la plus simple de la théorie des ensembles en Lazi ?

Étude

Références

L'objet des fondations classiques est le prédicat et non l'ensemble

Tout ensemble E a un prédicat unaire correspondant : P(x) = x ∈ E
D'autre part règles sur les prédicats n'ont pas de correspondance directes en Lazi. Donc en Lazi il nous faut voir les prédicats comme des objets d'étude.

Donc pour représenter un modèle de la théorie des ensembles en Lazi il faut représenter :

  • les prédicats : Pred,
  • les ensembles (qui sont une sous partie des prédicats : Set).
  • les vérités : Truths

Essai 1 : représentation concrète

Idée

L'idée est d'utiliser l'adéquation de certains éléments de Lazi avec la fondation classique :

  • l'implication classique et ⊢ de lazi
  • vra et la vérité lazi
  • l'ensemble vide, représenté par constF \ 1b=0b
  • ⊤ et (1b=1b)
  • ⊥ et (1b=0b)

Les points ne correspondant pas :

  • ∃ ? à voir
  • le tiers exclu

Si on garde le tiers exclue on a un problème fatal avec cette correspondance. Donc cette correspondance n'est intéressante que pour voir le lien entre Lazi et la théorie des ensembles avec le tiers exclu de Lazi.

On peut aussi étudier une extension de Lazi qui permet d'assimiler les ¬¬A à A : pour cela on ajoute une règle qui déduit A de ¬¬A avec un critère de validité qui fait que l'on peut après traduire les preuves en ajoutant partout sur les vérités le nombre de double négations nécessaires à rendre la preuve valide. En effet de X on peut déduire ¬¬X donc on peut toujours ajouter des doubles négations aux vérités. Donc si l'objet X de la preuve vérifie (sans l'extension) X = ¬¬X, la traduction d'une preuve utilisant cette extension est possible.

Réponse

@todo