Dans un système formel F, on se demande si on peut trouver une preuve de l'énoncé math S t.q. le nb de symboles de la preuve < n. Le problème est décidable, il faut chercher la preuve dans tout le code de F dont les cordes (bit-strings) < n (c'est comme...

Un énoncé peut être vrai s'il peut être vérifié. Un énoncé a du sens s'il est vrai ou faux, et nous savons ce qui est le cas quand il est vrai. Nous savons ce qui est le cas si l'énoncé (A) "Il y aura de la neige au sommet du mont Everest même après que...