Logique De Justification

Table des matières:

Logique De Justification
Logique De Justification

Vidéo: Logique De Justification

Vidéo: Logique De Justification
Vidéo: Notions de logique #21# exercice 18 2024, Mars
Anonim

Ceci est un fichier dans les archives de l'Encyclopédie de Stanford de Philosophie. Informations sur l'auteur et la citation | Aperçu PDF d'amis | Recherche InPho | Bibliographie PhilPapers

Logique de justification

Publié pour la première fois le 22 juin 2011; révision de fond mer.20 juil.2011

Vous pouvez dire: «Je sais qu'Abraham Lincoln était un homme de grande taille. »À son tour, on vous demandera peut-être comment vous le savez. Vous ne répondriez presque certainement pas de manière sémantique, à la Hintikka, qu'Abraham Lincoln était grand dans toutes les situations compatibles avec vos connaissances. Au lieu de cela, vous diriez plus probablement: «J'ai lu la taille d'Abraham Lincoln dans plusieurs livres et j'ai vu des photographies de lui à côté d'autres personnes. «On certifie les connaissances en fournissant une raison, une justification. La sémantique Hintikka capture la connaissance comme une vraie croyance. Les logiques de justification fournissent le troisième élément manquant de la caractérisation par Platon de la connaissance comme croyance vraie justifiée.

  • 1. Pourquoi la logique de justification?

    • 1.1 Tradition épistémique
    • 1.2 Tradition logique mathématique
  • 2. Les composants de base de la logique de justification

    • 2.1 La logique du langage de la justification
    • 2.2 Logique de justification de base J 0
    • 2.3 Conscience logique et spécifications constantes
    • 2.4 Factivité
    • 2.5 Introspection positive
    • 2.6 Introspection négative
  • 3. Sémantique

    • 3.1 Modèles de justification mondiale possibles à agent unique pour J
    • 3.2 Complétude faible et forte
    • 3.3 La famille à agent unique
    • 3.4 Modèles de justification du monde unique
  • 4. Théorèmes de réalisation
  • 5. Généralisations

    • 5.1 Mélanger les connaissances explicites et implicites
    • 5.2 Modèles de justification mondiale possibles multi-agents
  • 6. Exemple de Russell: Factivité induite
  • 7. Autoréférentialité des justifications
  • 8. Quantificateurs dans la logique de justification
  • 9. Notes historiques
  • Bibliographie
  • Outils académiques
  • Entrées connexes
  • Autres ressources Internet

1. Pourquoi la logique de justification?

Les logiques de justification sont des logiques épistémiques qui permettent de «déplier» les modalités de connaissance et de croyance en termes de justification: au lieu de □ X on écrit t: X, et le lit comme «X est justifié par la raison t». On peut considérer les opérateurs modaux traditionnels comme des modalités implicites, et les termes de justification comme leurs élaborations explicites qui complètent les logiques modales par un mécanisme épistémique plus fin. La famille des termes de justification a une structure et des opérations. Le choix des opérations donne lieu à différentes logiques de justification. Pour toutes les logiques épistémiques courantes, leurs modalités peuvent être complètement développées sous une forme de justification explicite. À cet égard, Justification Logic révèle et utilise le contenu explicite, mais caché, de la logique modale épistémique traditionnelle.

La logique de justification a vu le jour dans le cadre d'un projet réussi visant à fournir une sémantique constructive pour les termes de justification logique intuitionniste qui ont fait abstraction de toutes les caractéristiques des preuves mathématiques, sauf les plus élémentaires. Les preuves sont peut-être des justifications dans leur forme la plus pure. Par la suite, des logiques de justification ont été introduites dans l'épistémologie formelle. Cet article présente la gamme générale des logiques de justification telles qu'elles sont actuellement comprises. Il discute de leurs relations avec les logiques modales conventionnelles. Outre les mécanismes techniques, l'article examine de quelle manière l'utilisation de termes de justification explicite éclaire un certain nombre de problèmes philosophiques traditionnels. Le sujet dans son ensemble est encore en développement actif. Ce qui est présenté ici est un instantané de celui-ci au moment de la rédaction.

Les racines de la logique de justification remontent à de nombreuses sources différentes, dont deux sont discutées en détail: l'épistémologie et la logique mathématique.

1.1 Tradition épistémique

Les propriétés de la connaissance et de la croyance font l'objet de la logique formelle au moins depuis von Wright et Hintikka (Hintikka 1962, von Wright 1951). La connaissance et la croyance sont toutes deux traitées comme des modalités d'une manière qui est maintenant très familière - la logique épistémique. Mais des trois critères de Platon pour la connaissance, justifié, vrai, croyance (Gettier 1963, Hendricks 2005), la logique épistémique ne fonctionne vraiment qu'avec deux d'entre eux. Mondes possibles et croyance modèle indiscernable - on croit ce qui est ainsi dans toutes les circonstances que l'on croit possible. La factivité met en jeu une composante de justesse - si quelque chose n'est pas ainsi dans le monde réel, il ne peut pas être connu, seulement cru. Mais il n'y a pas de représentation pour la condition de justification. Toutefois,l'approche modale a remarquablement réussi à permettre le développement d'une riche théorie mathématique et de ses applications (Fagin, Halpern, Moses et Vardi 1995, van Ditmarsch, van der Hoek et Kooi 2007). Pourtant, ce n'est pas une vue d'ensemble.

L'approche modale de la logique de la connaissance est, en un sens, construite autour du quantificateur universel: X est connu dans une situation si X est vrai dans toutes les situations indiscernables de celle-là. Les justifications, par contre, apportent un quantificateur existentiel dans l'image: X est connu dans une situation s'il existe une justification pour X dans cette situation. Cette dichotomie universelle / existentielle est familière aux logiciens - dans les logiques formelles, il existe une preuve pour une formule X si et seulement si X est vrai dans tous les modèles de la logique. On considère les modèles comme intrinsèquement non constructifs et les preuves comme des choses constructives. On ne se trompera pas beaucoup en pensant aux justifications en général comme aux preuves mathématiques. En effet, la première logique de justification a été explicitement conçue pour capturer des preuves mathématiques en arithmétique,quelque chose qui sera discuté plus en détail dans la section 1.2.

Dans la logique de la justification, outre la catégorie des formules, il existe une deuxième catégorie de justifications. Les justifications sont des termes formels, construits à partir de constantes et de variables utilisant divers symboles d'opération. Les constantes représentent des justifications pour des vérités communément acceptées, généralement des axiomes. Les variables indiquent des justifications non spécifiées. Différentes logiques de justification diffèrent sur les opérations autorisées (et également d'autres manières). Si t est un terme de justification et X est une formule, t: X est une formule, et est destiné à être lu:

t est une justification de X.

Une opération, commune à toutes les logiques de justification, est l'application, écrite comme une multiplication. L'idée est que si s est une justification pour A → B et t est une justification pour A, alors [s ⋅ t] est une justification pour B [1]. Autrement dit, la validité de ce qui suit est généralement supposée:

(1) s:(A → B) → (t: A → [s ⋅ t]: B).

C'est la version explicite de la distributivité habituelle des opérateurs de connaissances, et des opérateurs modaux en général, à travers l'implication:

(2) □ (A → B) → (□ A → □ B).

En fait, la formule (2) est à l'origine de nombreux problèmes d'omniscience logique. Elle affirme qu'un agent sait que tout ce qu'implique la connaissance-connaissance de l'agent est fermé sous la conséquence. Alors que connaissable en principe, la connaissabilité est fermée sous l'effet des conséquences, on ne peut en dire autant de toute version plausible de la connaissance réelle. La distinction entre (1) et (2) peut être exploitée dans une discussion de l'exemple paradigmatique de la grange rouge de Goldman et Kripke; voici une version simplifiée de l'histoire tirée de (Dretske 2005).

Supposons que je traverse un quartier dans lequel, à mon insu, des granges en papier mâché sont dispersées, et que je vois que l'objet devant moi est une grange. Parce que j'ai des perceptions de la grange avant moi, je crois que l'objet devant moi est une grange. Nos intuitions suggèrent que je ne connais pas Grange. Mais maintenant supposons que le quartier n'ait pas de fausses granges rouges, et je remarque également que l'objet en face de moi est rouge, donc je sais qu'une grange rouge est là. Cette juxtaposition, être une grange rouge, ce que je connais, implique qu'il y ait une grange, ce que je ne fais pas, «est un embarras».

Dans la première formalisation de l'exemple de la grange rouge, la dérivation logique sera effectuée dans une logique modale de base dans laquelle □ est interprété comme la modalité de «croyance». Ensuite, certaines des occurrences de □ seront interprétées en externe comme des «connaissances» selon la description du problème. Soit B la phrase «l'objet devant moi est une grange», et soit R la phrase «l'objet devant moi est rouge».

  1. □ B, «Je crois que l'objet devant moi est une grange»;
  2. □ (B ∧ R), «Je crois que l'objet devant moi est une grange rouge».

Au méta-niveau, 2 est en fait la connaissance, alors que par la description du problème, 1 n'est pas la connaissance.

□ (B ∧ R → B), une assertion de connaissance d'un axiome logique

Dans cette formalisation, il apparaît que la clôture épistémique sous sa forme modale (2) est violée: ligne 2, □ (B ∧ R), et ligne 3, □ (B ∧ R → B) sont des cas de connaissance alors que □ B (ligne 1) n'est pas la connaissance. Le langage modal ici ne semble pas aider à résoudre ce problème.

Considérons ensuite l'exemple de la grange rouge dans la logique de justification où t: F est interprété comme «je crois F pour la raison t». Soit u une justification individuelle spécifique pour la croyance que B, et v, pour la croyance que B ∧ R. De plus, soit a une justification de la vérité logique B ∧ R → B. Ensuite, la liste des hypothèses est:

  1. u: B, «u est une raison de croire que l'objet en face de moi est une grange»;
  2. v:(B ∧ R), 'v est une raison de croire que l'objet devant moi est une grange rouge'
  3. a:(B ∧ R → B).

Au niveau méta, la description du problème indique que 2 et 3 sont des cas de connaissance, et pas simplement de croyance, alors que 1 est une croyance qui n'est pas une connaissance. Voici comment se déroule le raisonnement formel:

  1. a:(B ∧ R → B) → (v:(B ∧ R) → [a ⋅ v]: B), par principe (1);
  2. v:(B ∧ R) → [a ⋅ v]: B, de 3 et 4, par logique propositionnelle;
  3. [a ⋅ v]: B, de 2 et 5, par logique propositionnelle.

Notez que la conclusion 6 est [a ⋅ v]: B, et non u: B; la clôture épistémique tient. En raisonnant en logique de justification, on a conclu que [a ⋅ v]: B est un cas de connaissance, c'est-à-dire «je connais B pour la raison a ⋅ v». Le fait que u: B ne soit pas un cas de connaissance ne gâche pas le principe de clôture, puisque ce dernier revendique une connaissance spécifiquement pour [a ⋅ v]: B. Donc après avoir observé une façade rouge, je connais bien B, mais cette connaissance n'a rien à voir avec 1, qui reste un cas de croyance plutôt que de connaissance. La formalisation de la logique de justification représente la situation équitablement.

Les justifications de suivi représentent la structure de l'exemple de la grange rouge d'une manière qui n'est pas capturée par les outils modaux épistémiques traditionnels. La formalisation de la logique de justification modélise ce qui semble se produire dans un tel cas; la fermeture de la connaissance sous implication logique est maintenue même si «grange» n'est pas perceptuellement connue. [2]

1.2 Tradition logique mathématique

Selon Brouwer, la vérité en mathématiques constructives (intuitionnistes) signifie l'existence d'une preuve, cf. (Troelstra et van Dalen 1988). En 1931-1934, Heyting et Kolmogorov ont donné une description informelle de la sémantique basée sur la preuve prévue pour la logique intuitionniste (Kolmogorov 1932, Heyting 1934), qui est maintenant appelée la sémantique de Brouwer-Heyting-Kolmogorov (BHK). Selon les conditions BHK, une formule est «vraie» si elle a une preuve. De plus, une preuve d'un énoncé composé est reliée aux preuves de ses composants de la manière suivante:

  • une preuve de A ∧ B consiste en une preuve de la proposition A et une preuve de la proposition B;
  • une preuve de A ∨ B est donnée en présentant soit une preuve de A, soit une preuve de B;
  • une preuve de A → B est une construction transformant des preuves de A en preuves de B;
  • le mensonge ⊥ est une proposition qui n'a pas de preuve, ¬ A est un raccourci pour A → ⊥.

Kolmogorov a explicitement suggéré que les objets de type preuve dans son interprétation («solutions aux problèmes») provenaient des mathématiques classiques (Kolmogorov 1932). En effet, d'un point de vue fondamental, il n'a pas beaucoup de sens de comprendre les «preuves» ci-dessus comme des preuves dans un système intuitionniste que ces conditions sont censées spécifier.

La valeur fondamentale de la sémantique BHK est qu'elle suggère de manière informelle mais sans ambiguïté de traiter les justifications, ici les preuves mathématiques, comme des objets avec des opérations.

Dans (Gödel 1933), Gödel a fait le premier pas vers le développement d'une sémantique rigoureuse basée sur la preuve pour l'intuitionnisme. Gödel considérait la logique modale classique S4 comme un calcul décrivant les propriétés de la prouvabilité:

  • Axiomes et règles de la logique propositionnelle classique;
  • □ (F → G) → (□ F → □ G);
  • □ F → F;
  • □ F → □□ F;
  • Règle de nécessité: si ⊢ F, alors ⊢ □ F.

Sur la base de la compréhension de Brouwer de la vérité logique comme prouvabilité, Gödel a défini une traduction tr (F) de la formule propositionnelle F dans le langage intuitionniste dans le langage de la logique modale classique: tr (F) est obtenu en préfixant chaque sous-formule de F avec la prouvabilité modalité □. De manière informelle, lorsque la procédure habituelle de détermination de la vérité classique d'une formule est appliquée à tr (F), elle testera la prouvabilité (et non la vérité) de chacune des sous-formules de F, en accord avec les idées de Brouwer. D'après les résultats de Gödel et les travaux de McKinsey-Tarski sur la sémantique topologique pour la logique modale, il s'ensuit que la traduction tr (F) fournit une incorporation appropriée du calcul propositionnel intuitionniste, IPC, dans S4, c'est-à-dire une incorporation de la logique intuitionniste dans la logique classique étendu par l'opérateur de prouvabilité.

(3) Si IPC prouve F, alors S4 prouve tr (F).

Pourtant, l'objectif initial de Gödel de définir la logique intuitionniste en termes de prouvabilité classique n'a pas été atteint, puisque la connexion de S4 à la notion mathématique habituelle de prouvabilité n'a pas été établie. De plus, Gödel a noté que l'idée simple d'interpréter la modalité □ F comme F est prouvable dans un système formel donné T contredit le deuxième théorème d'incomplétude de Gödel. En effet, □ (□ F → F) peut être dérivé en S4 par la règle de nécessité à partir de l'axiome □ F → F. D'un autre côté, interpréter la modalité □ comme le prédicat de la prouvabilité formelle en théorie T et F comme contradiction, convertit cette formule en une fausse affirmation que la cohérence de T est prouvable en interne dans T.

La situation après (Gödel 1933) peut être décrite par la figure suivante où 'X ↪ Y' doit être lu comme 'X est interprété dans Y'

IPC ↪ S4 ↪? ↪ ÉPREUVES CLASSIQUES

Lors d'une conférence publique à Vienne en 1938, Gödel a observé qu'en utilisant le format des preuves explicites:

(4) t est une preuve de F

peut aider à interpréter son calcul de prouvabilité S4 (Gödel 1938). Malheureusement, le travail de Gödel (Gödel 1938) est resté inédit jusqu'en 1995, date à laquelle la logique gödelienne des preuves explicites avait déjà été redécouverte, et axiomatisée comme Logic of Proofs LP et dotée de théorèmes d'exhaustivité la reliant à la fois aux preuves S4 et classiques (Artemov 1995).

Le LP Logic of Proofs est devenu le premier de la famille Justification Logic. Les termes de preuve dans LP ne sont rien d'autre que des termes BHK compris comme des preuves classiques. Avec LP, la logique intuitionniste propositionnelle a reçu la sémantique BHK rigoureuse souhaitée:

IPC ↪ S4 ↪ LP ↪ PROOFS CLASSIQUES

Pour une discussion plus approfondie de la tradition de la logique mathématique, voir la section 1 du document supplémentaire Some More Technical Matters.

2. Les composants de base de la logique de justification

Cette section présente la syntaxe et l'axiomatique des systèmes les plus courants de logique de justification.

2.1 La logique du langage de la justification

Afin de construire un compte rendu formel des logiques de justification, il faut faire une hypothèse structurelle de base: les justifications sont des objets abstraits qui ont une structure et des opérations sur eux. Un bon exemple de justifications est fourni par les preuves formelles, qui ont longtemps été des objets d'étude en logique mathématique et en informatique (cf. section 1.2).

Justification La logique est un cadre logique formel qui incorpore des assertions épistémiques t: F, signifiant «t est une justification de F». Justification Logic n'analyse pas directement ce que signifie t justifier F au-delà du format t: F, mais tente plutôt de caractériser cette relation de manière axiomatique. Ceci est similaire à la façon dont la logique booléenne traite ses connecteurs, disons disjonction: elle n'analyse pas la formule p ∨ q mais suppose plutôt certains axiomes logiques et tables de vérité concernant cette formule.

Plusieurs décisions de conception sont prises. Justification La logique commence par la base la plus simple: la logique booléenne classique, et pour de bonnes raisons. Les justifications constituent un défi suffisamment sérieux, même au niveau le plus simple. Les exemples paradigmatiques de Russell, Goldman-Kripke, Gettier et autres peuvent être traités avec la logique de justification booléenne. Le cœur de la logique épistémique se compose de systèmes modaux avec une base booléenne classique (K, T, K4, S4, K45, KD45, S5, etc.), et chacun d'eux a été fourni avec un compagnon logique de justification correspondant basé sur la logique booléenne. Enfin, la factivité des justifications n'est pas toujours supposée. Cela permet de saisir l'essence des discussions en épistémologie impliquant des questions de croyance et non de connaissance.

L'opération de base sur les justifications est l'application et la somme. L'opération d'application prend les justifications s et t et produit une justification s ⋅ t telle que si s:(F → G) et t: F, alors [s ⋅ t]: G. Symboliquement,

s:(F → G) → (t: F → [s ⋅ t]: G)

Il s'agit d'une propriété fondamentale des justifications supposées en logique combinatoire et λ -calculi (Troelstra et Schwichtenberg 1996), la sémantique de Brouwer-Heyting-Kolmogorov (Troelstra et van Dalen 1988), la réalisabilité de Kleene (Kleene 1945), la logique des preuves LP, etc..

Deux justifications peuvent être combinées en toute sécurité en quelque chose avec une portée plus large. Ceci est fait en utilisant la somme d'opération '+'. Si s: F, quelle que soit la preuve t, la preuve combinée s + t reste une justification de F. Plus exactement, l'opération «+» prend des justifications s et t et produit s + t, qui justifie tout ce qui est justifié par s ou par t.

s: F → [s + t]: F et t: F → [s + t]: F

Comme motivation, on pourrait penser à s et t comme deux volumes d'une encyclopédie, et s + t comme l'ensemble de ces deux volumes. Imaginons que l'un des volumes, disons s, contienne une justification suffisante pour une proposition F, c'est-à-dire s: F est le cas. Alors l'ensemble plus grand s + t contient également une justification suffisante pour F, [s + t]: F. Dans la Logic of Proofs LP, Section 1.2, «s + t» peut être interprété comme une concaténation de preuves s et t.

2.2 Logique de justification de base J 0

Les termes de justification sont construits à partir des variables de justification x, y, z,… et des constantes de justification a, b, c,… (avec des indices i = 1, 2, 3,… qui sont omis chaque fois que cela est sûr) au moyen des opérations » ⋅ 'et' + '. Des logiques plus élaborées examinées ci-dessous permettent également des opérations supplémentaires sur les justifications. Les constantes désignent des justifications atomiques que le système n'analyse pas; les variables dénotent des justifications non spécifiées. La logique de base des justifications, J 0 est axiomatisée par ce qui suit.

Logique classique
Axiomes propositionnels classiques et règle Modus Ponens
Axiome d'application
s:(F → G) → (t: F → [s ⋅ t]: G),
Axiomes de somme
s: F → [s + t]: F, s: F → [t + s]: F.

J 0 est la logique des justifications générales (pas nécessairement factives) pour un agent absolument sceptique pour lequel aucune formule n'est justifiée de manière prouvée, c'est-à-dire que J 0 ne dérive pas t: F pour tout t et F. Un tel agent est cependant capable de tirer des conclusions de justification relative de la forme

Si x: A, y: B,…, z: C sont maintenus, alors t: F.

Avec cette capacité, J 0 est capable d'émuler de manière adéquate d'autres systèmes de logique de justification dans son langage.

2.3 Conscience logique et spécifications constantes

Le principe de la Conscience Logique stipule que les axiomes logiques sont justifiés d'office: un agent accepte les axiomes logiques comme justifiés (y compris ceux concernant les justifications). Comme je viens de le dire, la conscience logique peut être trop forte dans certaines situations épistémiques. Cependant Justification Logic offre le mécanisme flexible des spécifications constantes pour représenter différentes nuances de conscience logique.

Bien entendu, on distingue entre une hypothèse et une hypothèse justifiée. En Justification Les constantes logiques sont utilisées pour représenter des justifications d'hypothèses dans des situations où elles ne sont plus analysées. Supposons que l'on souhaite postuler qu'un axiome A est justifié pour le connaissant. On postule simplement e 1: A pour une constante de preuve e 1 (d'indice 1). Si, par ailleurs, on souhaite postuler que ce nouveau principe e 1: A est également justifié, on peut postuler e 2:(e 1: A) pour une constante e 2(avec index 2). Etc. Le suivi des indices n'est pas nécessaire, mais c'est facile et aide dans les procédures de décision (Kuznets 2008). L'ensemble de toutes les hypothèses de ce type pour une logique donnée est appelé une spécification constante. Voici la définition formelle:

Une spécification constante CS pour une logique de justification donnée L est un ensemble de formules de la forme

e n: e n −1:…: e 1: A (n ≥ 1),

où A est un axiome de L, et e 1, e 2,…, e n sont des constantes similaires d'indices 1, 2,…, n. On suppose que CS contient toutes les spécifications intermédiaires, c'est-à-dire chaque fois que e n: e n −1:…: e 1: A est dans CS, alors e n −1:…: e 1: A est aussi dans CS.

Un certain nombre de conditions spéciales ont été placées sur des spécifications constantes dans la littérature. Les éléments suivants sont les plus courants.

Vide
CS = ∅. Cela correspond à un agent absolument sceptique. Cela revient à travailler avec la logique J 0.
Fini
CS est un ensemble fini de formules. Il s'agit d'un cas pleinement représentatif, car toute dérivation spécifique dans la logique de justification n'impliquera qu'un ensemble fini de constantes.
Axiomatiquement approprié
Chaque axiome, y compris ceux nouvellement acquis par la spécification constante elle-même, a des justifications. Dans le cadre formel, pour chaque axiome A il existe une constante e 1 telle que e 1: A est dans CS, et si e n: e n −1:…: e 1: A ∈ CS, alors e n +1: e n: e n −1:…: e 1: A ∈ CS, pour chaque n ≥ 1. Des spécifications de constantes axiomatiquement appropriées sont nécessaires pour assurer la propriété d'Internalisation, discutée à la fin de cette section.
Total

Pour chaque axiome A et toutes les constantes e 1, e 2,… e n,

e n: e n −1:…: e 1: A ∈ CS.

Le nom TCS est réservé à la spécification de la constante totale (pour une logique donnée). Naturellement, la spécification de la constante totale est axiomatiquement appropriée.

Nous pouvons maintenant préciser:

Logique des justifications avec une spécification de constante donnée:

Soit CS une spécification de constante. J CS est la logique J 0 + CS; les axiomes sont ceux de J 0 avec les membres de CS, et la seule règle d'inférence est Modus Ponens. Notez que J 0 est J .

Logique des justifications

J est la logique J 0 + règle d'internalisation axiome. La nouvelle règle stipule:

Pour chaque axiome A et toutes les constantes e 1, e 2,…, e n infer e n: e n −1:…: e 1: A.

Cette dernière incarne l'idée d'une conscience logique illimitée pour J. Une règle similaire est apparue dans Logic of Proofs LP, et a également été anticipée dans Goldman (Goldman 1967). La Conscience Logique, exprimée par des Spécifications de Constantes axiomatiquement appropriées, est une incarnation explicite de la Règle de Nécessitation en Logique Modale: ⊢ F ⇒ ⊢ □ F, mais restreinte aux axiomes. Notez que J coïncide avec J TCS.

La caractéristique clé des systèmes de logique de justification est leur capacité à internaliser leurs propres dérivations en tant qu'affirmations de justification prouvables dans leurs langues. Cette propriété était prévue en (Gödel 1938).

Théorème 1: Pour chaque spécification de constante axiomatiquement appropriée CS, J CS bénéficie d'une internalisation:

Si ⊢ F, alors ⊢ p: F pour un terme de justification p.

Preuve. Induction sur longueur de dérivation. Supposons que ⊢ F. Si F est un membre de J 0, ou un membre de CS, il existe une constante e n (où n pourrait être 1) telle que e n: F est dans CS, puisque CS est axiomatiquement approprié. Alors e n: F est dérivable. Si F est obtenu par Modus Ponens à partir de X → F et X, alors, par l'hypothèse d'induction, ⊢ s:(X → F) et ⊢ t: X pour certains s, t. En utilisant l'Axiome d'application, ⊢ [s ⋅ t]: F.

Voir la section 2 du document supplémentaire Quelques questions plus techniques pour des exemples de dérivations syntaxiques concrètes dans la logique de justification.

2.4 Factivité

La factivité déclare que les justifications suffisent à un agent pour conclure à la vérité. Ceci est incarné dans ce qui suit.

Axiome de Factivité t: F → F.

L'axiome de factivité a une motivation similaire à l'axiome de vérité de la logique épistémique, □ F → F, qui est largement accepté comme une propriété de base de la connaissance.

Contrairement aux principes d'application et de somme, la factivité des justifications n'est pas requise dans les systèmes de logique de justification de base, ce qui les rend capables de représenter à la fois des justifications partielles et factives. L'axiome de Factivité est apparu dans la Logic of Proofs LP, Section 1.2, comme une caractéristique principale des preuves mathématiques. En effet, dans ce contexte, la factivité est clairement valide: s'il existe une preuve mathématique t de F, alors F doit être vrai.

L'axiome de factivité est adopté pour les justifications qui conduisent à la connaissance. Cependant, la factivité seule ne justifie pas la connaissance, comme l'ont démontré les exemples de Gettier (Gettier 1963).

Logique des justifications factuelles

  • JT 0 = J 0 + Factivité;
  • JT = J + Factivité.

Les systèmes JT CS correspondant aux spécifications constantes CS sont définis comme dans la section 2.3.

2.5 Introspection positive

L'un des principes communs de la connaissance est d'identifier le savoir et le savoir que l'on sait. Dans un cadre modal, cela correspond à □ F → □□ F. Ce principe a une contrepartie explicite adéquate: le fait qu'un agent accepte t comme preuve suffisante pour F sert de preuve suffisante pour t: F. Souvent, ces «méta-preuves» ont une forme physique: un rapport d'arbitrage certifiant qu'une preuve dans un papier est correcte; une sortie de vérification informatique avec une preuve formelle t de F comme entrée; une preuve formelle que t est une preuve de F, etc. Une opération d'introspection positive '!' peut être ajouté à la langue à cet effet; on suppose alors que donné t, l'agent produit une justification! t de t: F tel que t: F →! t:(t: F). L'introspection positive sous cette forme opérationnelle est apparue pour la première fois dans Logic of Proofs LP.

Axiome d'introspection positif: t: F →! t:(t: F).

On définit alors:

  • J4: = J + Introspection positive;
  • LP: = JT + Introspection positive. [3]

Les logiques J4 0, J4 CS, LP 0 et LP CS sont définies de manière naturelle (cf. section 2.3). L'analogue direct du théorème 1 vaut également pour J4 CS et LP CS.

En présence de l'axiome d'introspection positive, on peut limiter la portée de la règle d'internalisation d'axiome aux axiomes d'internalisation qui ne sont pas de la forme e: A. C'est ainsi que cela a été fait dans LP: l'internalisation Axiom peut alors être émulée en utilisant !! e:(! e:(e: A)) au lieu de e 3:(e 2:(e 1: A)), etc. La notion de spécification de constante peut également être simplifiée en conséquence. Ces modifications sont mineures et n'affectent pas les principaux théorèmes et applications de la logique de justification.

2.6 Introspection négative

(Pacuit 2006, Rubtsova 2006) a considéré l'opération d'introspection négative '?' qui vérifie qu'une assertion de justification donnée est fausse. Une motivation possible pour envisager une telle opération est que l'opération d'introspection positive "!" peut très bien être considéré comme capable de fournir des jugements de vérification concluants sur la validité des assertions de justification t: F, donc lorsque t n'est pas une justification pour F, un tel «!» devrait conclure que ¬ t: F. C'est normalement le cas pour les vérificateurs de preuves informatiques, les vérificateurs de preuves dans les théories formelles, etc. Cette motivation est cependant nuancée: les exemples de vérificateurs de preuve et de vérificateurs de preuve fonctionnent avec t et F comme entrées, alors que le format Pacuit-Rubtsova? t suggère que la seule entrée pour «?» est une justification t, et le résultat? t est censé justifier des propositions ¬ t:F uniformément pour tous les F s pour lesquels t: F ne tient pas. Une telle opération '?' n'existe pas pour les preuves mathématiques formelles depuis? t devrait alors être une preuve unique d'une infinité de propositions ¬ t: F, ce qui est impossible.

Axiome d'introspection négatif ¬ t: F →? t: (¬ t: F)

Nous définissons les systèmes:

  • J45 = J4 + Introspection négative;
  • JD45 = J45 + ¬ t: ⊥;
  • JT45 = J45 + Factivité

et étendre naturellement ces définitions à J45 CS, JD45 CS et JT45 CS. L'analogue direct du théorème 1 est valable pour J45 CS, JD45 CS et JT45 CS.

3. Sémantique

La sémantique désormais standard de la logique de justification trouve son origine dans (Fitting 2005) - les modèles utilisés sont généralement appelés modèles d'ajustement dans la littérature, mais seront appelés ici modèles de justification mondiale possibles. Les modèles de justification du monde possibles sont un amalgame de la sémantique du monde possible familière pour les logiques de la connaissance et de la croyance, due à Hintikka et Kripke, avec des mécanismes spécifiques aux termes de justification, introduits par Mkrtychev dans (Mkrtychev 1997), (cf. Section 3.4).

3.1 Modèles de justification mondiale possibles à agent unique pour J

Pour être précis, une sémantique pour J CS, où CS est une spécification constante, doit être définie. Formellement, un modèle logique de justification du monde possible pour J CS est une structure M = ⟨G, R, E, V⟩. De cela, ⟨G, R⟩ est un cadre K standard, où G est un ensemble de mondes possibles et R est une relation binaire sur celui-ci. V est un mappage de variables propositionnelles à des sous-ensembles de G, spécifiant la vérité atomique à des mondes possibles.

Le nouvel élément est E, une fonction de preuve, qui a son origine dans (Mkrtychev 1997). Cela mappe les termes et formules de justification à des ensembles de mondes. L'idée intuitive est que si le monde possible Γ est dans E (t, X), alors t est une preuve pertinente ou admissible pour X au monde Γ. Il ne faut pas considérer les preuves pertinentes comme concluantes. Pensez-y plutôt comme une preuve qui peut être admise devant un tribunal: ce témoignage, ce document est quelque chose qu'un jury devrait examiner, quelque chose qui est pertinent, mais quelque chose dont le statut déterminant la vérité n'a pas encore été pris en considération. Les fonctions de preuve doivent remplir certaines conditions, mais celles-ci seront abordées un peu plus tard.

Étant donné un modèle de justification du monde possible J CS M = ⟨G, R, E, V⟩, la vérité de la formule X au monde possible Γ est notée M, Γ ⊩ X, et doit remplir les conditions standard suivantes:

Pour chaque Γ ∈ G:

  1. M, Γ ⊩ P ssi Γ ∈ V (P) pour P une lettre propositionnelle;
  2. ce n'est pas le cas que M, Γ ⊩ ⊥;
  3. M, Γ ⊩ X → Y ssi ce n'est pas le cas que M, Γ ⊩ X ou M, Γ ⊩ Y.

Ceux-ci disent simplement que la vérité atomique est spécifiée arbitrairement et que les connecteurs propositionnels se comportent de manière vérité-fonctionnelle dans chaque monde. L'élément clé est le suivant.

M, Γ ⊩ (t: X) si et seulement si Γ ∈ E (t, X) et, pour tout Δ ∈ G avec Γ R Δ, on a que M, Δ ⊩ X

Cette condition se divise en deux parties. Clause exigeant que M, Δ ⊩ X pour tout Δ ∈ G tel que Γ R Δ soit la condition familière de Hintikka / Kripke pour que X soit cru, ou crédible, en Γ. La clause exigeant que Γ ∈ E (t, X) ajoute que t devrait être une preuve pertinente pour X en Γ. Alors, de manière informelle, t: X est vrai dans un monde possible si X est crédible dans ce monde au sens habituel de la logique épistémique, et t est une preuve pertinente de X dans ce monde.

Il est important de réaliser que, dans cette sémantique, on peut ne pas croire quelque chose pour une raison particulière dans un monde, soit parce que ce n'est tout simplement pas crédible, soit parce que c'est mais la raison n'est pas appropriée.

Certaines conditions doivent encore être placées sur les fonctions de preuve, et la spécification constante doit également être prise en compte. Supposons que l'on donne s et t comme justifications. On peut les combiner de deux manières différentes: utiliser simultanément les informations des deux; ou utilisez les informations d'un seul d'entre eux, mais choisissez d'abord lequel. Chacune donne lieu à une opération de base sur les termes de justification, ⋅ et +, introduite de manière axiomatique dans la section 2.2.

Supposons que s est une preuve pertinente pour une implication et t est une preuve pertinente pour l'antécédent. Ensuite, s et t fournissent ensemble des preuves pertinentes pour le conséquent. La condition suivante sur les fonctions de preuve est supposée:

E (s, X → Y) ∩E (t, X) ⊆ E (s ⋅ t, Y)

Avec cette condition ajoutée, la validité de

s:(X → Y) → (t: X → [s ⋅ t]: Y)

est sécurisé.

Si s et t sont des éléments de preuve, on pourrait dire que quelque chose est justifié par l'un des s ou t, sans se soucier de préciser lesquels, et cela restera une preuve. L'exigence suivante est imposée aux fonctions de preuve.

E (s, X) ∪ E (t, X) ⊆ E (s + t, X)

Sans surprise, les deux

s: X → [s + t]: X

et

t: X → [s + t]: X

maintenant tenez.

Enfin, la spécification constante CS doit être prise en compte. Rappelez-vous que les constantes sont destinées à représenter les raisons des hypothèses de base qui sont acceptées d'emblée. Un modèle M = ⟨G, R, E, V⟩ répond à la spécification constante CS à condition: si c: X ∈ CS alors E (c, X) = G.

Modèle de justification du monde possible Un modèle de justification du monde possible pour J CS est une structure M = ⟨G, R, E, V⟩ satisfaisant toutes les conditions énumérées ci-dessus et répondant à la spécification de constante CS.

Malgré leurs similitudes, les modèles de justification du monde possibles permettent une analyse fine qui n'est pas possible avec les modèles Kripke. Voir la section 3 du document supplémentaire Quelques questions techniques supplémentaires pour plus de détails.

3.2 Complétude faible et forte

Une formule X est valide dans un modèle particulier pour J CS si elle est vraie dans tous les mondes possibles du modèle. L'axiomatique pour J CS a été donnée dans les sections 2.2 et 2.3. Un théorème de complétude prend maintenant la forme attendue.

Théorème 2: Une formule X est prouvable dans J CS si et seulement si X est valide dans tous les modèles J CS.

Le théorème d'exhaustivité tel qu'il vient d'être énoncé est parfois appelé complétude faible. Il peut être un peu surprenant qu'il soit beaucoup plus facile à prouver que l'exhaustivité de la logique modale K. Les commentaires sur ce point suivent. D'autre part, il est très général, fonctionnant pour toutes les spécifications constantes.

Dans (Fitting 2005), une version plus forte de la sémantique a également été introduite. Un modèle M = ⟨G, R, E, V⟩ est dit pleinement explicatif s'il remplit la condition suivante. Pour chaque Γ ∈ G, si M, Δ ⊩ X pour tout Δ ∈ G tel que Γ R Δ, alors M, Γ ⊩ t: X pour un terme de justification t. Notons que la condition M, Δ ⊩ X pour tout Δ ∈ G tel que Γ R Δ, est la condition habituelle pour que X soit crédible en Γ au sens Hintikka / Kripke. Donc, tout à fait explicatif dit vraiment que si une formule est crédible dans un monde possible, il y a une justification à cela.

Tous les modèles faibles ne remplissent pas la condition pleinement explicative. Les modèles qui le font sont appelés modèles forts. Si la spécification constante CS est suffisamment riche pour qu'un théorème d'internalisation soit vrai, alors on a l'exhaustivité par rapport aux modèles forts rencontrant CS. En effet, dans un sens approprié, l'exhaustivité par rapport à des modèles forts équivaut à être capable de prouver l'Internalisation.

La preuve d'exhaustivité vis-à-vis des modèles forts présente une similitude étroite avec la preuve d'exhaustivité utilisant des modèles canoniques pour la logique modale K. À leur tour, des modèles forts peuvent être utilisés pour donner une preuve sémantique du théorème de réalisation (cf. Section 4).

3.3 La famille à agent unique

Jusqu'à présent, une sémantique mondiale possible pour une logique de justification a été discutée, pour J, le pendant de K. Maintenant, les choses sont élargies pour englober les analogues de justification d'autres logiques modales familières.

En ajoutant simplement la réflexivité de la relation d'accessibilité R aux conditions d'un modèle de la section 3.1, on gagne la validité de t: X → X pour tout t et X, et obtient une sémantique pour JT, la logique de justification analogique de la logique modale T, la logique la plus faible de la connaissance. En effet, si M, Γ ⊩ t: X alors, en particulier, X est vrai à tout état accessible depuis Γ. Puisque la relation d'accessibilité doit être réflexive, M, Γ ⊩ X. Les théorèmes de complétude faibles et forts peuvent être prouvés en utilisant le même mécanisme que celui appliqué dans le cas de J, et une preuve sémantique d'un théorème de réalisation reliant JT et T est également disponible. La même chose s'applique aux logiques décrites ci-dessous.

Pour une justification analogue de K4, un opérateur unaire supplémentaire '!' est ajouté au terme langue, voir Section 2.5. Rappelons que cet opérateur mappe les justifications aux justifications, où l'idée est que si t est une justification de X, alors! t devrait être une justification pour t: X. Sémantiquement, cela ajoute des conditions à un modèle M = ⟨G, R, E, V⟩, comme suit.

Premièrement, bien sûr, R doit être transitif, mais pas nécessairement réflexif. Deuxièmement, une condition de monotonie des fonctions de preuve est requise:

Si Γ R Δ et Γ ∈ E (t, X) alors Δ ∈ E (t, X)

Et enfin, une autre condition de fonction de preuve est nécessaire.

E (t, X) ⊆ E (! T, t: X)

Ces conditions ensemble impliquent la validité de t: X →! t: t: X et produire une sémantique pour J4, un analogue de justification de K4, avec un théorème de réalisation les reliant. L'ajout de réflexivité conduit à une logique qui s'appelle LP pour des raisons historiques.

On peut également ajouter un opérateur d'introspection négatif, «?», Voir Section 2.6. Les modèles de logiques de justification qui incluent cet opérateur ajoutent trois conditions. Le premier R est symétrique. Deuxièmement, on ajoute une condition qui est devenue connue sous le nom de preuve forte: M, Γ ⊩ t: X pour tout Γ ∈ E (t, X). Enfin, il existe une condition sur la fonction de preuve:

E (t, X) ⊆ E (? T, ¬ t: X)

Si cette machinerie est ajoutée à celle de J4, nous obtenons la logique J45, une contrepartie de justification de K45. La solidité et l'exhaustivité axiomatiques peuvent être prouvées. De la même manière, les logiques associées JD45 et JT45 peuvent être formulées.

Un théorème de réalisation prenant en compte cet opérateur a été montré dans (Rubtsova 2006).

3.4 Modèles de justification du monde unique

Les modèles de justification du monde unique ont été développés considérablement avant les modèles de justification du monde plus généraux possibles dont nous avons discuté (Mkrtychev 1997). Aujourd'hui, ils peuvent tout simplement être considérés comme de possibles modèles de justification mondiale qui se trouvent avoir un seul monde. La preuve d'exhaustivité pour J et les autres logiques de justification mentionnées ci-dessus peuvent facilement être modifiées pour établir l'exhaustivité par rapport aux modèles de justification de monde unique, bien que ce n'était bien sûr pas l'argument original. Ce que l'exhaustivité des modèles de justification de monde unique nous dit, c'est que les informations sur la structure mondiale possible des modèles de justification peuvent être complètement codées par la fonction de preuve admissible, du moins pour les logiques discutées jusqu'à présent. Mkrtychev a utilisé des modèles de justification mondiale unique pour établir la décidabilité de LP,et d'autres en ont fait un usage fondamental pour fixer des limites de complexité pour les logiques de justification, ainsi que pour montrer les résultats de conservativité pour les logiques de justification de la croyance (Kuznets 2000, Kuznets 2008, Milnikel 2007, Milnikel 2009). Les résultats de complexité ont en outre été utilisés pour résoudre le problème de l'omniscience logique.

4. Théorèmes de réalisation

La contrepartie épistémique modale naturelle de l'assertion de preuve t: F est □ F, lisez pour certains x, x: F. Cette observation conduit à la notion de projection oublieuse qui remplace chaque occurrence de t: F par □ F et convertit donc une phrase logique de justification S en une phrase logique modale S o correspondante. La projection oublieuse s'étend de manière naturelle des phrases aux logiques.

De toute évidence, différentes phrases de logique de justification peuvent avoir la même projection oublieuse, par conséquent S o perd certaines informations contenues dans S. Cependant, il est facile d'observer que la projection oublieuse mappe toujours des formules valides de logique de justification (par exemple, les axiomes de J) à des formules valides d'une logique épistémique correspondante (K dans ce cas). L'inverse est également vrai: toute formule valide de logique épistémique est la projection oublieuse d'une formule valide de logique de justification. Cela découle du théorème de correspondance 3.

Théorème 3: J o = K.

Cette correspondance vaut pour d'autres paires de systèmes de justification et d'épistémie, par exemple J4 et K4, ou LP et S4, et bien d'autres. Dans une telle forme étendue, le théorème de correspondance montre que les logiques modales majeures telles que K, T, K4, S4, K45, S5 et quelques autres ont des équivalents exacts de logique de justification.

Au cœur du théorème de correspondance se trouve le théorème de réalisation suivant.

Théorème 4: Il existe un algorithme qui, pour chaque formule modale F dérivable dans K, attribue des termes de preuve à chaque occurrence de modalité dans F de telle sorte que la formule résultante F r soit dérivable dans J. De plus, la réalisation assigne des variables de preuve aux occurrences négatives des opérateurs modaux en F, respectant ainsi la lecture existentielle de la modalité épistémique.

Les algorithmes de réalisation connus qui récupèrent les termes de preuve dans les théorèmes modaux utilisent des dérivations sans coupure dans les logiques modales correspondantes. Alternativement, le théorème de réalisation peut être établi sémantiquement par la méthode de Fitting ou ses modifications appropriées. En principe, ces arguments sémantiques produisent également des procédures de réalisation basées sur une recherche exhaustive.

Ce serait une erreur de tirer la conclusion que toute logique modale a une contrepartie logique de logique de justification. Par exemple, la logique de la prouvabilité formelle, GL, (Boolos 1993) contient le principe de Löb:

(5) □ (□ F → F) → □ F,

qui ne semble pas avoir de version explicite épistémiquement acceptable. Considérons, par exemple, le cas où F est la constante propositionnelle ⊥ pour faux. Si un analogue du théorème 4 couvrait le principe de Löb, il y aurait des termes de justification s et t tels que x:(s: ⊥ → ⊥) → t: ⊥. Mais c'est intuitivement faux pour une justification factuelle. En effet, s: ⊥ → ⊥ est une instance de l'axiome de factivité. Appliquez l'internalisation d'axiome pour obtenir c:(s: ⊥ → ⊥) pour une certaine constante c. Ce choix de c rend l'antécédent de c:(s: ⊥ → ⊥) → t: ⊥ intuitivement vrai et la conclusion fausse [4]. En particulier, le principe de Löb (5) n'est pas valable pour l'interprétation de la preuve (cf. (Goris 2007) pour un compte rendu complet des principes de GL sont réalisables).

Le théorème de correspondance donne un nouvel aperçu des logiques modales épistémiques. Plus particulièrement, il fournit une nouvelle sémantique pour les principales logiques modales. En plus de la lecture `` universelle '' traditionnelle à la Kripke de □ F comme F dans toutes les situations possibles, il existe maintenant une sémantique `` existentielle '' rigoureuse pour □ F qui peut être lue car il y a un témoin (preuve, justification) pour F.

La sémantique de justification joue un rôle similaire dans la logique modale à celui joué par la réalisabilité de Kleene dans la logique intuitionniste. Dans les deux cas, la sémantique envisagée est existentielle: l'interprétation de Brouwer-Heyting-Kolmogorov de la logique intuitionniste (Heyting 1934, Troelstra et van Dalen 1988, van Dalen 1986) et la lecture de la prouvabilité de Gödel de S4 (Gödel 1933, Gödel 1938). Dans les deux cas, il existe une sémantique mondiale possible de l' universelcaractère qui est un outil technique très puissant et dominant. Il n'aborde cependant pas le caractère existentiel de la sémantique voulue. Il a fallu la réalisabilité de Kleene (Kleene 1945, Troelstra 1998) pour révéler la sémantique computationnelle de la logique intuitionniste et de la logique des preuves pour fournir une sémantique BHK exacte des preuves pour la logique intuitionniste et modale.

Dans le contexte épistémique, la logique de justification et le théorème de correspondance ajoutent une nouvelle composante de «justification» aux logiques modales de la connaissance et de la croyance. Encore une fois, cette nouvelle composante était, en fait, une notion ancienne et centrale qui a été largement discutée par les épistémologues traditionnels, mais qui est restée hors du champ de la logique épistémique classique. Le théorème de correspondance nous dit que les justifications sont compatibles avec les systèmes de style Hintikka et peuvent donc être incorporées en toute sécurité dans la base de la logique modale épistémique.

Voir la section 4 du document supplémentaire Quelques questions techniques supplémentaires pour en savoir plus sur les théorèmes de réalisation.

5. Généralisations

Jusqu'à présent, dans cet article, seules les logiques de justification à agent unique, analogues aux logiques de connaissance à agent unique, ont été considérées. Justification La logique peut être considérée comme une logique de connaissance explicite, liée à des logiques plus conventionnelles de connaissance implicite. Un certain nombre de systèmes au-delà de ceux discutés ci-dessus ont été étudiés dans la littérature, impliquant plusieurs agents, ou ayant à la fois des opérateurs implicites et explicites, ou une combinaison de ceux-ci.

5.1 Mélanger les connaissances explicites et implicites

Puisque les logiques de justification fournissent des justifications explicites, alors que les logiques conventionnelles de la connaissance fournissent un opérateur de connaissance implicite, il est naturel d'envisager de combiner les deux dans un seul système. La logique conjointe la plus courante de connaissances explicites et implicites est S4LP (Artemov et Nogina 2005). Le langage de S4LP est comme celui de LP, mais avec un opérateur de connaissance implicite ajouté, écrit soit K ou □. L'axiomatique est comme celle de LP, combinée à celle de S4 pour l'opérateur implicite, avec un axiome de connexion, t: X → □ X, tout ce qui a une justification explicite est connaissable.

Sémantiquement, les modèles de justification mondiale possibles pour LP ne nécessitent aucune modification, car ils ont déjà toutes les machines des modèles Hintikka / Kripke. On modélise l'opérateur □ de la manière habituelle, en utilisant uniquement la relation d'accessibilité, et on modélise les termes de justification comme décrit dans la section 3.1 en utilisant à la fois l'accessibilité et la fonction de preuve. Puisque la condition habituelle pour que □ X soit vrai dans un monde est l'une des deux clauses de la condition pour t: X étant vrai, cela donne immédiatement la validité de t: X → □ X, et la solidité suit facilement. L'exhaustivité axiomatique est également assez simple.

Dans S4LP, les connaissances implicites et explicites sont représentées, mais dans la sémantique possible du modèle de justification mondiale, une seule relation d'accessibilité sert pour les deux. Ce n’est pas la seule façon de procéder. Plus généralement, une relation explicite d'accessibilité des connaissances pourrait être une extension appropriée de celle des connaissances implicites. Cela représente la vision d'une connaissance explicite comme ayant des normes plus strictes pour ce qui compte comme connu que celle de la connaissance implicite. L'utilisation de relations d'accessibilité différentes pour des connaissances explicites et implicites devient nécessaire lorsque ces notions épistémiques obéissent à des lois logiques différentes, par exemple S5 pour la connaissance implicite et LP pour l'explicite. Le cas des relations d'accessibilité multiples est communément connu dans la littérature sous le nom de modèles Artemov-Fitting, mais sera appelé ici modèles de mondes possibles multi-agents. (cf. section 5.2).

Curieusement, alors que la logique S4LP semble tout à fait naturelle, un théorème de réalisation lui a posé problème: aucun théorème de ce genre ne peut être prouvé si l'on insiste sur ce qu'on appelle des réalisations normales (Kuznets 2010). La réalisation de modalités de connaissance implicites en S4LP par des justifications explicites qui respecteraient la structure épistémique reste un enjeu majeur dans ce domaine.

Les interactions entre connaissances implicites et explicites peuvent parfois être assez délicates. À titre d'exemple, considérons le principe mixte d'introspection négative suivant (encore une fois, □ doit être lu comme un opérateur épistémique implicite),

(6) ¬ t: X → □ ¬ t: X.

Du point de vue de la prouvabilité, c'est la bonne forme d'introspection négative. En effet, soit □ F soit interprété comme F est prouvable et t: F comme t est une preuve de F dans une théorie formelle donnée T, par exemple dans Peano Arithmetic PA. Puis (6) énonce un principe prouvable. En effet, si t n'est pas une preuve de F alors, puisque cet énoncé est décidable, il peut être établi à l'intérieur de T, donc en T cette phrase est prouvable. D'autre part, la preuve p de 't n'est pas une preuve de F' dépend à la fois de t et de F, p = p (t, F) et ne peut pas être calculée étant donné t seulement. À cet égard, □ ne peut être remplacé par aucun terme de preuve spécifique dépendant de t uniquement et (6) ne peut pas être présenté dans un format de type justification entièrement explicite.

Les premiers exemples de systèmes de connaissances explicites / implicites sont apparus dans le domaine de la logique de prouvabilité. Dans (Sidon 1997, Yavorskaya (Sidon) 2001), un LPP logique a été introduit qui combinait la logique de la prouvabilité GL avec la logique des preuves LP, mais pour s'assurer que le système résultant avait des propriétés logiques souhaitables, certaines opérations supplémentaires en dehors des langages d'origine de GL et LP ont été ajoutés. Dans (Nogina 2006, Nogina 2007) un système logique complet, GLA, pour les preuves et la prouvabilité a été offert, dans la somme des langues originales de GL et LP. LPP et GLA bénéficient tous deux de l'exhaustivité par rapport à la classe des modèles arithmétiques, et également par rapport à la classe des modèles de justification mondiale possibles.

Un autre exemple de principe de prouvabilité qui ne peut être rendu complètement explicite est le principe de Löb (5). Pour chacun des LPP et GLA, il est facile de trouver un terme de preuve l (x) tel que

(7) x: (□ F → F) → l (x): F

tient. Cependant, il n'y a aucune réalisation qui rend les trois □ dans (5) explicites. En fait, l'ensemble des principes de prouvabilité réalisables est l'intersection de GL et S4 (Goris 2007).

5.2 Modèles de justification mondiale possibles multi-agents

Dans les modèles de justification du monde possible multi-agents, de multiples relations d'accessibilité sont utilisées, avec des connexions entre elles (Artemov 2006). L'idée est qu'il y a plusieurs agents, chacun avec un opérateur de connaissance implicite, et il y a des termes de justification, que chaque agent comprend. En gros, tout le monde comprend des raisons explicites; ceux-ci sont des connaissances communes fondées sur des preuves.

Un modèle de justification du monde possible à n-agents est une structure ⟨G, R 1,…, R n, R, E, V⟩ remplissant les conditions suivantes. G est un ensemble de mondes possibles. Chacun de R 1,…, R n est une relation d'accessibilité, une pour chaque agent. Ceux-ci peuvent être supposés être réflexifs, transitifs ou symétriques, selon les besoins. Ils sont utilisés pour modéliser les connaissances implicites des agents pour la famille des agents. La relation d'accessibilité R répond aux conditions LP, réflexivité et transitivité. Il est utilisé dans la modélisation des connaissances explicites. E est une fonction de preuve, remplissant les mêmes conditions que celles de LP dans la section 3.3. V mappe les lettres propositionnelles à des ensembles de mondes, comme d'habitude. Il y a une condition particulière imposée: pour chaque i = 1,…, n, R i ⊆ R.

Si M = ⟨G, R 1,…, R n, R, E, V⟩ est un modèle de justification du monde possible multi-agents, une relation vérité-dans-un-monde, M, Γ ⊩ X, est définie avec la plupart des les clauses habituelles. Ceux qui présentent un intérêt particulier sont les suivants:

  • M, Γ ⊩ K i X si et seulement si, pour tout Δ ∈ G avec Γ R i Δ, on a que M, Δ ⊩ X.
  • M, Γ ⊩ t: X si et seulement si Γ ∈ E (t, X) et, pour tout Δ ∈ G avec Γ R Δ, on a que M, Δ ⊩ X.

La condition R i ⊆ R entraîne la validité de t: X → K i X, pour chaque agent i. S'il n'y a qu'un seul agent et que la relation d'accessibilité pour cet agent est réflexive et transitive, cela fournit une autre sémantique pour S4LP. Quel que soit le nombre d'agents, chaque agent accepte des raisons explicites comme établissant des connaissances.

Une version de LP avec deux agents a été introduite et étudiée dans (Yavorskaya (Sidon) 2008), bien qu'elle puisse être généralisée à n'importe quel nombre fini d'agents. En cela, chaque agent a son propre ensemble d'opérateurs de justification, de variables et de constantes, plutôt que d'avoir un seul ensemble pour tout le monde, comme ci-dessus. En outre, une communication limitée entre agents peut être autorisée, en utilisant un nouvel opérateur qui permet à un agent de vérifier l'exactitude des justifications de l'autre agent. Des versions de la sémantique de justification du monde unique et plus générale possible ont été créées pour les logiques à deux agents. Cela implique une extension directe de la notion de fonction de preuve, et pour d'éventuels modèles de justification mondiale, en utilisant deux relations d'accessibilité. Les théorèmes de réalisation ont été prouvés syntaxiquement,bien que vraisemblablement une preuve sémantique fonctionnerait également.

Il y a eu une exploration récente du rôle des annonces publiques dans les logiques de justification multi-agents (Renne 2008, Renne 2009).

Il y a plus sur la notion de connaissances communes fondées sur des preuves dans la section 5 du document supplémentaire Some More Technical Matters.

6. Exemple de Russell: Factivité induite

Il existe une technique permettant d'utiliser la logique de justification pour analyser différentes justifications d'un même fait, en particulier lorsque certaines des justifications sont factuelles et d'autres non. Pour démontrer la technique, considérons un exemple bien connu:

Si un homme croit que le nom de famille du défunt premier ministre a commencé par un «B», il croit ce qui est vrai, puisque le défunt premier ministre était Sir Henry Campbell Bannerman [5]. Mais s'il croit que M. Balfour était le défunt premier ministre [6], il croira toujours que le nom de famille du défunt premier ministre commençait par un «B», mais cette croyance, bien que vraie, ne serait pas considérée comme une connaissance. (Russell 1912)

Comme dans l'exemple de la grange rouge, discuté dans la section 1.1, il faut ici traiter de deux justifications pour une déclaration vraie, dont l'une est correcte et l'autre ne l'est pas. Soit B une phrase (atome propositionnel), w une variable de justification désignée pour la mauvaise raison de B et ra une variable de justification désignée pour la bonne raison (donc factive) de B. Ensuite, l'exemple de Russell amène l'ensemble suivant d'hypothèses [7]:

R = {w: B, r: B, r: B → B}

Un peu contraire à l'intuition, on peut logiquement déduire la factivité de w de R:

  1. r: B (hypothèse)
  2. r: B → B (hypothèse)
  3. B (de 1 et 2 par Modus Ponens)
  4. B → (w: B → B) (axiome propositionnel)
  5. w: B → B (de 3 et 4 par Modus Ponens)

Cependant, cette dérivation utilise le fait que r est une justification factive pour que B conclue w: B → B, ce qui constitue un cas de «factivité induite» pour w: B. La question est de savoir comment distinguer la factivité «réelle» de r: B de la «factivité induite» de w: B? Une sorte de suivi de la vérité est nécessaire ici, et la logique de justification est un outil approprié. L'approche naturelle consiste à considérer l'ensemble des hypothèses sans r: B, c'est-à-dire

S = {w: B, r: B → B}

et établir que la factivité de w, c'est-à-dire w: B → B n'est pas dérivable de S. Voici un modèle de justification du monde possible M = (G, R, E, V) dans lequel S est vrai mais w: B → B ne:

  • G = { 1 },
  • R = ∅,
  • V (B) = ∅ (et donc pas - 1 ⊩ B),
  • E (t, F) = { 1 } pour toutes les paires (t, F) sauf (r, B), et
  • E (r, B) = ∅.

Il est facile de voir que les conditions de fermeture Application et Somme sur E sont remplies. En 1, w: B est valable, c'est-à-dire

1 ⊩ w: B

puisque w est une preuve admissible pour B en 1 et qu'il n'y a pas de mondes possibles accessibles à partir de 1. En outre,

pas- 1 ⊩ r: B

puisque, selon E, r n'est pas une preuve admissible pour B en 1. Par conséquent:

1 ⊩ r: B → B

D'autre part,

pas- 1 ⊩ w: B → B

puisque B ne tient pas à 1.

7. Autoréférentialité des justifications

Les algorithmes de Réalisation produisent parfois des Spécifications Constantes contenant des assertions de justification autoréférentielle c: A (c), c'est-à-dire des assertions dans lesquelles la justification (ici c) se produit dans la proposition affirmée (ici A (c)).

L'autoréférentialité des justifications est un phénomène nouveau qui n'est pas présent dans le langage modal conventionnel. En plus d'être des objets épistémiques intrigants, de telles affirmations autoréférentielles constituent un défi particulier du point de vue sémantique en raison du cercle vicieux intégré. En effet, pour évaluer c, on s'attendrait d'abord à évaluer A puis à attribuer un objet de justification pour A à c. Cependant, cela ne peut pas être fait car A contient c qui doit encore être évalué. La question de savoir si les logiques modales peuvent être réalisées ou non sans utiliser de justifications autoréférentielles était une question ouverte majeure dans ce domaine.

Le principal résultat de Kuznets dans (Brejnev et Kuznets 2006) indique que l'auto-référentialité des justifications est inévitable dans la réalisation de S4 en LP. L'état actuel des choses est donné par le théorème suivant dû à Kuznets:

Théorème 5: L'auto-référentialité peut être évitée dans les réalisations des logiques modales K et D. L'auto-référentialité ne peut pas être évitée dans les réalisations des logiques modales T, K4, D4 et S4.

Ce théorème établit qu'un système de termes de justification pour S4 sera nécessairement auto-référentiel. Cela crée une contrainte sérieuse, mais pas directement visible, sur la sémantique de la prouvabilité. Dans le contexte gödelien des preuves arithmétiques, le problème a été résolu par une méthode générale d'assignation de la sémantique arithmétique aux assertions autoréférentielles c: A (c) indiquant que c est une preuve de A (c). Dans Logic of Proofs LP, il a été traité par une construction en virgule fixe non triviale.

L'auto-référentialité donne une perspective intéressante sur le paradoxe de Moore. Voir la section 6 du document supplémentaire Quelques questions techniques supplémentaires pour plus de détails.

8. Quantificateurs dans la logique de justification

Si l’enquête sur la logique de justification propositionnelle est loin d’être terminée, des travaux sporadiques ont également été menés sur les versions de premier ordre. Les versions quantifiées de Modal Logic offrent déjà des complexités au-delà de la logique standard du premier ordre. La quantification a un champ encore plus large à jouer lorsque des logiques de justification sont impliquées. Classiquement, on quantifie sur des «objets», et les modèles sont équipés d'un domaine sur lequel les quantificateurs vont. Modalement, on peut avoir un seul domaine commun à tous les mondes possibles, ou on peut avoir des domaines séparés pour chaque monde. Le rôle de la formule Barcan est ici bien connu. Des options de domaine constant et variable sont également disponibles pour la logique de justification. De plus, il existe une possibilité qui n'a pas d'analogue pour la logique modale: on pourrait quantifier sur les justifications elles-mêmes.

Les premiers résultats concernant la possibilité d'une logique de justification quantifiée étaient notablement défavorables. La sémantique de la prouvabilité arithmétique pour Logic of Proofs LP, se généralise naturellement à une version de premier ordre avec des quantificateurs conventionnels, et à une version avec des quantificateurs sur les preuves. Dans les deux cas, les questions d'axiomatisabilité ont reçu une réponse négative.

Théorème 6: La logique du premier ordre des preuves n'est pas récursivement énumérable (Artemov et Yavorskaya (Sidon) 2001). La logique des preuves avec quantificateurs sur les preuves n'est pas récursivement énumérable (Yavorsky 2001).

Bien qu'une sémantique arithmétique ne soit pas possible, dans (Fitting 2008) une sémantique mondiale possible, et une théorie de la preuve axiomatique, a été donnée pour une version de LP avec des quantificateurs allant sur les justifications. La solidité et l'exhaustivité ont été prouvées. À ce stade, la sémantique mondiale possible se sépare de la sémantique arithmétique, qui peut ou non être une cause d'alarme. Il a également été montré que S4 s'intègre dans la logique quantifiée en traduisant □ Z par «il existe une justification x telle que x: Z * », où Z * est la traduction de Z. Bien que cette logique soit quelque peu compliquée, elle a trouvé des applications, par exemple, dans (Dean et Kurokawa 2009b), elle est utilisée pour analyser le paradoxe du connaisseur, bien que des objections aient été soulevées contre cette analyse dans (Arlo-Costa et Kishida 2009).

Des travaux ont également été réalisés sur des versions de Justification Logic avec des quantificateurs sur des objets, avec et sans un analogue de la formule de Barcan. Rien de tout cela n'a été publié et devrait être considéré comme toujours en cours.

9. Notes historiques

Le système de logique de justification initial, la logique des preuves LP, a été introduit en 1995 dans (Artemov 1995) (cf. également (Artemov 2001)) où des propriétés de base telles que l'internalisation, la réalisation, l'exhaustivité arithmétique, ont été établies pour la première fois. LP a offert une sémantique de prouvabilité prévue pour la logique de prouvabilité de Gödel S4, fournissant ainsi une formalisation de la sémantique de Brouwer-Heyting-Kolmogorov pour la logique propositionnelle intuitionniste. La sémantique et l'exhaustivité épistémiques (Fitting 2005) ont d'abord été établies pour LP. Les modèles symboliques et la décidabilité pour LP sont dus à Mkrtychev (Mkrtychev 1997). Les estimations de la complexité sont apparues pour la première fois dans (Brejnev et Kuznets 2006, Kuznets 2000, Milnikel 2007). Un aperçu complet de tous les résultats de décidabilité et de complexité peut être trouvé dans (Kuznets 2008). Systèmes J, J4,et JT ont d'abord été considérés dans (Brejnev 2001) sous des noms différents et dans un cadre légèrement différent. JT45 est apparu indépendamment dans (Pacuit 2006) et (Rubtsova 2006), et JD45 dans (Pacuit 2006). La logique des preuves à conclusion unique a été trouvée dans (Krupski 1997). Une approche plus générale des connaissances communes basée sur des connaissances justifiées a été proposée dans (Artemov 2006). La sémantique du jeu de la logique de justification et la logique épistémique dynamique avec justifications ont été étudiées dans (Renne 2008, Renne 2009). Les liens entre la logique de justification et le problème de l'omniscience logique ont été examinés dans (Artemov et Kuznets 2009, Wang 2009). Le nom Justification Logic a été introduit dans (Artemov 2008), dans lequel les exemples de Kripke, Russell et Gettier ont été officialisés; cette formalisation a été utilisée pour la résolution de paradoxes, la vérification,l'analyse des hypothèses cachées et l'élimination des redondances. Dans (Dean et Kurokawa 2009a), la logique de justification a été utilisée pour l'analyse des paradoxes de la connaissance et de la connaissance.

Bibliographie

  • Antonakos, E. (2007). «Justified and Common Knowledge: Limited Conservativity», dans S. Artemov et A. Nerode (eds.), Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, 4-7 juin 2007, Actes (Notes de cours en informatique: volume 4514), Berlin: Springer, pp. 1–11.
  • Arlo-Costa, H. et K. Kishida (2009). «Three proofs and the Knower in the Quantified Logic of Proofs», dans Formal Epistemology Workshop / FEW 2009. Actes, Université Carnegie Mellon, Pittsburgh, PA, USA.
  • Artemov, S. (1995). «Logique modale opérationnelle», rapport technique MSI 95–29, Université Cornell.
  • –––. (2001). «Prouvabilité explicite et sémantique constructive», The Bulletin of Symbolic Logic, 7 (1): 1–36.
  • –––. (2006). «Connaissance commune justifiée», Theoretical Computer Science, 357 (1–3): 4–22.
  • –––. (2008). «La logique de la justification», The Review of Symbolic Logic, 1 (4): 477–513.
  • Artemov, S. et R. Kuznets (2009). «L'omniscience logique comme problème de complexité computationnelle», dans A. Heifetz (éd.), Aspects théoriques de la rationalité et de la connaissance, Actes de la douzième conférence (TARK 2009), ACM Publishers, pp. 14–23.
  • Artemov, S. et E. Nogina (2005). «Introduire la justification dans la logique épistémique», Journal of Logic and Computation, 15 (6): 1059–1073.
  • Artemov, S. et T. Yavorskaya (Sidon) (2001). «Sur la logique du premier ordre des preuves», Moscow Mathematical Journal, 1 (4): 475–490.
  • Boolos, G. (1993). The Logic of Provability, Cambridge: Cambridge University Press.
  • Brejnev, V. (2001). «Sur la logique des preuves», dans K. Striegnitz (éd.), Actes de la sixième session étudiante ESSLLI, 13e université européenne d'été en logique, langage et information (ESSLLI'01), pp. 35–46.
  • Brejnev, V. et R. Kuznets (2006). «Rendre la connaissance explicite: combien c'est difficile», Theoretical Computer Science, 357 (1–3): 23–34.
  • Cubitt, RP et R. Sugden (2003). «Connaissances communes, saillance et convention: une reconstruction de la théorie des jeux de David Lewis», Economics and Philosophy, 19: 175–210.
  • Dean, W. et H. Kurokawa (2009a). «Du paradoxe de la connaissance à l'existence des preuves», Synthese, 176 (2): 177-225.
  • –––. (2009b). «La connaissance, la preuve et le connaisseur», dans A. Heifetz (éd.), Aspects théoriques de la rationalité et de la connaissance, Actes de la douzième conférence (TARK 2009), ACM Publications, pp. 81–90.
  • Dretske, F. (2005). «La connaissance est-elle fermée sous un engagement connu? The Case against Closure », dans M. Steup et E. Sosa (éd.), Contemporary Debates in Epistemology, Oxford: Blackwell, pp. 13–26.
  • Fagin, R., J. Halpern, Y. Moses et M. Vardi (1995). Raisonnement sur la connaissance, Cambridge, MA: MIT Press.
  • Montage, M. (2005). «La logique des preuves, sémantiquement», Annals of Pure and Applied Logic, 132 (1): 1–25.
  • –––. (2006). «Un théorème de remplacement pour LP », Rapport technique TR-2006002, Département d'informatique, Université de la ville de New York.
  • –––. (2008). «Une logique quantifiée de preuves», Annals of Pure and Applied Logic, 152 (1–3): 67–83.
  • –––. (2009). «Réalisations et LP », Annals of Pure and Applied Logic, 161 (3): 368–387.
  • Gettier, E. (1963). «La vraie croyance justifiée est-elle une connaissance? Analysis, 23: 121–123.
  • Girard, J.-Y., P. Taylor et Y. Lafont (1989). Preuves et types (Cambridge Tracts in Computer Science: Volume 7), Cambridge: Cambridge University Press.
  • Gödel, K. (1933). «Interprétation Eine des intuitionistischen Aussagenkalkuls», Ergebnisse Math. Kolloq., 4: 39–40. Traduction anglaise dans: S. Feferman et al. (eds.), Kurt Gödel Collected Works (Volume 1), Oxford et New York: Oxford University Press et Clarendon Press, 1986, pp. 301-303.
  • –––. (1938). «Vortrag bei Zilsel / Lecture at Zilsel's» (* 1938a), in S. Feferman, JJ Dawson, W. Goldfarb, C. Parsons et R. Solovay (eds.), Essais et conférences non publiés (Kurt Gödel Collected Works: Volume III), Oxford: Oxford University Press, 1995, pp. 86-113.
  • Goldman, A. (1967). «Une théorie causale du sens», The Journal of Philosophy, 64: 335-372.
  • Goodman, N. (1970). «Une théorie des constructions équivaut à l'arithmétique», dans J. Myhill, A. Kino et R. Vesley (éds.), Intuitionism and Proof Theory, Amsterdam: North-Holland, pp. 101-120.
  • Goris, E. (2007). «Les preuves explicites dans la logique formelle de la prouvabilité», dans S. Artemov et A. Nerode (éd.), Logical Foundations of Computer Science, Symposium international, LFCS 2007, New York, NY, États-Unis, 4-7 juin 2007, Actes (ecture Notes in Computer Science: Volume 4514), Berlin: Springer, pp. 241–253.
  • Hendricks, V. (2005). Épistémologie grand public et formelle, New York: Cambridge University Press.
  • Heyting, A. (1934). Mathematische Grundlagenforschung. Intuitionnisme. Beweistheorie, Berlin: Springer.
  • Hintikka, J. (1962). Connaissance et croyance, Ithaque: Cornell University Press.
  • Kleene, S. (1945). «Sur l'interprétation de la théorie intuitionniste des nombres», The Journal of Symbolic Logic, 10 (4): 109-124.
  • Kolmogorov, A. (1932). «Zur Deutung der Intuitionistischen Logik», Mathematische Zeitschrift, 35: 58–65. Traduction en anglais dans VM Tikhomirov (ed.), Sélection d'ouvrages d'AN Kolmogorov. Volume I: Mathématiques et mécanique, Dordrecht: Kluwer, 1991, pp. 151–158.
  • Kreisel, G. (1962). «Fondements de la logique intuitionniste», dans E. Nagel, P. Suppes et A. Tarski (éd.), Logic, Methodology and Philosophy of Science. Actes du Congrès international de 1960, Stanford: Stanford University Press, pp. 198-210.
  • –––. (1965). «Mathematical logic», dans T. Saaty (ed.), Lectures in Modern Mathematics III, New York: Wiley and Sons, pp. 95–195.
  • Krupski, V. (1997). «Logique opérationnelle des preuves avec condition de fonctionnalité sur prédicat de preuve», dans S. Adian et A. Nerode (éds.), Logical Foundations of Computer Science, 4e Symposium international, LFCS'97, Yaroslavl, Russie, 6-12 juillet 1997, Actes (Notes de cours en informatique: volume 1234), Berlin: Springer, pp. 167–177.
  • Kurokawa, H. (2009). «Tableaux and Hypersequents for Justification Logic», dans S. Artemov et A. Nerode (eds.), Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, 3–6 janvier 2009, Actes (Notes de cours en informatique: volume 5407), Berlin: Springer, pp. 295–308.
  • Kuznets, R. (2000). «On the Complexity of Explicit Modal Logics», dans P. Clote et H. Schwichtenberg (éd.), Computer Science Logic, 14th International Workshop, CSL 2000, Annual Conference of the EACSL, Fischbachau, Allemagne, 21-26 août 2000, Proceedings (Notes de cours en informatique: Volume 1862), Berlin: Springer, pp. 371–383.
  • –––. (2008). Complexity Issues in Justification Logic, thèse de doctorat, Département d'informatique, City University of New York Graduate Center.
  • –––. (2010). «Une note sur l'anomalie des réalisations de S4LP », dans K. Brünnler et T. Studer (eds.), Proof, Computation, Complexity PCC 2010, International Workshop, Proceedings, IAM Technical Reports IAM-10-001, Institute of Computer Sciences et mathématiques appliquées, Université de Berne.
  • McCarthy, J., M. Sato, T. Hayashi et S. Igarishi (1978). «Sur la théorie modèle de la connaissance», rapport technique STAN-CS-78-667, Département d'informatique, Université de Stanford.
  • Milnikel, R. (2007). «La dérivabilité dans certains sous-systèmes de la logique des preuves est Π 2 p - complète», Annals of Pure and Applied Logic, 145 (3): 223-239.
  • –––. (2009). «Conservativity for Logics of Justified Belief», dans S. Artemov et A. Nerode (eds.), Logical Foundations of Computer Science, International Symposium, LFCS 2009, Deerfield Beach, FL, USA, 3–6 janvier 2009, Actes (Notes de cours en informatique: volume 5407), Berlin: Springer, pp. 354–364.
  • Mkrtychev, A. (1997). «Models for the Logic of Proofs», in S. Adian et A. Nerode (dir.), Logical Foundations of Computer Science, 4e Symposium international, LFCS'97, Yaroslavl, Russie, 6-12 juillet 1997, Actes (Conférence Notes in Computer Science: Volume 1234), Berlin: Springer, pp. 266-275.
  • Nogina, E. (2006). «Sur la logique des preuves et de la prouvabilité», en 2005 Réunion d'été de l'Association pour la logique symbolique, Logic Colloquium'05, Athènes, Grèce (28 juillet - 3 août 2005), The Bulletin of Symbolic Logic, 12 (2): 356.
  • –––. (2007). «Complétude épistémique de la GLA », lors de la réunion annuelle 2007 de l'Association for Symbolic Logic, Université de Floride, Gainesville, Floride (10-13 mars 2007), The Bulletin of Symbolic Logic, 13 (3): 407.
  • Pacuit, E. (2006). «A Note on Some Explicit Modal Logics», rapport technique PP – 2006–29, Institut de logique, de langage et de calcul, Université d'Amsterdam.
  • Plaza, J. (2007). «Logiques des communications publiques», Synthèse, 158 (2): 165–179.
  • Renne, B. (2008). Logique épistémique dynamique avec justification, thèse de doctorat, département d'informatique, CUNY Graduate Center, New York, NY, États-Unis.
  • –––. (2009). «Evidence Elimination in Multi-Agent Justification Logic», dans A. Heifetz (ed.), Theoretical Aspects of Rationality and Knowledge, Actes de la douzième conférence (TARK 2009), ACM Publications, pp. 227-236.
  • Rose, G. (1953). «Calcul propositionnel et réalisabilité», Transactions de l'American Mathematical Society, 75: 1–19.
  • Rubtsova, N. (2006). «Sur la réalisation de la modalité S5 par des termes de preuve», Journal of Logic and Computation, 16 (5): 671–684.
  • Russell, B. (1912). Les problèmes de la philosophie, Oxford: Oxford University Press.
  • Sidon, T. (1997). «Logique de la prouvabilité avec opérations sur les preuves», dans S. Adian et A. Nerode (eds.), Logical Foundations of Computer Science, 4th International Symposium, LFCS'97, Yaroslavl, Russie, 6-12 juillet 1997, Actes (Conférence Notes in Computer Science: Volume 1234), Berlin: Springer, pp. 342–353.
  • Troelstra, A. (1998). «Realizability», dans S. Buss (éd.), Handbook of Proof Theory, Amsterdam: Elsevier, pp. 407–474.
  • Troelstra, A. et H. Schwichtenberg (1996). Théorie de base de la preuve, Amsterdam: Cambridge University Press.
  • Troelstra, A. et D. van Dalen (1988). Constructivisme en mathématiques (Volumes 1, 2), Amsterdam: Hollande du Nord.
  • van Dalen, D. (1986). «Logique intuitionniste», dans D. Gabbay et F. Guenther (éd.), Handbook of Philosophical Logic (Volume 3), Bordrecht: Reidel, pp. 225–340.
  • van Ditmarsch, H., W. van der Hoek et B. Kooi (éd.), (2007). Dynamic Epistemic Logic (Synthese Library, Volume 337), Berlin: Springer.
  • von Wright, G. (1951). Un essai en logique modale, Amsterdam: Hollande du Nord.
  • Wang, R.-J. (2009). «Knowledge, Time, and Logical Omniscience», in H. Ono, M. Kanazawa, and R. de Queiroz (eds.), Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japon, 21 juin -24, 2009, Actes (Notes de cours sur l'intelligence artificielle: volume 5514), Berlin: Springer, pp. 394–407.
  • Yavorskaya (Sidon), T. (2001). «Logique des preuves et prouvabilité», Annals of Pure and Applied Logic, 113 (1–3): 345–372.
  • –––. (2008). «Interacting Explicit Evidence Systems», Théorie des systèmes informatiques, 43 (2): 272-293.
  • Yavorsky, R. (2001). «Logiques de prouvabilité avec quantificateurs sur preuves», Annals of Pure and Applied Logic, 113 (1–3): 373–387.

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 ce sujet d'entrée au Indiana Philosophy Ontology Project (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

Recommandé: