Muodollinen järjestelmä

Kokeneet kirjoittajat eivät ole vielä tarkistaneet sivun nykyistä versiota, ja se voi poiketa merkittävästi 31. elokuuta 2021 tarkistetusta versiosta . tarkastukset vaativat 3 muokkausta .

Formaalinen järjestelmä ( formaaliteoria , aksiomaattinen teoria , aksiomatiikka , deduktiivinen järjestelmä ) on tulos teorian tiukasta formalisaatiosta , joka olettaa täydellisen abstraktion käytetyn kielen sanojen merkityksestä ja kaikista kielen käyttöä ohjaavista ehdoista nämä sanat teoriassa ilmaistaan ​​eksplisiittisesti aksioomien ja sääntöjen kautta, jotka mahdollistavat yhden lauseen johtamisen muista [1] .

Formaalinen järjestelmä on kokoelma abstrakteja objekteja, jotka eivät liity ulkomaailmaan, jossa symbolijoukon kanssa toimimisen säännöt esitetään tiukasti syntaktisessa tulkinnassa ottamatta huomioon semanttista sisältöä eli semantiikkaa. Tiukasti kuvatut muodolliset järjestelmät ilmestyivät Hilbertin ongelman esittämisen jälkeen . Ensimmäinen FS ilmestyi Russellin ja Whiteheadin "Formal Systems" -kirjojen julkaisemisen jälkeen.[ määritä ] . Näille FS:lle asetettiin tietyt vaatimukset.

Perusteet

Formaali teoria katsotaan määritellyksi, jos [2] :

  1. On annettu äärellinen tai laskettava joukko mielivaltaisia ​​symboleja. Äärillisiä symbolijonoja kutsutaan teorialausekkeiksi .
  2. On olemassa osajoukko lausekkeita, joita kutsutaan kaavoiksi .
  3. Kaavojen osajoukko, jota kutsutaan aksioomiksi , on erotettu .
  4. Kaavojen välillä on rajallinen joukko suhteita, joita kutsutaan päättelysäännöiksi .

Yleensä on olemassa tehokas menettely, jonka avulla tietty lauseke voi määrittää, onko se kaava. Usein joukko kaavoja annetaan induktiivisella määritelmällä . Yleensä tämä joukko on ääretön. Symbolijoukko ja kaavajoukko määrittelevät yhdessä muodollisen teorian kielen tai allekirjoituksen .

Useimmiten on mahdollista selvittää tehokkaasti, onko tietty kaava aksiooma; Tällaisessa tapauksessa teorian sanotaan olevan tehokkaasti aksiomatisoitu tai aksiomaattinen . Aksioomien joukko voi olla äärellinen tai ääretön. Jos aksioomien lukumäärä on äärellinen, niin teorian sanotaan olevan äärellisesti aksiomatisoitavissa . Jos aksioomijoukko on ääretön, niin se yleensä määritellään käyttämällä äärellistä määrää aksioomakaavioita ja sääntöjä tiettyjen aksioomien generoimiseksi aksioomakaaviosta. Tavallisesti aksioomit jaetaan kahteen tyyppiin: loogisiin aksioomiin (yhteisiä koko muodollisten teorioiden luokalle) ja ei- loogisiin tai oikeisiin aksioomiin (jotka määrittävät tietyn teorian erityispiirteet ja sisällön).

Jokaiselle päättelysäännölle R ja jokaiselle kaavalle A ratkaistaan ​​tehokkaasti, onko valittu kaavajoukko suhteessa R:ään kaavan A kanssa , ja jos on, niin A: ta kutsutaan näiden kaavojen suoraksi seuraukseksi kaavan A mukaisesti. viivotin.

Johdannainen on mikä tahansa kaavojen sekvenssi, jossa mikä tahansa sekvenssin kaava on joko aksiooma tai suora seuraus joistakin aikaisemmista kaavoista jonkin johtamissäännön mukaisesti.

Kaavaa kutsutaan lauseeksi , jos on johdannainen, jossa tämä kaava on viimeinen.

Teoriaa, jolle on olemassa tehokas algoritmi, jonka avulla voit selvittää annetusta kaavasta, onko sen johtaminen olemassa, kutsutaan ratkaistavaksi ; muuten teorian sanotaan olevan ratkaisematon .

Teorian, jossa kaikki kaavat eivät ole lauseita, sanotaan olevan ehdottoman johdonmukainen .

Määritelmä ja lajikkeet

Deduktiivisen teorian katsotaan olevan annettu, jos:

  1. Aakkoset ( joukko ) ja säännöt ilmausten ( sanojen ) muodostamiseksi tässä aakkostossa on annettu .
  2. Säännöt kaavojen muodostamiselle (hyvin muotoillut, oikeat lausekkeet) annetaan.
  3. Kaavojen joukosta valitaan jollain tavalla lauseiden osajoukko T ( todistettavat kaavat ).

Deduktiivisten teorioiden lajikkeet

Riippuen lausejoukon muodostamismenetelmästä:

Aksioomien ja päättelysääntöjen määrittäminen

Kaavojen joukossa erotetaan aksioomien osajoukko ja määritellään äärellinen määrä päättelysääntöjä - sellaisia ​​sääntöjä, joiden avulla (ja vain niiden avulla) voidaan muodostaa uusia lauseita aksioomeista ja aiemmin johdetuista lauseita. Myös kaikki aksioomit sisältyvät lauseiden määrään. Joskus (esimerkiksi Peanon aksiomatiikassa ) teoria sisältää äärettömän määrän aksioomia, jotka määritetään käyttämällä yhtä tai useampaa aksioomakaaviota . Aksioomia kutsutaan joskus "piilotetuiksi määritelmiksi". Tällä tavalla määritellään muodollinen teoria ( formaalinen aksiomaattinen teoria , formaalinen (looginen) laskenta ).

Kysytään vain aksioomia

Vain aksioomit on annettu, päättelysääntöjen katsotaan olevan hyvin tunnettuja.

Tällaisella lauseiden määrittelyllä sanotaan, että puolimuodollinen aksiomaattinen teoria on annettu . Esimerkkejä

Geometria

Vain päättelysääntöjen määrittäminen

Aksioomia ei ole (aksioomien joukko on tyhjä), vain päättelysäännöt annetaan.

Itse asiassa näin määritelty teoria on muodollisen teorian erikoistapaus, mutta sillä on oma nimensä: luonnollisen päättelyn teoria .

Deduktiivisten teorioiden ominaisuudet

Johdonmukaisuus

Teoriaa, jossa lausejoukko kattaa koko kaavajoukon (kaikki kaavat ovat lauseita, "tosia väitteitä"), kutsutaan epäjohdonmukaiseksi . Muuten teorian sanotaan olevan johdonmukainen . Teorian epäjohdonmukaisuuden selvittäminen on yksi formaalilogiikan tärkeimmistä ja joskus vaikeimmista tehtävistä.

Täydellisyys

Teoriaa kutsutaan täydelliseksi , jos siinä jollekin lauseelle (suljetulle kaavalle) joko itse tai sen negaatio on johdettavissa . Muuten teoria sisältää todistamattomia väitteitä (väittämiä, joita ei voida todistaa tai kumota itse teorian avulla), ja sitä kutsutaan epätäydellisiksi .

Aksioomien riippumattomuus

Teorian yksittäisen aksiooman sanotaan olevan riippumaton , jos sitä ei voida päätellä muista aksioomista. Riippuva aksiooma on olennaisesti redundantti, eikä sen poistaminen aksioomijärjestelmästä vaikuta teoriaan millään tavalla. Koko teorian aksioomajärjestelmää kutsutaan itsenäiseksi , jos jokainen siinä oleva aksiooma on riippumaton.

Ratkaisevuus

Teoriaa kutsutaan ratkaistavaksi , jos lauseen käsite on siinä tehokas , eli on olemassa tehokas prosessi (algoritmi), jonka avulla mikä tahansa kaava voi määrittää äärellisessä määrässä vaiheita, onko se lause vai ei.

Tärkeimmät tulokset

  • 30-luvulla. 1900-luvulla Kurt Gödel osoitti, että on olemassa kokonainen luokka ensimmäisen asteen teorioita, jotka ovat epätäydellisiä. Lisäksi teorian johdonmukaisuutta ilmaiseva kaava ei myöskään ole johdettavissa itse teorian avulla (ks . Gödelin epätäydellisyyslauseet ). Tällä johtopäätöksellä oli suuri merkitys matematiikan kannalta, koska muodollinen aritmetiikka (ja mikä tahansa teoria, joka sisältää sen osateoriana) on juuri tällainen ensimmäisen asteen teoria ja siksi epätäydellinen.
  • Tästä huolimatta teoria todellisista suljetuista kentistä yhteen-, kertolasku- ja järjestyssuhteen kanssa on valmis ( Tarski-Seidenberg-lause ).
  • Alonzo Church osoitti, että minkä tahansa mielivaltaisen predikaattilogiikan kaavan pätevyyden määrittämisen ongelma on algoritmisesti ratkaisematon .
  • Propositiolaskenta on johdonmukainen, täydellinen, päätettävissä oleva teoria.

Katso myös

Esimerkkejä muodollisista järjestelmistä

Muistiinpanot

  1. ↑ Kleene S.K. Johdatus metamatematiikkaan . - M .: IL, 1957. - S. 59-60. Arkistoitu 1. toukokuuta 2013 Wayback Machinessa
  2. ↑ Mendelssohn E. Johdatus matemaattiseen logiikkaan . - M . : "Nauka", 1971. - S. 36. Arkistokopio päivätty 1. toukokuuta 2013 Wayback Machinessa

Kirjallisuus

  Siirry Wikidata-kohteeseen  Sanakirjat ja tietosanakirjat
 Logiikka
Filosofia • Semantiikka • Syntaksi • Historia
Logiikkaryhmät
klassista logiikkaa
matemaattinen logiikka
Ei-klassinen logiikka
Filosofinen logiikka
Komponentit
Luettelo loogisista symboleista