Być może należałoby przeprosić za zadanie kolejnego pytania na temat warunków wstępnych, ale byłem zdezorientowany co do punktów wyjścia. Spotkałem różne terminy, takie jak „logika modalna”, „logika czasowa”, „logika pierwszego rzędu”, „logika drugiego rzędu” i „logika wyższego rzędu”.

Co dokładnie oznacza „logika” w tym kontekście? Jak rygorystycznie definiujemy słowo „logika”?

Po przejściu na początkowe strony kilku książek mogę z grubsza stwierdzić, że „Logika jest sposobem decydowania o tym, co wynika z tego, co jest znaczące w projektowaniu języków programowania, ponieważ dyktuje i ułatwia projektowanie programów w celu automatycznego rozumowania i rozumienia programów. Chcę zrozumieć nieco drugi punkt w nieco rozbudowany sposób.

Teraz dochodzę do tych logiki.

Czy wszystkie te logiki, „logika czasowa”, „logika modalna”, „logika pierwszego rzędu”, „logika wyższego rzędu” są od siebie niezależne, czy też musimy zrozumieć kilka z nich, aby zrozumieć kilka innych w tej grupie? W skrócie, jakie będą dla nich warunki wstępne? (Świetnie będzie, jeśli będę mógł uzyskać sugestie dotyczące niektórych materiałów.)

PS: Wielkie dzięki za życzliwość

Zasadniczo logika składa się z dwóch rzeczy.

• Składnia to zestaw reguł, które określają, co jest, a nie jest formułą.
• Semantyka to zestaw reguł, które określają, które formuły są „prawdziwe”, a które „fałszywe”. Dla teoretyka modeli wyraża się to poprzez powiązanie wzorów ze strukturami matematycznymi, w których są prawdziwe; dla teoretyka dowodów , prawda odpowiada udowodnieniu z wybranego zestawu aksjomatów z wybranym zestawem reguł (technik) dowodowych.

Różnica między różnymi logikami polega najprościej przy wyborze składni i semantyki. Większość logiki to rozszerzenia logiki zdań lub logiki pierwszego rzędu . W pewnym sensie możesz zobaczyć te rozszerzenia jako „dodające więcej funkcji” do logiki. Na przykład logika czasowa dotyczy prawd, które mogą się zmieniać w czasie.

Ogólnie rzecz biorąc, funkcje te można wyrazić prostszą logiką, kosztem konieczności pisania dłuższych wzorów. Na przykład pojęcie czasowe „  jest prawdziwe od tego momentu na wieczność” można wyrazić w sposób pierwszego rzędu, dodając parametr czasu do wszystkich swoich zdań i mówiąc „Dla wszystkich czasów  , jeżeli  jest większe lub równe do aktualnego czasu, wtedy  jest prawdziwe w czasie  . " W pewnym sensie można myśleć o tych logikach jako o dodawaniu bibliotek do podstawowego języka programowania, aby łatwiej było mówić.t t φ $\varphi$$t$$t$$\varphi$$t$

Ponieważ prawie wszystkie logiki opierają się na logice zdań i pierwszego rzędu, zaleciłbym zapoznanie się z nimi w pierwszej kolejności.

Podczas gdy dziedziny takie jak informatyka, matematyka i fizyka są stosunkowo dobrze zorganizowane, Logika ma chaotyczną historię. Jego organizacja jest naprawdę myląca, więc uważam, że ważne jest, aby przeczytać historię, aby zrozumieć gęstą strukturę pola.

Ścieżka, którą powinieneś wybrać, będzie zależeć od twojego pochodzenia i celów .

Co to jest logika?

1. Tradycyjny punkt widzenia mówi, że logika to system formalny z językiem formalnym (składnią), semantycznym (znaczenie zewnętrzne, myśl o tłumaczach programów) i zestawem reguł do wywnioskowania wypowiedzi z innych (pomyśl o regułach redukcje programów). Logika jest postrzegana jako zwykły obiekt matematyczny.

2. Współczesny punkt widzenia, mówi, poprzez słynny izomorfizm Curry'ego-Howarda, że logika jest spójnym systemem typów (dowody to programy, a typy to formuły). Mówiąc dokładniej: system wnioskowania oparty na twierdzeniu eliminacji cięć i twierdzeniu Church-Rosser / twierdzeniu o konfluencji sugerującym, że leżący u jego podstaw system programowania będzie się dobrze zachowywał.

3. W przypadku zamówień logikę zdań można postrzegać jako układ zerowy (powiedzmy, że zmienne dla zdań są oznaczone ). Zachowują się jak funkcja bez argumentów (stałych).$p, q$

   • Kiedy przejdziemy do logiki pierwszego rzędu, zmienne dla zdań stają się zmiennymi predykatów i przyjmują obiekt jako argument , . Zachowują się, jakby funkcje przyjmujące obiekty (pary, liczby całkowite, ciąg) były argumentami. Pomyśl o języku C.P ( x 1 , . . . , X n ) P ( x 1 , . . . , X n$P, Q$$P(x_1, ..., x_n)$$Q(x_1, ..., x_n)$
   • W logice drugiego rzędu zmienna dla predykatów staje się rodzajem funkcji przyjmujących funkcje pierwszego rzędu. Zachowują się jak funkcje przyjmujące funkcje pierwszego rzędu za argument. Na przykład możemy mieć predykaty i kwantyfikację w stosunku do predykatów.
   • Takie samo rozumowanie trzeciego rzędu itp. Logiki wyższego rzędu przyjmują każde zamówienie. Pomyśl o Haskell i OCaml, które mają argumenty przyjmujące funkcje funkcji funkcji itp.

4. Zasadniczo nie ma konsensusu co do prawdziwej logiki. Niektórzy filozofowie używają systemów, które nie mają spójnego systemu programowania. Właściwie powiedziałbym, że każde pole wykorzystujące Logikę ma swoją własną koncepcję logiki. I większość matematyków prawdopodobnie nie przejmuje się logiką.

Struktura pola

Historia Logiki jest zbyt duża, więc przedstawię jedynie strukturę pola. Dziedzina logiki formalnej jest podzielona na: zastosowanie filozoficzne, matematyczne i obliczeniowe. Formalna logika rozpoczyna się w XIX i XX wieku.

• Najpierw powinieneś studiować logikę zdań i logikę pierwszego rzędu . Są to najbardziej standardowe. Zostały one utworzone w celu przedstawienia formalnego / matematycznego opisu starej logiki czasów starożytnej Grecji.

  • Teoria modeli (semantyka), badanie struktur matematycznych z perspektywy logiki
  • Teoria dowodu (składnia), niezależnie, studiuje dowody jako obiekt matematyczny.

• Logika drugiego rzędu jest rozszerzeniem logiki pierwszego rzędu, która jest rozszerzeniem logiki zdań. Jest to szczególnie interesujące, ponieważ arytmetyka „żyje” w drugim rzędzie (predykaty na predykatach z indukcją). Podobnie topologia żyje w „trzecim rzędzie” (predykaty na zbiorach, które same mogą być postrzegane jako predykaty).

• Potem pojawił się LEJ Brouwer, który podzielił logikę na dwie części:

  • Logika klasyczna to zwykła logika zdefiniowana wcześniej. W szczególności, dla wszystkich , obejmuje (z wyłączeniem środkowego).A ∨ ¬ $A$$A \lor \lnot A$
  • Logika intuicyjna jest rodzajem logiki odrzucającej wykluczone prawo środkowe i wszystkie równoważne prawa (z przyczyn technicznych i filozoficznych nie wyjaśnię tutaj).

• W innym kontekście filozofowie zainteresowali się logiką formalną i sądzili, że może odpowiedzieć na pytania filozoficzne (filozofia analityczna). Stworzyli swoje własne niezależne systemy logiczne (logiki parakonsekwentne, logiki istotności i logiki modalne, takie jak logika deontyczna, logika czasowa, logika epistemiczna, ...). Logika modalna nie działa z prawdą, ale z modalnościami takimi jak możliwość, konieczność, czas, wiedza. Wszystkie są niezależne od powyższej logiki.

• Korespondencja Curry-Howarda daje formalną korespondencję (izomorfizm) pomiędzy dowodami a programami. Teraz wiele logiki można postrzegać jako systemy programowania i odwrotnie. Intuicyjna logika, która została nieco zignorowana, jest teraz postrzegana jako funkcjonalny system programowania ( -calculus). Prowadzi to do studium teorii typów . Jest to obecnie aktywny temat badań.$\lambda$

• Informatycy chcieli formalnie zweryfikować i udowodnić głośność systemów i wydaje się, że logika modalna jest istotna. Dziś używają logiki czasowej i logiki modalnej do wnioskowania w systemach (patrz: metody formalne, sprawdzanie modelu). Systemy są modelowane za pomocą teorii automatów (na przykład) i weryfikowane za pomocą narzędzi logicznych. Doprowadziło to do Linear Temporal Logic (LTL) i Computational Tree Logic (CTL) .

• Z tej samej motywacji informatycy chcieli zweryfikować solidność i udowodnić właściwości programów. Wynaleźliśmy więc Hoare Logic dla programów imperatywnych i, bardziej ogólnie, Separation Logics .

• Badając izomorfizm Curry-Howarda, pojawiła się nowa logika: Logika liniowa, która ogranicza reguły strukturalne (osłabienie i skurcz), postrzegane jako usuwanie i powielanie działające w dowodach i programach. Wyjaśniono potencjalną nieskończoność prawdy. Wydaje się, że logika ta jest uogólnieniem logiki klasycznej i intuicyjnej i daje zupełnie nową koncepcję logiki opartą na obliczeniach i paradygmacie proceduralnym. Jest to głównie badane przez informatyków.

• Logika liniowa również wywodzi się z tego, co nazywamy logiką podstrukturalną, odrzucając reguły strukturalne logiki. Odpowiednia logika i Affine Logic są przykładami takich systemów.

Podsumowanie i wybór ścieżki

• Dowolną logiką może być: logika zdaniowa, pierwszego rzędu, drugiego rzędu, trzeciego rzędu, ..., wyższego rzędu (każda przedłużająca poprzednią).

• Możemy dodawać lub usuwać reguły, aby tworzyć warianty istniejących systemów:

  • Usuń wykluczone-środkowe: intuicyjna logika
  • Dodaj modalności: logikę modalną
  • Ogranicz sprzeczność i osłabienie: logika liniowa
  • Usuń skurcz: logika afiniczna
  • Usuń osłabienie: odpowiednia logika
  • Postępuj z negacją inaczej: logika parakonsekwentna

• Naucz się najpierw logiki zdań i pierwszego rzędu oraz:

  • teoria modeli, drugi rząd, wyższy porządek, jeśli interesuje Cię matematyka
  • teoria dowodu, logika intuicyjna, logika drugiego rzędu, logika liniowa, jeśli interesują Cię podstawy informatyki
  • logika modalna, logika hoare, logika separacji, jeśli interesuje Cię weryfikacja systemów i programów
  • logika modalna, ogólnie logika nieklasyczna, jeśli interesuje Cię filozofia

Referencje (książki)

Osobiście zalecam mieszanie referencji, jeśli to możliwe.

• Logika matematyczna (Chiswell i Hodges) : bardzo zwięzła i prosta książka na początek.
• Pierwszy kurs logiki (Hedman) : trochę podobny do powyższego, ale podaj więcej szczegółów i uwzględnij obliczalność.
• Podręcznik praktycznej logiki i automatycznego rozumowania (Harrison) : Jeśli chcesz zrozumieć, jak niektóre koncepcje związane z logiką są wdrażane w praktyce. Bardziej zorientowany na automatyczne rozumowanie.
• Logika w informatyce (Huth i Ryan) : bardzo przejrzysta i zorientowana na informatyków (weryfikacja programów i systemów, logika Hoare'a, praktyczne zastosowanie logiki modalnej, logiki czasowej, sprawdzanie modelu).
• Wprowadzenie do teorii dowodów (Buss) : wprowadzenie do teorii dowodów. Lepiej przeczytać to po ogólnej logice.

Referencje (Wikipedia)

• https://en.wikipedia.org/wiki/Philosophical_logic
• https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
• https://en.wikipedia.org/wiki/Non-classical_logic
• https://en.wikipedia.org/wiki/Intuitionistic_logic
• https://en.wikipedia.org/wiki/Modal_logic
• https://en.wikipedia.org/wiki/Model_theory
• https://en.wikipedia.org/wiki/Proof_theory
• https://en.wikipedia.org/wiki/Linear_temporal_logic
• https://en.wikipedia.org/wiki/Computation_tree_logic
• https://en.wikipedia.org/wiki/Separation_logic
• https://en.wikipedia.org/wiki/Hoare_logic
• https://en.wikipedia.org/wiki/Linear_logic
• https://en.wikipedia.org/wiki/Substructural_logic

Wszystkie te logiki znajdują się pod logiką matematyczną .

Logika matematyczna jest często podzielona na dziedziny teorii zbiorów, teorii modeli, teorii rekurencji i teorii dowodów. Obszary te dzielą podstawowe wyniki dotyczące logiki, w szczególności logiki pierwszego rzędu i definiowalności. W informatyce (szczególnie w klasyfikacji ACM) logika matematyczna obejmuje dodatkowe tematy, które nie zostały szczegółowo opisane w tym artykule; zobacz Logika w informatyce dla tych.

Ponadto, jeśli chcesz poznać logikę w ogólności, ten artykuł może być przydatny.

Logika, pierwotnie oznaczająca „słowo” lub „to, co się wypowiada”, ale rozumiana jako „myśl” lub „rozum”, jest przedmiotem zainteresowanym najbardziej ogólnymi prawami prawdy i obecnie ogólnie uważa się, że składa się z systematycznych badań formy prawidłowego wnioskowania. Prawidłowe wnioskowanie to takie, w którym istnieje specyficzna relacja logicznego wsparcia między założeniami wnioskowania i jego wnioskiem.