Jaka jest różnica między twierdzeniami a osądami?

27

Jestem zdezorientowany subtelną różnicą między twierdzeniami a osądami, gdy jestem narażony na intuicyjną teorię typów. Czy ktoś może mi wyjaśnić, po co je rozróżniać, a co je wyróżnia? Zwłaszcza w świetle curry-Howarda Isomorphsima.

dzień
źródło
Być może zainteresuje Cię przeczytanie en.wikipedia.org/wiki/…
Anthony

Odpowiedzi:

17

Po pierwsze, powinieneś wiedzieć, że generalnie nie ma zgody co do tych terminów, a ich definicje zależą od systemu, w którym działa. Ponieważ zapytałeś o intuicyjną teorię typów, zacytuję Pfenninga:

Osąd jest czymś, co możemy znać, to znaczy przedmiotem wiedzy. Wyrok jest oczywisty, jeśli faktycznie go znamy.

Z drugiej strony, zdaniem Martina-Löfa, są to dowody. W tej interpretacji, jeśli zestaw dowodów dla zdania jest pusty, to jest on fałszywy i poza tym prawdziwy.

Zdanie jest interpretowane jako zbiór, którego elementy reprezentują dowody zdania

mówi Nordström i in. Z drugiej strony, w logice klasycznej i ogólnie, zdania są przedmiotami wyrażonymi w języku, który może być „prawdziwy” lub „fałszywy”.

Aby dać ci dodatkową intuicję; z mojego punktu widzenia sądy są metalogiczne, a zdania logiczne.

Proponuję „Konstruktywną logikę” Franka Pfenninga , „Dowody i typy” Jean-Yvesa Girarda oraz „Programowanie w teorii typów Martina-Löfa” Bengta Nordströma i in. Wszystkie trzy są bezpłatnie dostępne w Internecie. Ten ostatni jest prawdopodobnie najbliższy temu, czego chcesz, ponieważ jest zorientowany na programowanie i szczegółowo opisuje szczegółowo te terminy i wiele innych.

Anthony
źródło
2
Ten pierwszy cytat to Frank Pfenning, a nie Girard.
Noam Zeilberger,
Jedno pytanie: czy słuszne jest stwierdzenie, że (niedopuszczalne jako paradygmat typu) twierdzenia są typami, a osądy są sekwencjami / wyrażeniami teorii typów (ramy logiczne)?
Giorgio Mossa
1
Skąd wiemy, że coś wiemy? (W odniesieniu do „Wyrok jest oczywisty, jeśli w rzeczywistości go znamy”?)
CMCDragonkai
16

Być może mogę spróbować dać mniej metafizyczną odpowiedź.

Jest język, język logiczny, którego się uczymy. W tym języku istnieją rzeczy zwane „twierdzeniami”, które mają być prawdą lub fałszem.

Istnieje metajęzyk, który jest także językiem logicznym, w którym próbujemy wyjaśnić, które rzeczy w języku podstawowym są prawdziwe, czy fałszywe. Oświadczenia, które wypowiadamy w tym meta-języku, nazywane są „osądami”.

Zauważ, że wszystkie propozycje języka podstawowego mają status danych w metajęzyku. Są tak dobre jak struny. Nie możesz zapytać o ciąg znaków, czy jest to prawda czy fałsz. Wyrok jest interpretatorem, który interpretuje ciąg jako propozycję i decyduje, czy jest on prawdziwy, czy fałszywy.

Uday Reddy
źródło
14

Postaram się streścić tam, gdzie inne odpowiedzi były bardziej wyczerpujące. Istnieje różnica między fragmentem tekstu z napisem „Lokaj to zrobił”. , a pani Marple głosi „Lokaj to zrobił”. W drugim przypadku lokaj może stracić wolność.

Andrej Bauer
źródło
1
Zwykle lubię twoje odpowiedzi Andrej, ale w tym przypadku nie podążam. Dlaczego środek wypowiedzi miałby mieć znaczenie? Czy jest to różnica w czasownikach „mówienie” i „głoszenie”. W takim razie, skąd wiemy, że tekst nie głosi, a pani Marple nie mówi? Jedyną inną różnicą, którą widzę, jest to, że tekst jest pasywny, podczas gdy pani Marple jest aktywna; ale ktoś napisał tekst, prawda?
Anthony
6
Fakt, że możemy sformułować zdanie „Lokaj to zrobił”, nic nie znaczy. Fakt, że istnieje na kartce papieru, nic nie znaczy. Ale kiedy pani Marple wydaje osąd „Lokaj to zrobił” przed wszystkimi zgromadzonymi w ładnej wiktoriańskiej czytelni, to zupełnie inna sprawa. Być może byłem zbyt tajemniczy.
Andrej Bauer,
@Andrej Bauer: Muszę przeprosić za wcześniejsze głosowanie, teraz rozumiem o co chodzi. Wielkie dzięki.
dzień
12

W typach teorii Martina-Löfa sądy są częścią aktów mowy . Istnieją cztery (lub pięć według Wikipedii) wyroki:

  • A Type ( jest typem / zestawem / propozycją),A
  • s:A ( jest członkiem / dowodem ),sA
  • s=t:A ( i są równymi członami / dowodami ),stA
  • A=B ( i są równymi typami / zestawami / propozycjami),AB
  • Γ Context ( to dobrze sformułowany kontekst).Γ

Aby zrozumieć, co to oznacza, musimy wrócić do Frege. Symbol bramki jest mową. To potwierdza się treść (co wynika i jest to orzeczenie). W typach teorii Martina-Löfa mamy cztery (pięć?) Wyroki wymienione powyżej. W tych teoriach zdania są tylko typami.

Załóżmy, że jest propozycją. Zatem jest typem. Załóżmy, że jest określenie typu . Zatem jest osądem (możesz myśleć o tym jako o jest dowodzie ). Teraz możemy stwierdzić, że jest to przypadek, w którym to przypadku używamy .AAtAt:AtAt:A

Do sugestii w odpowiedzi Anthony'ego dodałbym „Podstawy matematyki konstrukcyjnej” Michaela Beesona. Martin-Löf wygłosił kilka przemówień, które bardzo ładnie wyjaśniają jego teorię, ale niestety większość z nich nie zmieniła się w opublikowaną przez niego formę (ale sprawdź tę stronę internetową ).

Kaveh
źródło
Dzięki za wyliczenie. Ale moje pytanie brzmi teraz: czy te wyroki nie są trywialnie przekształcane w zdania? np. „A jest typem” jest sprawiedliwym predykatem, kiedy A jest tworzone przez, powiedzmy, Nat, staje się propozycją, prawda?
dzień
Powiedziałbym, że jest osądem. Γt:A
Dave Clarke
1
@Dave, śledziłem tutaj relację Beesona z 1980 roku, ale masz rację do pewnego stopnia (chociaż Per wydaje się preferować do sądów warunkowych, historycznie zapisany zapis jest powszechnym nadużyciem, nie powinno cokolwiek na lewo od bramki. t:A(Γ)
Kaveh
2
@plmday, poniższe informacje mogą być pomocne, dlaczego nie może się to zdarzyć z matematycznego punktu widzenia: „nie możesz mieć wszechświata, traktuj„ p dowodzi, że A ”jako propozycję i mieć rozstrzygający dowód-predykat”. [Beeson 1980, s. 1 409]. (Ale dla Martina-Löfa głównym problemem jest to, że są one koncepcyjnie różne, a ich pomieszanie doprowadzi do nieuzasadnionych podstaw, co może prowadzić do paradoksalnych rezultatów.)
Kaveh
2
Chciałbym dodać, że wydaje mi się to zbyt specyficzne, ponieważ istnieje wiele innych wersji ITT z innymi osądami (np. Prop CoC). Myślę, że ważniejsza jest tutaj druga uwaga Kaveha: próba przekształcenia niektórych sądów w zdania może wprowadzić do teorii subtelne i niebezpieczne problemy. Nie oznacza to, że teorii typów nie można opisać w teorii typów, lecz jedynie wyraźne linie między metateheorią, teorią i wyrażeniami w tej teorii.
Anthony
4

Wyroki składają się z dwóch rzeczy:

  1. Twierdzenie ; iP
  2. Zdaniowej postawa - to jest to, co filozofowie nazywają, cf. raporty o postawie propozycyjnej, które wiążą postawy propozycyjne z aktami, o których mówi Kaveh;A

podając podstawową formę . Bardziej złożone składnie są możliwe, jeśli pozwolimy na wielorakie sądy zdań.A[P]

Zwykłe sformułowania logiki pierwszego rzędu wymagają tylko jednego zdania zdaniowego, którym jest zwykle albo „ jest twierdzeniem”, albo osąd binarny „ jest konsekwencją ”. W dwustronnym rachunku sekwencyjnym mamy bardziej złożoną teorię osądów, najczęściej , gdzie niektóre logiki mają takie osądy, które nie są w sposób trywialny równoważne żadnej propozycji język logiki. Różne rodzaje zdań są widziane w dość elementarnej logice klasycznej.[ P ] [ T ] H 1 , , H nA 1 , , A n[P][P][T]H1,,HnA1,,An

Teoria typów Martina-Löfa odwołuje się do bardziej złożonej rodziny osądów z trzech powodów: Po pierwsze, jest ona typowo zależna, co oznacza, że ​​zdania występują jako byty składniowe wewnątrz terminów. Po drugie, zrezygnował z gramatyki, aby zdefiniować, które ciągi symboli są prawidłowymi terminami i zdaniami, ale użył do tego systemu wnioskowania - rozsądne, aby to zrobić, ponieważ zdania w takich typach teorii na ogół nie są pozbawione kontekstu. Po trzecie, opracował nową teorię równości, często zwaną równością zdań, która wykorzystuje teorię beta-eta (lub w niektórych wariantach tylko teorię beta), a osądy, że dwa terminy mają tę samą normalną formę, są wyrażane przy użyciu wyrażeń równoważność dwóch terminów beta / eta - znowu rozsądna,

Osądy wyrażające równoważność beta / eta można wyeliminować bez większych trudności - mają podstawę do wprowadzenia zasady równości zdań, ponieważ oba terminy są równoważne beta (równoważność beta-eta jest nieco bardziej problematyczna) - ale eliminacja wyroku że warunki zamieszkiwania typów są znacznie trudniejsze; najmniejszym złym sposobem na zrobienie tego jest zrekonstruowanie wnioskowania typu w gramatyce, co prowadzi do bardziej złożonej i mniej intuicyjnej ogólnej teorii.

Charles Stewart
źródło
-3

Roszczenia, propozycje i oświadczenia są takie same; ale dzierżawa to propozycja, która została zweryfikowana (poprawna lub zła), zatwierdzona lub wykorzystana jako wniosek. Nie potrzeba wymyślnych formuł, takich jak powyższe odpowiedzi, wydają się nadużywać ...

Samuel Duclos
źródło
1
Mylisz się twierdząc, że wyrok został zweryfikowany. Sprawdzony (udowodniony) wyrok nazywa się twierdzeniem.
Andrej Bauer,