Logika prvního řádu - First-order logic

Logika prvního řádu- také známá jako predikátová logika , kvantifikační logika a predikátový kalkul prvního řádu- je souborem formálních systémů používaných v matematice , filozofii , lingvistice a informatice . Logika prvního řádu používá kvantifikované proměnné nad nelogickými objekty a umožňuje použití vět, které proměnné obsahují, takže místo výroků typu „Sokrates je muž“ lze mít výrazy ve formě „existuje x takové, že x je Sokrates a x je muž “, kde„ existuje je kvantifikátor, zatímco x je proměnná. Tím se odlišuje od výrokové logiky , která nepoužívá kvantifikátory ani relace ; v tomto smyslu je výroková logika základem logiky prvního řádu.

Teorie na téma je obvykle logikou prvního řádu společně se specifikovanou doménou diskurzu (nad níž se kvantifikované proměnné pohybují), konečným množstvím funkcí od této domény k sobě, konečným množstvím predikátů definovaných pro danou doménu a množinou axiomů věřil, že o nich drží. Někdy je „teorie“ chápána ve formálnějším smyslu, což je jen soubor vět v logice prvního řádu.

Adjektivum „prvního řádu“ odlišuje logiku prvního řádu od logiky vyššího řádu , ve které existují predikáty mající predikáty nebo funkce jako argumenty nebo ve kterých jsou povoleny predikátové kvantifikátory nebo kvantifikátory funkcí nebo obojí. V teoriích prvního řádu jsou predikáty často spojeny se sadami. V interpretovaných teoriích vyššího řádu mohou být predikáty interpretovány jako sady množin.

Existuje mnoho deduktivních systémů pro logiku prvního řádu, které jsou jak zvukové (tj. Všechny prokazatelné výroky platí ve všech modelech), tak úplné (tj. Všechny výroky, které jsou pravdivé ve všech modelech, jsou prokazatelné). Přestože vztah logických důsledků je pouze semidecidable , hodně pokroku bylo dosaženo v automatizovaném dokazování teorém v logice prvního řádu. Logika prvního řádu také splňuje několik metalogických vět, díky nimž je možné ji analyzovat v teorii důkazů , jako je například Löwenheim – Skolemova věta a věta kompaktnosti .

Logika prvního řádu je standardem pro formalizaci matematiky na axiomy a studuje se v základech matematiky . Peanoova aritmetika a teorie množin Zermelo – Fraenkel jsou axiomatizace teorie čísel a teorie množin do logiky prvního řádu. Žádná teorie prvního řádu však nemá sílu jednoznačně popsat strukturu s nekonečnou doménou, jako jsou přirozená čísla nebo skutečná přímka . Axiomové systémy, které plně popisují tyto dvě struktury (tj. Kategorické axiomatické systémy), lze získat v silnějších logikách, jako je logika druhého řádu .

Základy logiky prvního řádu vyvinuli nezávisle Gottlob Frege a Charles Sanders Peirce . Historie logiky prvního řádu a způsob, jakým dominuje formální logice, viz José Ferreirós (2001).

Úvod

Zatímco výroková logika se zabývá jednoduchými deklarativními výroky, logika prvního řádu navíc pokrývá predikáty a kvantifikaci .

Predikát bere jako vstup entitu nebo entity v doméně diskurzu , zatímco výstupy jsou True nebo False . Zvažte dvě věty „Sokrates je filozof“ a „Platón je filozof“. V výrokové logice jsou tyto věty nahlíženy jako nesouvisející a mohou být označovány například proměnnými jako p a q . Predikát „je filozof“ se vyskytuje v obou větách, které mají společnou strukturu „ a je filozof“. Proměnná a je v první větě vytvořena jako „Socrates“ a ve druhé větě je vytvořena jako „Platón“. Zatímco logika prvního řádu umožňuje použití predikátů, jako je v tomto případě „je filozof“, výroková logika nikoli.

Vztahy mezi predikáty lze určit pomocí logických spojek . Vezměme si například vzorec prvního řádu „pokud a je filozof, pak a je učenec“. Tento vzorec je podmíněným tvrzením, jehož hypotézou je „ a je filozof“ a závěrem „ a je učenec“. Pravdivost tohoto vzorce závisí na tom, který předmět je označen a , a na interpretacích predikátů „je filozof“ a „je učenec“.

Kvantifikátory lze použít na proměnné ve vzorci. Proměnnou a v předchozím vzorci lze univerzálně kvantifikovat například větou prvního řádu „Pro každé a , pokud a je filozof, pak a je učenec“. Univerzální quantifier „pro každého“ v této větě vyjadřuje myšlenku, že tvrzení „pokud je filozof, pak je učenec“ platí pro všechny volby .

Negace věty „Pro každé A , pokud je filozof, pak je vědec“ je logicky ekvivalent k větě „Existuje takže je filozof a není učenec“. Existenční kvantifikátor „existuje“ vyjadřuje myšlenku, že tvrzení „ je filozof a není učenec“ platí i pro nějakou volbu .

Predikáty „je filozof“ a „je učenec“ mají každý jednu proměnnou. Predikáty mohou obecně mít několik proměnných. Ve větě prvního řádu „Sokrates je učitel Platóna“ má predikát „je učitelem“ dvě proměnné.

Interpretace (nebo model) vzorce prvního řádu určuje, co jednotlivé predikáty znamenají, a entity, které mohou instancovat proměnné. Tyto entity tvoří doménu diskurzu nebo vesmíru, který je obvykle vyžadován jako neprázdná množina. Například ve výkladu s doménou diskursu sestávající ze všech lidských bytostí a predikát „je filozof“ chápán jako „Byl autorem republiky “, věta „Existuje takže je filozof“ je vidět jako pravdivý, o čemž svědčí Platón.

Syntax

Existují dvě klíčové části logiky prvního řádu. Syntaxe určuje, které konečné sekvence symbolů jsou dobře vytvořené výrazy v logiky prvního řádu, zatímco sémantiku určuje významy za těmito výrazy.

Abeceda

Na rozdíl od přirozených jazyků, jako je angličtina, je jazyk logiky prvního řádu zcela formální, takže lze mechanicky určit, zda je daný výraz dobře formován. Existují dva klíčové typy dobře vytvořených výrazů: termíny , které intuitivně představují objekty, a vzorce , které intuitivně vyjadřují predikáty, které mohou být pravdivé nebo nepravdivé. Termíny a vzorce logiky prvního řádu jsou řetězce symbolů , kde všechny symboly dohromady tvoří abecedu jazyka. Jako u všech formálních jazyků je povaha samotných symbolů mimo rámec formální logiky; jsou často považováni jednoduše za písmena a interpunkční symboly.

Je běžné rozdělit symboly abecedy na logické symboly , které mají vždy stejný význam, a nelogické symboly , jejichž význam se liší podle interpretace. Například logický symbol vždy představuje „a“; nikdy není interpretován jako „nebo“, což je reprezentováno logickým symbolem . Na druhou stranu nelogický predikátový symbol, jako je Phil ( x ), lze interpretovat tak, že znamená „ x je filozof“, „ x je muž jménem Philip“ nebo jakýkoli jiný unární predikát v závislosti na interpretaci, která je k dispozici.

Logické symboly

V abecedě je několik logických symbolů, které se liší podle autora, ale obvykle obsahují:

  • Tyto quantifier symboly: pro univerzální kvantifikaci a pro existenční kvantifikace
  • Tyto logické spojky : pro spojení , pro disjunkci , za samozřejmost , pro biconditional , ¬ pro negaci. Občas jsou zahrnuty další logické spojovací symboly. Někteří autoři používají C pq místo a E pq místo , zejména v kontextech, kde → slouží k jiným účelům. Podkova ⊃ navíc může nahradit ; trojitý pruh může nahradit ; vlnovka ( ~ ), Np nebo Fp , může nahradit ¬ ; dvojitá čára , nebo A pq může nahradit ; a ampersand & , K pq , nebo prostřední tečka, , mohou nahradit , zvláště pokud tyto symboly nejsou z technických důvodů k dispozici. (V polské notaci jsou použity výše uvedené symboly C pq , E pq , N p , A pq a K pq .)
  • Zátvorky, závorky a další symboly interpunkce. Volba takových symbolů se liší v závislosti na kontextu.
  • Nekonečná sada proměnných , často označovaných malými písmeny na konci abecedy x , y , z , .... Předpisy se často používají k rozlišení proměnných: x 0 , x 1 , x 2 , ....
  • Symbol rovnosti (někdy, symbol identity ) = (viz § rovnosti a jeho axiomy níže).

Ne všechny tyto symboly jsou povinné - stačí pouze jeden z kvantifikátorů, negace a spojky, proměnné, závorky a rovnost. Existuje řada drobných variací, které mohou definovat další logické symboly:

  • V některých případech jsou zahrnuty pravdivostní konstanty T, V pq nebo pro „true“ a F, O pq nebo pro „false“. Bez jakýchkoli takových logických operátorů valence 0 lze tyto dvě konstanty vyjádřit pouze pomocí kvantifikátorů.
  • Při jiných příležitostech jsou zahrnuty další logické spojky, jako například Shefferův zdvih , D pq (NAND) a exkluzivní nebo J pq .

Nelogické symboly

Tyto non-logické symboly představují predikáty (vztahy), funkce a konstanty v doméně projevu. Bývalo standardní praxí používat pro všechny účely fixní, nekonečnou sadu nelogických symbolů. Novější praxí je používat různé nelogické symboly podle aplikace, kterou má člověk na mysli. Proto je nutné pojmenovat sadu všech nelogických symbolů používaných v konkrétní aplikaci. Tato volba se provádí prostřednictvím podpisu .

Tradičním přístupem je mít pouze jednu, nekonečnou, sadu nelogických symbolů (jeden podpis) pro všechny aplikace. V důsledku toho v rámci tradičního přístupu existuje pouze jeden jazyk logiky prvního řádu. Tento přístup je stále běžný, zejména ve filozoficky zaměřených knihách.

  1. Pro každé celé číslo n  ≥ 0 existuje kolekce n - ary nebo n - place , predikátových symbolů . Protože představují vztahy mezi n prvky, jsou také nazývány vztahovými symboly . Pro každou aritu n máme nekonečnou zásobu:
    P n 0 , P n 1 , P n 2 , P n 3 , ...
  2. Pro každé celé číslo n  ≥ 0 existuje nekonečně mnoho n -arych funkčních symbolů :
    f n 0 , f n 1 , f n 2 , f n 3 , ...

V současné matematické logice se podpis liší podle aplikace. Typické podpisy v matematice jsou {1, ×} nebo jen {×} pro skupiny nebo {0, 1, +, ×, <} pro seřazená pole . Počet nelogických symbolů není nijak omezen. Podpis může být prázdný , konečný nebo nekonečný, dokonce nepočitatelný . Nesčetné podpisy se vyskytují například v moderních důkazech Löwenheim – Skolemovy věty .

V tomto přístupu je každý nelogický symbol jednoho z následujících typů.

  1. Symbol predikát (nebo symbol vazby ) s nějakým valencí (nebo arity , počet argumentů) větší než nebo rovno 0. Tyto jsou často označeny velkými písmeny, jako je P , Q a R .
    • Vztahy valence 0 lze identifikovat pomocí výrokových proměnných . Například P , což může znamenat jakékoli prohlášení.
    • Například P ( x ) je predikátová valenční proměnná 1. Jednou z možných interpretací je „ x je muž“.
    • Q ( x , y ) je predikátová valenční proměnná 2. Možné interpretace zahrnují „ x je větší než y “ a „ x je otec y “.
  2. Symbol funkce , s nějakým valenčním větší než nebo rovno 0. Ty jsou často označovány malými latinkou , jako je f , g a h .
    • Příklady: f ( x ) lze interpretovat jako „otec x “. V aritmetice to může znamenat "-x". V teorii množin to může znamenat „ mocninovou sadu x“. V aritmetice může g ( x , y ) znamenat „ x + y “. V teorii množin to může znamenat „spojení x a y “.
    • Funkční symboly valence 0 se nazývají konstantní symboly a často se na začátku abecedy označují malými písmeny, například a , b a c . Symbol a může znamenat Socrates. V aritmetice to může znamenat 0. V teorii množin může taková konstanta znamenat prázdnou množinu .

Tradiční přístup lze obnovit v moderním přístupu jednoduchým zadáním „vlastního“ podpisu tak, aby sestával z tradičních sekvencí nelogických symbolů.

Pravidla formace

Pravidla formace definují termíny a vzorce logiky prvního řádu. Když jsou výrazy a vzorce reprezentovány jako řetězce symbolů, lze tato pravidla použít k napsání formální gramatiky pro výrazy a vzorce. Tato pravidla jsou obecně bezkontextová (každá inscenace má na levé straně jeden symbol), kromě toho, že sada symbolů může být povolena nekonečná a může existovat mnoho počátečních symbolů, například proměnné v případě výrazů .

Podmínky

Sada výrazů je indukčně definována následujícími pravidly:

  1. Proměnné. Jakákoli proměnná je termín.
  2. Funkce. Jakýkoli výraz f ( t 1 , ..., t n ) z n argumentů (kde každý argument t i je termín a f je funkční symbol valence n ) je termín. Zejména symboly označující jednotlivé konstanty jsou symboly s nulovou funkcí, a proto jsou termíny.

Pouze výrazy, které lze získat v konečném důsledku mnoha aplikací pravidel 1 a 2, jsou termíny. Například žádný výraz zahrnující predikátový symbol není termín.

Vzorce

Sada vzorců (také nazývaných dobře formulované vzorce nebo WFF ) je indukčně definována následujícími pravidly:

  1. Predikátové symboly. Pokud P je n -ary predikátový symbol a t 1 , ..., t n jsou termíny, pak P ( t 1 , ..., t n ) je vzorec.
  2. Rovnost . Pokud je symbol rovnosti považován za součást logiky a t 1 a t 2 jsou termíny, pak t 1 = t 2 je vzorec.
  3. Negace. Pokud je vzorec, pak je vzorec.
  4. Binární spojky. Pokud a jsou vzorce, pak ( ) je vzorec. Podobná pravidla platí pro další binární logická připojení.
  5. Kvantifikátory. Pokud je vzorec a x je proměnná, pak (pro všechna x platí) a (existuje x takových ) jsou vzorce.

Pouze výrazy, které lze získat v konečném důsledku mnoha aplikací pravidel 1–5, jsou vzorce. Vzorce získané z prvních dvou pravidel jsou údajně atomové vzorce .

Například,

je vzorec, pokud f je unární funkční symbol, P unární predikátový symbol a Q ternární predikátový symbol. Na druhou stranu to není vzorec, i když je to řetězec symbolů z abecedy.

Úlohou závorek v definici je zajistit, aby jakýkoli vzorec mohl být získán pouze jedním způsobem - podle indukční definice (tj. Pro každý vzorec existuje jedinečný strom analýzy ). Tato vlastnost je známá jako jedinečná čitelnost vzorců. Existuje mnoho konvencí, kde jsou ve vzorcích použity závorky. Někteří autoři například používají místo závorek dvojtečky nebo tečky nebo mění místa, do kterých jsou vloženy závorky. Ke každé konkrétní definici autora musí být přiložen doklad o jedinečné čitelnosti.

Tato definice vzorce nepodporuje definování funkce if-then-else ite(c, a, b), kde „c“ je podmínka vyjádřená jako vzorec, která by vrátila „a“, je-li c pravdivá, a „b“, pokud je nepravdivá. Důvodem je, že predikáty i funkce mohou jako parametry přijímat pouze výrazy, ale prvním parametrem je vzorec. Některé jazyky postavené na logice prvního řádu, například SMT-LIB 2.0, to přidávají.

Notační konvence

Pro pohodlí byly vyvinuty konvence o přednostech logických operátorů, aby se v některých případech vyhnula nutnosti psát závorky. Tato pravidla jsou podobná pořadí operací v aritmetice. Běžnou konvencí je:

  • je vyhodnocen jako první
  • a jsou vyhodnoceny dále
  • Dále jsou vyhodnoceny kvantifikátory
  • je vyhodnocen jako poslední.

Kromě toho lze vložit další interpunkci, která definice nevyžaduje - aby se vzorce snáze četly. Tedy vzorec

může být napsáno jako

V některých oblastech je obvyklé používat pro binární relace a funkce infixovou notaci namísto výše definované předponové notace. Například v aritmetice typicky píše „2 + 2 = 4“ místo „= ( + (2,2), 4)“. Je běžné považovat vzorce v infixovém zápisu za zkratky pro odpovídající vzorce v předponovém zápisu, srov. také struktura termínu vs. reprezentace .

Výše uvedené definice používají zápis infixů pro binární spojky, jako např . Méně časté konvence je polská notace , ve kterém jeden píše , a tak dále v přední části svých argumentů spíše než mezi nimi. Tato konvence je výhodná v tom, že umožňuje zahodit všechny symboly interpunkce. Polský zápis jako takový je kompaktní a elegantní, ale v praxi se používá jen zřídka, protože je pro lidi těžké číst. V polské notaci vzorec

se stává „∀x∀y → Pfx¬ → PxQfyxz“.

Volné a vázané proměnné

Ve vzorci může být proměnná volná nebo vázaná (nebo obojí). Intuitivně je výskyt proměnné ve vzorci volný, pokud není kvantifikován: v y P ( x , y ) je jediný výskyt proměnné x volný, zatímco y je vázán. Výskyty volných a vázaných proměnných ve vzorci jsou definovány indukčně následovně.

Atomové vzorce
Pokud φ je atomový vzorec, pak se x vyskytuje volně v φ právě tehdy, když se x vyskytuje v φ . Navíc v žádném atomovém vzorci nejsou žádné vázané proměnné.
Negace
x se vyskytuje volně v ¬ φ právě tehdy, když se x vyskytuje volně v φ . x se vyskytuje vázané v ¬ φ právě tehdy, když se x vyskytuje vázané v φ
Binární spojky
x se vyskytuje volně v ( φψ ) právě tehdy, když se x vyskytuje volně v φ nebo ψ . x se vyskytuje vázané v ( φψ ) právě tehdy, když se x vyskytuje vázané buď v φ nebo ψ . Stejné pravidlo platí pro jakékoli jiné binární spojivo místo →.
Kvantifikátory
x se vyskytuje volně v y φ , právě tehdy, když se x vyskytuje volně v φ a x je jiný symbol než y . Také x se vyskytuje vázané v y φ , právě tehdy, když x je y nebo x se vyskytuje vázané v φ . Stejné pravidlo platí i pro místo .

Například v xy ( P ( x ) → Q ( x , f ( x ), z )) , x a y vyskytují vázán pouze z dochází pouze volný, a w , ani proto, že nedochází v vzorec.

Volné a vázané proměnné vzorce nemusí být disjunktní množiny: ve vzorci P ( x ) → ∀ x Q ( x ) je první výskyt x jako argumentu P volný, zatímco druhý jako argument Q , vázána.

Vzorec v logice prvního řádu bez volných výskytů proměnných se nazývá věta prvního řádu . Toto jsou vzorce, které budou mít při interpretaci dobře definované pravdivostní hodnoty . Například to, zda je vzorec, jako je Phil ( x ), pravdivý, musí záviset na tom, co x představuje. Ale věta x Phil ( x ) bude v dané interpretaci buď pravdivá, nebo nepravdivá.

Příklad: seřazené abelianské skupiny

V matematice má jazyk uspořádaných abelianských skupin jeden konstantní symbol 0, jeden unární funkční symbol -, jeden symbol binární funkce +a jeden symbol binární relace ≤. Pak:

  • Výrazy +( x , y ) a +( x , +( y , - ( z ))) jsou termíny . Obvykle se zapisují jako x + y a x + y - z .
  • Výrazy +( x , y ) = 0 a ≤ ( +( x , +( y , - ( z ))), +( x , y )) jsou atomové vzorce . Ty se obvykle zapisují jako x + y = 0 a x + y - z  ≤  x + y .
  • Výraz je vzorec , který se obvykle zapisuje jako Tento vzorec má jednu volnou proměnnou, z .

Axiomy pro uspořádané abelianské skupiny mohou být vyjádřeny jako sada vět v jazyce. Obvykle je například napsán axiom, který uvádí, že skupina je komutativní

Sémantika

Výklad jazyka prvního řádu přiřadí denotaci ke každému non-logický symbol v tomto jazyce. Rovněž určuje doménu diskurzu, která určuje rozsah kvantifikátorů. Výsledkem je, že každému výrazu je přiřazen objekt, který představuje, každému predikátu je přiřazena vlastnost objektů a každé větě je přiřazena pravdivostní hodnota. Tímto způsobem interpretace poskytuje sémantický význam termínům, predikátům a vzorcům jazyka. Studium výkladů formálních jazyků se nazývá formální sémantika . Následuje popis standardní nebo tarskovské sémantiky pro logiku prvního řádu. (Je také možné definovat sémantiku hry pro logiku prvního řádu , ale kromě vyžadování axiomu volby souhlasí sémantika hry s tarskovskou sémantikou pro logiku prvního řádu, takže sémantika hry zde nebude zpracována.)

Doménou diskurzu D je neprázdná sada „objektů“ nějakého druhu. Intuitivně je vzorec prvního řádu tvrzením o těchto objektech; například uvádí existenci objektu x tak, že predikát P je pravdivý, pokud je na něj odkazován. Doménou diskurzu je množina uvažovaných objektů. Například může být množina celočíselných čísel.

Interpretace symbolu funkce je funkce. Pokud například doména diskurzu sestává z celých čísel, symbol funkce f arity 2 lze interpretovat jako funkci, která udává součet jejích argumentů. Jinými slovy, symbol f je spojen s funkcí, která je v této interpretaci navíc.

Interpretace konstantní symbol je funkce z jednoho prvku nastavené D 0D , která může být identifikována s objektem v D . Interpretace může například přiřadit hodnotu konstantnímu symbolu .

Interpretace n -arytního predikátového symbolu je množina n - n -tic prvků oblasti diskurzu. To znamená, že s ohledem na interpretaci, predikátový symbol a n prvků oblasti diskurzu lze podle dané interpretace zjistit, zda je predikát pro tyto prvky pravdivý. Například interpretace I (P) binárního predikátového symbolu P může být množinou párů celých čísel tak, že první je menší než druhý. Podle této interpretace by predikát P byl pravdivý, pokud by jeho první argument byl menší než druhý.

Struktury prvního řádu

Nejběžnějším způsobem určení interpretace (zejména v matematice) je určit strukturu (také nazývanou model ; viz níže). Struktura se skládá z neprázdné množiny D, která tvoří doménu diskurzu, a interpretace I nelogických podmínek podpisu. Tato interpretace je sama o sobě funkcí:

  • Každá funkce symbol f arity n je přiřazena funkce z až D . Zejména je každému konstantnímu symbolu podpisu přiřazena osoba v doméně diskurzu.
  • Každému predikátovému symbolu P arity n je přiřazen vztah k nebo, ekvivalentně, funkci od do . Tím je každý predikát symbol interpretován Logická hodnotou funkce na D .

Vyhodnocení pravdivostních hodnot

Vzorec se vyhodnotí jako pravdivý nebo nepravdivý vzhledem k interpretaci a přiřazení proměnné μ, které ke každé proměnné přiřadí prvek oblasti diskurzu. Důvodem, proč je požadováno přiřazení proměnné, je dávat významy vzorcům s volnými proměnnými, jako je například . Pravdivostní hodnota tohoto vzorce se mění podle toho, zda x a y označují stejného jedince.

Nejprve lze variabilní přiřazení μ rozšířit na všechny termíny jazyka, což má za následek, že každý termín se mapuje na jeden prvek domény diskurzu. K provedení tohoto úkolu se používají následující pravidla:

  1. Proměnné. Každá proměnná x se vyhodnotí na μ ( x )
  2. Funkce. Vzhledem k výrazům , které byly vyhodnoceny jako prvky domény diskurzu, a symbolu n -arytní funkce f se termín vyhodnotí jako .

Dále je každému vzorci přiřazena pravdivostní hodnota. Indukční definice použitá k provedení tohoto přiřazení se nazývá T-schéma .

  1. Atomové vzorce (1). Vzorce je přiřazena hodnota pravdivá nebo nepravdivá v závislosti na tom , zda , kde jsou hodnocení pojmů a je interpretace , která je za předpokladu podmnožinou .
  2. Atomové vzorce (2). Vzorec je přiřazen true if a vyhodnocen ke stejnému objektu domény diskurzu (viz část o rovnosti níže).
  3. Logická spojení. Vzorec ve formě , atd je hodnocena podle pravdivostní tabulky pro pojivové se jedná, jak je ve výrokové logice.
  4. Existenciální kvantifikátory. Vzorec je pravdivý podle M a pokud existuje hodnocení proměnných, které se liší pouze od hodnocení x a takové, že φ je pravdivé podle interpretace M a přiřazení proměnné . Tato formální definice zachycuje myšlenku, která je pravdivá tehdy a jen tehdy, pokud existuje způsob, jak zvolit hodnotu pro x tak, aby byla splněna φ ( x ).
  5. Univerzální kvantifikátory. Vzorec platí podle M a pokud φ ( x ) platí pro každý pár složený z interpretace M a nějakého přiřazení proměnné, které se liší pouze od hodnoty x . To zachycuje myšlenku, která je pravdivá, pokud každá možná volba hodnoty pro x způsobí, že φ ( x ) je pravdivé.

Pokud vzorec neobsahuje volné proměnné, stejně jako věta, pak počáteční přiřazení proměnné neovlivní jeho pravdivostní hodnotu. Jinými slovy, věta je pravdivá podle M a právě tehdy, pokud je pravdivá podle M a každého dalšího přiřazení proměnné .

Existuje druhý běžný přístup k definování pravdivostních hodnot, který nespoléhá na funkce proměnného přiřazení. Místo toho, vzhledem k interpretaci M , jeden nejprve přidá k podpisu soubor konstantních symbolů, jeden pro každý prvek oblasti diskurzu v M ; řekněme, že pro každé d v doméně je fixní konstantní symbol c d . Interpretace je rozšířena tak, že každému novému konstantnímu symbolu je přiřazen odpovídající prvek domény. Nyní se syntakticky definuje pravda pro kvantifikované vzorce takto:

  1. Existenciální kvantifikátory (alternativní). Vzorec je pravdivý podle M, pokud existuje nějaké d v doméně diskurzu, který platí. Zde je výsledek nahrazení c d za každý volný výskyt x v φ.
  2. Univerzální kvantifikátory (alternativní). Vzorec platí podle M , jestliže pro každou d v doméně projevu, je pravda, podle M .

Tento alternativní přístup dává všem větám přesně stejné pravdivostní hodnoty jako přístup prostřednictvím proměnných přiřazení.

Platnost, uspokojitelnost a logické důsledky

Pokud se věta φ vyhodnotí jako pravdivá při dané interpretaci M , říká se, že M splňuje φ; toto je označeno . Věta je uspokojivá, pokud existuje nějaký výklad, podle kterého je pravdivá.

Uspokojitelnost vzorců s volnými proměnnými je složitější, protože interpretace sama o sobě neurčuje pravdivostní hodnotu takového vzorce. Nejběžnější konvencí je, že vzorec s volnými proměnnými je údajně uspokojen interpretací, pokud vzorec zůstane pravdivý bez ohledu na to, kteří jednotlivci z oblasti diskurzu jsou přiřazeni jeho volným proměnným. To má stejný účinek, jako říkat, že vzorec je splněn tehdy a jen tehdy, když je splněno jeho univerzální uzavření .

Vzorec je logicky platný (nebo jednoduše platný ), pokud je pravdivý v každé interpretaci. Tyto vzorce hrají roli podobnou tautologiím ve výrokové logice.

Formule φ je logickým důsledkem vzorce ψ, pokud každá interpretace, která činí ψ pravdivou, také činí φ pravdivou. V tomto případě se říká, že φ je logicky implikováno ψ.

Algebraizace

Alternativní přístup k sémantice logiky prvního řádu probíhá prostřednictvím abstraktní algebry . Tento přístup generalizuje Lindenbaum -Tarskiho algebry výrokové logiky. Existují tři způsoby eliminace kvantifikovaných proměnných z logiky prvního řádu, které nezahrnují nahrazení kvantifikátorů jinými operátory termínů vázajících proměnné:

Tyto algebry jsou všechny mříže, které řádně rozšiřují dvouprvkovou booleovskou algebru .

Tarski a Givant (1987) ukázali, že fragment logiky prvního řádu, který nemá atomovou větu ležící v rozsahu více než tří kvantifikátorů, má stejnou výrazovou sílu jako relační algebra . Tento fragment je velmi zajímavý, protože postačuje pro Peanovu aritmetickou a nejvíce axiomatickou teorii množin , včetně kanonického ZFC . Dokazují také, že logika prvního řádu s primitivní uspořádanou dvojicí je ekvivalentní relační algebře se dvěma funkcemi projekce uspořádané dvojice .

Teorie, modely a základní třídy prvního řádu

Teorie prvního řádu konkrétního podpisu je množina axiomů , které jsou věty se skládají z symbolů z tohoto podpisu. Sada axiomů je často konečná nebo rekurzivně vyčíslitelná , v takovém případě se teorie nazývá efektivní . Někteří autoři vyžadují, aby teorie zahrnovaly také všechny logické důsledky axiomů. Axiomy jsou považovány za držené v teorii a z nich lze odvodit další věty, které v teorii platí.

Struktura prvního řádu, která splňuje všechny věty v dané teorii, je údajně modelem teorie. Základní třída je množina všech konstrukcí, které splňují určité teorii. Tyto třídy jsou hlavním předmětem studia v modelové teorii .

Mnoho teorií má zamýšlenou interpretaci , určitý model, který je při studiu teorie pamatován. Například zamýšlená interpretace Peanoovy aritmetiky se skládá z obvyklých přirozených čísel s jejich obvyklými operacemi. Věta Löwenheim – Skolem však ukazuje, že většina teorií prvního řádu bude mít i jiné, nestandardní modely .

Teorie je konzistentní, pokud není možné prokázat rozpor s axiomy teorie. Teorie je úplná, jestliže pro každý vzorec v jejím podpisu je buďto tento vzorec nebo jeho negace logickým důsledkem axiomů teorie. Gödelova věta o neúplnosti ukazuje, že efektivní teorie prvního řádu, které obsahují dostatečnou část teorie přirozených čísel, nemohou být nikdy konzistentní ani úplné.

Další informace k tomuto tématu naleznete v Seznamu teorií a teorie prvního řádu a teorie (matematická logika)

Prázdné domény

Výše uvedená definice vyžaduje, aby doména diskurzu jakékoli interpretace byla neprázdná. Existují nastavení, jako je například logika , kde jsou povoleny prázdné domény. Navíc pokud třída algebraických struktur obsahuje prázdnou strukturu (například existuje prázdná množina ), tato třída může být elementární třídou v logice prvního řádu pouze tehdy, jsou-li povoleny prázdné domény nebo je-li prázdná struktura ze třídy odstraněna .

S prázdnými doménami však existuje několik potíží:

  • Mnoho společných pravidel odvozování je platných pouze tehdy, když je požadována doména diskurzu, že je neprázdná. Jedním z příkladů je pravidlo o tom, že znamená, pokud x není volná proměnná . Toto pravidlo, které se používá k převedení vzorců do normální formy prenexu , je v prázdných doménách zdravé, ale pokud je prázdná doména povolena, je nezdravé.
  • Definice pravdy v interpretaci, která používá funkci proměnného přiřazení, nemůže fungovat s prázdnými doménami, protože neexistují žádné funkce přiřazení proměnných, jejichž rozsah je prázdný. (Podobně nelze přiřazovat interpretace ke konstantním symbolům.) Tato definice pravdy vyžaduje, aby člověk před definováním pravdivostních hodnot pro sudé atomové vzorce vybral proměnnou funkci přiřazení (μ výše). Potom je pravdivostní hodnota věty definována jako její pravdivostní hodnota při jakémkoli variabilním přiřazení a je dokázáno, že tato pravdivostní hodnota nezávisí na tom, které přiřazení je vybráno. Tato technika nefunguje, pokud vůbec neexistují žádné přiřazovací funkce; musí být změněn, aby vyhovoval prázdným doménám.

Když je tedy prázdná doména povolena, musí být často považována za zvláštní případ. Většina autorů však prázdnou doménu podle definice jednoduše vylučuje.

Deduktivní systémy

Odvozovací systém se používá k prokázání, na čistě syntaktické bázi, že jeden vzorec je logickým důsledkem jiného vzorce. Existuje mnoho takových systémů pro logiku prvního řádu, včetně dedukčních systémů ve stylu Hilberta , přirozené dedukce , sekvenčního počtu , metody tableaux a rozlišení . Tito sdílejí společnou vlastnost, že odpočet je konečný syntaktický objekt; formát tohoto objektu a způsob jeho konstrukce se velmi liší. Těmto konečným dedukcím se v teorii důkazů často říká derivace . Často se jim také říká důkazy, ale na rozdíl od matematických důkazů v přirozeném jazyce jsou zcela formalizovány .

Deduktivní systém je zdravý, pokud je logicky platný jakýkoli vzorec, který lze v systému odvodit. Naopak, deduktivní systém je úplný, pokud je každý logicky platný vzorec odvozitelný. Všechny systémy popsané v tomto článku jsou zdravé a úplné. Rovněž sdílejí majetek, že je možné účinně ověřit, že údajně platný odpočet je ve skutečnosti odpočet; takové systémy odpočtu se nazývají efektivní .

Klíčovou vlastností deduktivních systémů je, že jsou čistě syntaktické, takže derivace lze ověřit bez ohledu na jakoukoli interpretaci. Zvukový argument je tedy správný v každé možné interpretaci jazyka, bez ohledu na to, zda se tato interpretace týká matematiky, ekonomiky nebo nějaké jiné oblasti.

Obecně platí, že logický důsledek v logice prvního řádu je pouze semidecidable : pokud věta A logicky implikuje větu B, pak to lze zjistit (například hledáním důkazu, dokud není nalezen, pomocí nějakého efektivního, zdravého a úplného důkazu Systém). Pokud však A logicky neznamená B, neznamená to, že A logicky implikuje negaci B. Neexistuje účinný postup, který by podle vzorců A a B vždy správně rozhodl, zda A logicky implikuje B.

Pravidla odvozování

Pravidlo inference uvádí, že jelikož konkrétní vzorec (nebo skupina vzorce) s určitou vlastnost jako hypotéza, jiný specifický vzorec (nebo sadu vzorců), mohou být odvozeny jako závěr. Pravidlo je zdravé (nebo zachovávající pravdu), pokud zachovává platnost v tom smyslu, že kdykoli jakákoli interpretace uspokojí hypotézu, tato interpretace také uspokojí závěr.

Jedním z běžných pravidel odvozování je například pravidlo substituce . Pokud t je termín, a φ je vzorec, který může obsahovat proměnné x , pak φ [ t / x ] je výsledkem nahrazení všech volných výskyty x o t v cp. Substituční pravidlo uvádí, že pro jakýkoli φ a jakýkoli termín t lze z φ uzavřít φ [ t / x ] za předpokladu, že se během substitučního procesu neváže žádná volná proměnná t . (Pokud se nějaká volná proměnná t stane vázanou, pak k nahrazení t za x je nejprve nutné změnit vázané proměnné φ, aby se lišily od volných proměnných t .)

Chcete -li zjistit, proč je omezení omezených proměnných nutné, zvažte logicky platný vzorec φ daný vztahem (0,1,+, ×, =) aritmetiky. Pokud t je výraz „x + 1“, je vzorec φ [ t / y ] , což bude v mnoha interpretacích nepravdivé. Problém je v tom, že volná proměnná x z t se během substituce vázala. Zamýšlenou náhradu lze získat přejmenováním vázané proměnné x z φ na něco jiného, ​​řekněme z , takže vzorec po substituci je , což je opět logicky platné.

Substituční pravidlo ukazuje několik běžných aspektů odvozovacích pravidel. Je zcela syntaktický; bez odvolání k jakémukoli výkladu lze říci, zda byla správně použita. Má (syntakticky definovaná) omezení, kdy může být použita, která musí být respektována, aby byla zachována správnost derivací. Navíc, jak se často stává, jsou tato omezení nezbytná kvůli interakcím mezi volnými a vázanými proměnnými, ke kterým dochází během syntaktických manipulací vzorců zahrnutých do odvozovacího pravidla.

Systémy ve stylu Hilberta a přirozená dedukce

Odpočet v deduktivním systému ve stylu Hilberta je seznam vzorců, z nichž každý je logickým axiomem , hypotézou, která byla předpokládána pro odvození na dosah ruky, nebo vyplývá z předchozích vzorců pomocí pravidla odvozování. Logické axiomy se skládají z několika schémat axiomů logicky platných vzorců; tyto zahrnují značné množství výrokové logiky. Pravidla odvození umožňují manipulaci s kvantifikátory. Typické systémy ve stylu Hilberta mají malý počet pravidel odvozování spolu s několika nekonečnými schématy logických axiomů. Je obvyklé mít jako modus odvození pouze modus ponens a univerzální zobecnění .

Přirozené dedukční systémy připomínají systémy ve stylu Hilberta v tom, že dedukce je konečný seznam vzorců. Systémy přirozené dedukce však nemají žádné logické axiomy; kompenzují přidáním dalších odvozovacích pravidel, která lze použít k manipulaci s logickými spojkami ve vzorcích v důkazu.

Sekvenční počet

Sekvenční počet byl vyvinut ke studiu vlastností přirozených dedukčních systémů. Namísto práce s jedním vzorcem najednou používá sekvence , což jsou výrazy formuláře

kde A 1 , ..., A n , B 1 , ..., B k jsou vzorce a symbol turniketu se používá jako interpunkce k oddělení obou polovin. Intuitivně sekvence vyjadřuje myšlenku, která z ní vyplývá .

Tableauxova metoda

Tableaux proof for the propositional formula ((a ∨ ¬b) ∧ b) → a.

Na rozdíl od právě popsaných metod nejsou derivace v metodě tableaux seznamy vzorců. Místo toho je derivace stromem vzorců. Aby se ukázalo, že vzorec A je prokazatelný, metoda tableaux se pokouší prokázat, že negace A je neuspokojivá. Strom odvození má svůj kořen; větve stromu způsobem, který odráží strukturu vzorce. Například ukázat, že je neuspokojitelný, vyžaduje ukázat, že C a D jsou neuspokojitelné; to odpovídá bodu větvení ve stromu s rodiči a dětmi C a D.

Řešení

Pravidlo rozlišení je jediné pravidlo odvozování, které je spolu s unifikací zdravé a úplné pro logiku prvního řádu. Stejně jako u metody tableaux je vzorec prokázán ukázkou, že negace vzorce je neuspokojivá. Rozlišení se běžně používá v automatizovaném dokazování teorémů.

Metoda rozlišení funguje pouze se vzorci, které jsou disjunkce atomových vzorců; libovolné vzorce je třeba nejprve převést do této formy prostřednictvím Skolemizace . Pravidlo rozlišení uvádí, že z hypotéz a lze vyvodit závěr .

Prokazatelné identity

Lze dokázat mnoho identit, které vytvářejí ekvivalenty mezi konkrétními vzorci. Tyto identity umožňují přeskupení vzorců přesunutím kvantifikátorů přes jiné spojky a jsou užitečné pro uvedení vzorců do normální formy prenexu . Některé prokazatelné identity zahrnují:

(kde se nesmí vyskytovat zdarma v )
(kde se nesmí vyskytovat zdarma v )

Rovnost a její axiomy

Existuje několik různých konvencí pro používání rovnosti (nebo identity) v logice prvního řádu. Nejběžnější konvence, známá jako logika prvního řádu s rovností , zahrnuje symbol rovnosti jako primitivní logický symbol, který je vždy interpretován jako skutečný vztah rovnosti mezi členy domény diskurzu, takže „dva“ dané členy jsou stejný člen. Tento přístup také přidává do použitého deduktivního systému určité axiomy o rovnosti. Tyto axiomy rovnosti jsou:

  1. Reflexivita . U každé proměnné x , x = x .
  2. Náhrada funkcí. Pro všechny proměnné x a y a všechny funkční symboly f ,
    x = yf (..., x , ...) = f (..., y , ...).
  3. Náhrada za vzorce . Pro libovolné proměnné x a y a pro jakýkoli vzorec φ ( x ), je -li φ 'získáno nahrazením libovolného počtu volných výskytů x v φ y , tak, že tyto zůstávají volnými výskyty y , pak
    x = y → (φ → φ ').

Toto jsou schémata axiomů , z nichž každé určuje nekonečnou sadu axiomů. Třetí schéma je známé jako Leibnizův zákon , „princip substitučnosti“, „nerozeznatelnost identik“ nebo „náhradní vlastnost“. Druhé schéma, zahrnující funkční symbol f , je (ekvivalent) speciálním případem třetího schématu pomocí vzorce

x = y → ( f (..., x , ...) = z → f (..., y , ...) = z).

Mnoho dalších vlastností rovnosti je důsledkem výše uvedených axiomů, například:

  1. Symetrie. Pokud x = y, pak y = x .
  2. Přechodnost. Pokud x = y a y = z, pak x = z .

Logika prvního řádu bez rovnosti

Alternativní přístup považuje vztah rovnosti za nelogický symbol. Tato konvence je známá jako logika prvního řádu bez rovnosti . Pokud je v podpisu zahrnut vztah rovnosti, musí být nyní axiomy rovnosti přidány k uvažovaným teoriím, pokud je to žádoucí, místo aby byly považovány za pravidla logiky. Hlavní rozdíl mezi touto metodou a logikou prvního řádu s rovnoprávností spočívá v tom, že interpretace může nyní interpretovat dva odlišné jedince jako „rovnocenné“ (i když podle Leibnizova zákona tyto uspokojí přesně stejné vzorce při jakékoli interpretaci). To znamená, že vztah rovnosti může být nyní interpretován vztahem libovolné ekvivalence v oblasti diskurzu, který je shodný s ohledem na funkce a vztahy interpretace.

Když se postupuje podle této druhé konvence, termín normální model se používá k označení interpretace, kde žádné odlišné jedince a a b nesplňují a = b . V logice prvního řádu s rovností se berou v úvahu pouze normální modely, a proto neexistuje žádný jiný model než normální model. Když je studována logika prvního řádu bez rovnosti, je nutné upravit výsledky, jako je Löwenheim – Skolemova věta, tak, aby byly brány v úvahu pouze normální modely.

Logika prvního řádu bez rovnosti se často používá v kontextu aritmetiky druhého řádu a dalších teorií aritmetiky vyššího řádu, kde se obvykle vynechává vztah rovnosti mezi množinami přirozených čísel.

Definování rovnosti v rámci teorie

Pokud má teorie binární vzorec A ( x , y ), který splňuje reflexivitu a Leibnizův zákon, říká se, že teorie má rovnost, nebo je to teorie s rovností. Teorie nemusí mít všechny instance výše uvedených schémat jako axiomy, ale spíše jako odvozitelné věty. Například v teoriích bez funkčních symbolů a konečného počtu vztahů je možné definovat rovnost z hlediska vztahů definováním dvou pojmů s a t, aby byly stejné, pokud se jakýkoli vztah nezmění změnou s na t v jakýkoli argument.

Některé teorie umožňují další ad hoc definice rovnosti:

  • V teorii dílčích řádů s jedním vztahovým symbolem ≤ by bylo možné definovat s = t jako zkratku pro stts .
  • V teorii množin s jedním vztahem ∈ lze definovat s = t jako zkratku pro x ( sxtx ) ∧ ∀ x ( xsxt ) . Tato definice rovnosti pak automaticky splňuje axiomy pro rovnost. V tomto případě je třeba nahradit obvyklý axiom extenze , který lze uvést jako , alternativní formulací , která říká, že pokud sady x a y mají stejné prvky, pak také patří do stejných množin.

Metalogické vlastnosti

Jednou z motivací pro použití logiky prvního řádu namísto logiky vyššího řádu je, že logika prvního řádu má mnoho metalogických vlastností, které silnější logika nemá. Tyto výsledky se týkají spíše obecných vlastností samotné logiky prvního řádu než vlastností jednotlivých teorií. Poskytují základní nástroje pro konstrukci modelů teorií prvního řádu.

Úplnost a nerozhodnutelnost

Gödelova věta o úplnosti , kterou dokázal Kurt Gödel v roce 1929, stanoví, že existují logické, úplné a účinné deduktivní systémy pro logiku prvního řádu, a tedy vztah logického důsledku prvního řádu je zachycen konečnou prokazatelností. Naivně tvrzení, že vzorec φ logicky implikuje vzorec ψ, závisí na každém modelu φ; tyto modely budou mít obecně libovolně velkou mohutnost, a logické důsledky tedy nelze účinně ověřit kontrolou každého modelu. Je však možné vyjmenovat všechny konečné derivace a hledat derivaci ψ z φ. Pokud ψ je logicky implikováno φ, taková derivace bude nakonec nalezena. Logický důsledek prvního řádu je tedy semidecidovatelný : je možné provést efektivní výčet všech dvojic vět (φ, ψ) tak, že ψ je logickým důsledkem φ.

Na rozdíl od výrokové logiky je logika prvního řádu nerozhodnutelná (i když polorozhodnutelná) za předpokladu, že jazyk má alespoň jeden predikát arity alespoň 2 (jiný než rovnost). To znamená, že neexistuje žádný rozhodovací postup, který by určoval, zda jsou libovolné vzorce logicky platné. Tento výsledek nezávisle stanovili Alonzo Church a Alan Turing v letech 1936 a 1937, což dalo negativní odpověď na problém Entscheidungs, který představovali David Hilbert a Wilhelm Ackermann v roce 1928. Jejich důkazy ukazují souvislost mezi neřešitelností problému rozhodování pro první- logika řádu a neřešitelnost problému zastavení .

Existují systémy slabší než úplná logika prvního řádu, pro které je rozhodnutelný vztah logických důsledků. Patří sem výroková logika a monadická predikátová logika , což je logika prvního řádu omezená na unární predikátové symboly a žádné funkční symboly. Další logiky bez funkčních symbolů, o nichž lze rozhodnout, jsou střežený fragment logiky prvního řádu a logika dvou proměnných . Třída Bernays-Schönfinkel prvního řádu vzorců je také decidable. Rozhodovací podmnožiny logiky prvního řádu jsou studovány také v rámci logiky popisu .

Věta Löwenheim – Skolem

Tyto Löwenheim-Skolem věta ukazuje, že v případě, že teorie prvního pořadí mohutnosti lambda má nekonečný modelu, pak to má modelů každého nekonečného mohutnost větší než nebo rovný do lambda. Jeden z prvních výsledků v modelové teorii , to znamená, že není možné charakterizovat počitatelnost nebo nespočitatelnost v jazyce prvního řádu s počitatelným podpisem. To znamená, že neexistuje vzorec prvního řádu φ ( x ) tak, aby libovolná struktura M splňovala φ právě tehdy, pokud je doména diskursu M spočitatelná (nebo, v druhém případě, nepočitatelná).

Věta Löwenheim – Skolem naznačuje, že nekonečné struktury nelze v logice prvního řádu kategoricky axiomatizovat. Například neexistuje teorie prvního řádu, jejímž jediným modelem je skutečná linie: jakákoli teorie prvního řádu s nekonečným modelem má také model mohutnosti větší než kontinuum. Protože skutečná přímka je nekonečná, jakákoli teorie uspokojená skutečnou přímkou ​​je také uspokojena některými nestandardními modely . Když se na teorie množin prvního řádu aplikuje Löwenheim – Skolemova věta, neintuitivní důsledky jsou známy jako Skolemův paradox .

Věta o kompaktnosti

Tyto kompaktnost věta uvádí, že sada prvního řádu vět má model, tehdy a jen tehdy, pokud každý konečný podmnožina má model. To znamená, že pokud je vzorec logickým důsledkem nekonečné množiny axiomů prvního řádu, pak je to logický důsledek určitého konečného počtu těchto axiomů. Tuto větu poprvé prokázal Kurt Gödel jako důsledek věty o úplnosti, ale postupem času bylo získáno mnoho dalších důkazů. Je to ústřední nástroj v teorii modelů a poskytuje základní metodu pro konstrukci modelů.

Věta kompaktnosti má omezující účinek na to, že kolekce struktur prvního řádu jsou elementární třídy. Například z věty o kompaktnosti vyplývá, že jakákoli teorie, která má libovolně velké konečné modely, má nekonečný model. Třída všech konečných grafů tedy není elementární třídou (totéž platí pro mnoho dalších algebraických struktur).

Existuje také jemnější omezení logiky prvního řádu, která jsou implikována větou o kompaktnosti. Například v informatice lze mnoho situací modelovat jako směrovaný graf stavů (uzlů) a spojů (směrované hrany). Ověření takového systému může vyžadovat prokázání, že z žádného „dobrého“ stavu nelze dosáhnout žádného „špatného“ stavu. Snaží se tedy určit, zda jsou dobré a špatné stavy v různých spojených částech grafu. Větu kompaktnosti však lze použít k ukázání, že spojené grafy nejsou v logice prvního řádu elementární třídou, a neexistuje logika vzorce φ ( x , y ) logiky prvního řádu, která v logice grafů vyjadřuje představa, že existuje cesta od x k y . Propojenost může být vyjádřena v logice druhého řádu , ale ne pouze s existenciálními množinovými kvantifikátory, protože má také kompaktnost.

Lindströmova věta

Per Lindström ukázal, že právě diskutované metalogické vlastnosti ve skutečnosti charakterizují logiku prvního řádu v tom smyslu, že tyto vlastnosti nemůže mít ani žádná silnější logika (Ebbinghaus a Flum 1994, kapitola XIII). Lindström definoval třídu abstraktních logických systémů a přísnou definici relativní síly člena této třídy. Pro systémy tohoto typu založil dvě věty:

  • Logický systém splňující Lindströmovu definici, který obsahuje logiku prvního řádu a splňuje jak Löwenheim – Skolemovu větu, tak větu o kompaktnosti, musí být ekvivalentní logice prvního řádu.
  • Logický systém splňující Lindströmovu definici, který má semidecidovatelný logický důsledkový vztah a splňuje Löwenheim – Skolemovu větu, musí být ekvivalentní logice prvního řádu.

Omezení

Ačkoli logika prvního řádu postačuje k formalizaci velké části matematiky a běžně se používá v informatice a dalších oborech, má určitá omezení. Patří sem omezení jeho expresivity a omezení fragmentů přirozených jazyků, které dokáže popsat.

Například logika prvního řádu je nerozhodnutelná, což znamená, že není možný spolehlivý, úplný a ukončovací rozhodovací algoritmus prokazatelnosti. To vedlo ke studiu zajímavých rozhoditelných fragmentů, jako je C 2 : logika prvního řádu se dvěma proměnnými a počítacími kvantifikátory a .

Expresivita

Tyto löwenheimova-skolemova věta ukazuje, že pokud se teorie prvního řádu má nějakou nekonečnou modelu, pak to má nekonečné modely každého mohutnosti. Zejména žádná teorie prvního řádu s nekonečným modelem nemůže být kategorická . Neexistuje tedy teorie prvního řádu, jejíž jediný model má jako doménu množinu přirozených čísel nebo jehož jediný model má jako doménu množinu reálných čísel. Mnoho rozšíření logiky prvního řádu, včetně infinitární logiky a logiky vyššího řádu, je výraznějších v tom smyslu, že umožňují kategorické axiomatizace přirozených čísel nebo reálných čísel. Tato expresivita však stojí za metalogické náklady: podle Lindströmovy věty nemůže věta o kompaktnosti a sestupná věta Löwenheim – Skolem v žádné logice obstát silněji než první řád.

Formalizace přirozených jazyků

Logika prvního řádu je schopna formalizovat mnoho jednoduchých kvantifikačních konstrukcí v přirozeném jazyce, například „každý člověk, který žije v Perthu, žije v Austrálii“. Existuje však mnoho komplikovanějších rysů přirozeného jazyka, které nelze vyjádřit v (jednorázově tříděné) logice prvního řádu. „Každý logický systém, který je vhodný jako nástroj pro analýzu přirozeného jazyka, potřebuje mnohem bohatší strukturu než predikátová logika prvního řádu“.

Typ Příklad Komentář
Kvantifikace vlastností Pokud je John spokojený sám se sebou, pak má s Peterem společnou alespoň jednu věc. Příklad vyžaduje kvantifikátor nad predikáty, který nelze implementovat v logice prvního řádu s jedním tříděním : Zj → ∃X (Xj∧Xp) .
Kvantifikace vlastností Santa Claus má všechny atributy sadisty. Příklad vyžaduje kvantifikátory nad predikáty, které nelze implementovat v logice prvního řádu s jedním tříděním : ∀X (∀x (Sx → Xx) → Xs) .
Predikát příslovečný John jde rychle. Příklad nelze analyzovat jako Wj ∧ Qj ;
příslovce predikátu nejsou totéž jako predikáty druhého řádu, jako je barva.
Relativní přídavné jméno Jumbo je malý slon. Příklad nelze analyzovat jako Sj ∧ Ej ;
adjektiva predikátu nejsou stejný druh věcí jako predikáty druhého řádu, jako je barva.
Predikátový příslovečný modifikátor John jde velmi rychle. -
Relativní modifikátor adjektiva Jumbo je strašně malý. Výraz jako „strašně“, když je aplikován na relativní adjektivum jako „malý“, má za následek nový složený relativní adjektivum „strašně malý“.
Předložky Mary sedí vedle Johna. Předložka „vedle“ při použití na „Jana“ má za následek příslovečné příslovce „vedle Jana“.

Omezení, rozšíření a variace

Existuje mnoho variant logiky prvního řádu. Některé z nich jsou nepodstatné v tom smyslu, že pouze mění zápis, aniž by ovlivnily sémantiku. Jiní výrazněji mění výrazovou sílu rozšířením sémantiky o další kvantifikátory nebo jiné nové logické symboly. Infinitární logika například umožňuje vzorce nekonečné velikosti a modální logika přidává symboly pro možnost a nutnost.

Omezené jazyky

Logiku prvního řádu lze studovat v jazycích s menším počtem logických symbolů, než bylo popsáno výše.

  • Protože může být vyjádřen jako a může být vyjádřen jako jeden z obou kvantifikátorů a může být vypuštěn.
  • Protože může být vyjádřeno jako a může být vyjádřeno jako , buď nebo může být zrušeno. Jinými slovy, stačí mít a , nebo a jako jediné logické spojky.
  • Podobně stačí mít pouze a jako logická spojení, nebo mít pouze Shefferův tah (NAND) nebo operátor Peirce arrow (NOR).
  • Je možné zcela se vyhnout funkčním symbolům a konstantním symbolům, jejich odpovídajícím způsobem přepisovat pomocí predikátových symbolů. Například, namísto použití konstantní symbol, je možné použít predikát (interpretován jako ), a nahradit každý predikát, jako s . Funkce, která bude podobně nahrazena predikátem interpretovaným jako . Tato změna vyžaduje přidání dalších axiomů k teorii, aby interpretace použitých predikátových symbolů měla správnou sémantiku.

Takováto omezení jsou užitečná jako technika ke snížení počtu odvozovacích pravidel nebo schémat axiomů v deduktivních systémech, což vede ke kratším důkazům metalogických výsledků. Náklady na omezení spočívají v tom, že je stále obtížnější vyjadřovat výroky v přirozeném jazyce v daném formálním systému, protože logické spojky používané v prohlášeních v přirozeném jazyce musí být nahrazeny jejich (delšími) definicemi, pokud jde o omezené shromažďování logické spojky. Podobně derivace v omezených systémech mohou být delší než derivace v systémech, které obsahují další konektory. Existuje tedy kompromis mezi snadností práce ve formálním systému a snadností prokazování výsledků o formálním systému.

Je také možné omezit pole funkčních symbolů a predikátových symbolů v dostatečně expresivních teoriích. V teoriích, které obsahují párovací funkci, lze v zásadě zcela upustit od funkcí arity větších než 2 a predikátů arity větších než 1 . Toto je funkce arity 2, která vezme páry prvků domény a vrátí uspořádaný pár, který je obsahuje. Stačí také mít dva predikátové symboly arity 2, které definují projekční funkce z uspořádaného páru do jeho komponent. V obou případech je nutné, aby byly splněny přirozené axiomy pro párovací funkci a její projekce.

Mnohostranná logika

Běžné interpretace prvního řádu mají jedinou doménu diskurzu, ve které se pohybují všechny kvantifikátory. Mnoho tříděná logika prvního řádu umožňuje proměnným různé druhy , které mají různé domény. Tomu se také říká napsaná logika prvního řádu a druhy se nazývají typy (jako v datovém typu ), ale není to stejné jako teorie typů prvního řádu . Mnohočleněná logika prvního řádu se často používá při studiu aritmetiky druhého řádu .

Když v teorii existuje jen konečný počet druhů, logiku více seřazených prvního řádu lze redukovat na logiku prvního řádu s jedním tříděním. Do teorie s jedním tříděním se zavádí unární predikátový symbol pro každé třídění v teorii s mnoha třídami a přidává se axiom, který říká, že tyto unární predikáty rozdělují doménu diskurzu. Pokud existují například dva druhy, jeden přidá predikátové symboly a axiom

.

Potom jsou prvky uspokojující považovány za prvky prvního druhu a prvky uspokojující jako prvky druhého druhu. Lze kvantifikovat v každém třídění pomocí odpovídajícího predikátového symbolu k omezení rozsahu kvantifikace. Například, když řekneme, že existuje prvek prvního druhu uspokojující vzorec φ ( x ), píše se

.

Další kvantifikátory

Do logiky prvního řádu lze přidat další kvantifikátory.

  • Někdy je užitečné říci, že „ P ( x ) platí přesně pro jedno x “, což lze vyjádřit jako ∃! x P ( x ) . Tento zápis, nazývaný kvantifikace jedinečnosti , může být použit pro zkrácení vzorce, jako je x ( P ( x ) ∧∀ y ( P ( y ) → ( x = y ))) .
  • Logika prvního řádu s extra kvantifikátory má nové kvantifikátory Qx , ..., s významy jako „existuje mnoho x takových, že ...“. Viz také větvení quantifiers a množné quantifiers z George Boolos a další.
  • Vázané kvantifikátory se často používají při studiu teorie množin nebo aritmetiky.

Infinitární logika

Infinitární logika umožňuje nekonečně dlouhé věty. Například lze povolit spojení nebo disjunkci nekonečně mnoha vzorců nebo kvantifikaci nekonečně mnoha proměnných. Nekonečně dlouhé věty vznikají v oblastech matematiky včetně topologie a teorie modelů .

Infinitární logika generalizuje logiku prvního řádu, aby umožňovala vzorce nekonečné délky. Nejběžnějším způsobem, jakým se vzorce mohou stát nekonečnými, jsou nekonečné konjunkce a disjunkce. Je však také možné připustit zobecněné podpisy, ve kterých mohou mít symboly funkcí a vztahů nekonečné arity, nebo v nichž kvantifikátory mohou vázat nekonečně mnoho proměnných. Protože nekonečný vzorec nelze reprezentovat konečným řetězcem, je nutné zvolit nějaké jiné znázornění vzorců; obvyklou reprezentací v tomto kontextu je strom. Vzorce jsou tedy v podstatě identifikovány s jejich analyzovanými stromy, spíše než s analyzovanými řetězci.

Nejčastěji studované infinitární logiky jsou označeny L αβ , kde α a β jsou buď základní čísla, nebo symbol ∞. V tomto zápisu je obyčejná logika prvního řádu L ωω . V logice L ∞ω jsou při vytváření vzorců povoleny libovolné spojky nebo disjunkce a existuje neomezená nabídka proměnných. Obecněji je logika, která umožňuje spojení nebo disjunkce s méně než κ složkami, známá jako L κω . Například L ω 1 ω umožňuje spočítatelné konjunkce a disjunkce.

Množina volných proměnných ve vzorci L κω může mít jakoukoli mohutnost striktně menší než κ, přesto jen nakonec mnoho z nich může být v rozsahu jakéhokoli kvantifikátoru, když se vzorec jeví jako subformula jiného. V jiných infinitárních logikách může být podformula v rozsahu nekonečně mnoha kvantifikátorů. Například v L κ∞ může jeden univerzální nebo existenciální kvantifikátor vázat libovolně mnoho proměnných současně. Podobně logika L κλ umožňuje simultánní kvantifikaci na méně než λ proměnných, stejně jako spojky a disjunkce velikosti menší než κ.

Neklasická a modální logika

  • Intuicionistická logika prvního řádu používá spíše intuicionistický než klasický propoziční kalkul; například ¬¬φ nemusí být ekvivalentní φ.
  • Modální logika prvního řádu umožňuje popsat další možné světy i tento podmíněně pravdivý svět, který obýváme. V některých verzích se sada možných světů liší v závislosti na tom, jaký možný svět člověk obývá. Modální logika má další modální operátory s významy, které lze neformálně charakterizovat jako například „je nutné, aby φ“ (pravdivé ve všech možných světech) a „je možné, že φ“ (pravdivé v nějakém možném světě). Se standardní logikou prvního řádu máme jedinou doménu a každému predikátu je přiřazeno jedno rozšíření. S modální logikou prvního řádu máme doménovou funkci, která každému možnému světu přiřadí vlastní doménu, takže každý predikát dostane rozšíření pouze vzhledem k těmto možným světům. To nám umožňuje modelovat případy, kdy je například Alex filozof, ale možná byl matematik a možná vůbec neexistoval. V prvním možném světě je P ( a ) pravdivé, ve druhém P ( a ) je nepravdivé a ve třetím možném světě není v doméně vůbec žádné a .
  • Fuzzy logika prvního řádu je spíše rozšířením výrokové fuzzy logiky prvního řádu než klasickým propozičním kalkulem .

Logika pevných bodů

Logika Fixpoint rozšiřuje logiku prvního řádu přidáním uzavření pod nejméně pevné body kladných operátorů.

Logika vyššího řádu

Charakteristickým rysem logiky prvního řádu je, že jednotlivce lze kvantifikovat, nikoli však predikáty. Tím pádem

je legální vzorec prvního řádu, ale

není, ve většině formalizací logiky prvního řádu. Logika druhého řádu rozšiřuje logiku prvního řádu přidáním posledního typu kvantifikace. Jiné logiky vyššího řádu umožňují kvantifikaci na ještě vyšších typech, než povoluje logika druhého řádu. Mezi tyto vyšší typy patří vztahy mezi vztahy, funkce od vztahů ke vztahům mezi vztahy a další objekty vyššího typu. „První“ v logice prvního řádu tedy popisuje typ objektů, které lze kvantifikovat.

Na rozdíl od logiky prvního řádu, pro kterou je studována pouze jedna sémantika, existuje několik možných sémantik pro logiku druhého řádu. Nejčastěji používaná sémantika pro logiku druhého a vyššího řádu je známá jako úplná sémantika . Kombinace dalších kvantifikátorů a úplné sémantiky pro tyto kvantifikátory činí logiku vyššího řádu silnější než logiku prvního řádu. Zejména (sémantický) vztah logických důsledků pro logiku druhého a vyššího řádu není semidecidovatelný; neexistuje žádný účinný systém dedukce pro logiku druhého řádu, který je zdravý a úplný podle úplné sémantiky.

Logika druhého řádu s plnou sémantikou je expresivnější než logika prvního řádu. Například je možné vytvořit systémy axiomů v logice druhého řádu, které jedinečně charakterizují přirozená čísla a skutečnou přímku. Náklady na tuto expresivitu jsou v tom, že logika druhého a vyššího řádu má méně atraktivních metalogických vlastností než logika prvního řádu. Například věta Löwenheim – Skolem a věta o kompaktnosti logiky prvního řádu se stanou nepravdivými, když jsou zobecněny na logiku vyššího řádu s plnou sémantikou.

Automatizované dokazování teorémů a formální metody

Automatizované dokazování teorémů se týká vývoje počítačových programů, které hledají a nacházejí derivace (formální důkazy) matematických vět. Hledání derivací je obtížný úkol, protože vyhledávací prostor může být velmi velký; vyčerpávající hledání všech možných derivací je teoreticky možné, ale výpočetně neproveditelné pro mnoho systémů zájmu o matematiku. Tak jsou vyvinuty komplikované heuristické funkce, aby se pokusily najít derivaci za kratší dobu než slepé hledání.

Související oblast automatizovaného ověřování důkazů pomocí počítačových programů kontroluje správnost důkazů vytvořených lidmi. Na rozdíl od komplikovaných automatických ověřovačů teorém mohou být ověřovací systémy dostatečně malé, aby jejich správnost bylo možné kontrolovat jak ručně, tak prostřednictvím automatizovaného ověřování softwaru. Toto ověření ověřovače důkazů je potřebné k získání jistoty, že jakákoli derivace označená jako „správná“ je skutečně správná.

Někteří ověřovatelé důkazů, například Metamath , trvají na tom, že jako vstup bude mít úplnou derivaci. Jiní, jako například Mizar a Isabelle , si vezmou dobře naformátovaný náčrt (který může být stále velmi dlouhý a podrobný) a doplní chybějící části jednoduchým prostým prohledáváním nebo použitím známých rozhodovacích postupů: výsledné odvození je poté ověřeno malé jádro „jádro“. Mnoho takových systémů je primárně určeno k interaktivnímu použití lidskými matematiky: tyto systémy jsou známé jako asistenti důkazu . Mohou také používat formální logiku, která je silnější než logika prvního řádu, například teorii typů. Protože úplné odvození jakéhokoli netriviálního výsledku v deduktivním systému prvního řádu bude pro člověka extrémně dlouhé na psaní, výsledky jsou často formalizovány jako řada lemmatů, pro které lze derivace konstruovat samostatně.

Pro implementaci formálního ověření v počítačové vědě se používají také automatizované ověřovače teorémů . V tomto nastavení se pro ověření správnosti programů a hardwaru, jako jsou procesory, s ohledem na formální specifikaci používají ověřovače vět . Protože je taková analýza časově náročná, a proto drahá, je obvykle vyhrazena pro projekty, u nichž by porucha měla vážné lidské nebo finanční důsledky.

Pokud jde o problém kontroly modelu , je známo , že efektivní algoritmy rozhodují, zda konečná struktura vstupu splňuje vzorec prvního řádu, kromě hranic složitosti výpočtu : viz Kontrola modelu § Logika prvního řádu .

Viz také

Poznámky

Reference

externí odkazy