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

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.

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.

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.

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ść.

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

• $A \ \mathsf{Type}$ ( jest typem / zestawem / propozycją),$A$
• $s : A$ ( jest członkiem / dowodem ),$s$$A$
• $s=t : A$ ( i są równymi członami / dowodami ),$s$$t$$A$
• $A=B$ ( i są równymi typami / zestawami / propozycjami),$A$$B$
• $\Gamma \ \mathsf{Context}$ ( to dobrze sformułowany kontekst).$\Gamma$

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.$\vdash$

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 .$A$$A$$t$$A$$t : A$$t$$A$$\vdash t: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ą ).

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

1. Twierdzenie ; i$P$
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;$\cal A$

podając podstawową formę . Bardziej złożone składnie są możliwe, jeśli pozwolimy na wielorakie sądy zdań.${\cal 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 n ⊢ A 1 , … , A $[P]$$[P]$$[T]$$H_1, \dots, H_n \vdash A_1, \dots, A_n$

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.

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ć ...