Metalogiczny - Metalogic

Metalogic jest badanie metateorii z logiką . Podczas gdy logika bada, w jaki sposób systemy logiczne mogą być używane do konstruowania ważnych i solidnych argumentów , metalogika bada właściwości systemów logicznych. Logika dotyczy prawd, które można wyprowadzić za pomocą systemu logicznego; Metalogic dotyczy prawd, które mogą być uzyskane informacje o języku i systemów, które są używane do wyrażania prawdy.

Podstawowymi przedmiotami badań metalologicznych są języki formalne, systemy formalne i ich interpretacje . Badanie interpretacji systemów formalnych to dział logiki matematycznej , znany jako teoria modeli , a badanie systemów dedukcyjnych to dział znany jako teoria dowodu .

Przegląd

Język formalny

Formalny język jest zorganizowanym zbiorem symboli , symbole, które precyzyjnie określają ją kształcie i miejscu. Taki język można zatem zdefiniować bez odniesienia do znaczeń jego wyrażeń; może istnieć, zanim zostanie mu przypisana jakakolwiek interpretacja, to znaczy zanim nabierze znaczenia. Logika pierwszego rzędu jest wyrażona w jakimś języku formalnym. Gramatyka formalna określa, które symbole i zbiory symboli są formułami w języku formalnym.

Język formalny można formalnie zdefiniować jako zbiór A ciągów (ciągów skończonych) na ustalonym alfabecie α. Niektórzy autorzy, w tym Rudolf Carnap , definiują język jako uporządkowaną parę <α, A >. Carnap wymaga również, aby każdy element α występował w co najmniej jednym ciągu w A .

Zasady formacji

Reguły formacji (zwane również gramatykami formalnymi ) to dokładny opis dobrze sformułowanych formuł języka formalnego. Są synonimem zestawu z ciągów nad alfabetem formalnego języka, który stanowi dobrze formuł. Nie opisuje jednak ich semantyki (tj. ich znaczenia).

Systemy formalne

System formalny (zwany także rachunkiem logicznym lub systemem logicznym ) składa się z języka formalnego wraz z aparatem dedukcyjnym (zwanym również systemem dedukcyjnym ). Aparat dedukcyjny może składać się ze zbioru reguł transformacji (zwanych również regułami wnioskowania ) lub zbioru aksjomatów , lub mieć oba. System formalny służy do wyprowadzania jednego wyrażenia z jednego lub więcej innych wyrażeń.

System formalny można formalnie zdefiniować jako uporządkowaną trójkę <α, , d>, gdzie d jest relacją bezpośredniej wyprowadzalności. Relacja ta jest rozumiana w sposób kompleksowy sensie takim, że prymitywne zdania formalnego systemu są traktowane jako bezpośrednio wyprowadzić z pustym zbiorem zdań. Bezpośrednia wyprowadzalność to relacja między zdaniem a skończonym, być może pustym zbiorem zdań. Aksjomaty są tak dobrane, że każdy element członkowski pierwszego miejsca d jest członkiem, a każdy element drugiego miejsca jest skończonym podzbiorem . ${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {I}}}$

System formalny można również zdefiniować tylko za pomocą relacji d. Tym samym można pominąć i α w definicjach interpretowanego języka formalnego oraz interpretowanego systemu formalnego . Jednak ta metoda może być trudniejsza do zrozumienia i użycia. ${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {I}}}$

Dowody formalne

Formalny dowód to ciąg formuł z formalnego języka, z których ostatni jest twierdzenie formalnego systemu. Twierdzenie jest syntaktyczną konsekwencją wszystkich dobrze uformowanych formuł, które je poprzedzają w systemie dowodowym. Aby prawidłowo uformowana formuła kwalifikowała się jako część dowodu, musi to wynikać z zastosowania reguły aparatu dedukcyjnego jakiegoś systemu formalnego do poprzednich dobrze uformowanych formuł w ciągu dowodowym.

Interpretacje

Interpretacja formalnego systemu jest przyporządkowanie znaczeń symboli i prawdy wartościach do zdań w systemie formalnym. Badanie interpretacji nazywa się Semantyką formalną . Nadanie interpretacji jest równoznaczne z konstruowaniem modelu .

Ważne wyróżnienia

Metajęzyk–język przedmiotowy

W metalogice języki formalne są czasami nazywane językami przedmiotowymi . Język używany do wypowiadania się na temat języka obiektowego nazywa się metajęzykiem . To rozróżnienie jest kluczową różnicą między logiką a metalogiką. Podczas gdy logika zajmuje się dowodami w systemie formalnym , wyrażonymi w jakimś języku formalnym, metalogika zajmuje się dowodami dotyczącymi systemu formalnego, które są wyrażone w metajęzyku o jakimś języku przedmiotowym.

Składnia–semantyka

W metalogice „składnia” dotyczy języków formalnych lub systemów formalnych bez względu na ich interpretację, podczas gdy „semantyka” dotyczy interpretacji języków formalnych. Termin „syntaktyka” ma nieco szerszy zakres niż „dowód teoretyczny”, ponieważ może być stosowany zarówno do własności języków formalnych bez żadnych systemów dedukcyjnych, jak i do systemów formalnych. „Semantyczny” jest synonimem „teorii modeli”.

Użyj-wzmianka

W metalogice słowa „użycie” i „wzmianka”, zarówno w formie rzeczownika, jak i czasownika, nabierają znaczenia technicznego w celu zidentyfikowania ważnego rozróżnienia. Rozróżnienie use-wzmianka (czasem określane jako słowa-as-słowy wyróżnieniem ) jest rozróżnienie między użyciem słowo (lub wyrażenie) i wymienić ją. Zwykle wskazuje się, że wyrażenie jest wymieniane, a nie używane, umieszczając je w cudzysłowie, drukując kursywą lub umieszczając samo wyrażenie w wierszu. Zamknięcie wyrażenia w cudzysłowie daje nam nazwę wyrażenia, na przykład:

„Metalogika” to nazwa tego artykułu.

Ten artykuł dotyczy metalogiki.

Typ-token

Typu Token rozróżnienie to rozróżnienie w metalogice, który oddziela abstrakcyjne pojęcie z przedmiotów, które są szczególne przypadki koncepcji. Na przykład, zwłaszcza rower w garażu jest wyrazem tego typu rzeczy zwanej „rower”. Natomiast rower w Twoim garażu jest w określonym miejscu o określonej godzinie, co nie jest prawdą w przypadku „roweru” użytego w zdaniu: „ Rower stał się ostatnio bardziej popularny”. Rozróżnienie to służy do wyjaśnienia znaczenia symboli z języków formalnych .

Historia

Pytania metalologiczne stawiane są od czasów Arystotelesa . Jednak dopiero wraz z rozwojem języków formalnych pod koniec XIX i na początku XX wieku zaczęły rozwijać się badania nad podstawami logiki. W 1904 David Hilbert zauważył, że badając podstawy matematyki , pojęcia logiczne są z góry założone, a zatem wymagane jest jednoczesne uwzględnienie zasad metalologicznych i metamatematycznych . Dziś metalogika i metamatematyka są w dużej mierze synonimami i obie zostały w dużej mierze podporządkowane logice matematycznej w środowisku akademickim. Możliwy alternatywny, mniej matematyczny model można znaleźć w pismach Charlesa Sandersa Peirce'a i innych semiotyków .

Wyniki

Wyniki w metalogice składają się z takich rzeczy, jak dowody formalne wykazujące spójność , kompletność i rozstrzygalność poszczególnych systemów formalnych .

Główne wyniki w metalogice obejmują:

• Dowód uncountability z zestawu zasilającego z liczb naturalnych ( Cantor twierdzenie 1891)
• Twierdzenie Löwenheima-Skolema ( Leopold Löwenheim 1915 i Thoralf Skolem 1919)
• Dowód spójności logiki prawdziwościowo-funkcjonalnej zdań ( Emil Post 1920)
• Dowód semantycznej kompletności prawdziwościowo-funkcjonalnej logiki zdań ( Paul Bernays 1918), (Emil Post 1920)
• Dowód na zupełność składniową prawdziwościowo-funkcjonalnej logiki zdań (Emil Post 1920)
• Dowód rozstrzygalności prawdziwościowo-funkcjonalnej logiki zdań (Emil Post 1920)
• Dowód spójności monadycznej logiki predykatów pierwszego rzędu ( Leopold Löwenheim 1915)
• Dowód semantycznej kompletności monadycznej logiki predykatów pierwszego rzędu (Leopold Löwenheim 1915)
• Dowód rozstrzygalności monadycznej logiki predykatów pierwszego rzędu (Leopold Löwenheim 1915)
• Dowód spójności logiki predykatów pierwszego rzędu ( David Hilbert i Wilhelm Ackermann 1928)
• Dowód semantycznej zupełności logiki predykatów pierwszego rzędu ( Twierdzenie o zupełności Gödla 1930)
• Dowód twierdzenia cięcia eliminacji na rachunku następczy ( Gentzen jest Hauptsatz 1934)
• Dowód nierozstrzygalności logiki predykatów pierwszego rzędu ( Twierdzenie Churcha 1936)
• Pierwsze twierdzenie Gödla o niezupełności 1931
• Drugie twierdzenie Gödla o niezupełności 1931
• Twierdzenie Tarskiego o niedefiniowalności (Gödel i Tarski w latach 30. XX wieku)

Zobacz też

• Programowanie metalogiczne
• Metamatematyka

Bibliografia

Linki zewnętrzne

• Multimedia związane z Metalogic w Wikimedia Commons
• Dragalin, AG (2001) [1994], "Meta-logika" , Encyklopedia Matematyki , EMS Press