#HoTT The Book : 1.11 propositions as types

The HoTT Book

https://hott.github.io/book/nightly/hott-online-1075-g3c53219.pdf

Je passe sur ce qui n’est pas essentiel pour aller plus vite car il faut accélérer pour en arriver aux choses sérieuses qui commencent au chapitre 2.

Passons donc Page 41 au 1.11:

Les termes ou éléments d’un type comme proposition sont conçus comme des « évidences », des « témoins » de la vérité de cette proposition.

Ainsi les propositions sont des types particuliers, dont les éléments sont des preuves.

Dans le système de Bolzano:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/08/bolzano-une-theorie-des-idees/

Les propositions sont de nature lectologique comme les autres idées : elles n’existent pas dans le monde comme les étants, objets ou qualités.

Ce sont des idées qui réfèrent à leur valeur de vérité , 1 si elles sont vraies et 0 si elles sont fausses.

Le tableau en deux colonnes page 41 donne la correspondance entre les opérations logiques sur des propositions en langue naturelle et les opérations de la théorie des types.

Ainsi Vrai correspond à 1, faux à 0, «  et » au produit de deux types, « ou «  à la somme, «  si » à A → B, « non » à A → 0

La logique de la théorie des types est constructive ce qui veut dire qu’elle se limite à des constructions qui peuvent être effectivement menées à bout. Des principes comme le tiers exclus’ ou les démonstrations par l’absurde n’y sont pas valides .
Le caractère constructif signifie aussi que les procédures ont un intérêt calculatoire intrinsèque, ce qui intéresse les «  computer scientists »

Page 44 le tableau à deux colonnes de la page 41 se poursuit au delà de la logique propositionnelle, par la logique des prédicats, qui fait intervenir des quantificateurs.

Ainsi une assertion : » pour tout x: A on a P(x) » correspond en théorie des types à :

Πx:A P(x)

Tandis qu’une assertion d’existence «  il existe un x:A tel que P(x) » correspond à :

Σx:AP(x)

À voir aussi:

https://gciruelos.com/propositions-as-types.html

http://math.andrej.com/2004/05/04/propositions-as-types/

http://math.andrej.com/data/bracket_types.pdf

Constructive Validity

https://golem.ph.utexas.edu/category/2012/01/propositions_as_some_types_and.html

https://ncatlab.org/nlab/show/propositions+as+types

Advertisements
This entry was posted in homotopy type theory. Bookmark the permalink.