Quelle est la différence entre les propositions et les jugements?

27

Je suis confus par la subtile différence entre les propositions et les jugements lorsqu'ils sont exposés à la théorie du type intuitionniste. Quelqu'un peut-il m'expliquer à quoi bon les distinguer et qu'est-ce qui les distingue? Surtout au vu de l'isomorphe de Curry-Howard.

journée
la source
Vous pouvez être intéressé à lire en.wikipedia.org/wiki/…
Anthony

Réponses:

17

Tout d'abord, vous devez savoir qu'en général, il n'y a pas de consensus sur ces termes et que leurs définitions dépendent du système dans lequel on travaille.Puisque vous avez posé des questions sur la théorie du type intuitionniste, je citerai Pfenning:

Un jugement est quelque chose que nous pouvons savoir, c'est-à-dire un objet de connaissance. Un jugement est évident si nous le savons.

Les propositions, en revanche, selon Martin-Löf, sont des ensembles de preuves. Dans cette interprétation, si l'ensemble des preuves d'une proposition est vide, il est faux et sinon vrai.

Une proposition est interprétée comme un ensemble dont les éléments représentent les preuves de la proposition

dit Nordström et al. En revanche, dans la logique classique et en général, les propositions sont des objets exprimés dans un langage qui peut être "vrai" ou "faux".

Pour vous donner une intuition supplémentaire; de mon point de vue, les jugements sont métalogiques et les propositions logiques.

Je suggère "Logique constructive" par Frank Pfenning , "Preuves et types" par Jean-Yves Girard et "Programmation dans la théorie des types de Martin-Löf" par Bengt Nordström et al. Les trois sont disponibles gratuitement sur Internet. Le dernier est probablement le plus proche de ce que vous voulez car il est orienté vers la programmation et va dans le détail, en détail, sur la signification de ces termes et bien d'autres.

Anthony
la source
2
Cette première citation est Frank Pfenning, pas Girard.
Noam Zeilberger
Une question: est-il correct d'affirmer que (sous la proposition comme paradigme de type) les propositions sont des types tandis que les jugements sont des séquences / expression de la théorie des types (du cadre logique)?
Giorgio Mossa
1
Comment savons-nous que nous savons quelque chose? (En ce qui concerne "Un jugement est évident si nous le savons en fait"?)
CMCDragonkai
16

Je peux peut-être essayer de donner une réponse moins métaphysique.

Il y a une langue, une langue logique, que nous étudions. Dans ce langage, il y a des choses appelées «propositions» qui sont censées être des choses vraies ou fausses.

Il y a un méta-langage, qui est aussi un langage logique, dans lequel nous essayons d'expliquer quelles choses dans le langage de base sont vraies ou fausses. Les déclarations que nous faisons dans ce méta-langage sont appelées "jugements".

Notez que toutes les propositions du langage de base ont le statut de données dans le méta-langage. Ils sont aussi bons que des cordes. Vous ne pouvez pas demander à une chaîne si elle est vraie ou fausse. Un jugement est l'interprète qui interprète la chaîne comme une proposition et décide si elle est vraie ou fausse.

Uday Reddy
la source
14

J'essaierai d'être bref là où les autres réponses étaient plus exhaustives. Il y a une différence entre un morceau de texte disant "Le majordome l'a fait". , et Mme Marple proclamant "Le majordome l'a fait." Dans le deuxième cas, le majordome pourrait perdre sa liberté.

Andrej Bauer
la source
1
J'aime généralement vos réponses Andrej, mais dans ce cas, je ne suis pas. Pourquoi le support d'une déclaration importerait-il? Ou est-ce la différence entre les verbes «dire» et «proclamer». Dans ce cas, comment savons-nous que le texte ne proclame pas et que Mme Marple ne le dit pas? La seule autre différence que je vois est que le texte est passif, tandis que Mme Marple est active; mais, quelqu'un a écrit le texte, non?
Anthony
6
Le fait que nous puissions formuler la phrase "Le majordome l'a fait" ne veut rien dire. Le fait qu'il existe sur un morceau de papier ne veut rien dire. Mais quand Mme Marple fait le jugement "Le majordome l'a fait" devant tout le monde réuni dans une belle salle de lecture victorienne, c'est une chose entièrement différente. J'étais peut-être trop énigmatique.
Andrej Bauer
@Andrej Bauer: Je dois m'excuser d'avoir voté contre avant, maintenant je vois le point. Merci beaucoup.
jour
12

Dans les théories de type de Martin-Löf , les jugements font partie des actes de discours . Il y a quatre (ou cinq selon Wikipedia) jugements:

  • ( A est un type / ensemble / proposition),A TypeA
  • ( s est membre / preuve de A ),s:AsA
  • ( s et t sont des membres / preuves égaux de A ),s=t:AstA
  • ( A et B sont des types / ensembles / propositions égaux),A=BAB
  • ( Γ est un contexte bien formé).Γ ContextΓ

Pour comprendre ce que cela signifie, nous devons retourner à Frege. Le symbole de tourniquet de Frege est un acte de parole. Il affirme le contenu (qui le suit et constitue un jugement). Dans les théories de type de Martin-Löf, nous avons les quatre (cinq?) Jugements énumérés ci-dessus. Dans ces théories, les propositions ne sont que des types.

AAtAt:AtAt:A

J'ajouterais les «fondements des mathématiques constructives» de Michael Beeson aux suggestions de la réponse d'Anthony. Martin-Löf a donné plusieurs conférences qui expliquent très bien sa théorie mais malheureusement la plupart d'entre elles ne se sont pas transformées en forme publiée par lui (mais consultez ce site ).

Kaveh
la source
Merci pour l'énumération. Mais ma question est maintenant: ces jugements ne sont-ils pas trivialement transformés en propositions? par exemple, "A est un type" est un prédicat juste, quand A est instancié par, disons Nat, cela devient une proposition, n'est-ce pas?
jour
Γt:A
1
t:A(Γ)
2
@plmday, ce qui suit pourrait être utile pour expliquer pourquoi cela ne peut pas se produire du point de vue mathématique: "vous ne pouvez pas avoir un univers, traiter" p prouve A "comme une proposition, et avoir un prédicat de preuve décidable." [Beeson 1980, p. 409]. (Mais pour Martin-Löf, le principal problème est que ceux-ci sont conceptuellement différents et les confondre conduira à des fondations injustifiées qui pourraient conduire à des résultats paradoxaux.)
Kaveh
2
Je voudrais ajouter que cela me semble trop spécifique car il existe de nombreuses autres versions d'ITT avec d'autres jugements (par exemple le CoC Prop). Je pense que le concept le plus important ici est dans le deuxième commentaire de Kaveh: essayer de transformer certains jugements en propositions peut introduire des problèmes subtils et dangereux dans la théorie. Cela ne veut pas dire qu'une théorie des types ne puisse pas être décrite dans une théorie des types, mais seulement qu'il existe des lignes claires tracées entre la métathéorie, la théorie et les expressions de cette théorie.
Anthony
4

Les jugements sont la composition de deux choses:

  1. P
  2. A

A[P]

[P][P][T]H1,,HnA1,,An, où certaines logiques ont des jugements qui ne sont trivialement équivalents à aucune proposition du langage de la logique. Ainsi, différents types de propositions sont vus dans une logique classique assez élémentaire.

La théorie des types de Martin-Löf recourt à une famille de jugements plus complexe pour trois raisons: premièrement, elle est typée de manière dépendante, ce qui signifie que les propositions se produisent sous la forme d'entités syntaxiques à l'intérieur des termes. Deuxièmement, il s'est dispensé d'utiliser une grammaire pour définir quelles chaînes de symboles sont des termes et des propositions valides, mais a utilisé le système inférentiel pour le faire - une chose raisonnable à faire puisque les propositions dans de telles théories typées ne sont généralement pas dépourvues de contexte. Troisièmement, il a conçu une nouvelle théorie de l'égalité, souvent appelée égalité propositionnelle, qui exploite la théorie bêta-eta (ou dans certaines variantes, juste la théorie bêta), et les jugements selon lesquels deux termes partagent la même forme normale sont exprimés à l'aide de jugements exprimant l'équivalence bêta / eta de deux termes - encore une fois raisonnable,

Les jugements exprimant l'équivalence beta / eta peuvent être éliminés sans trop de difficulté - ont pour fondement la règle d'introduction de l'égalité propositionnelle étant que les deux termes sont équivalents beta (l'équivalence beta-eta est légèrement plus problématique) - mais en éliminant le jugement que les termes habitent les types est beaucoup plus délicat; la façon la moins mauvaise à laquelle je peux penser pour faire cela est de reconstruire l'inférence de type dans le terme grammaire, ce qui conduit à une théorie plus complexe et moins intuitive dans l'ensemble.

Charles Stewart
la source
-3

Les revendications, propositions et déclarations sont toutes les mêmes; mais un jugement est une proposition qui a été vérifiée (à tort ou à raison), approuvée ou utilisée comme conclusion. Pas besoin de formules sophistiquées comme les réponses ci-dessus semblent abuser ...

Samuel Duclos
la source
1
Vous avez tort de dire qu'un jugement a été vérifié. Un jugement vérifié (prouvé) est appelé un théorème.
Andrej Bauer