Sekvencinis skaičiavimas

Sekvencinis skaičiavimas  – matematinės logikos formulių įrodymo būdas. Šis būdas pasižymi tuo, kad įrodymo metu yra konstruojama formulių seka, dar kitaip vadinama sekvencija, kurioje kiekviena formulė yra gaunama iš prieš tai buvusių formulių pagal skaičiavimo taisykles arba aksiomas.
  
Sekvencinis skaičiavimas yra formulių įrodymo sritis, kuri susideda iš šių skaičiavimų:
 Hilberto tipo teiginių skaičiavimo,
 Gentzeno tipo teiginių skaičiavimo, kuris susideda iš:
 Natūraliosios dedukcijos,
 Sekvencinio skaičiavimo (kartais dar vadinamo skaičiavimu ).

Kontekstas
XX a. pradėjus atsirasti informatikos užuomazgoms, matematikai stengėsi formalizuoti matematines žinias, jog šios galėtų būti panaudotos algoritmų kūrime, tad vienas iš formalizavimo rezultatų - sekvencinis skaičiavimas. Hilberto tipo teiginių skaičiavimas buvo aprašytas vokiečių mokslininko Deivido Hilberto kaip tiesioginis tapačiai teisingų formulių formalus įrodymo būdas. Gentzeno tipo sekvencinis skaičiavimas (natūralioji dedukcija ir sekvencinis skaičiavimas) - 1934 m. vokiečių matematiko Gerardo Gentzeno aprašytas formalizavimo būdas, kuris nustato tapačiai teisingas formules. Sekvencinį skaičiavimą taip pat tyrinėjo mokslininkai Dagas Pravitsas, Džordžas Kreisleris ir kiti.

Hilberto tipo teiginių skaičiavimas  
Hilberto tipo teiginių skaičiavimas - tai skaičiavimas su aksiomų schemomis 1.1-4.3 ir Modus Ponens taisykle. Formulė  įrodoma Hilberto tipo teiginių skaičiavime, jei yra tokia formulių seka, kurioje kiekviena formulė yra aksioma arba gauta pagal Modus Ponens taisyklę iš prieš tai parašytų ir kuri (seka) baigiasi formule   .  
 
Formulė  įrodoma Hilberto tipo teiginių skaičiavime tada ir tik tada, kai ji yra tapačiai teisinga. Iš to išplaukia, jog galime įrodyti ir faktą, jog formulė  yra tapačiai klaidinga įrodydami, kad  yra tapačiai teisinga. Jeigu formulės tapataus teisingumo arba klaidingumo įrodyti nepavyksta, šis skaičiavimas nieko nepasako apie formulės teisingumą ar klaidingumą.  
  
Aksiomų schemos 

 

 

 

 

 

 

 

 

 

 

 

Taisyklė Modus ponens:

Gentzeno tipo sekvencinis skaičiavimas 
Gentzeno tipo sekvenciniuose skaičiavimuose yra formuojamas išvedimo medis tikrinamai formulei . Jis konstruojamas pagal tam skaičiavimui priklausančias taisykles bandant gauti visose šakose aksiomas. Sekvencinio skaičiavimo taisyklė yra apverčiama, jei taisyklės išvada išvedama tada ir tik tada, kai išvedamos visos taisyklės prielaidos. Ne visos natūraliosios dedukcijos taisyklės yra apverčiamos, sekvenciniame skaičiavime apverčiamos taisyklės yra visos. 

Tiek natūralioji dedukcija, tiek ir sekvencinis skaičiavimas vienodai įrodo formulės tapatų teisingumą, todėl yra įrodyta, jog šie skaičiavimai rezultatų prasme yra izomorfiški. Taip pat yra įrodyta, jog Gentzeno tipo sekvencinis skaičiavimas rezultato prasme yra ekvivalentus Hilberto tipo teiginių skaičiavimui.

Natūralioji dedukcija 

Natūralioji dedukcija yra sekvencinis skaičiavimas su aksioma  ir taisyklėmis. Įrodymo metodas  įrodymu yra laikomas tada ir tik tada, kai jam pakanka taisyklių, kad būtų gaunama aksioma. Nagrinėjamas skaičiavimas apibendrina natūraliųjų skaičiavimų variantus ir skiriasi nuo pradinių tokio tipo skaičiavimų. Kaip ir sekvenciniame skaičiavime, sekvencija  išvedama tada ir tiktai tada, kai  tapačiai teisinga .
 
Natūraliojo skaičiavimo įrodymas paremtas implikacijos taisykle: jei  gali būti gaunama iš  pagal išvedimo taisyklę, tai   įrodyta. Implikacijos () operacijos simbolis taisyklėse žyminas  simboliu. Svarbu, kad sekvencijų dešinėje pusėje nuo paskutinės implikacijos taisyklės yra ne daugiau kaip viena formulė . 
 
Natūraliosios dedukcijos taisyklės  

Čia  yra baigtinės formulių sekos (gali būti ir tuščios).  — formulės. Taisyklių prielaidose esančių formulių tvarka yra nesvarbi. Žvaigždute pažymėtos taisyklės yra apverčiamos.

Skaičiavimai vadinami natūraliosiomis sistemomis, nes perėjimai nuo prielaidų prie išvadų modeliuoja tiek šnekamosios kalbos, tiek mokslininkų įrodymuose vartojamus samprotavimus.

Sekvencinis skaičiavimas 
Sekvencinis skaičiavimas (Gentzeno tipo sekvencinis skaičiavimas arba sekvencinis skaičiavimas ) - tai skaičiavimas su aksioma  ir taisyklėmis , , , , , , ,  .
  
Sekvencija  išvedama sekvenciniame skaičiavime, jeigu yra toks medis, kuriam teisinga : 
kiekvienoje medžio viršūnėje yra sekvencija, 
medžio šaknyje yra sekvencija , 
jei viršūnė  turi vaikus  (ir ) ir viršūnėse , (, ) yra atitinkamai sekvencijos , (, ), tai sekvencija  yra gauta pagal kurią nors sekvencinio skaičiavimo taisyklę iš sekvencijų  (ir ), 
visuose medžio lapuose yra sekvencijos, kurios yra aksiomos. 
Logikos formulė  yra tapačiai teisinga tada ir tik tada, kai sekvencija  yra išvedama sekvenciniame skaičiavime. Iš to išplaukia, jog formulė  yra tapačiai klaidinga tada ir tik tada, kai yra išvedama skaičiavime sekvencija . 
  
Aksioma: , kur  yra formulė, o  ir  yra formulių sekos (gali būti ir tuščios). 

Taisyklės:  
 
 
Čia ,  yra formulės, ,  - formulių sekos (gali būti ir tuščios). Formulių išsidėstymo tvarka nėra svarbi.

Išnašos 

Matematika
Logika