Une sémantique qui interprète les formules logiques par des ensembles de témoins constructifs ou d'objets computationnels (réalisateurs) qui montrent comment la formule peut être exhibée ou calculée, reliant la syntaxe des preuves au contenu exécutable.

Principe

Attribuer à chaque formule une classe d'objets constructifs de sorte que conjonctions, implications et quantificateurs se traduisent par des opérations combinatoires ou computationnelles correspondantes ; une formule est considérée vraie si elle admet un réalisateur.

Démonstration

La réalisabilité à la Kleene pour l'arithmétique : un entier naturel (ou l'indice d'une fonction récursive) joue le rôle de témoin qui calcule la sortie exigée par une assertion existentielle ou transforme des témoins d'antécédents en témoins de conséquents pour les implications.

Mauvaise application

Considérer qu'une preuve d'existence classique non constructive fournit un réalisateur sans extraire de témoin explicite, ou confondre la réalisabilité avec la vérité au sens modèle-théorique lorsque la calculabilité est cruciale.

Conséquence

Correctement appliquée, la réalisabilité fournit des algorithmes explicites issus des preuves, des résultats de consistance constructifs et un pont entre théorie des preuves et calcul, par exemple l'extraction de programmes via des correspondances de type Curry–Howard.

Inversion

Au lieu de témoins qui construisent la vérité, considérer des réfutations ou falsificateurs (contre-réalisateurs) qui attestent de l'échec ; on inverse ainsi l'accent de la construction du contenu vers la démonstration d'impossibilité.

Limite

S'applique principalement en logique constructive ou intuitionniste et aux théories où le contenu computationnel a du sens ; elle ne capture pas directement la sémantique classique non constructive ni la vérité purement modèle-théorique sans adaptations.

Tension sémantique

Tension avec la vérité modèle-théorique : la réalisabilité met l'accent sur la manière dont une formule est exhibée computationnellement, alors que la sémantique classique se concentre sur l'appartenance d'une formule à une structure abstraite ; les deux perspectives peuvent converger ou diverger.

Synthèse

La réalisabilité est une affectation de témoins computationnels aux formules qui rend les preuves exécutables : elle organise les connecteurs logiques en opérations sur les réalisateurs, permettant l'extraction d'algorithmes et l'interprétation constructive du raisonnement formel.