Formális rendszer

Az oldal jelenlegi verzióját még nem ellenőrizték tapasztalt közreműködők, és jelentősen eltérhet a 2021. augusztus 31-én felülvizsgált verziótól ; az ellenőrzések 3 szerkesztést igényelnek .

A formális rendszer ( formális elmélet , axiomatikus elmélet , axiomatika , deduktív rendszer ) az elmélet szigorú formalizálásának eredménye , amely teljes absztrakciót feltételez a használt nyelv szavainak jelentésétől, és minden, a használatot szabályozó feltételtől. ezeket a szavakat az elméletben kifejezetten kimondják olyan axiómák és szabályok révén, amelyek lehetővé teszik egy kifejezés levezetését a többiből [1] .

A formális rendszer olyan absztrakt objektumok gyűjteménye, amelyek nem kapcsolódnak a külvilághoz, amelyben a szimbólumkészlettel való működés szabályait szigorúan szintaktikai értelmezésben mutatják be, anélkül, hogy figyelembe vennék a szemantikai tartalmat, vagyis a szemantikát. A szigorúan leírt formális rendszerek a Hilbert-probléma felvetése után jelentek meg . Az első FS Russell és Whitehead "Formal Systems" című könyvének megjelenése után jelent meg.[ adja meg ] . Ezeket az FS-eket bizonyos követelményekkel támasztották alá.

Alapok

Egy formális elmélet akkor tekinthető definiáltnak, ha [2] :

  1. Adott egy véges vagy megszámlálható tetszőleges szimbólumkészlet. A véges szimbólumsorozatokat elméleti kifejezéseknek nevezzük.
  2. A kifejezéseknek van egy részhalmaza, amelyet képleteknek neveznek .
  3. A képletek egy részhalmazát, az úgynevezett axiómákat elkülönítették .
  4. A képletek között véges kapcsolatok állnak rendelkezésre, amelyeket következtetési szabályoknak nevezünk .

Általában van egy hatékony eljárás, amely lehetővé teszi, hogy egy adott kifejezés meghatározza, hogy képlet-e. Gyakran egy képletkészletet induktív definíció ad meg . Általános szabály, hogy ez a halmaz végtelen. A szimbólumok halmaza és a képletkészlet együttesen határozza meg a formális elmélet nyelvét vagy aláírását .

Leggyakrabban hatékonyan ki lehet deríteni, hogy egy adott képlet axióma-e; ilyen esetben az elméletet hatékonyan axiomatizáltnak vagy axiomatikusnak mondják . Az axiómák halmaza lehet véges vagy végtelen. Ha az axiómák száma véges, akkor az elméletet véges axiomatizálhatónak mondjuk . Ha az axiómák halmaza végtelen, akkor általában véges számú axióma sémával és az axióma sémából meghatározott axiómák generálására vonatkozó szabályokkal adjuk meg. Az axiómákat általában két típusra osztják: logikai axiómákra (amelyek a formális elméletek egész osztályára jellemzőek) és nem logikai vagy megfelelő axiómákra (amelyek meghatározzák egy adott elmélet sajátosságait és tartalmát).

Minden R következtetési szabályra és minden A képletre hatékonyan megoldódik az a kérdés, hogy a választott képlethalmaz viszonyul-e R-hez az A képlettel , és ha igen, akkor A -t e képletek egyenes következményének nevezzük a vonalzó.

A levezetés bármely képletsorozat, amelyben a sorozat bármely formulája vagy axióma, vagy valamely korábbi képlet közvetlen következménye az egyik levezetési szabály szerint.

Egy képletet tételnek nevezünk , ha van olyan levezetés, amelyben ez a képlet az utolsó.

Azt az elméletet, amelyre létezik egy hatékony algoritmus, amely lehetővé teszi, hogy egy adott képletből megtudja, létezik-e származtatása, eldönthetőnek nevezzük ; különben az elmélet eldönthetetlennek mondható .

Abszolút konzisztensnek mondják azt az elméletet, amelyben nem minden képlet tétel .

Definíció és fajták

A deduktív elmélet adottnak tekinthető, ha:

  1. Adott egy ábécé ( készlet ) és a kifejezések ( szavak ) kialakításának szabályai ebben az ábécében.
  2. A képletek (jól formált, helyes kifejezések) kialakításának szabályai adottak.
  3. A képletek halmazából valamilyen módon kiválasztjuk a tételek T részhalmazát ( bizonyítható formulák ).

A deduktív elméletek változatai

A tételkészlet felépítésének módszerétől függően:

Axiómák és következtetési szabályok megadása

A képletkészletben az axiómák egy részhalmazát különítjük el, és véges számú következtetési szabályt adunk meg - olyan szabályokat, amelyek segítségével (és csakis ezek segítségével) axiómákból és korábban levezetett új tételek alkothatók. tételek. Az összes axióma is benne van a tételek számában. Néha (például Peano axiomatikájában ) egy elmélet végtelen számú axiómát tartalmaz, amelyeket egy vagy több axiómaséma segítségével határoznak meg . Az axiómákat néha "rejtett definícióknak" nevezik. Ily módon egy formális elméletet határozunk meg ( formális axiomatikus elmélet , formális (logikai) kalkulus ).

Csak axiómák kérése

Csak axiómák vannak megadva, a következtetési szabályokat jól ismertnek tekintjük.

A tételek ilyen specifikációjával azt mondjuk, hogy egy félformális axiomatikus elmélet adott . Példák

Geometria

Csak a következtetési szabályok megadása

Nincsenek axiómák (az axiómák halmaza üres), csak következtetési szabályok vannak megadva.

Valójában az így meghatározott elmélet a formális egy speciális esete, de megvan a maga neve: a természetes következtetés elmélete .

A deduktív elméletek tulajdonságai

Konzisztencia

Azt az elméletet, amelyben a tételek halmaza lefedi a képletek teljes halmazát (minden képlet tétel, „igaz állítás”), inkonzisztensnek nevezzük . Ellenkező esetben az elmélet konzisztensnek mondható . Egy elmélet következetlenségének feltárása a formális logika egyik legfontosabb és olykor legnehezebb feladata.

Teljesség

Egy elméletet akkor nevezünk teljesnek , ha bármely mondatra (zárt képletre) önmagában vagy annak tagadása származtatható . Ellenkező esetben az elmélet bizonyíthatatlan állításokat tartalmaz (olyan állításokat, amelyek nem bizonyíthatóak és nem is cáfolhatók magával az elmélettel), és hiányosnak nevezzük .

Az axiómák függetlensége

Egy elmélet egyéni axiómáját függetlennek mondjuk, ha az axióma nem vezethető le a többi axiómából. A függő axióma lényegében redundáns, az axiómarendszerből való eltávolítása semmilyen módon nem befolyásolja az elméletet. Egy elmélet teljes axiómarendszerét függetlennek nevezzük , ha minden axióma független.

Feloldhatóság

Egy elméletet akkor nevezünk eldönthetőnek , ha egy tétel fogalma hatásos benne , vagyis létezik egy hatékony folyamat (algoritmus), amely lehetővé teszi, hogy bármely képlet véges számú lépésben meghatározza, hogy tétel-e vagy sem.

Legfontosabb eredmények

  • A 30-as években. A 20. században Kurt Gödel megmutatta, hogy az elsőrendű elméletek egész osztálya hiányos. Ráadásul az elmélet konzisztenciáját kimondó képlet magával az elmélettel sem származtatható (lásd Gödel hiányossági tételeit ). Ez a következtetés nagy jelentőséggel bírt a matematika számára, mivel a formális aritmetika (és minden olyan elmélet, amely alelméletként tartalmazza) csak egy ilyen elsőrendű elmélet, ezért nem teljes.
  • Ennek ellenére a valós zárt mezők elmélete összeadási, szorzási és sorrendi viszonyokkal teljes ( Tarski-Seidenberg tétel ).
  • Alonzo Church bebizonyította, hogy bármely tetszőleges predikátum logikai képlet érvényességének meghatározásának problémája algoritmikusan eldönthetetlen .
  • A propozíciós kalkulus egy következetes, teljes, eldönthető elmélet.

Lásd még

Példák formális rendszerekre

Jegyzetek

  1. ↑ Kleene S.K. Bevezetés a metamatematikába . - M. : IL, 1957. - S. 59-60. Archiválva : 2013. május 1. a Wayback Machine -nél
  2. ↑ Mendelssohn E. Bevezetés a matematikai logikába . - M . : "Nauka", 1971. - P. 36. Archív másolat 2013. május 1-i dátummal a Wayback Machine -nél

Irodalom

  Ugrás a Wikidata elemre  Szótárak és enciklopédiák
 Logikák
Filozófia • Szemantika • Szintaxis • Történelem
Logikai csoportok
klasszikus logika
matematikai logika
Nem klasszikus logika
Filozófiai logika
Alkatrészek
Logikai szimbólumok listája