System formalny - Formal system

System formalny to abstrakcyjna struktura używana do wnioskowania twierdzeń z aksjomatów zgodnie z zestawem reguł. Reguły te, które służą do wnioskowania twierdzeń z aksjomatów, są rachunkiem logicznym systemu formalnego. System formalny jest zasadniczo „ systemem aksjomatycznym ”.

W 1921 roku David Hilbert zaproponował wykorzystanie takiego systemu jako podstawy wiedzy matematycznej . System formalny może reprezentować dobrze zdefiniowany system abstrakcyjnego myślenia .

Termin formalizm jest czasami szorstki synonim systemie formalnym , ale także odnosi się do danego stylu notacji , na przykład, Paul Dirac „s Notacja Diraca .

Tło

Każdy system formalny wykorzystuje symbole pierwotne (które wspólnie tworzą alfabet ) do skończonego konstruowania języka formalnego ze zbioru aksjomatów poprzez inferencyjne reguły formacji .

System składa się zatem z prawidłowych formuł zbudowanych przez skończone kombinacje pierwotnych symboli — kombinacje utworzone z aksjomatów zgodnie z określonymi regułami.

Bardziej formalnie można to wyrazić następująco:

  1. Skończony zbiór symboli, znany jako alfabet, który łączy formuły, tak że formuła jest tylko skończonym ciągiem symboli wziętych z alfabetu.
  2. Gramatyka składający się z zasadami, które tworzą wzory z prostszych wzorów. Mówi się, że formuła jest dobrze uformowana, jeśli może być utworzona przy użyciu reguł gramatyki formalnej. Często wymagana jest procedura decyzyjna pozwalająca na podjęcie decyzji, czy formuła jest prawidłowo sformułowana.
  3. Zbiór aksjomatów lub schemat aksjomatów składający się z dobrze uformowanych formuł.
  4. Zestaw reguł wnioskowania . Dobrze sformułowana formuła, którą można wywnioskować z aksjomatów, jest znana jako twierdzenie o systemie formalnym.

Rekurencyjne

Mówi się, że system formalny jest rekurencyjny (tj. efektywny) lub rekurencyjnie przeliczalny, jeśli zbiór aksjomatów i zbiór reguł wnioskowania są odpowiednio zbiorami rozstrzygalnymi lub półrozstrzygalnymi .

Wnioskowanie i wnioskowanie

Entailment systemu przez jego logiczny fundament, co odróżnia od innych formalny system, który może mieć pewne podstawy w abstrakcyjny wzór. Często system formalny będzie podstawą lub nawet utożsamiany z większą teorią lub dziedziną (np. geometrią euklidesową ) zgodnie z zastosowaniem we współczesnej matematyce, takiej jak teoria modeli .

Język formalny

Formalny język jest językiem, który jest zdefiniowany przez system formalny. Podobnie jak języki w lingwistyce , języki formalne mają na ogół dwa aspekty:

  • składnia języka jest to, co wygląda jak język (bardziej formalnie: zbiór możliwych wyrażeń, które są ważne wypowiedzi w języku) studiował w teorii języków formalnych
  • że semantyka danego języka są co wypowiedziach średniej języka (który jest sformalizowane na różne sposoby, w zależności od rodzaju języka w pytaniu)

W informatyce i lingwistyce zwykle tylko składnia języka formalnego jest rozważana poprzez pojęcie gramatyki formalnej . Formalne gramatyka jest dokładny opis składni formalnej języku: w zestawie z strun . Dwie główne kategorie gramatyki formalnej to gramatyki generatywne , które są zbiorami reguł, w jaki sposób mogą być generowane ciągi w języku, oraz gramatyki analityczne (lub gramatyka redukcyjna), które są zbiorami reguł, jak można tworzyć ciągi analizowane w celu ustalenia, czy jest członkiem języka. Krótko mówiąc, gramatyka analityczna opisuje, jak rozpoznać, kiedy łańcuchy są członkami zbioru, podczas gdy gramatyka generatywna opisuje, jak napisać tylko te łańcuchy w zbiorze.

W matematyce język formalny zwykle nie jest opisywany przez gramatykę formalną, ale przez (a) język naturalny, taki jak angielski. Systemy logiczne są definiowane zarówno przez system dedukcyjny, jak i język naturalny. Z kolei systemy dedukcyjne są definiowane tylko przez język naturalny (patrz niżej).

System dedukcyjny

System dedukcyjny , zwany także aparatem dedukcyjnym lub logiką , składa się z aksjomatów (lub schematów aksjomatów ) i reguł wnioskowania, które można wykorzystać do wyprowadzenia twierdzeń systemu.

Takie systemy dedukcyjne zachowują właściwości dedukcyjne w formułach wyrażanych w systemie. Zwykle jakość, o którą się troszczymy, to prawda, a nie fałsz. Jednak zamiast tego mogą zostać zachowane inne modalności , takie jak uzasadnienie lub przekonanie .

Aby utrzymać swoją dedukcyjną integralność, aparat dedukcyjny musi być definiowalny bez odniesienia do jakiejkolwiek zamierzonej interpretacji języka. Celem jest zapewnienie, że każdy wiersz wyprowadzenia jest jedynie syntaktyczną konsekwencją wierszy, które go poprzedzają. Nie powinno być żadnego elementu jakiejkolwiek interpretacji języka, który wiąże się z dedukcyjną naturą systemu.

Przykładem systemu dedukcyjnego jest logika predykatów pierwszego rzędu .

System logiczny

Logiczny system lub język (nie mylić z rodzaju „języku formalne” omówiony powyżej, który jest opisany przez formalne gramatyczne), to system dedukcji (patrz powyżej, najczęściej rzędu pierwszego logiki bazowego ) wraz z dodatkowymi (nie logiczne) aksjomaty i semantyka . Zgodnie z interpretacją modelowo-teoretyczną semantyka systemu logicznego opisuje, czy dana struktura spełnia prawidłowo sformułowaną formułę. Struktura spełniająca wszystkie aksjomaty systemu formalnego jest znana jako model systemu logicznego. System logiczny jest słuszny, jeśli każda dobrze sformułowana formuła, którą można wywnioskować z aksjomatów, jest spełniona przez każdy model systemu logicznego. I odwrotnie, system logiczny jest kompletny, jeśli każda dobrze sformułowana formuła, którą spełnia każdy model systemu logicznego, można wywnioskować z aksjomatów.

Przykładem systemu logicznego jest arytmetyka Peano .

Historia

Wczesne systemy logiczne obejmują indyjską logikę Panini , sylogistyczną logikę Arystotelesa, logikę zdań stoicyzmu i chińską logikę Gongsun Longa (ok. 325-250 pne). W ostatnich czasach współautorami są George Boole , Augustus De Morgan i Gottlob Frege . Logika matematyczna rozwinęła się w XIX-wiecznej Europie .

Formalizm

Program Hilberta

David Hilbert zapoczątkował ruch formalistyczny, który został ostatecznie złagodzony przez twierdzenia Gödla o niezupełności .

Manifest QED

Manifest QED był kolejnym, jak dotąd nieudanym, wysiłkiem na rzecz sformalizowania znanej matematyki.

Przykłady

Przykłady systemów formalnych obejmują:

Warianty

Następujące systemy są odmianami systemów formalnych.

System dowodowy

Dowody formalne to sekwencje dobrze sformułowanych formuł (w skrócie wff). Aby wff kwalifikował się jako część dowodu, może to być aksjomat lub produkt zastosowania reguły wnioskowania na poprzednich wffs w sekwencji dowodowej. Ostatni wff w sekwencji jest rozpoznawany jako twierdzenie .

Punkt widzenia, że ​​generowanie dowodów formalnych jest wszystkim, co jest w matematyce, jest często nazywany formalizmem . David Hilbert założył metamatematykę jako dyscyplinę do omawiania systemów formalnych. Każdy język używany do mówienia o systemie formalnym nazywany jest metajęzykiem . Metajęzyk może być językiem naturalnym lub może być sam częściowo sformalizowany, ale na ogół jest on mniej całkowicie sformalizowany niż komponent języka formalnego badanego systemu formalnego, który jest wówczas nazywany językiem przedmiotowym , to znaczy przedmiotem kwestionowana dyskusja.

Mając dany system formalny, można zdefiniować zbiór twierdzeń, które można udowodnić wewnątrz systemu formalnego. Ten zestaw składa się ze wszystkich wffs, na które istnieje dowód. Tak więc wszystkie aksjomaty są uważane za twierdzenia. W przeciwieństwie do gramatyki dla wffs, nie ma gwarancji, że będzie procedura decyzyjna do decydowania, czy dany wff jest twierdzeniem, czy nie. Pojęcie właśnie zdefiniowanego twierdzenia nie powinno być mylone z twierdzeniami o systemie formalnym , które dla uniknięcia pomyłek nazywane są zwykle metateoremami .

Zobacz też

Bibliografia

Dalsza lektura

Zewnętrzne linki