Szekvenskalkulus

A matematikai logikában, a szekvenskalkulus lényegében a formális logikai érvelés egy stílusa, ahol a bizonyítás minden sora feltételes tautológia (Gerhard Gentzen nyomán szekvensnek hívva) feltétel nélküli tautológia helyett. Minden feltételes tautológiát a korábbi sorok egyéb feltételes tautológiáiból következtetünk egy formális argumentumban, a következtetési szabályok és eljárások szerint, ezzel jobb megközelítést adva a matematikusok által használt természetes levezetési stílushoz, mint David Hilbert korábbi stílusú formális logikája, ahol minden sor feltétel nélküli tautológia volt. Előfordulhat, hogy finomabb megkülönböztetéseket kell tenni; például, előfordulhatnak nem logikus axiómák, amelyekre minden ítélet implicit módon függ. Ezután a szekvenciák a feltételes tautológiák helyett a feltételes tételeket jelzik egy elsőrendű nyelvben.

A szekvenskalkulus egyike a bizonyítási kalkulus számos létező stílusának, ami a soronkénti logikai argumentumok kifejezésére szolgál.

• Hilbert-stílus. Minden sor feltétel nélküli tautológia (vagy tétel).
• Gentzen-stílus. Minden sor feltételes tautológia (vagy tétel), amelynek nulla vagy több feltétele van a bal oldalon.
  • Természetes levezetés. Minden (feltételes) sornak pontosan egy állított ítélete van a jobb oldalon.
  • Szekvens kalkulus. Minden (feltételes) sornak nulla vagy több állított ítélete van a jobb oldalon.

Más szóval, a természetes levezetés és a szekvenskalkulus rendszerek a Gentzen-stílusú rendszerek sajátosan eltérő fajtái. A Hilbert-stílusú rendszereknek általában nagyon kevés számú következtetési szabályuk van, jobban támaszkodnak az axiómák halmazára. A Gentzen-stílusú rendszereknek általában nagyon kevés axiómájuk van, ha vannak ilyenek, inkább a szabályrendszerekre támaszkodnak.

A Gentzen-stílusú rendszerek jelentős gyakorlati és elméleti előnyökkel rendelkeznek a Hilbert-stílusú rendszerekhez képest. Például mind a természetes levezetés, mind a szekvens kalkulusrendszerek megkönnyítik az egyetemes és egzisztenciális kvantorok eliminációját és bevezetését annak érdekében, hogy a nem definiált logikai kifejezések manipulálhatók legyenek az Ítéletlogika sokkal egyszerűbb szabályai szerint. Egy tipikus argumentumban a kvantorok megszűnnek, majd az ítéletlogikát alkalmazzák a nem definiált kifejezésekre (amelyek általában szabad változókat tartalmaznak), majd a kvantorok újra bevezetésre kerülnek. Ez nagyon hasonlít a matematikai bizonyítások gyakorlatban történő végrehajtásának módjára a matematikusok szerint. A predikátum kalkulus bizonyításait általában sokkal könnyebb felfedezni ezzel a megközelítéssel, és gyakran még rövidebbek is. A természetes levezetéses rendszerek jobban megfelelnek a gyakorlati tétel-bizonyításnak. A Szekvens kalkulus rendszerek jobban megfelelnek az elméleti elemzésnek.