Théories Axiomatiques De La Vérité

Table des matières:

Théories Axiomatiques De La Vérité
Théories Axiomatiques De La Vérité

Vidéo: Théories Axiomatiques De La Vérité

Vidéo: Théories Axiomatiques De La Vérité
Vidéo: Малыш Панда Кики Плачет в Детском Саду | Анимации и Детские Песни | BabyBus 2024, Mars
Anonim

Navigation d'entrée

  • Contenu de l'entrée
  • Bibliographie
  • Outils académiques
  • Aperçu du PDF des amis
  • Informations sur l'auteur et la citation
  • Retour au sommet

Théories axiomatiques de la vérité

Publié pour la première fois le 26 décembre 2005; révision de fond jeu.18 janv.2018

Une théorie axiomatique de la vérité est une théorie déductive de la vérité en tant que prédicat primitif non défini. En raison du menteur et d'autres paradoxes, les axiomes et les règles doivent être choisis avec soin afin d'éviter les incohérences. De nombreux systèmes d'axiomes pour le prédicat de vérité ont été discutés dans la littérature et leurs propriétés respectives ont été analysées. Plusieurs philosophes, dont de nombreux déflationnistes, ont approuvé les théories axiomatiques de la vérité dans leurs récits de la vérité. Les propriétés logiques des théories formelles sont pertinentes pour diverses questions philosophiques, telles que les questions sur le statut ontologique des propriétés, les théorèmes de Gödel, le déflationnisme théorique de la vérité, l'éliminabilité des notions sémantiques et la théorie du sens.

  • 1. Motivations

    • 1.1 Vérité, propriétés et ensembles
    • 1.2 Vérité et réflexion
    • 1.3 Déflationnisme théorique de la vérité
  • 2. La théorie de base

    • 2.1 Le choix de la théorie de base
    • 2.2 Conventions de notation
  • 3. Théories de la vérité typées

    • 3.1 Prédicats de vérité définissables
    • 3.2 Les phrases (T) -
    • 3.3 Vérité compositionnelle
    • 3.4 Théories hiérarchiques
  • 4. Vérité sans type

    • 4.1 Sans type (T) - phrases
    • 4.2 Compositionnalité
    • 4.3 La théorie de Friedman – Sheard et la sémantique de la révision
    • 4.4 La théorie de Kripke-Feferman
    • 4.5 Capture du point fixe minimal
    • 4.6 Axiomatisations de la théorie de Kripke avec des supervaluations
  • 5. Approches non classiques de l'auto-référence

    • 5.1 Le prédicat de vérité dans la logique intuitionniste
    • 5.2 Axiomatiser la théorie de Kripke
    • 5.3 Ajout d'un conditionnel
  • Bibliographie
  • Outils académiques
  • Autres ressources Internet
  • Entrées connexes

1. Motivations

Il y a eu de nombreuses tentatives pour définir la vérité en termes de correspondance, de cohérence ou d'autres notions. Cependant, il est loin d'être clair que la vérité soit une notion définissable. Dans des contextes formels satisfaisant certaines conditions naturelles, le théorème de Tarski sur l'indéfinissabilité du prédicat de vérité montre qu'une définition d'un prédicat de vérité nécessite des ressources qui vont au-delà de celles du langage formel pour lequel la vérité va être définie. Dans ces cas, les approches définitionnelles de la vérité doivent échouer. En revanche, l'approche axiomatique ne présuppose pas que la vérité puisse être définie. Au lieu de cela, un langage formel est développé par un nouveau prédicat primitif pour la vérité ou la satisfaction, et des axiomes pour ce prédicat sont ensuite posés. Cette approche en elle-même n'exclut pas la possibilité que le prédicat de vérité soit définissable,bien que dans de nombreux cas, on puisse montrer que le prédicat de vérité n'est pas définissable.

Dans les théories sémantiques de la vérité (par exemple, Tarski 1935, Kripke 1975), en revanche, un prédicat de vérité est défini pour un langage, le soi-disant langage objet. Cette définition est effectuée dans un métalangage ou métathéorie, qui est généralement considérée comme incluant la théorie des ensembles ou au moins une autre théorie forte ou un langage interprété expressivement riche. Le théorème de Tarski sur l'indéfinissabilité du prédicat de vérité montre que, étant donné certaines hypothèses générales, les ressources du métalangage ou de la métathéorie doivent dépasser les ressources du langage-objet. Les approches sémantiques nécessitent donc généralement l'utilisation d'un métalangage plus puissant que le langage objet pour lequel il fournit une sémantique.

Comme avec d'autres systèmes déductifs formels, les théories axiomatiques de la vérité peuvent être présentées dans des cadres logiques très faibles. Ces frameworks nécessitent très peu de ressources, et en particulier, évitent le besoin d'un métalangage et d'une métathéorie forts.

Un travail formel sur les théories axiomatiques de la vérité a contribué à éclairer les théories sémantiques de la vérité. Par exemple, il a fourni des informations sur ce qui est exigé d'un métalangage suffisant pour définir un prédicat de vérité. Les théories sémantiques de la vérité, quant à elles, fournissent les outils théoriques nécessaires pour étudier les modèles de théories axiomatiques de la vérité et les motivations de certaines théories axiomatiques. Ainsi, les approches axiomatiques et sémantiques de la vérité sont étroitement liées.

Cette entrée décrit les théories axiomatiques les plus populaires de la vérité et mentionne certains des résultats formels qui ont été obtenus à leur sujet. Nous ne donnons que des indications quant à leurs applications philosophiques.

1.1 Vérité, propriétés et ensembles

Les théories de la vérité et de la prédication sont étroitement liées aux théories des propriétés et de l'attribution des propriétés. Dire qu'une formule ouverte (phi (x)) est vraie pour un individu (a) semble équivalent (dans un certain sens) à l'affirmation que (a) a la propriété d'être telle que (phi) (cette propriété est signifiée par la formule ouverte). Par exemple, on pourrait dire que «(x) est un pauvre philosophe» est vrai de Tom au lieu de dire que Tom a la propriété d'être un pauvre philosophe. La quantification sur des propriétés définissables peut alors être imitée dans un langage avec un prédicat de vérité en quantifiant sur des formules. Au lieu de dire, par exemple, que (a) et (b) ont exactement les mêmes propriétés, on dit qu'exactement les mêmes formules sont vraies pour (a) et (b). La réduction des propriétés à la vérité fonctionne aussi dans une certaine mesure pour des ensembles d'individus.

Il y a aussi des réductions dans l'autre sens: Tarski (1935) a montré que certaines hypothèses d'existence de second ordre (par exemple, les axiomes de compréhension) peuvent être utilisées pour définir la vérité (voir l'entrée sur la définition de la vérité de Tarski). L'analyse mathématique des théories axiomatiques de la vérité et des systèmes du second ordre a montré de nombreuses équivalences entre ces hypothèses d'existence de second ordre et les hypothèses de la théorie de la vérité.

Ces résultats montrent exactement ce qui est nécessaire pour définir un prédicat de vérité qui satisfait certains axiomes, affinant ainsi les idées de Tarski sur la définissabilité de la vérité. En particulier, les équivalences de la théorie de la preuve décrites dans la section 3.3 ci-dessous expliquent dans quelle mesure un métalangage (ou plutôt une métathéorie) doit être plus riche que le langage objet pour pouvoir définir un prédicat de vérité.

L'équivalence entre les théories du second ordre et les théories de la vérité a également une incidence sur les sujets métaphysiques traditionnels. Les réductions des théories du second ordre (c'est-à-dire des théories des propriétés ou des ensembles) en théories axiomatiques de la vérité peuvent être conçues comme des formes de nominalisme réducteur, car elles remplacent les hypothèses d'existence d'ensembles ou de propriétés (par exemple, les axiomes de compréhension) par des hypothèses ontologiquement inoffensives, dans le cas présent par des hypothèses sur le comportement du prédicat de vérité.

1.2 Vérité et réflexion

Selon les théorèmes d'incomplétude de Gödel, l'affirmation selon laquelle Peano Arithmetic (PA) est cohérente, sous sa forme d'énoncé de la théorie des nombres (étant donné la technique de numérotation de Gödel), ne peut pas être dérivée dans PA lui-même. Mais l'AP peut être renforcée en ajoutant cette déclaration de cohérence ou par des axiomes plus forts. En particulier, des axiomes exprimant partiellement la solidité du PA peuvent être ajoutés. Ce sont des principes de réflexion. Un exemple de principe de réflexion pour PA serait l'ensemble des phrases (Bew_ {PA} (ulcorner / phi / urcorner) rightarrow / phi) où (phi) est une formule du langage de l'arithmétique, (ulcorner / phi / urcorner) un nom pour (phi) et (Bew_ {PA} (x)) est le prédicat de prouvabilité standard pour PA ('(Bew)' a été introduit par Gödel et est l'abréviation du mot allemand «beweisbar», c'est-à-dire «prouvable»).

Le processus d'ajout de principes de réflexion peut être itéré: on peut ajouter, par exemple, un principe de réflexion R pour PA à PA; il en résulte une nouvelle théorie PA + R. Puis on ajoute le principe de réflexion du système PA + R à la théorie PA + R. Ce processus peut être poursuivi dans le transfini (voir Feferman 1962 et Franzén 2004).

Les principes de réflexion expriment - au moins partiellement - la solidité du système. L'expression la plus naturelle et la plus complète de la solidité d'un système implique le prédicat de vérité et est connue sous le nom de principe de réflexion globale (voir Kreisel et Lévy 1968). Le principe de réflexion globale pour un système formel S stipule que toutes les phrases prouvables en S sont vraies:

) forall x (Bew_S (x) rightarrow Tx))

(Bew_S (x)) exprime ici la prouvabilité des phrases dans le système S (nous omettons ici la discussion des problèmes de définition de (Bew_S (x))). Le prédicat de vérité doit satisfaire certains principes; sinon, le principe de la réflexion globale serait vide de sens. Ainsi, non seulement le principe de la réflexion globale doit être ajouté, mais aussi les axiomes de la vérité. Si une théorie naturelle de la vérité comme T (PA) ci-dessous est ajoutée, cependant, il n'est plus nécessaire de postuler explicitement le principe de réflexion globale, car des théories comme T (PA) prouvent déjà le principe de réflexion globale pour PA. On peut donc considérer les théories de la vérité comme des principes de réflexion car elles prouvent la justesse des déclarations et ajoutent les ressources pour exprimer ces déclarations.

Ainsi, au lieu d'itérer des principes de réflexion entièrement formulés dans le langage de l'arithmétique, on peut ajouter par itération de nouveaux prédicats de vérité et en conséquence de nouveaux axiomes pour les nouveaux prédicats de vérité. On pourrait ainsi espérer rendre explicites toutes les hypothèses implicites dans l'acceptation d'une théorie comme PA. La théorie qui en résulte est appelée la clôture réflexive de la théorie initiale. Feferman (1991) a proposé l'utilisation d'un seul prédicat de vérité et d'une seule théorie (KF), plutôt que d'une hiérarchie de prédicats et de théories, afin d'expliquer la fermeture réflexive de l'AP et d'autres théories. (KF est discuté plus en détail dans la section 4.4 ci-dessous.)

La relation entre les théories de la vérité et les principes de réflexion (itérée) est également devenue importante dans la discussion sur le déflationnisme théorique de la vérité (voir Tennant 2002 et la discussion de suivi).

1.3 Déflationnisme théorique de la vérité

De nombreux partisans des théories déflationnistes de la vérité ont choisi de traiter la vérité comme une notion primitive et de l'axiomatiser, en utilisant souvent une version des phrases (T) - comme axiomes. (T) - les phrases sont des équivalences de la forme (T / ulcorner / phi / urcorner / leftrightarrow / phi), où (T) est le prédicat de vérité, (phi) est une phrase et (ulcorner / phi / urcorner) est un nom pour la phrase (phi). (Des axiomes plus raffinés ont également été discutés par les déflationnistes.) À première vue du moins, l'approche axiomatique semble beaucoup moins `` déflationniste '' que les théories plus traditionnelles qui reposent sur une définition de la vérité en termes de correspondance ou autre. Si la vérité peut être explicitement définie, elle peut être éliminée, alors qu'une notion axiomatisée de la vérité peut s'accompagner d'engagements qui dépassent souvent celui de la théorie de base.

Si la vérité n'a aucune force explicative, comme le prétendent certains déflationnistes, les axiomes de la vérité ne devraient pas nous permettre de prouver de nouveaux théorèmes qui n'impliquent pas le prédicat de vérité. En conséquence, Horsten (1995), Shapiro (1998) et Ketland (1999) ont suggéré qu'une axiomatisation déflationniste de la vérité devrait être au moins conservatrice. Les nouveaux axiomes pour la vérité sont conservateurs s'ils n'impliquent aucune phrase supplémentaire (exempte d'occurrences du prédicat de vérité) qui ne sont pas déjà prouvables sans les axiomes de vérité. Ainsi, une théorie non conservatrice de la vérité ajoute un nouveau contenu non sémantique à une théorie et possède un véritable pouvoir explicatif, contrairement à de nombreuses vues déflationnistes. Cependant, certaines théories naturelles de la vérité ne sont pas conservatrices (voir la section 3.3 ci-dessous, Field 1999 et Shapiro 2002 pour une discussion plus approfondie).

Selon de nombreux déflationnistes, la vérité ne sert qu'à exprimer des conjonctions infinies. Il est clair que toutes les conjonctions infinies ne peuvent pas être exprimées parce qu'il existe un nombre incalculable de conjonctions infinies (non équivalentes) sur une langue dénombrable. Étant donné que le langage avec un prédicat de vérité ajouté n'a qu'un nombre infini de formules, toutes les conjonctions infinies ne peuvent pas être exprimées par une formule finie différente. Le travail formel sur les théories axiomatiques de la vérité a aidé à spécifier exactement quelles conjonctions infinies peuvent être exprimées avec un prédicat de vérité. Feferman (1991) fournit une analyse théorique de la preuve d'un système assez fort. (Encore une fois, cela sera expliqué dans la discussion sur KF dans la section 4.4 ci-dessous.)

2. La théorie de base

2.1 Le choix de la théorie de base

Dans la plupart des théories axiomatiques, la vérité est conçue comme un prédicat d'objets. Il y a une discussion philosophique approfondie sur la catégorie des objets auxquels s'applique la vérité: des propositions conçues comme des objets indépendants de tout langage, des types et des jetons de phrases et d'énoncés, de pensées et de nombreux autres objets ont été proposés. La structure des phrases considérées comme des types étant relativement claire, les types de phrases ont souvent été utilisés comme objets pouvant être vrais. Dans de nombreux cas, il n'est pas nécessaire de prendre des engagements métaphysiques très spécifiques, car seules certaines hypothèses modestes sur la structure de ces objets sont nécessaires, indépendamment du fait qu'ils soient finalement considérés comme des objets syntaxiques, des propositions ou encore autre chose. La théorie qui décrit les propriétés des objets auxquels la vérité peut être attribuée est appelée théorie de base. La formulation de la théorie de base n'implique pas le prédicat de vérité ni aucune hypothèse spécifique de la théorie de la vérité. La théorie de base pourrait décrire la structure des phrases, des propositions et autres, de sorte que des notions comme la négation d'un tel objet puissent ensuite être utilisées dans la formulation des axiomes de la théorie de la vérité.

Dans de nombreuses théories de la vérité axiomatique, la vérité est prise comme un prédicat s'appliquant aux nombres de phrases de Gödel. L'arithmétique de Peano s'est avérée être une théorie polyvalente des objets à laquelle la vérité est appliquée, principalement parce que l'ajout d'axiomes de la théorie de la vérité à l'arithmétique de Peano donne des systèmes intéressants et parce que l'arithmétique de Peano est équivalente à de nombreuses théories simples de la syntaxe et même des théories des propositions. Cependant, d'autres théories de base ont également été considérées, y compris les théories de syntaxe formelle et les théories des ensembles.

Bien sûr, nous pouvons également étudier les théories qui résultent de l'ajout des axiomes de la théorie de la vérité à des théories beaucoup plus fortes comme la théorie des ensembles. Habituellement, il n'y a aucune chance de prouver la cohérence de la théorie des ensembles plus d'autres axiomes de la théorie de la vérité parce que la cohérence de la théorie des ensembles elle-même ne peut être établie sans des hypothèses transcendant la théorie des ensembles. Dans de nombreux cas, même les preuves de cohérence relative ne sont pas réalisables. Cependant, si l'ajout de certains axiomes de la théorie de la vérité à l'AP donne une théorie cohérente, il semble au moins plausible que l'ajout d'axiomes analogues à la théorie des ensembles ne conduise pas à une incohérence. Par conséquent, l'espoir est que la recherche sur les théories de la vérité sur l'AP donnera une certaine indication de ce qui se passera lorsque nous étendrons des théories plus fortes avec des axiomes pour le prédicat de vérité. cependant,Fujimoto (2012) a montré que certaines théories de vérité axiomatiques sur la théorie des ensembles diffèrent de leurs homologues sur l'arithmétique de Peano à certains égards.

2.2 Conventions de notation

Par souci de précision, nous supposons que le langage de l'arithmétique a exactement (neg, / wedge) et (vee) comme connecteurs et (forall) et (existe) comme quantificateurs. Il n'a pour constantes individuelles que le symbole 0 pour zéro; son seul symbole de fonction est le symbole successeur unaire (S); l'addition et la multiplication sont exprimées par des symboles de prédicat. Par conséquent, les seuls termes fermés du langage de l'arithmétique sont les chiffres (0, S) (0), (S (S) (0)), (S (S (S) (0))),….

Le langage de l'arithmétique ne contient pas le symbole de prédicat unaire (T), donc soit (mathcal {L} _T) le langage de l'arithmétique augmenté du nouveau symbole de prédicat unaire (T) pour la vérité. Si (phi) est une phrase de (mathcal {L} _T, / ulcorner / phi / urcorner) est un nom pour (phi) dans la langue (mathcal {L} _T); formellement parlant, c'est le chiffre du nombre de Gödel de (phi). En général, les lettres grecques comme (phi) et (psi) sont des variables du métalangage, c'est-à-dire de la langue utilisée pour parler des théories de la vérité et de la langue dans laquelle cette entrée est écrite (c'est-à-dire l'anglais enrichi de quelques symboles). (phi) et (psi) s'étendent sur les formules du langage formel (mathcal {L} _T).

Dans ce qui suit, nous utilisons de petites lettres italiques majuscules comme ({ scriptsize A}, { scriptsize B}, / ldots) comme variables dans (mathcal {L} _T) s'étendant sur des phrases (ou leur Nombres de Gödel, pour être précis). Ainsi (forall { scriptsize A} (ldots { scriptsize A} ldots)) signifie (forall x (Sent_T (x) rightarrow / ldots x / ldots)), où (Sent_T (x)) exprime dans le langage de l'arithmétique que (x) est une phrase du langage de l'arithmétique étendue par le symbole du prédicat (T). Les opérations syntaxiques de formation d'une conjonction de deux phrases et des opérations similaires peuvent être exprimées dans le langage de l'arithmétique. Puisque le langage de l'arithmétique ne contient aucun symbole de fonction en dehors du symbole du successeur, ces opérations doivent être exprimées par des expressions de prédicat sutiables. Ainsi on peut dire dans le langage (mathcal {L} _T) qu'une négation d'une phrase de (mathcal {L} _T) est vraie si et seulement si la phrase elle-même n'est pas vraie. Nous écririons ceci comme

) forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A}).)

Les crochets indiquent que l'opération de formation de la négation de ({ scriptsize A}) est exprimée dans le langage de l'arithmétique. Puisque le langage de l'arithmétique ne contient pas de symbole de fonction représentant la fonction qui envoie des phrases à leurs négations, des paraphrases appropriées impliquant des prédicats doivent être données.

Ainsi, par exemple, l'expression

) forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} wedge { scriptsize B}] leftrightarrow (T { scriptsize A} wedge T { scriptsize B})))

est une seule phrase du langage (mathcal {L} _T) disant qu'une conjonction de phrases de (mathcal {L} _T) est vraie si et seulement si les deux phrases sont vraies. En revanche, [T / ulcorner / phi / wedge / psi / urcorner / leftrightarrow (T / ulcorner / phi / urcorner / wedge T / ulcorner / phi / urcorner))

n'est qu'un schéma. Autrement dit, il représente l'ensemble de toutes les phrases qui sont obtenues à partir de l'expression ci-dessus en substituant des phrases de (mathcal {L} _T) aux lettres grecques (phi) et (psi). La phrase unique (forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} wedge { scriptsize B}] leftrightarrow (T { scriptsize A} wedge T { scriptsize B}))) implique toutes les phrases qui sont des instances du schéma, mais les instances du schéma n'impliquent pas la seule phrase universellement quantifiée. En général, les versions quantifiées sont plus solides que les schémas correspondants.

3. Théories de la vérité typées

Dans les théories typées de la vérité, seule la vérité des phrases ne contenant pas le même prédicat de vérité est prouvable, évitant ainsi les paradoxes en observant la distinction de Tarski entre objet et métalangage.

3.1 Prédicats de vérité définissables

Certains prédicats de vérité peuvent être définis dans le langage de l'arithmétique. Les prédicats appropriés comme prédicats de vérité pour les sous-langues du langage de l'arithmétique peuvent être définis dans le langage de l'arithmétique, tant que la complexité quantification des formules dans le sous-langage est restreinte. En particulier, il existe une formule (Tr_0 (x)) qui exprime que (x) est une vraie phrase atomique du langage de l'arithmétique, c'est-à-dire une phrase de la forme (n = k), où (k) et (n) sont des chiffres identiques. Pour plus d'informations sur les prédicats de vérité partielle, voir, par exemple, Hájek et Pudlak (1993), Kaye (1991) et Takeuti (1987).

Les prédicats de vérité définissables sont vraiment redondants, car ils sont exprimables en PA; il n'est donc pas nécessaire de les introduire de manière axiomatique. Tous les prédicats de vérité dans ce qui suit ne sont pas définissables dans le langage de l'arithmétique, et donc pas redondants au moins dans le sens où ils ne sont pas définissables.

3.2 Les phrases (T) -

Les phrases typées (T) - sont toutes des équivalences de la forme (T / ulcorner / phi / urcorner / leftrightarrow / phi), où (phi) est une phrase ne contenant pas le prédicat de vérité. Tarski (1935) a qualifié toute théorie prouvant ces équivalences de «matériellement adéquate». Tarski (1935) a critiqué une axiomatisation de la vérité reposant uniquement sur les phrases (T) -, non pas parce qu'il visait une définition plutôt qu'une axiomatisation de la vérité, mais parce qu'une telle théorie semblait trop faible. Ainsi, bien que la théorie soit matériellement adéquate, Tarski pense que les phrases (T) - sont déductivement trop faibles. Il a observé, en particulier, que les phrases (T) - ne prouvent pas le principe de complétude, c'est-à-direla phrase (forall { scriptsize A} (T { scriptsize A} vee T) neg { scriptsize A})]) où le quantificateur (forall { scriptsize A}) est limité à phrases ne contenant pas T.

Les théories de la vérité basées sur les phrases (T) -, et leurs propriétés formelles, ont également été récemment un centre d'intérêt dans le contexte des théories dites déflationnistes de la vérité. Les (T) - phrases (T / ulcorner / phi / urcorner / leftrightarrow / phi) (où (phi) ne contient pas (T)) ne sont pas conservatrices sur la logique du premier ordre avec identité, c'est-à-dire qu'ils prouvent une phrase ne contenant pas (T) qui n'est pas logiquement valide. Pour les phrases (T) - prouvez que les phrases (0 = 0) et (neg 0 = 0) sont différentes et qu'il existe donc au moins deux objets. En d'autres termes, les phrases (T) - ne sont pas conservatrices par rapport à la théorie des bases vides. Si les phrases (T) - sont ajoutées à PA, la théorie résultante est conservatrice sur PA. Cela signifie que la théorie ne prouve pas (T) - des phrases libres qui ne sont pas déjà prouvables en PA. Ce résultat est valable même si, en plus des phrases (T) -, tous les axiomes d'induction contenant le prédicat de vérité sont ajoutés. Cela peut être démontré en faisant appel au théorème de compacité.

Dans la forme décrite ci-dessus, les phrases T expriment l'équivalence entre (T / ulcorner / phi / urcorner) et (phi) uniquement lorsque (phi) est une phrase. Afin de capturer l'équivalence des propriétés ((x) a la propriété P ssi 'P' est vrai de (x)), il faut généraliser les phrases T. Le résultat est généralement appelé les phrases T uniformes et est formalisé par les équivalences (forall x (T / ulcorner / phi (underline {x}) urcorner / leftrightarrow / phi (x))) pour chaque ouvrir la formule (phi (v)) avec au plus (v) libre dans (phi). Le fait de souligner la variable indique qu'elle est liée de l'extérieur. Plus précisément, (ulcorner / phi (underline {x}) urcorner) représente le résultat du remplacement de la variable (v) dans (ulcorner / phi (v) urcorner) par le chiffre de (x).

3.3 Vérité compositionnelle

Comme déjà observé par Tarski (1935), certaines généralisations souhaitables ne découlent pas des phrases T. Par exemple, avec les théories de base raisonnables, ils n'impliquent pas qu'une conjonction est vraie si les deux conjonctures sont vraies.

Afin d'obtenir des systèmes qui prouvent également des principes de théorie de la vérité universellement quantifiés, on peut transformer les clauses inductives de la définition de la vérité de Tarski en axiomes. Dans les axiomes suivants, (AtomSent_ {PA} (ulcorner { scriptsize A} urcorner)) exprime que ({ scriptsize A}) est une phrase atomique du langage de l'arithmétique, (Sent_ {PA } (ulcorner { scriptsize A} urcorner)) exprime que ({ scriptsize A}) est une phrase du langage de l'arithmétique.

  1. (forall { scriptsize A} (AtomSent_ {PA} ({ scriptsize A}) rightarrow (T { scriptsize A} leftrightarrow Tr_0 ({ scriptsize A}))))
  2. (forall { scriptsize A} (Sent_ {PA} ({ scriptsize A}) rightarrow (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})))
  3. (forall { scriptsize A} forall { scriptsize B} (Sent_ {PA} ({ scriptsize A}) wedge Sent_ {PA} ({ scriptsize B}) rightarrow (T [{ scriptsize A } wedge { scriptsize B}] leftrightarrow (T { scriptsize A} wedge T { scriptsize B}))))
  4. (forall { scriptsize A} forall { scriptsize B} (Sent_ {PA} ({ scriptsize A}) wedge Sent_ {PA} ({ scriptsize B}) rightarrow (T [{ scriptsize A } vee { scriptsize B}] leftrightarrow (T { scriptsize A} vee T { scriptsize B}))))
  5. (forall { scriptsize A} (v) (Sent_ {PA} (forall v { scriptsize A}) rightarrow (T) forall v { scriptsize A} (v)] leftrightarrow / forall xT [{ scriptsize A} (underline {x}))]))
  6. (forall { scriptsize A} (v) (Sent_ {PA} (forall v { scriptsize A}) rightarrow (T) exists v { scriptsize A} (v)] leftrightarrow / exists xT [{ scriptsize A} (underline {x}))]))

L'axiome 1 dit qu'une phrase atomique du langage de l'arithmétique Peano est vraie si et seulement si elle est vraie selon le prédicat de vérité arithmétique pour ce langage ((Tr_0) a été défini dans la section 3.1). Les axiomes 2–6 affirment que la vérité commute avec tous les connecteurs et quantificateurs. L'axiome 5 dit qu'une phrase universellement quantifiée du langage de l'arithmétique est vraie si et seulement si toutes ses instances numériques sont vraies. (Sent_ {PA} (forall v { scriptsize A})) dit que ({ scriptsize A} (v)) est une formule avec au plus (v) free (car (forall v { scriptsize A} (v)) est une phrase).

Si ces axiomes doivent être formulés pour un langage comme la théorie des ensembles qui manque de noms pour tous les objets, alors les axiomes 5 et 6 nécessitent l'utilisation d'une relation de satisfaction plutôt que d'un prédicat de vérité unaire.

Les axiomes du style 1–6 ci-dessus ont joué un rôle central dans la théorie du sens de Donald Davidson et dans plusieurs approches déflationnistes de la vérité.

La théorie donnée par tous les axiomes de PA et Axiomes 1–6 mais avec induction uniquement pour les formules (T) - libres est conservatrice sur PA, c'est-à-dire qu'elle ne prouve pas de nouveaux théorèmes (T) - libres qui pas déjà prouvable en PA. Cependant, tous les modèles de PA ne peuvent pas être étendus aux modèles de PA + axiomes 1–6. Cela découle d'un résultat de Lachlan (1981). Kotlarski, Krajewski et Lachlan (1981) ont prouvé la conservativité très similaire aux axiomes PA + 1–6 par des moyens théoriques du modèle. Bien que plusieurs auteurs aient affirmé que ce résultat est également prouvable de manière définitive, aucune preuve de ce type n'était disponible jusqu'à Enayat & Visser (2015) et Leigh (2015). De plus, la théorie donnée par les axiomes PA + 1–6 est relativement interprétable en PA. Cependant, ce résultat est sensible au choix de la théorie de base: il échoue pour les théories finement axiomatisées (Heck 2015, Nicolai 2016). Ces résultats de la théorie de la preuve ont été largement utilisés dans la discussion du déflationnisme de la théorie de la vérité (voir Cieśliński 2017).

Bien sûr, les axiomes PA + 1–6 sont restrictifs dans la mesure où ils ne contiennent pas les axiomes d'induction dans le langage avec le prédicat de vérité. Il existe différentes étiquettes pour le système obtenu en ajoutant tous les axiomes d'induction impliquant le prédicat de vérité au système PA + axiomes 1–6: T (PA), CT, PA (S) ou PA + 'il y a une pleine satisfaction inductive classe'. Cette théorie n'est plus conservatrice par rapport à sa théorie de base PA. Par exemple, on peut formaliser le théorème de solidité ou le principe de réflexion globale pour PA, c'est-à-dire l'affirmation selon laquelle toutes les phrases prouvables dans PA sont vraies. Le principe de réflexion globale pour l'AP implique à son tour la cohérence de l'AP, ce qui n'est pas prouvable dans l'AP pure par le deuxième théorème d'incomplétude de Gödel. Ainsi T (PA) n'est pas conservateur par rapport à PA. T (PA) est beaucoup plus fort que la simple déclaration de cohérence pour PA:T (PA) est équivalent au système de second ordre ACA de la compréhension arithmétique (voir Takeuti 1987 et Feferman 1991). Plus précisément, T (PA) et ACA sont inter-traduisibles d'une manière qui préserve toutes les phrases arithmétiques. ACA est donné par les axiomes de PA avec induction complète dans la langue du second ordre et le principe de compréhension suivant:

) existe X / forall y (y / in X / leftrightarrow / phi (x)))

où (phi (x)) est n'importe quelle formule (dans laquelle (x) peut ou non être libre) qui ne contient aucun quantificateur du second ordre, mais peut-être des variables libres du second ordre. En T (PA), la quantification sur des ensembles peut être définie comme une quantification sur des formules avec une variable libre et l'appartenance comme la vérité de la formule appliquée à un nombre.

Comme le principe de réflexion globale implique une cohérence formelle, le résultat de conservativité pour les axiomes PA + 1–6 implique que le principe de réflexion globale pour l'arithmétique Peano ne peut pas être dérivé dans la théorie de la composition typée sans étendre les axiomes d'induction. En fait, cette théorie ne prouve ni l'affirmation que toutes les validités logiques sont vraies (réflexion globale pour la logique pure du premier ordre) ni que tous les axiomes de l'arithmétique Peano sont vrais. Étonnamment peut-être, de ces deux déclarations non démontrables, c'est la première qui est la plus forte. Ce dernier peut être ajouté comme un axiome et la théorie reste conservatrice sur l'AP (Enayat et Visser 2015, Leigh 2015). En revanche, sur les axiomes PA + 1–6, le principe de réflexion globale pour la logique du premier ordre équivaut à la réflexion globale pour l'arithmétique de Peano (Cieśliński 2010),et ces deux théories ont les mêmes conséquences arithmétiques que l'ajout de l'axiome d'induction pour les formules ((Delta_0)) bornées contenant le prédicat de vérité (Wcisło et Łełyk 2017).

Le passage de PA à T (PA) peut être imaginé comme un acte de réflexion sur la vérité des phrases (mathcal {L}) - dans PA. De même, le passage des phrases typées (T) - aux axiomes compositionnels est également lié à un principe de réflexion, en particulier le principe de réflexion uniforme sur les phrases (T) - uniformes typées. Il s'agit de la collection de phrases (forall x \, Bew_S (ulcorner / phi (underline {x}) urcorner) rightarrow / phi) (x) où (phi) s'étend sur les formules dans (mathcal {L} _T) avec une variable libre et S est la théorie des phrases T typées uniformes. La réflexion uniforme saisit exactement la différence entre les deux théories: le principe de réflexion est à la fois dérivable en T (PA) et suffit à dériver les six axiomes compositionnels (Halbach 2001). De plus, l'équivalence s'étend aux itérations de réflexion uniforme,en ce que pour toute itération ordinale (alpha, 1 + / alpha) de réflexion uniforme sur les phrases typées (T) - coïncide avec T (PA) étendu par induction transfinie jusqu'à l'ordinal (varepsilon _ { alpha}), à savoir le (alpha) - ème ordinal avec la propriété que (omega ^ { alpha} = / alpha) (Leigh 2016).

Des fragments beaucoup plus forts de l'arithmétique du second ordre peuvent être interprétés par des systèmes de vérité sans type, c'est-à-dire par des théories de la vérité qui prouvent non seulement la vérité des phrases arithmétiques mais aussi la vérité des phrases du langage (mathcal {L} _T) avec le prédicat de vérité; voir la section 4 ci-dessous.

3.4 Théories hiérarchiques

Les théories de vérité mentionnées ci-dessus peuvent être répétées en introduisant des prédicats de vérité indexés. On ajoute au langage des prédicats de vérité PA indexés par des ordinaux (ou notations ordinales) ou on ajoute un prédicat de vérité binaire qui s'applique aux notations et aux phrases ordinales. À cet égard, l'approche hiérarchique ne correspond pas au cadre décrit dans la section 2, car le langage ne comporte pas un seul prédicat de vérité unaire s'appliquant aux phrases mais plutôt de nombreux prédicats de vérité unaire ou un seul prédicat de vérité binaire (ou même un seul prédicat de vérité unaire s'appliquant aux paires de notations ordinales et de phrases).

Dans un tel langage, une axiomatisation de la hiérarchie des prédicats de vérité de Tarski peut être formulée. Du côté de la théorie de la preuve, itérer les théories de la vérité dans le style de T (PA) correspond à l'itération de la compréhension élémentaire, c'est-à-dire à l'itération de l'ACA. Le système des théories de la vérité itérées correspond au système de l'analyse ramifiée (voir Feferman 1991).

Visser (1989) a étudié les hiérarchies non bien fondées des langages et leurs axiomatisations. Si l'on ajoute les (T) - phrases (T_n / ulcorner / phi / urcorner / leftrightarrow / phi) au langage de l'arithmétique où (phi) ne contient que des prédicats de vérité (T_k) avec (k / gt n) à PA, on obtient une théorie qui n'a pas de modèle ((omega) -) standard.

4. Vérité sans type

Les prédicats de vérité dans les langages naturels ne sont accompagnés d'aucune restriction de type ouvert. Par conséquent, les théories typées de la vérité (tant axiomatiques que sémantiques) ont été considérées comme inadéquates pour analyser le prédicat de vérité du langage naturel, bien que des théories hiérarchiques récentes aient été préconisées par Glanzberg (à paraître) et d'autres. C'est un motif pour enquêter sur les théories de la vérité sans type, c'est-à-dire les systèmes de vérité qui permettent de prouver la vérité de phrases impliquant le prédicat de vérité. Certaines théories de la vérité sans type ont un pouvoir expressif beaucoup plus élevé que les théories typées qui ont été étudiées dans la section précédente (au moins tant que les prédicats de vérité indexés sont évités). Par conséquent, les théories de la vérité sans type sont des outils beaucoup plus puissants dans la réduction d'autres théories (par exemple, celles du second ordre).

4.1 Sans type (T) - phrases

L'ensemble de toutes les (T) - phrases (T / ulcorner / phi / urcorner / leftrightarrow / phi), où (phi) est une phrase du langage (mathcal {L} _T), c'est-à-dire où (phi) peut contenir (T), est incompatible avec PA (ou toute théorie qui prouve le lemme diagonal) à cause du paradoxe du menteur. Par conséquent, on pourrait essayer de supprimer de l'ensemble de toutes les phrases (T) - uniquement celles qui conduisent à une incohérence. En d'autres termes, on peut considérer des ensembles cohérents maximaux de phrases (T) -. McGee (1992) a montré qu'il existe un nombre incalculable d'ensembles maximaux de phrases (T) - cohérentes avec PA. La stratégie ne conduit donc pas à une seule théorie. Pire encore, étant donné une phrase arithmétique (c'est-à-dire une phrase ne contenant pas (T)) qui ne peut être ni prouvée ni réfutée en PA, on peut trouver une phrase (T) - cohérente qui décide de cette phrase (McGee 1992). Cela implique que de nombreux ensembles cohérents de phrases (T) - prouvent de fausses déclarations arithmétiques. Ainsi, la stratégie consistant à ne supprimer que les phrases (T) - qui produisent une incohérence est vouée à l'échec.

Un ensemble de (T) - phrases qui n'implique aucune fausse déclaration arithmétique peut être obtenu en n'autorisant que ces (phi) dans (T) - phrases (T / ulcorner / phi / urcorner / leftrightarrow / phi) qui contiennent (T) uniquement positivement, c'est-à-dire dans la portée d'un nombre pair de symboles de négation. Comme la théorie typée de la section 3.2, cette théorie ne prouve pas certaines généralisations mais prouve les mêmes phrases sans T que la théorie de Kripke-Feferman compositionnelle forte sans type ci-dessous (Halbach 2009). Schindler (2015) a obtenu une théorie de la vérité déductivement très forte basée sur des principes de disquotation stratifiés.

4.2 Compositionnalité

Outre la caractéristique disquotationnelle de la vérité, on aimerait aussi capturer les caractéristiques compositionnelles de la vérité et généraliser les axiomes de la vérité compositionnelle typée au cas sans type. Pour cela, il faudra ajouter des axiomes ou des règles concernant la vérité des phrases atomiques avec le prédicat de vérité et la restriction aux phrases libres (T) dans les axiomes de composition devra être levée. Afin de traiter la vérité comme les autres prédicats, on ajoutera l'axiome (forall { scriptsize A} (T [T { scriptsize A}] leftrightarrow T { scriptsize A})) (où (forall { scriptsize A}) s'étend sur toutes les phrases). Si la restriction de type de l'axiome compositionnel typé pour la négation est supprimée, l'axiome (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})) est obtenu.

Cependant, les axiomes (forall { scriptsize A} (T [T { scriptsize A}] leftrightarrow T { scriptsize A})) et (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})) sont incohérents sur des théories de syntaxe faibles, donc l'une d'elles doit être abandonnée. Si (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})) est retenu, il faudra trouver des axiomes plus faibles ou des règles d'itération de vérité, mais la vérité reste un concept classique en ce sens que (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})) implique la loi du milieu exclu (pour toute phrase, soit la phrase elle-même ou sa négation est vraie) et la loi de non-contradiction (pour aucune phrase la phrase elle-même et sa négation sont vraies). Si, en revanche,(forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})) est rejeté et (forall { scriptsize A} (T [T { scriptsize A}] leftrightarrow T { scriptsize A})) retenu, alors il deviendra prouvable que soit certaines phrases sont vraies avec leurs négations, soit que pour certaines phrases ni elles ni leurs négations ne sont vraies, et donc des systèmes de la vérité non classique est obtenue, bien que les systèmes eux-mêmes soient encore formulés dans la logique classique. Dans les deux sections suivantes, nous présentons le système le plus important de chaque type.alors il deviendra prouvable que soit certaines phrases sont vraies avec leurs négations, soit que pour certaines phrases ni elles ni leurs négations ne sont vraies, et ainsi des systèmes de vérité non classique sont obtenus, bien que les systèmes eux-mêmes soient encore formulés dans la logique classique. Dans les deux sections suivantes, nous présentons le système le plus important de chaque type.alors il deviendra prouvable que soit certaines phrases sont vraies avec leurs négations, soit que pour certaines phrases ni elles ni leurs négations ne sont vraies, et ainsi des systèmes de vérité non classique sont obtenus, bien que les systèmes eux-mêmes soient encore formulés dans la logique classique. Dans les deux sections suivantes, nous présentons le système le plus important de chaque type.

4.3 La théorie de Friedman – Sheard et la sémantique de la révision

Le système FS, nommé d'après Friedman et Sheard (1987), conserve l'axiome de négation (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})). Les autres axiomes de composition sont obtenus en levant la restriction de type à leurs homologues non typés:

  1. (forall { scriptsize A} (AtomSent_ {PA} ({ scriptsize A}) rightarrow (T { scriptsize A} leftrightarrow Tr_0 ({ scriptsize A}))))
  2. (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A}))
  3. (forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} wedge { scriptsize B}] leftrightarrow (T { scriptsize A} wedge T { scriptsize B})))
  4. (forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} vee { scriptsize B}] leftrightarrow (T { scriptsize A} vee T { scriptsize B})))
  5. (forall { scriptsize A} (v) (Envoyé (forall v { scriptsize A}) rightarrow (T) forall v { scriptsize A} (v)] leftrightarrow / forall xT [{ scriptsize A} (underline {x}))])
  6. (forall { scriptsize A} (v) (Envoyé (forall v { scriptsize A}) rightarrow (T) exists v { scriptsize A} (v)] leftrightarrow / exists xT [{ scriptsize A} (underline {x}))]))

Ces axiomes sont ajoutés à PA formulé dans le langage (mathcal {L} _T). Comme l'axiome d'itération de vérité (forall { scriptsize A} (T [T { scriptsize A}] leftrightarrow T { scriptsize A})) est incohérent, seules les deux règles suivantes sont ajoutées:

Si (phi) est un théorème, on peut déduire (T / ulcorner / phi / urcorner), et inversement, si (T / ulcorner / phi / urcorner) est un théorème, on peut en déduire (phi).

Il découle des résultats de McGee (1985) que FS est (omega) - incohérent, c'est-à-dire que FS prouve (existe x / neg / phi (x)), mais prouve également (phi) (0), (phi) (1), (phi) (2),… pour une formule (phi (x)) de (mathcal {L} _T). Les théorèmes arithmétiques de FS, cependant, sont tous corrects.

En FS, on peut définir tous les niveaux finis de la hiérarchie tarskienne classique, mais FS n'est pas assez fort pour permettre de récupérer l'un de ses niveaux transfinis. En effet, Halbach (1994) a déterminé que sa force théorique de preuve était précisément celle de la théorie de la vérité ramifiée pour tous les niveaux finis (c.-à-d. tous les niveaux finis. Si l'une ou l'autre des directions de la règle est abandonnée mais que l'autre est conservée, FS conserve sa force théorique de la preuve (Sheard 2001).

C'est une vertu de FS qu'il est tout à fait classique: il est formulé en logique classique; si une phrase est prouvable en FS, alors la phrase elle-même est prouvable en FS; et inversement, si une phrase est prouvable, elle l'est également. Son inconvénient est son (omega) - incohérence. FS peut être vu comme une axiomatisation de la sémantique des règles de révision pour tous les niveaux finis (voir l'entrée sur la théorie de la révision de la vérité).

4.4 La théorie de Kripke-Feferman

La théorie de Kripke-Feferman conserve l'axiome d'itération de vérité (forall { scriptsize A} (T [T { scriptsize A}] leftrightarrow T { scriptsize A})), mais la notion de vérité axiomatisée n'est plus classique car l'axiome de négation (forall { scriptsize A} (T) neg { scriptsize A}] leftrightarrow / neg T { scriptsize A})) est abandonné.

La construction sémantique capturée par cette théorie est une généralisation de la définition inductive typée tarskienne de la vérité capturée par T (PA). Dans la définition généralisée on part de la vraie phrase atomique du langage arithmétique et ensuite on déclare vraies les phrases complexes selon que ses composantes sont vraies ou non. Par exemple, comme dans le cas typé, si (phi) et (psi) sont vrais, leur conjonction (phi / wedge / psi) sera également vrai. Dans le cas des phrases quantifiées, leur valeur de vérité est déterminée par les valeurs de vérité de leurs instances (on pourrait rendre les clauses de quantification purement compositionnelles en utilisant un prédicat de satisfaction); par exemple, une phrase universellement quantifiée sera déclarée vraie si et seulement si toutes ses instances sont vraies. On peut maintenant étendre cette définition inductive de la vérité au langage (mathcal {L} _T) en déclarant une phrase de la forme (T / ulcorner / phi / urcorner) true si (phi) est déjà vrai. De plus on déclarera (neg T / ulcorner / phi / urcorner) true si (neg / phi) est vrai. En précisant cette idée, on obtient une variante de la théorie de la vérité de Kripke (1975) avec le système de valorisation dit de Strong Kleene (voir l'entrée sur la logique à plusieurs valeurs). S'il est axiomatisé, il conduit au système suivant, connu sous le nom de KF («Kripke – Feferman»), dont plusieurs variantes apparaissent dans la littérature:on obtient une variante de la théorie de la vérité de Kripke (1975) avec le soi-disant schéma d'évaluation Strong Kleene (voir l'entrée sur la logique à plusieurs valeurs). S'il est axiomatisé, il conduit au système suivant, connu sous le nom de KF («Kripke – Feferman»), dont plusieurs variantes apparaissent dans la littérature:on obtient une variante de la théorie de la vérité de Kripke (1975) avec le soi-disant schéma d'évaluation Strong Kleene (voir l'entrée sur la logique à plusieurs valeurs). S'il est axiomatisé, il conduit au système suivant, connu sous le nom de KF («Kripke – Feferman»), dont plusieurs variantes apparaissent dans la littérature:

  1. (forall { scriptsize A} (AtomSent_ {PA} ({ scriptsize A}) rightarrow (T { scriptsize A} leftrightarrow Tr_0 ({ scriptsize A}))))
  2. (forall { scriptsize A} (AtomSent_ {PA} ({ scriptsize A}) rightarrow (T) neg { scriptsize A}] leftrightarrow / neg Tr_0 ({ scriptsize A}))))
  3. (forall { scriptsize A} (T [T { scriptsize A}] leftrightarrow T { scriptsize A}))
  4. (forall { scriptsize A} (T) neg T { scriptsize A}] leftrightarrow T) neg { scriptsize A})])
  5. (forall { scriptsize A} (T) neg / neg { scriptsize A}] leftrightarrow T { scriptsize A}))
  6. (forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} wedge { scriptsize B}] leftrightarrow (T { scriptsize A} wedge T { scriptsize B})))
  7. (forall { scriptsize A} forall { scriptsize B} (T) neg ({ scriptsize A} wedge { scriptsize B})] leftrightarrow (T) neg { scriptsize A}] vee T) neg { scriptsize B})]))
  8. (forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} vee { scriptsize B}] leftrightarrow (T { scriptsize A} vee T { scriptsize B})))
  9. (forall { scriptsize A} forall { scriptsize B} (T) neg ({ scriptsize A} vee { scriptsize B})] leftrightarrow (T) neg { scriptsize A}] coin T) neg { scriptsize B})]))
  10. (forall { scriptsize A} (v) (Envoyé (forall v { scriptsize A}) rightarrow (T) forall v { scriptsize A} (v)] leftrightarrow / forall xT [{ scriptsize A} (underline {x}))])
  11. (forall { scriptsize A} (v) (Sent (forall v { scriptsize A}) rightarrow (T) neg / forall v { scriptsize A} (v)] leftrightarrow / exists xT) neg { scriptsize A} (underline {x}))])
  12. (forall { scriptsize A} (v) (Envoyé (forall v { scriptsize A}) rightarrow (T) exists v { scriptsize A} (v)] leftrightarrow / exists xT [{ scriptsize A} (underline {x}))]))
  13. (forall { scriptsize A} (v) (Envoyé (forall v { scriptsize A}) rightarrow (T) neg / exists v { scriptsize A} (v)] leftrightarrow / forall xT) neg { scriptsize A} (underline {x}))]))

Hormis les axiomes de la théorie de la vérité, KF comprend tous les axiomes de PA et tous les axiomes d'induction impliquant le prédicat de vérité. Le système est crédité à Feferman sur la base de deux conférences pour l'Association of Symbolic Logic, l'une en 1979 et la seconde en 1983, ainsi que dans des manuscrits ultérieurs. Feferman a publié sa version du système sous le label Ref (PA) (`` faible réflexion de la fermeture de PA '') seulement en 1991, après que plusieurs autres versions de KF aient déjà paru en version imprimée (par exemple, Reinhardt 1986, Cantini 1989, qui font référence à cet ouvrage inédit de Feferman).

KF lui-même est formulé en logique classique, mais il décrit une notion non classique de vérité. Par exemple, on peut prouver (T / ulcorner L / urcorner / leftrightarrow T / ulcorner / neg L / urcorner) si (L) est la phrase du menteur. Ainsi KF prouve que soit la phrase du menteur et sa négation sont vraies soit que ni l'une ni l'autre n'est vraie. Ainsi, soit la notion de vérité est paraconsistante (une phrase est vraie avec sa négation) ou paracomplète (aucune n'est vraie). Certains auteurs ont augmenté KF avec un axiome excluant les surabondances de valeur de vérité, ce qui rend KF sonore pour la construction du modèle de Kripke, car Kripke avait exclu les surabondances de valeur de vérité.

Feferman (1991) a montré que KF est théoriquement équivalent à la théorie de l'analyse ramifiée à tous les niveaux inférieurs à (varepsilon_0), la limite de la séquence (omega, / omega ^ { omega}, / omega ^ { omega ^ { omega}}, / ldots), ou une théorie de la vérité ramifiée par les mêmes ordinaux. Ce résultat montre que dans KF exactement (varepsilon_0) plusieurs niveaux de la hiérarchie tarskienne classique sous sa forme axiomatisée peuvent être récupérés. Ainsi KF est beaucoup plus fort que FS, sans parler de T (PA). Feferman (1991) a également conçu un renforcement de KF qui est aussi fort que l'analyse prédicative complète, c'est-à-dire l'analyse ramifiée ou vérité jusqu'à l'ordinal (Gamma_0).

Tout comme pour le prédicat de vérité typé, la théorie KF (plus précisément une variante commune de celle-ci) peut être obtenue par un acte de réflexion sur un système de phrases (T) - non typées. Le système de (T) - phrases en question est l'extension des phrases uniformes positives non typées (T) - par un prédicat primitif de fausseté, c'est-à-dire que la théorie comporte deux prédicats unaires (T) et (F) et axiomes

) begin {align *} & / forall x (T / ulcorner / phi (underline {x}) urcorner / leftrightarrow / phi (x)) & / forall x (F / ulcorner / phi (underline {x}) urcorner / leftrightarrow / phi '(x)) end {align *})

pour chaque formule (phi (v)) positive à la fois dans (T) et (F), où (phi ') représente le dual De Morgan de (phi) (échange (T) pour (F) et vice versa). À partir d'une application d'une réflexion uniforme sur cette théorie disquotationnelle, les axiomes de vérité pour la version à deux prédicats correspondante de KF sont dérivables (Horsten et Leigh, 2016). L'inverse est également vrai, tout comme la généralisation aux itérations finies et transfinies de réflexion (Leigh, 2017).

4.5 Capture du point fixe minimal

Comme remarqué ci-dessus, si KF prouve (T / ulcorner / phi / urcorner) pour une phrase (phi) alors (phi) est valable dans tous les modèles à virgule fixe de Kripke. En particulier, il existe des (2 ^ { aleph_0}) points fixes qui forment un modèle de la théorie interne de KF. Ainsi, du point de vue de KF, le point le moins fixe (à partir duquel la théorie de Kripke est définie) n'est pas distingué. Burgess (à paraître) fournit une extension de KF, nommée (mu) KF, qui tente de capturer le point fixe minimal de Kripkean. KF est développé par des axiomes supplémentaires qui expriment que la théorie interne de KF est la plus petite classe fermée sous les axiomes définissant la vérité kripkéenne. Cela peut être formulé comme un schéma d'axiome unique qui déclare, pour chaque formule ouverte (phi), Si (phi) satisfait les mêmes axiomes de KF que le prédicat (T) alors (phi) vaut pour chaque phrase vraie.

Du point de vue de la théorie de la preuve (mu) KF est significativement plus fort que KF. Le schéma d'axiome unique exprimant la minimalité du prédicat de vérité permet d'intégrer dans (mu) KF l'ID système (_ 1) d'une définition inductive arithmétique, une théorie imprédicative. Bien qu'intuitivement plausible, (mu) KF souffre de la même incomplétude expressive que KF: puisque le point fixe de Kripkean minimal forme un ensemble (Pi ^ {1} _1) complet et la théorie interne de (mu) KF reste récursivement énumérable, il existe des modèles standards de la théorie dans lesquels l'interprétation du prédicat de vérité n'est pas réellement le point fixe minimal. Il manque actuellement une analyse approfondie des modèles de (mu) KF.

4.6 Axiomatisations de la théorie de Kripke avec des supervaluations

KF se veut une axiomatisation de la théorie sémantique de Kripke (1975). Cette théorie est basée sur une logique partielle avec le schéma d'évaluation Strong Kleene. Dans la logique Strong Kleene, toutes les phrases (phi / vee / neg / phi) ne sont pas un théorème; en particulier, cette disjonction n'est pas vraie si (phi) n'a pas de valeur de vérité. Par conséquent (T / ulcorner L / vee / neg L / urcorner) (où (L) est la phrase du menteur) n'est pas un théorème de KF et sa négation est même prouvable. Cantini (1990) a proposé un système VF qui s'inspire du schéma des surévaluations. Dans VF, toutes les tautologies classiques sont prouvées vraies et (T / ulcorner L / vee / neg L / urcorner), par exemple, est un théorème de VF. VF peut être formulé en (mathcal {L} _T) et utilise la logique classique. Ce n'est plus une théorie compositionnelle de la vérité, car ce qui suit n'est pas un théorème de VF:

) forall { scriptsize A} forall { scriptsize B} (T [{ scriptsize A} vee { scriptsize B}] leftrightarrow (T { scriptsize A} vee T { scriptsize B})).)

Non seulement ce principe est incompatible avec les autres axiomes de VF, mais il ne correspond pas au modèle de supervaluationist car il implique (T / ulcorner L / urcorner / vee T / ulcorner / neg L / urcorner), ce qui bien sûr n'est pas correct car selon la sémantique voulue, ni la phrase du menteur ni sa négation ne sont vraies: les deux manquent de valeur de vérité.

Prolongeant un résultat dû à Friedman et Sheard (1987), Cantini a montré que VF est beaucoup plus fort que KF: VF est théoriquement équivalent à la théorie ID (_ 1) des définitions inductives non itérées, qui n'est pas prédicative.

5. Approches non classiques de l'auto-référence

Les théories de la vérité discutées jusqu'ici sont toutes axiomatisées dans la logique classique. Certains auteurs se sont également penchés sur les théories axiomatiques de la vérité basées sur une logique non classique (voir, par exemple, Field 2008, Halbach et Horsten 2006, Leigh et Rathjen 2012). Il y a un certain nombre de raisons pour lesquelles une logique plus faible que la logique classique peut être préférée. Le plus évident est qu'en affaiblissant la logique, certains ensembles d'axiomes de vérité qui étaient auparavant incompatibles deviennent cohérents. Une autre raison courante est que la théorie axiomatique en question a l'intention de capturer une sémantique non classique particulière de la vérité, pour laquelle une théorie de fond classique peut s'avérer malsaine.

Il existe également un grand nombre d'approches qui utilisent des logiques paraconsistantes ou sous-structurelles. Dans la plupart des cas, ces approches n'emploient pas une théorie de base axiomatique telle que l'arithmétique de Peano et s'écartent donc du cadre considéré ici, bien qu'il n'y ait aucun obstacle technique à appliquer des logiques paraconsistantes ou sous-structurelles aux théories de la vérité sur ces théories de base. Ici, nous ne couvrons que les comptes proches du paramètre considéré ci-dessus. Pour plus d'informations sur l'application des logiques sous-structurelles et paraconsistantes aux paradoxes de la théorie de la vérité, voir la section correspondante dans l'entrée sur le paradoxe du menteur.

5.1 Le prédicat de vérité dans la logique intuitionniste

L'incohérence des phrases (T) - ne repose pas sur un raisonnement classique. Il est également incohérent sur des logiques beaucoup plus faibles telles que la logique minimale et la logique partielle. Cependant, la logique classique joue un rôle dans la restriction du libre usage des principes de vérité. Par exemple, sur une théorie de base classique, l'axiome compositionnel pour l'implication ((rightarrow)) est équivalent au principe d'exhaustivité, (forall { scriptsize A} (T [{ scriptsize A}] vee T) neg { scriptsize A})]). Si la logique sous le prédicat de vérité est classique, la complétude équivaut à l'axiome compositionnel pour la disjonction. Sans la loi du milieu exclu, la FS peut être formulée comme une théorie entièrement compositionnelle sans prouver le principe vérité-complétude (Leigh & Rathjen 2012). En outre,la logique classique a un effet sur les tentatives de combiner des axiomes compositionnels et auto-applicables de la vérité. Si, par exemple, on supprime l'axiome de vérité-cohérence de FS (la direction de gauche à droite de l'axiome 2 dans la section 4.3) ainsi que la loi du milieu exclu pour le prédicat de vérité, il est possible d'ajouter de manière cohérente le axiome d'itération de vérité (forall { scriptsize A} (T [{ scriptsize A}] rightarrow T [T { scriptsize A}])). La théorie qui en résulte présente toujours une forte ressemblance avec FS en ce que la version constructive de la sémantique de la règle de révision pour tous les niveaux finis fournit un modèle naturel de la théorie, et les deux théories partagent le même (Pi ^ {0} _2) conséquences (Leigh & Rathjen 2012; Leigh, 2013). Ce résultat doit être comparé à KF qui, s'il est formulé sans la loi du milieu exclu,reste cohérent au maximum par rapport à son choix d'axiomes de vérité mais est une extension conservatrice de l'arithmétique de Heyting.

5.2 Axiomatiser la théorie de Kripke

La théorie de Kripke (1975) sous ses différentes formes repose sur une logique partielle. Afin d'obtenir des modèles pour une théorie en logique classique, l'extension du prédicat de vérité dans le modèle partiel est à nouveau utilisée comme extension de la vérité dans le modèle classique. Dans le modèle classique, les fausses phrases et celles sans valeur de vérité dans le modèle partiel sont déclarées non vraies. KF est solide par rapport à ces modèles classiques et incorpore ainsi deux logiques distinctes. La première est la logique «interne» des déclarations sous le prédicat de vérité et est formulée avec le schéma d'évaluation Strong Kleene. La seconde est la logique «externe» qui est une logique classique à part entière. Un effet de la formulation de KF en logique classique est que la théorie ne peut pas être systématiquement fermée sous la règle d'introduction de la vérité

Si (phi) est un théorème de KF, il en est de même pour (T / ulcorner / phi / urcorner).

Un deuxième effet de la logique classique est la déclaration du milieu exclu pour la phrase du menteur. Ni la phrase du menteur ni sa négation n'obtiennent une valeur de vérité dans la théorie de Kripke, donc la disjonction des deux n'est pas valide. Le résultat est que KF, s'il est considéré comme une axiomatisation de la théorie de Kripke, n'est pas solide par rapport à sa sémantique prévue. Pour cette raison, Halbach et Horsten (2006) et Horsten (2011) explorent une axiomatisation de la théorie de Kripke avec une logique partielle comme logique interne et externe. Leur suggestion, une théorie appelée PKF («KF partiel»), peut être axiomatisée comme un calcul séquentiel bilatéral de type Gentzen basé sur la logique Strong Kleene (voir l'entrée sur la logique à plusieurs valeurs). PKF est formé en ajoutant à ce calcul les axiomes d'arithmétique Peano-Dedekind, y compris l'induction complète et les règles de composition et d'itération de vérité pour le prédicat de vérité tel que proscrit par la théorie de Kripke. Le résultat est une théorie de la vérité qui est solide par rapport à la théorie de Kripke.

Halbach et Horsten montrent que cette axiomatisation de la théorie de Kripke est significativement plus faible que sa cousine classique KF. Le résultat démontre que restreindre la logique uniquement pour les phrases avec le prédicat de vérité peut également entraver la dérivation de théorèmes sans vérité.

5.3 Ajout d'un conditionnel

Field (2008) et d'autres ont critiqué les théories fondées sur une logique partielle de l'absence d'un conditionnel et biconditionnel «approprié». Divers auteurs ont proposé des conditionnelles et des bi-conditionnelles qui ne sont pas définissables en termes de (neg, / vee) et (wedge). Field (2008) vise une théorie axiomatique de la vérité non différente de PKF mais avec un nouveau conditionnel. Feferman (1984) a également introduit un bi-conditionnel à une théorie en logique non classique. Contrairement à Field et à sa propre théorie de 1984, la théorie DT de Feferman (2008) est formulée en logique classique, mais sa logique interne est à nouveau une logique partielle avec un conditionnel fort.

Bibliographie

  • Aczel, Peter, 1980, «Les structures de Frege et la notion de proposition, de vérité et d'ensemble», The Kleene Symposium, Jon Barwise et al. (éditeurs), Amsterdam: North-Holland, 31–59.
  • Bealer, George, 1982, Qualité et Concept, Oxford: Clarendon Press.
  • Burgess, John P., 2014, «Friedman et l'axiomatisation de la théorie de la vérité de Kripke», dans Foundational Adventures: Essays in Honour of Harvey M. Friedman, édité par Neil Tennant, Londres: College Publications et Templeton Press (en ligne).
  • Cantini, Andrea, 1989, «Notes sur les théories formelles de la vérité», Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 35: 97-130.
  • –––, 1990, «Une théorie de la vérité formelle équivalente arithmétiquement à (mathrm {ID} _1)», Journal of Symbolic Logic, 55: 244–59.
  • –––, 1996, Cadres logiques de la vérité et de l'abstraction: une étude axiomatique, études de logique et fondements des mathématiques (n ° 135), Amsterdam: Elsevier.
  • Cieśliński, Cezary, 2010, «Vérité, conservativité et prouvabilité», Mind, 119: 409–422.
  • –––, 2007, «Deflationism, Conservativeness and Maximality», Journal of Philosophical Logic, 36: 695–705.
  • –––, 2017, La légèreté épistémique de la vérité: le déflationnisme et sa logique, Université de Cambridge.
  • Enayat, Ali et Albert Visser, 2015, «Nouvelles constructions de classes de satisfaction», dans Unifying the Philosophy of Truth, T. Achourioti, H. Galinon, K. Fujimoto, and J. Martínez-Fernández (eds.), Dordrecht: Springer, 321–335.
  • Feferman, Solomon, 1962, «Progressions récursives transfinies des théories axiomatiques», Journal of Symbolic Logic, 27: 259–316.
  • –––, 1984, «Vers des théories utiles sans type. JE." Journal of Symbolic Logic, 49: 75–111.
  • –––, 1991, «Reflecting on Incompleteness», Journal of Symbolic Logic, 56: 1–49.
  • –––, 2008, «Axiomes pour la détermination et la vérité», Review of Symbolic Logic, 1: 204–217.
  • Field, Hartry, 1999, «Deflating the Conservativeness Argument», Journal of Philosophy, 96: 533–40.
  • –––, 2003, «Une solution immunitaire contre la vengeance aux paradoxes sémantiques», Journal of Philosophical Logic, 32: 139-177.
  • –––, 2008, Sauver la vérité du paradoxe, Oxford: Oxford University Press.
  • Franzén, Torkel, 2004, Inexhaustibilité: un traitement non exhaustif, Association pour la logique symbolique.
  • Friedman, Harvey et Michael Sheard, 1987, «Une approche axiomatique de la vérité autoréférentielle», Annals of Pure and Applied Logic, 33: 1–21.
  • –––, 1988, «Les propriétés de disjonction et d'existence pour les systèmes axiomatiques de vérité», Annals of Pure and Applied Logic, 40: 1–10.
  • Fujimoto, Kentaro 2012, «Classes and Truths in Set Theory», Annals of Pure and Applied Logic, 163: 1484–1523.
  • Glanzberg, Michael, 2015, «Complexity and Hierarchy in Truth Predicates», dans Unifying the Philosophy of Truth, T. Achourioti, H. Galinon, K. Fujimoto, and J. Martínez-Fernández (eds.), Dordrecht: Springer, 211 –243.
  • Halbach, Volker, 1994, «Un système de vérité complète et cohérente», Notre Dame Journal of Formal Logic, 35: 311–27.
  • –––, 2001, «Disquotational Truth and Analyticity», Journal of Symbolic Logic, 66: 1959–1973.
  • –––, 2009, «Réduire la vérité compositionnelle en vérité disquotative», Revue de la logique symbolique 2 (2009), 786–798.
  • –––, 2011, Axiomatic Theories of Truth, Cambridge University, édition révisée 2014.
  • Halbach, Volker et Leon Horsten, 2006, «Axiomatisation de la théorie de la vérité de Kripke», Journal of Symbolic Logic, 71: 677–712.
  • Hájek, Petr et Pavel Pudlak, 1993, Métamathématiques de l'arithmétique du premier ordre, Berlin: Springer.
  • Heck, Richard, 2001, «Truth and Disquotation», Synthese, 142: 317–352.
  • –––, 2015, «La cohérence et la théorie de la vérité», Revue de la logique symbolique, 8: 424–466.
  • Horsten, Leon, 1995, «Les paradoxes sémantiques, la neutralité de la vérité et la neutralité de la théorie minimaliste de la vérité», dans The Many Problems of Realism (Studies in the General Philosophy of Science: Volume 3), P. Cortois (ed.), Tilburg: Presse universitaire de Tilburg, 173–87.
  • –––, 2011, The Tarskian Turn. Déflationnisme et vérité axiomatique, MIT Press.
  • Horsten, Leon et Graham E. Leigh, 2017, «La vérité est simple», Mind, 126 (501): 195-232.
  • Kahle, Reinhard, 2001, «La vérité dans les théories applicatives», Studia Logica, 68: 103–128.
  • Kaye, Richard, 1991, Models of Peano Arithmetic, Oxford Logic Guides, Oxford: Oxford University Press.
  • Ketland, Jeffrey, 1999, «Deflationism and Tarski's Paradise» Mind, 108 (429): 69–94.
  • Kotlarski, Henryk et Zygmunt Ratajczyk, 1990a, «Inductive Full Satisfaction Classes», Annals of Pure and Applied Logic, 47: 199-223.
  • –––, 1990b, «Plus d'informations sur l'induction dans la langue avec une classe de satisfaction», Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 36: 441–54.
  • Kotlarski, Henryk, Stanislav Krajewski et Alistair H. Lachlan, 1981, «Construction de classes de satisfaction pour les modèles non standard», Bulletin mathématique du Canada, 24: 283–93.
  • Kreisel, Georg et Azriel Lévy, 1968, «Principes de réflexion et leur utilisation pour établir la complexité des systèmes axiomatiques», Zeitschrift für Mathematische Logic und Grundlagen der Mathematik, 14: 97–142.
  • Kremer, Michael, 1988, «Kripke et la logique de la vérité», Journal of Philosophical Logic, 17: 225-278.
  • Kripke, Saul, 1975, «Aperçu d'une théorie de la vérité», Journal of Philosophy, 72: 690–716.
  • Lachlan, Alistair H., 1981, «Classes à satisfaction totale et saturation récursive», Bulletin mathématique canadien, 24: 295–97.
  • Leigh, Graham E., 2013, «Un compte rendu théorique de la preuve des principes classiques de la vérité.» Annales de la logique pure et appliquée, 164: 1009–1024.
  • –––, 2015, «Conservativity for Theories of Compositionitional Truth via Cut Elimination». Journal of Symbolic Logic, 80 (3): 845–865
  • –––, 2016, «Réflexion sur la vérité», IfCoLog Journal of Logics and their Applications, 3 (4): 557–594.
  • Leigh, Graham E. et Michael Rathjen, 2012, «Le programme Friedman-Sheard en logique intuitionniste», Journal of Symbolic Logic, 77: 777–806.
  • –––, 2010, «Une analyse ordinale pour les théories de la vérité autoréférentielle», Archive for Mathematical Logic, 49: 213–247.
  • Leitgeb, Hannes, 2001, «Théories de la vérité qui n'ont pas de modèles standard», Studia Logica, 68: 69–87.
  • Maudlin, Tim, 2004, Vérité et paradoxe. Résoudre les énigmes, Oxford: Clarendon Press.
  • McGee, Vann, 1985, «À quel point un prédicat peut-il être vrai? Un résultat négatif », Journal of Philosophical Logic, 14: 399–410.
  • –––, 1991, Truth, Vagueness, and Paradox: An Essay on the Logic of Truth, Indianapolis et Cambridge: Hackett Publishing.
  • –––, 1992, «Ensembles maximums cohérents d'instances du schéma de Tarski (T)», Journal of Philosophical Logic, 21: 235–241.
  • Myhill, John, 1950, «Un système qui peut définir sa propre vérité», Fundamenta Mathematicae, 37: 190–92.
  • Nicolai, Carlo, 2016, «Une note sur les affirmations typées de vérité et de cohérence», Journal of Philosophical Logic, 45: 89–119.
  • Reinhardt, William N., 1986, «Quelques remarques sur l'extension et l'interprétation des théories, avec un prédicat partiel de la vérité», Journal of Philosophical Logic, 15: 219–51.
  • Schindler, Thomas, 2015, «Une théorie perturbatrice de la vérité aussi forte que (mathrm {Z} ^ {-} _ 2)», Journal of Philosophical Logic, 44: 395–410.
  • Scott, Dana, 1975, «Combinators and classes», in (lambda) - calcul and Computer Science Theory (Notes de cours en informatique: volume 37), C. Böhm (éd.), Berlin: Springer, 1– 26.
  • Shapiro, Stewart, 1998, «Preuve et vérité: à travers épais et mince», Journal of Philosophy, 95 (10): 493-521.
  • –––, 2002, «Deflation and Conservation», Principes de vérité, Volker Halbach et Leon Horsten (eds.), Francfort aM: Dr. Hänsel-Hohenhausen, 103–128
  • Sheard, Michael, 1994, «Un guide des prédicats de vérité à l'ère moderne», Journal of Symbolic Logic, 59: 1032–54.
  • –––, 2001, «Théories faibles et fortes de la vérité», Studia Logica, 68: 89-101.
  • –––, 2002, «Vérité, probabilité et critères naïfs», Principes de vérité, Volker Halbach et Leon Horsten (éds.), Francfort aM: Dr Hänsel-Hohenhausen, 169–181.
  • Takeuti, Gaisi, 1987, Proof Theory (Studies in Logic and the Foundations of Mathematics: No. 81), Amsterdam: North-Holland, deuxième édition.
  • Tarski, Alfred, 1935, «Le concept de vérité dans les langues formalisées», dans Logic, Semantics, Metamathematics, Indianapolis: Hackett 1983, 2e édition, 152–278.
  • Tennant, Neil, 2002, «Deflationism and the Gödel-Phenomena», Mind, 111: 551–582.
  • Turner, Raymond, 1990, Truth and modality, Londres: Pitman.
  • Visser, Albert, 1989, «La sémantique et le paradoxe du menteur», Handbook of Philosophical Logic, 4: 617–706.
  • Yablo, Stephen, 1993, «Paradoxe sans auto-référence», Analyse, 53: 251–252.
  • Wcisło, Bartosz et Mateusz Łełyk, 2017, «Notes sur l'induction bornée pour le prédicat de vérité compositionnel», Review of Symbolic Logic, 10: 455-–480.

Outils académiques

icône de l'homme Sep
icône de l'homme Sep
Comment citer cette entrée.
icône de l'homme Sep
icône de l'homme Sep
Prévisualisez la version PDF de cette entrée à la Friends of the SEP Society.
icône inpho
icône inpho
Recherchez cette rubrique d'entrée sur le projet d'ontologie de philosophie Internet (InPhO).
icône de papiers phil
icône de papiers phil
Bibliographie améliorée pour cette entrée chez PhilPapers, avec des liens vers sa base de données.

Autres ressources Internet

[Veuillez contacter l'auteur avec des suggestions.]

Recommandé: