Was ist der Unterschied zwischen Aussagen und Urteilen?

27

Ich bin verwirrt über den subtilen Unterschied zwischen Aussagen und Urteilen, wenn ich der Theorie des intuitionistischen Typs ausgesetzt bin. Kann mir jemand erklären, woran es liegt, sie zu unterscheiden und was sie unterscheidet? Besonders im Hinblick auf den Curry-Howard Isomorphsim.

Tag
quelle
Es könnte Sie interessieren, en.wikipedia.org/wiki/…
Anthony

Antworten:

17

Zunächst sollten Sie wissen, dass es im Allgemeinen keinen Konsens über diese Begriffe gibt und ihre Definitionen von dem System abhängen, in dem man arbeitet. Nachdem Sie nach der Theorie des intuitionistischen Typs gefragt haben, zitiere ich Pfenning:

Ein Urteil ist etwas, das wir vielleicht wissen, das heißt ein Objekt des Wissens. Ein Urteil ist offensichtlich, wenn wir es tatsächlich wissen.

Propositionen hingegen sind nach Martin-Löf Beweismengen. Wenn in dieser Interpretation der Satz von Beweisen für einen Satz leer ist, ist er falsch und ansonsten wahr.

Ein Satz wird als eine Menge interpretiert, deren Elemente die Beweise des Satzes darstellen

sagt Nordström et al. Andererseits sind Sätze in der klassischen Logik und im Allgemeinen Objekte, die in einer Sprache ausgedrückt werden, die entweder "wahr" oder "falsch" sein kann.

Um Ihnen eine zusätzliche Intuition zu geben; aus meiner sicht sind urteile metalogisch und aussagen logisch.

Ich schlage "Konstruktive Logik" von Frank Pfenning , "Beweise und Typen" von Jean-Yves Girard und "Programmieren in Martin-Löfs Typentheorie" von Bengt Nordström et al. Alle drei sind im Internet frei verfügbar. Das letzte ist wahrscheinlich das, was Sie wollen, da es sich an der Programmierung orientiert und ausführlich auf die Bedeutung dieser und vieler weiterer Begriffe eingeht.

Anthony
quelle
2
Das erste Zitat ist Frank Pfenning, nicht Girard.
Noam Zeilberger
Eine Frage: Ist es richtig zu behaupten, dass (unter Satz als Typparadigma) Sätze Typen sind, während Urteile Folgen / Ausdrücke der (logischen Rahmen-) Typentheorie sind?
Giorgio Mossa
1
Woher wissen wir, dass wir etwas wissen? (In Bezug auf "Ein Urteil ist offensichtlich, wenn wir es tatsächlich wissen"?)
CMCDragonkai
16

Vielleicht kann ich versuchen, eine weniger metaphysische Antwort zu geben.

Es gibt eine Sprache, eine logische Sprache, die wir lernen. In dieser Sprache gibt es Dinge, die "Sätze" genannt werden und als wahr oder falsch angesehen werden.

Es gibt eine Metasprache, die auch eine logische Sprache ist, in der wir versuchen zu erklären, welche Dinge in der Basissprache wahr oder falsch sind. Die Aussagen, die wir in dieser Metasprache machen, heißen "Urteile".

Beachten Sie, dass alle Aussagen der Basissprache den Status von Daten in der Metasprache haben. Sie sind so gut wie Saiten. Sie können eine Zeichenfolge nicht danach fragen, ob sie wahr oder falsch ist. Ein Urteil ist der Interpreter, der den String als Satz interpretiert und entscheidet, ob er wahr oder falsch ist.

Uday Reddy
quelle
14

Ich werde versuchen, kurz zu fassen, wo andere Antworten erschöpfender waren. Es gibt einen Unterschied zwischen einem Text, der sagt: "Der Butler hat es getan." und Mrs. Marple verkündet: "Der Butler hat es getan." Im zweiten Fall könnte der Butler seine Freiheit verlieren.

Andrej Bauer
quelle
1
Normalerweise mag ich deine Antworten, aber in diesem Fall folge ich nicht. Warum sollte das Medium einer Aussage von Bedeutung sein? Oder ist es der Unterschied in den Verben "sagen" und "verkünden". Woher wissen wir dann, dass der Text nicht verkündet und Frau Marple nicht sagt? Der einzige andere Unterschied, den ich sehe, ist, dass der Text passiv ist, während Frau Marple aktiv ist; aber jemand hat den text geschrieben, oder?
Anthony
6
Die Tatsache, dass wir den Satz "Der Butler hat es getan" formulieren können, bedeutet nichts. Die Tatsache, dass es auf einem Blatt Papier existiert, bedeutet nichts. Aber als Frau Marple vor allen, die sich in einem schönen viktorianischen Lesesaal versammelt haben, das Urteil "Der Butler hat es getan" gefällt, ist das etwas ganz anderes. Vielleicht war ich zu kryptisch.
Andrej Bauer
@Andrej Bauer: Ich muss mich dafür entschuldigen, dass ich Sie zuvor abgewählt habe, jetzt verstehe ich den Punkt. Vielen Dank.
Tag
12

In Martin-Löfs Typentheorien sind Urteile Teil von Sprechhandlungen . Es gibt vier (oder fünf nach Wikipedia) Urteile:

  • A TypeA
  • s:AsA
  • s=t:AstA
  • A=BAB
  • Γ ContextΓ

AAtAt:AtAt:A

Ich würde Michael Beesons "Grundlagen der Konstruktiven Mathematik" zu den Vorschlägen in Anthonys Antwort hinzufügen. Martin-Löf hat mehrere Vorträge gehalten, die seine Theorie sehr gut erläutern, aber leider sind die meisten von ihnen nicht in von ihm veröffentlichte Form übergegangen (aber besuchen Sie diese Website ).

Kaveh
quelle
Danke für die Aufzählung. Aber meine Frage ist jetzt, ob diese Urteile nicht trivial in Aussagen umgewandelt werden können. Beispiel: "A ist ein Typ" ist ein einfaches Prädikat. Wenn A beispielsweise durch Nat instanziiert wird, wird es zu einem Satz, nicht wahr?
Tag
Γt:A
1
t:A(Γ)
2
@plmday, das Folgende könnte hilfreich sein, wenn es darum geht, warum dies aus mathematischer Sicht nicht möglich ist: "Sie können kein Universum haben, behandeln" p beweist A "als einen Satz und haben ein entscheidbares Beweis-Prädikat." [Beeson 1980, p. 409]. (Für Martin-Löf ist das Hauptproblem, dass diese konzeptionell unterschiedlich sind und verwirrend zu ungerechtfertigten Grundlagen führen, die zu paradoxen Ergebnissen führen können.)
Kaveh,
2
Ich möchte hinzufügen, dass dies für mich zu spezifisch erscheint, da es viele andere Versionen von ITT mit anderen Urteilen gibt (z. B. CoCs Prop). Ich denke, das wichtigere Konzept hier ist in Kavehs zweitem Kommentar: Der Versuch, einige Urteile in Aussagen umzusetzen, kann subtile und gefährliche Probleme in die Theorie einbringen. Das heißt nicht, dass eine Typentheorie nicht in einer Typentheorie beschrieben werden kann, sondern nur, dass klare Grenzen zwischen der Metatheorie, der Theorie und den Ausdrücken in dieser Theorie gezogen werden.
Anthony
4

Urteile setzen sich aus zwei Dingen zusammen:

  1. P
  2. A

A[P]

[P][P][T]H1,,HnA1,,An, wo einige Logiken solche Urteile haben, die keinem Satz der Logiksprache trivial äquivalent sind. In der ziemlich elementaren klassischen Logik werden also verschiedene Arten von Aussagen gesehen.

Die Typentheorie von Martin-Löf greift aus drei Gründen auf eine komplexere Familie von Urteilen zurück: Erstens ist sie abhängig von der Typisierung, was bedeutet, dass die Sätze als syntaktische Einheiten innerhalb von Begriffen auftreten. Zweitens verzichtete er auf eine Grammatik, um zu definieren, welche Zeichenfolgen gültige Ausdrücke und Sätze sind, verwendete jedoch das Inferenzsystem, um dies zu tun - eine vernünftige Sache, da Sätze in solchen typisierten Theorien im Allgemeinen nicht kontextfrei sind. Drittens entwickelte er eine neuartige Theorie der Gleichheit, die oft als Aussagengleichheit bezeichnet wird und die die Beta-Eta-Theorie (oder in einigen Varianten nur die Beta-Theorie) nutzt, und die Urteile, dass zwei Begriffe dieselbe Normalform haben, werden mit Urteilen ausgedrückt, die sie ausdrücken die Beta / Eta-Äquivalenz von zwei Begriffen - wieder angemessen,

Die Urteile, die die Beta / Eta-Äquivalenz ausdrücken, können ohne allzu große Schwierigkeiten beseitigt werden - als Begründung für die Einführungsregel für die Aussagengleichheit gilt, dass die beiden Begriffe Beta-Äquivalent sind (die Beta-Eta-Äquivalenz ist etwas problematischer) -, wobei das Urteil jedoch beseitigt wird Diese Begriffe bewohnen Typen ist viel schwieriger; Der am wenigsten schlechte Weg, den ich mir dabei vorstellen kann, ist die Rekonstruktion der Typinferenz im Begriff Grammatik, was insgesamt zu einer komplexeren und weniger intuitiven Theorie führt.

Charles Stewart
quelle
-3

Ansprüche, Vorschläge und Aussagen sind alle gleich; Ein Urteil ist jedoch ein Satz, der bestätigt (ob richtig oder falsch), gebilligt oder als Schlussfolgerung verwendet wurde. Keine Notwendigkeit für ausgefallene Formeln wie die Antworten oben scheinen zu missbrauchen ...

Samuel Duclos
quelle
1
Sie sagen zu Unrecht, dass ein Urteil bestätigt wurde. Ein verifiziertes (bewiesenes) Urteil wird Theorem genannt.
Andrej Bauer