Réalisabilité

Un article de Wikipédia, l'encyclopédie libre.

Si on se place dans un cadre où chaque formule \,A peut être « interprétée » par des programmes (voir l'article Correspondance de Curry-Howard), on dit qu'un programme \,p réalise la formule \,A et l'on écrit p\Vdash A si \,p est précisément l'un des programmes qui « interprète » A.

Remarque : On n'utilise pas la terminologie interprétation, car celle-ci a un sens précis et différent en logique.

La réalisabilité est un concept qui a des liens avec le forçage (ou forcing) dû à Paul Cohen.