Logika matematyczna lub metamatematyki jest dyscypliną z matematyki wprowadzonych na koniec XIX -go wieku, który jest podany jako przedmiot badania matematyki jako języka .
Podstawowymi obiektami logiki matematycznej są formuły reprezentujące zdania matematyczne, wyprowadzenia lub formalne dowody reprezentujące rozumowanie matematyczne oraz semantykę lub modele lub interpretacje w strukturach, które nadają ogólne matematyczne „znaczenie” formułom (a czasami nawet demonstracjom ) ) jak pewne niezmienniki: np. interpretacja formuł obliczania predykatów umożliwia przypisanie im wartości prawdy .
Logika matematyczna urodził się pod koniec XIX th wieku logiki w filozoficznym znaczeniu tego słowa; jest to jedna z dróg eksplorowanych przez ówczesnych matematyków w celu rozwiązania kryzysu podstaw spowodowanego złożonością matematyki i pojawieniem się paradoksów . Jej początki wyznacza spotkanie dwóch nowych pomysłów:
Logika matematyczna oparta jest na pierwszych prób formalnego traktowania matematyki, ze względu na Leibniza i Lambert (koniec XVII th wieku - na początku XVIII th wieku). W szczególności Leibniz wprowadził dużą część nowoczesnej notacji matematycznej (stosowanie kwantyfikatorów, symbol całkowania itp.). Jednak nie można mówić o logice matematycznej do połowy XIX th -wiecznym dziele George'a Boole'a (oraz w mniejszym stopniu te z Augustus De Morgan ), który wprowadza Obliczanie prawdy gdzie kombinacje logiczne jak koniunkcji, alternatywy i implikacji, są operacjami analogicznymi do dodawania lub mnożenia liczb całkowitych, ale obejmującymi wartości logiczne fałszywe i prawdziwe (lub 0 i 1); te operacje Boole'a są definiowane za pomocą tablic prawdy .
Rachunek Boole'a przekazywał pozornie paradoksalny pomysł, który miał jednak okazać się spektakularnie owocny, że język matematyki można zdefiniować matematycznie i stać się przedmiotem badań matematyków. Nie pozwoliła jednak jeszcze na rozwiązanie podstawowych problemów. W konsekwencji wielu matematyków usiłowało rozszerzyć je na ogólne ramy rozumowania matematycznego i widzieliśmy powstawanie sformalizowanych systemów logicznych ; jeden z pierwszych należy do Fregego z przełomu XIX i XX wieku.
W 1900 r. podczas bardzo znanego wykładu na Międzynarodowym Kongresie Matematyków w Paryżu David Hilbert zaproponował listę 23 najważniejszych nierozwiązanych wówczas problemów matematycznych. Druga dotyczyła spójności arytmetyki , to znaczy wykazania za pomocą środków finitystycznych niesprzeczności aksjomatów arytmetyki.
Tego programu Hilberta przyciąga wielu logiczną pracę w pierwszej ćwierci wieku, w tym rozwój systemów aksjomaty w matematyce: te aksjomaty Peano dla arytmetyki , ci z Zermelo uzupełnione Skolema i Fraenkel dla zestawów teorii i Whiteheada and Russella rozwoju z program formalizacji matematycznej, Principia Mathematica . Jest to również okres, w którym pojawiają się podstawowe zasady teorii modeli : pojęcie modelu teorii, twierdzenie Löwenheima-Skolema .
W 1929 Kurt Gödel przedstawia w swojej rozprawie doktorskiej swoje twierdzenie o zupełności, które stwierdza powodzenie przedsięwzięcia formalizacji matematyki: każde rozumowanie matematyczne można w zasadzie sformalizować przy obliczaniu predykatów . Twierdzenie to zostało przyjęte jako znaczący postęp w kierunku rozwiązania programu Hilberta , ale rok później Gödel zademonstrował twierdzenie o niezupełności (opublikowane w 1931), które bezsprzecznie wykazało niemożność zrealizowania tego programu.
Ten negatywny wynik nie powstrzymał jednak rozwoju logiki matematycznej. W latach 30. XX wieku przyszło nowe pokolenie angielskich i amerykańskich logików, w szczególności Alonzo Churcha , Alana Turinga , Stephena Kleene , Haskella Curry'ego i Emila Posta , którzy wnieśli duży wkład w zdefiniowanie pojęcia algorytmu i rozwój teorii. złożoność algorytmiczna ( teoria obliczalności , teoria złożoności algorytmów ). Dowód teorii Hilberta również rosło z pracą Gerhard Gentzen który spowodował pierwszy pokaz względnej spójności i dlatego zainicjowanego klasyfikacja programu aksjomatyczne teorii.
Najbardziej spektakularnym efektem okresu powojennego wynika Paul Cohen , który demonstruje przy użyciu zmuszając metoda niezależności hipotezy continuum w teorii mnogości, w ten sposób rozwiązywania Hilberta 1 st problem. Ale logika matematyczna również przechodzi rewolucję z powodu pojawienia się informatyki; odkrycie korespondencji Curry-Howarda , która łączy dowody formalne z rachunkiem lambda Churcha i nadaje tym dowodom zawartość obliczeniową, uruchomi rozległy program badawczy.
Głównym zainteresowaniem logiki są jej interakcje z innymi dziedzinami matematyki i nowe metody, które do nich wnosi. Z tego punktu widzenia najważniejsze osiągnięcia pochodzą z teorii modeli, uważanej czasem za gałąź algebry, a nie logiki; teoria modeli ma zastosowanie w szczególności do teorii grup i kombinatoryki ( teoria Ramseya ).
Istnieją jednak inne bardzo produktywne interakcje: rozwój teorii mnogości jest ściśle powiązany z teorią pomiarów i doprowadził do powstania w pełni rozwiniętej dziedziny matematyki, opisowej teorii mnogości . teoria obliczalności jest jednym z fundamentów teoretycznej.
Od końca XX th century widzieliśmy teoria dowodu wiązać się z teorią kategorii iw ten sposób rozpocząć interakcję z topologii algebraicznej . Z drugiej strony, wraz z pojawieniem się logiki liniowej, utrzymuje również coraz bliższe związki z algebrą liniową , a nawet z geometrią nieprzemienną . Niedawno homotopiczna teoria typów (w) stworzyła bogate powiązanie między logiką (teorią typów) a matematyką (teorią homotopii), której widzimy tylko początki.
Formalizacja matematyki w systemach logicznych, która w szczególności stała się impulsem do prac Whiteheada i Russella, była jedną z wielkich motywacji rozwoju logiki matematycznej. Pojawienie się specjalistycznych narzędzi komputerowych, automatycznych demonstratorów , systemów eksperckich i asystentów dowodowych zainteresowało ten program nowym zainteresowaniem. W szczególności asystenci sprawdzania mają kilka zastosowań w matematyce.
Pierwszy pod koniec XX th wieku i początku XXI -go wieku dwóch dawnych przypuszczeń zostały rozwiązane za pomocą komputera do przetwarzania dużej liczby przypadkach: twierdzenie o czterech kolorach i Postulat Keplera . Wątpliwości, jakie wzbudziło to użycie komputera, umotywowały formalizację i pełną weryfikację tych demonstracji.
Z drugiej strony, programy formalizacji matematyki wykorzystujące asystentów dowodu zostały opracowane w celu stworzenia całkowicie sformalizowanego korpusu matematyki; w matematyce istnienie takiego korpusu byłoby szczególnie interesujące, aby umożliwić przetwarzanie algorytmiczne, takie jak wyszukiwanie według wzorca: znajdź wszystkie twierdzenia, które są wyprowadzone z twierdzenia o liczbach pierwszych, znajdź wszystkie twierdzenia o funkcji zeta Riemanna itp.
W latach 30. ustalono kilka ważnych wyników:
Inne ważne wnioski powstały w drugiej połowie XX -go wieku.
Logiczny system lub system dedukcji to formalny system składający się z trzech elementów. Pierwsze dwa definiują jego składnię , trzeci jego semantykę :
Główną cechą formuł i dedukcji jest to, że są one obiektami skończonymi ; ponadto każdy ze zbiorów formuł i wnioskowania jest rekurencyjny , czyli dostępny jest algorytm, który określa, czy dany obiekt jest poprawną formułą, czy poprawnym wnioskowaniem systemu. Badanie logiki z punktu widzenia formuł i wyrażeń nazywa się składnią .
W semantyka jednak ucieka kombinatorycznych poprzez wywołanie (w ogóle) do nieskończonych obiektów. Po raz pierwszy użyto go do „definiowania” prawdy. Na przykład w rachunku zdań , formuły są interpretowane np. przez elementy algebry Boole'a .
Ostrzeżenie jest tutaj na miejscu, ponieważ Kurt Gödel (za nim Alfred Tarski ) wykazał swoim twierdzeniem o niezupełności niemożność matematycznego uzasadnienia matematycznego rygoru w matematyce. Dlatego bardziej właściwe jest postrzeganie semantyki jako metafory: formuły – obiekty syntaktyczne – są projektowane w inny świat. Ta technika – zanurzanie obiektów w większy świat w celu wytłumaczenia ich – jest powszechnie stosowana w matematyce i jest skuteczna.
Jednak semantyka to nie tylko „definiowanie” prawdy. Na przykład semantyka denotacyjna jest interpretacją nie formuł, ale dedukcji, której celem jest uchwycenie ich treści obliczeniowej .
W logice klasycznej i intuicjonistycznej rozróżniamy dwa rodzaje aksjomatów : aksjomaty logiczne, które wyrażają czysto logiczne własności, takie jak ( zasada wykluczonej trzeciej , obowiązująca w logice klasycznej, ale nie w logice intuicjonistycznej) oraz aksjomaty pozalogiczne, które definiują przedmioty matematyczne; na przykład aksjomaty Peano definiują liczby całkowite arytmetyki, a aksjomaty Zermelo-Fraenkla definiują zbiory . Gdy system ma aksjomaty pozalogiczne, mówimy o teorii aksjomatycznej. Przedmiotem teorii modeli jest badanie różnych modeli tej samej teorii aksjomatycznej .
Dwa systemy dedukcji mogą być równoważne w tym sensie, że mają dokładnie te same twierdzenia. Demonstrujemy tę równoważność, dostarczając tłumaczenia dedukcji jednego w dedukcjach drugiego. Na przykład, istnieją (co najmniej) trzy typy równoważnych systemów dedukcji do obliczania predykatów : systemy w stylu Hilberta , dedukcja naturalna i rachunek sekwencyjny . Czasami dodajemy styl Fitch, który jest wariantem dedukcji naturalnej, w której dowody są prezentowane w sposób liniowy.
Podczas gdy teoria liczb demonstruje własności liczb, zwracamy uwagę na główną cechę logiki jako teorii matematycznej: „demonstruje” ona własności systemów dedukcji, w których obiekty są „twierdzeniami”. Istnieje zatem podwójny poziom, na którym nie możemy się zgubić. Dla wyjaśnienia, „twierdzenia” stwierdzające własności systemów dedukcji są czasami nazywane „ metatwierdzeniami ”. Badany przez nas system dedukcji nazywamy „teorią”, a system, w którym stwierdzamy i dowodzimy metateoremów, nazywamy „metateorią”.
Podstawowe właściwości systemów dedukcyjnych są następujące:
korekta Poprawka stwierdza, że twierdzenia obowiązują we wszystkich modelach. Oznacza to, że reguły wnioskowania są dobrze dopasowane do tych modeli, innymi słowy, że system dedukcji poprawnie formalizuje rozumowanie w tych modelach. spójność System dedukcji jest spójny (stosuje się też spójny anglicyzm ), jeśli dopuszcza model, lub co sprowadza się do tego samego, jeśli nie pozwala na wykazanie żadnej formuły. O koherencji równań mówimy również wtedy, gdy system dopuszcza model nietrywialny, to znaczy posiadający co najmniej dwa elementy. Sprowadza się to do stwierdzenia, że system nie pozwala na udowodnienie żadnego równania. kompletność Jest definiowany w odniesieniu do rodziny modeli. System dedukcji jest kompletny w odniesieniu do rodziny modeli, jeśli jakiekolwiek twierdzenie, które jest ważne we wszystkich modelach rodziny, jest twierdzeniem. Krótko mówiąc, system jest kompletny, jeśli wszystko, co jest ważne, jest możliwe do wykazania.Inną właściwością systemów odliczeń związanych z kompletnością jest maksymalna spójność . System dedukcji jest maksymalnie spójny, jeśli dodanie nowego aksjomatu, który sam nie jest twierdzeniem, czyni system niespójnym.
Stwierdzenie „taki a taki system jest kompletny dla takiej rodziny modeli” jest typowym przykładem metateorematu.
W tym kontekście intuicyjne pojęcie prawdy daje początek dwóm formalnym pojęciom: prawomocności i dowodliwości. Trzy cechy poprawności, koherencji i kompletności określają, w jaki sposób można połączyć te pojęcia, mając nadzieję, że w ten sposób uda się zidentyfikować prawdę, poszukiwanie logika.
Zdania są formułami wyrażającymi fakty matematyczne, to znaczy własności, które nie zależą od żadnego parametru i które w związku z tym mogą być tylko prawdziwe lub fałszywe, np. „3 jest wielokrotnością 4” (w przeciwieństwie do „n jest wielokrotność 4" , co jest prawdą lub fałszem w zależności od wartości podanej parametrowi n ) lub "wszystkie nietrywialne zera funkcji zeta Riemanna mają część rzeczywistą 1/2" .
Zdania elementarne, zwane zmiennymi zdaniowymi , łączy się za pomocą łączników w złożone formuły. Zdania można interpretować, zastępując każdą zmienną zdaniową zdaniem. Na przykład interpretacja zdania (P ∧ ¬P) ⇒ Q może brzmieć "jeśli 3 jest parzyste, a 3 jest nieparzyste, to 0 = 1" .
Złącza przedstawiono wraz z ich interpretacją w logice klasycznej .
Rozłączenie Alternatywą dwóch propozycji P i Q jest propozycja zauważyć P ∨ Q lub „ P lub Q ”, co jest ważne, jeśli co najmniej jeden z tych propozycji jest prawdziwa; jest zatem fałszywe tylko wtedy, gdy te dwa zdania są fałszywe. Negocjacje Negacją zdania P , jest zdanie zanotowane ¬ P , czyli „nie P ”, które jest prawdziwe, gdy P jest fałszywe; jest zatem fałszem, gdy P jest prawdziwe.Z tych dwóch złączy możemy skonstruować inne przydatne złącza lub skróty:
Spójnik Połączenie dwóch propozycji P i Q są następujące propozycja: ¬ ((¬ P ) ∨ (¬ Q )) tj. nie ((nie P ) lub (nie Q )) Jest to oznaczone jako P ∧ Q lub „ P i Q ” i jest prawdziwe tylko wtedy, gdy P i Q są prawdziwe; i dlatego jest fałszywe, jeśli jedno z dwóch zdań jest fałszywe. Implikacja WPŁYW o Q o P jest propozycja (Ź P ) ∨ P , oznaczony „ P ⇒ Q ” lub „ P oznacza Q ”, i który jest fałszywy tylko wtedy, gdy p jest prawdziwe twierdzenie, a Q fałszywe. Równorzędność Logiczny równoważność z P i Q jest propozycja (( P ⇒ P ) ∧ ( P ⇒ P )) ((( P oznacza P ) oraz ( Q oznacza P ))), oznaczoną " P ⇔ Q ", w którym ( P jest równa to Q ), a to jest prawdziwe tylko wtedy, gdy dwa zdania P i Q mają tę samą wartość logiczną. Ekskluzywny lub Wyłączne lub lub wyłączne alternatywą z P i Q jest propozycja P ⊻ P (czasami oznaczany P ⊕ Q lub nawet p | Q lub projektanci układów ), co odpowiada ( P ∨ Q ) ∧ Ź ( P ∧ Q ), to to znaczy po francusku: albo P albo Q , ale nie oba jednocześnie. Wyłącznik lub P i Q odpowiada P ⇔ ¬ Q lub ponownie ¬ ( P ⇔ Q ). To twierdzenie jest prawdziwe tylko wtedy, gdy P i Q mają różne wartości prawdy.Cechą tak zwanego „ klasycznego ” rachunku zdań jest to, że wszystkie zdania można wyrazić z dwóch łączników: na przykład ∨ i ¬ ( lub i nie ). Możliwe są jednak inne wybory, takie jak ⇒ (implikacja) i ⊥ (fałsz). Możesz użyć tylko jednego złącza, symbolu Sheffera «| ( Henry M. Sheffer , 1913), nazwany przez projektanta „skokiem” , a obecnie nazywany Nand i odnotowany przez projektantów obwodów; można również używać tylko łącznika Nor (zaznaczone ), jak zauważył Charles Sanders Peirce (1880) bez jego publikowania. Krótko mówiąc, w logice klasycznej pojedynczy łącznik wystarcza do uwzględnienia wszystkich operacji logicznych.
Rachunek predykatów rozszerza rachunek zdań o możliwość pisania formuł zależnych od parametrów; w tym celu obliczanie predykatów wprowadza pojęcia zmiennych , symboli funkcji i relacji , terminów i kwantyfikatorów ; terminy uzyskuje się przez połączenie zmiennych za pomocą symboli funkcyjnych, wzory elementarne uzyskuje się przez zastosowanie symboli relacji do terminów.
Typowym wzorem do obliczania predykatów jest „∀ a , b (( p = a . B ) ⇒ (( a = 1) ∨ ( b = 1)))”, który interpretowany w liczbach całkowitych wyraża, że parametr p jest liczbą pierwszą (lub 1). Ta formuła używa dwóch symboli funkcji (punktu, funkcji binarnej interpretowanej przez mnożenie liczb całkowitych i symbolu „1”, funkcji 0-arnej, czyli stałej) oraz symbolu relacji (dla równości). Zmienne to a , b i p , warunki to a . b i 1, a podstawowe wzory to „ p = a . b ”,„ a = 1 ”i„ b = 1 ”. Zmienne a i b są określane ilościowo, ale nie zmienna p, od której zależy wzór.
Istnieje kilka odmian obliczania predykatów; w najprostszym obliczeniu predykatów pierwszego rzędu zmienne reprezentują wszystkie te same typy obiektów, na przykład w powyższym wzorze 3 zmienne a , b i p będą reprezentować liczby całkowite. W obliczeniach predykatów drugiego rzędu występują dwa rodzaje zmiennych: zmienne dla obiektów i inne dla predykatów , czyli relacji między obiektami. Na przykład w arytmetyce drugiego rzędu używamy zmiennych do reprezentowania liczb całkowitych, a inne do zbiorów liczb całkowitych. Ciągłe hierarchia i na 3 th zamówienie było 3 typy zmiennych dla obiektów, relacje między obiektami, relacje między stosunków itd
Aby opisać obliczenie predykatach, niezbędny operacja jest podstawienie , które polega na zastąpieniu we wzorze wszystkie wystąpienia zmiennej x przez perspektywie , otrzymując nowy wzór; na przykład, jeśli zastąpimy zmienną p terminem n! + 1 w powyższym wzorze otrzymujemy formułę „∀ a , b (( n ! + 1 = a . B ) ⇒ (( a = 1) ∨ ( b = 1)))” (co wyraża silnię liczba całkowita n plus 1 jest liczbą pierwszą).
Jeśli P jest formułą zależną od parametru x i a jest terminem, zespół otrzymany przez zastąpienie x przez a w P jest formułą, którą można zapisać P [ a / x ] lub ( a | x ) P , lub innymi odmianami tych notacji. i nazywa się wzorem otrzymanym przez podstawienie x przez a w P .
Aby wyróżnić parametr x, od którego zależy formuła P , zapisujemy go w postaci P { x }; wtedy istnieje P { is } propozycja ( a | x ) P .
Możemy spróbować znaleźć podstawienie (podstawienia), które sprawiają, że formuła jest dowodliwa; problem jest szczególnie interesujący w przypadku tzw. formuł równań , czyli postaci t(x) = t'(x) . Teoria, która stara się rozwiązać takie równania w ramach logiki matematycznej, nazywa się unifikacją .
Kwantyfikatory to specyficzne składniki składniowe obliczania predykatów. Podobnie jak łączniki zdaniowe pozwalają budować nowe formuły ze starych, ale w tym celu opierają się na wykorzystaniu zmiennych.
Lub wzór rachunku predykatów P . Następnie konstruujemy nową tzw. formułę egzystencjalną, oznaczoną ∃ x P, która brzmi: „istnieje x takie, że P”. Załóżmy, że P „zależy” tylko od x . Zdanie ∃ x P jest prawdziwe, gdy istnieje przynajmniej jeden przedmiot a (w rozważanej dziedzinie, w którym x „zmienia się” ) tak, że gdy podstawimy a za x w P, otrzymamy zdanie prawdziwe. Formuła P jest postrzegana jako właściwość, a ∃ x P jest prawdziwe, gdy istnieje obiekt o tej właściwości.
Znak ∃ nazywamy kwantyfikatorem egzystencjalnym .
Podobnie można skonstruować z P wspomniany wzór uniwersalny oznaczony ∀ x P , który brzmi "dla wszystkich x P " lub cokolwiek x P . Oznacza to, że wszystkie obiekty na danym obszarze (te x może wyznaczyć) mają właściwość opisaną przez P .
Znak ∀ nazywamy uniwersalnym kwantyfikatorem .
W logice klasycznej kwantyfikatory uniwersalne i egzystencjalne można zdefiniować względem siebie poprzez negację, ponieważ:
∀ x P jest równoważne ¬ ∃x ¬P, a ∃x P jest równoważne ¬ ∀ x ¬ PRzeczywiście „nieprawdą jest, że każdy przedmiot ma daną właściwość” oznacza „jest przynajmniej jeden, który nie ma tej właściwości”.
Stosowanie kwantyfikatorów Podstawowe właściwościNiech P i Q będą dwoma zdaniami, a x przedmiotem nieokreślonym.
Niech P będzie zdaniem, a x i y będą obiektami nieokreślonymi.
Jeśli A jest formułą, w której zmienna x nie występuje swobodnie , mamy:
Ale również :
Symbol relacji „=”, który reprezentuje równość, ma nieco szczególny status na pograniczu symboli logicznych (łączniki, kwantyfikatory) i nielogicznych (relacje, funkcje). Formuła A = B oznacza, że i b przedstawiają ten sam obiekt (lub i b są różne oznaczenia tego samego przedmiotu) i odczytuje „ jest równy B ”.
Modelu teorii klasycznego tworzy się najczęściej w ramach rachunku bazowego równości, to znaczy, że teorie uważane są równe: równe związek stosuje się dodatkowo do symboli podpisania teorii.
Z punktu widzenia dedukcji równość rządzi się aksjomatami, opisanymi poniżej, zasadniczo wyrażającymi, że dwa równe przedmioty mają te same właściwości (i, w logice drugiego rzędu , że odwrotność jest prawdziwa).
Negacją „=” jest relacja „≠”, która jest zdefiniowana przez a ≠ b wtedy i tylko wtedy, gdy ¬ ( a = b ).
Aksjomaty równości w logice pierwszego rzęduRelacja = będąc zwrotną, symetryczną i przechodnią, mówimy, że relacja = jest relacją równoważności .
Te dwie ostatnie własności intuicyjnie wyrażają, że = jest najlepszą z relacji równoważności.
Definicja w logice drugiego rzęduW logice drugiego rzędu możemy prościej zdefiniować równość przez:
Innymi słowy, dwa przedmioty są równe wtedy i tylko wtedy, gdy mają te same właściwości (zasada identyczności nieodróżnialnych stwierdzona przez Leibniza )
Nie wspominając już o książki odniesienia angielskiego w logicznych subklatek matematyki będących teoria dowodu , z teorii modeli , w teorii mnogości i obliczalności .
Prawie wszystkie podręczniki są w języku angielskim, jednak istnieją również podręczniki w języku francuskim, takie jak te wymienione poniżej: