Logika prvního řádu

Logika prvního řádu (FOL) je jazyk v symbolické vědě, který používají matematici, filozofové, lingvisté a počítačoví vědci. Používá se pod mnoha názvy, včetně: predikátový kalkul prvního řádu (FOPC), predikátový kalkul nižšího řádu, jazyk logiky prvního řádu nebo predikátové logiky. Nejpoužívanějším názvem je však FOL, vyslovuje se ef-oh-el. FOL je systém dedukce rozšiřující výrokovou logiku o schopnost vyjádřit vztahy mezi jednotlivci (např. lidmi, čísly a „věcmi“) obecněji.

Propoziční logika není vhodná pro formalizaci platných argumentů, které se opírají o vnitřní strukturu příslušných tvrzení. Například překlad platného argumentu

do výrokové logiky výnosy

což je neplatné (∴ znamená „proto“). Zbytek článku vysvětluje, jak je FOL schopen zvládnout tyto druhy argumentů.

Atomové věty logiky prvního řádu mají tvar P(t1, ..., tn) (predikát s jedním nebo více „argumenty“) spíše než výroková písmena jako v výrokové logice. To se obvykle píše bez závorek a čárek jako níže.

Novou složkou logiky prvního řádu, která se v výrokové logice nevyskytuje, je kvantifikace: kde φ je libovolný (dobře tvarovaný) vzorec, jsou zavedeny nové konstrukce ∀x φ a ∃x φ – čti „pro všechna x, φ“ a „pro některá x, φ“ – kde x je individuální proměnná, jejíž rozsah je množinou jedinců nějakého daného diskurzu (nebo domény) vesmíru. Například pokud vesmír sestává pouze z lidí, pak se x pohybuje nad lidmi. Pro zjednodušení napíšeme φ jako φ(x), abychom ukázali, že obsahuje pouze proměnnou x free a pro b a člen vesmíru necháme φ[b] vyjádřit, že b vyhovuje (tj. má vlastnost vyjádřenou) φ. Pak ∀x φ(x) uvádí, že φ[b] platí pro každé b ve vesmíru a ∃x φ(x) znamená, že existuje b (ve vesmíru) takové, že φ[b] platí.

Argument o Sokratovi může být formalizován v logice prvního řádu následovně. Nechť vesmír diskurzu je množinou všech lidí, žijících i zemřelých, a nechť je Man(x) predikátem (což neformálně znamená, že osoba reprezentovaná proměnnou x je člověk) a Mortal(x) je druhým predikátem. Pak se argument výše stává

Doslovný překlad prvního řádku by byl „Pro všechna x, pokud je x popsáno 'Člověkem', musí být x také popsáno 'Smrtelným'.“ Druhý řádek uvádí, že predikát „Člověk“ se vztahuje na Sokrata a třetí řádek se překládá na „Proto se popis 'Smrtelný' vztahuje na Sokrata.“

Všimněte si, že v logice prvního řádu Man(x) není funkcí, protože funkce převádí vstupy na výstupy prostřednictvím určitého procesu. Man(x) jednoduše znamená, že x je popsáno jako „Man“, nebo že x je (a) „Man“, nebo že x spadá do kategorie „Man“.

Logika prvního řádu má dostatečnou expresivní sílu pro formalizaci prakticky celé matematiky. Teorie prvního řádu se skládá z množiny axiomů (obvykle konečných nebo rekurzivně vyčíslitelných) a z nich odvozitelných výroků. Obvyklá teorie množin ZFC je příkladem teorie prvního řádu a obecně se uznává, že veškerá klasická matematika může být formalizována v ZFC. Existují i jiné teorie, které jsou běžně formalizovány nezávisle v logice prvního řádu (i když připouštějí implementaci v teorii množin), například Peanova aritmetika.

Definování logiky prvního řádu

Predikát kalkul se skládá z

Zde uvažované axiomy jsou logické axiomy, které jsou součástí klasického FOL. Dále jsou přidány nelogické axiomy, aby vznikly specifické teorie prvního řádu, které jsou založeny na axiomech klasického FOL (a proto jsou nazývány klasickými teoriemi prvního řádu, jako je klasická teorie množin). axiomy teorií prvního řádu nejsou považovány za pravdy logiky jako takové, ale spíše za pravdy konkrétní teorie, která s ní má obvykle spojenou zamýšlenou interpretaci jejích nelogických symbolů. (Viz analogická myšlenka u logických versus nelogických symbolů.) Klasický FOL s sebou nemá spojenou zamýšlenou interpretaci svého nelogického slovníku (kromě pravděpodobně symbolu označujícího identitu, podle toho, zda takový symbol někdo považuje za logický).

Je-li množina axiomů nekonečná, je nutné, aby existoval algoritmus, který může pro daný dobře tvarovaný vzorec rozhodnout, zda se jedná o axiom, či nikoli. Měl by existovat také algoritmus, který může rozhodnout, zda je dané použití odvozovacího pravidla správné, či nikoli.

Je důležité poznamenat, že FOL může být formalizován v mnoha rovnocennými způsoby; není nic kanonické o axiomy a pravidla odvození zde uveden. Existuje nekonečně mnoho rovnocenných formalizace z nichž všechny výnos stejné věty a non-věty, a všechny, které mají stejné právo na titul 'FOL'.

„Slovní zásoba“ se skládá z

Existuje několik menších variant uvedených níže:

Sady konstant, funkcí a relací jsou obvykle považovány za tvořící jazyk, zatímco proměnné, logické operátory a kvantifikátory jsou obvykle považovány za patřící do logiky. Například jazyk teorie grup se skládá z jedné konstanty (prvek identity), jedné funkce valence 1 (inverzní) jedné funkce valence 2 (součin) a jednoho vztahu valence 2 (rovnost), který by byl vynechán autory, kteří zahrnují rovnost do základní logiky.

Formační pravidla definují pojmy, vzorce a volné proměnné v nich následovně.

Vzhledem k tomu, že ¬ (φ → ¬ ψ) je logicky ekvivalentní (φ ∧ ψ), (φ ∧ ψ) se často používá jako krátká ruka. Stejný princip je za (φ ∨ ψ) a (φ ↔ ψ). Také ∃x φ je krátká ruka pro ¬∀y ¬φ. V praxi platí, že pokud je P vztahem valence 2, často píšeme „a P b“ místo „P a b“; například, píšeme 1 < 2 místo <(1 2). Podobně pokud f je funkce valence 2, někdy napíšeme „a f b“ místo „f(a b)“; například, napíšeme 1 + 2 místo +(1 2). Je také běžné vynechat některé závorky, pokud to nevede k nejednoznačnosti.

Někdy je užitečné říci, že „P(x) platí přesně pro jedno x“, což může být vyjádřeno jako ∃!x P(x). To může být také vyjádřeno jako ∃x (P(x) ∧ ∀y (P(y) → (x = y)))) .

Pokud t je výraz a φ(x) je vzorec obsahující x jako volnou proměnnou, pak v φ(t) je definováno jako výsledek nahrazení všech volných instancí x hodnotou t za předpokladu, že žádná volná proměnná z t se v tomto procesu neváže. Pokud se nějaká volná proměnná z t neváže, pak pro nahrazení t za x je nejprve nutné změnit názvy vázaných proměnných z φ na něco jiného než volné proměnné z t. Abychom viděli, proč je tato podmínka nutná, vezměme si vzorec φ(x) daný ∀y y ≤ x ("x je maximální"). Pokud t je výraz bez y jako volné proměnné, pak φ(t) znamená jen t je maximální. Nicméně pokud t je y, vzorec φ(y) je ∀y y ≤ y, který neříká, že y je maximální. Problém je, že volná proměnná y z t (=y) se stala vázanou, když jsme nahradili y za x v φ(x). Takže pro vytvoření φ(y) musíme nejprve změnit vázanou proměnnou y z φ na něco jiného, řekněme z, takže φ(y) je pak ∀z ≤ y. Zapomenutí této podmínky je notoricky známou příčinou chyb.

Existuje několik různých konvencí pro použití rovnosti (nebo identity) v logice prvního řádu. Tato část shrnuje ty hlavní. Všechny různé konvence dávají v podstatě stejné výsledky s přibližně stejným množstvím práce a liší se hlavně terminologií.

Pravidlo odvození modus ponens je jediné, které je vyžadováno z výrokové logiky pro zde uvedenou formalizaci. Uvádí, že pokud jsou φ a φ → ψ prokázány, pak lze odvodit ψ.

Pravidlo odvození nazývané univerzální generalizace je charakteristické pro predikátový počet. Lze ho uvést jako

kde φ má být zkratkou pro již osvědčenou větu predikátového počtu.

Všimněte si, že generalizace je analogická Necessitation Rule modální logiky, která je

Následující čtyři logické axiomy charakterizují predikátový počet:

Jsou to vlastně axiomová schémata: výraz W znamená jakékoliv wff, ve kterém x není volné, a výraz Z(x) znamená jakékoliv wff s dodatkovou konvencí, že Z(t) znamená výsledek substituce výrazu t za x v Z(x).

Predikátový kalkul je rozšířením výrokového kalkulu, který definuje, která tvrzení logiky prvního řádu jsou prokazatelná. Je to formální systém používaný k popisu matematických teorií. Pokud je výrokový kalkul definován vhodnou množinou axiomů a jediným pravidlem inference modus ponens (to může být provedeno mnoha různými způsoby), pak predikátový kalkul může být definován přidáním některých dalších axiomů a dodatečným inferenčním pravidlem „univerzální zobecnění“. Přesněji řečeno, jako axiomy pro predikátový kalkul bereme:

Věta je definována jako prokazatelná v logice prvního řádu, pokud ji lze získat pomocí axiomů predikátového počtu a opakovaným použitím pravidel odvození „modus ponens“ a „univerzální zobecnění“.

Máme-li teorii T (množinu tvrzení, v nějakém jazyce nazývanou axiomy), pak je věta φ definována jako prokazatelná v teorii T, jestliže a ∧ b ∧ ... → φ je prokazatelná v logice prvního řádu, pro nějakou konečnou množinu axiomů a, b,... teorie T.

Jeden zjevný problém s touto definicí prokazatelnosti je, že se zdá být spíše ad hoc: vzali jsme nějakou zjevně náhodnou sbírku axiomů a pravidel odvozování a je nejasné, že jsme náhodou nevynechali nějaký životně důležitý axiom nebo pravidlo. Gödelova věta o úplnosti nás ujišťuje, že to ve skutečnosti není problém: věta říká, že každý výrok pravdivý ve všech modelech je prokazatelný v logice prvního řádu. Zejména každá rozumná definice „prokazatelného“ v logice prvního řádu musí být rovnocenná té výše uvedené (i když je možné, aby se délky důkazů diametrálně lišily pro různé definice prokazatelnosti).

Existuje mnoho různých (ale rovnocenných) způsobů, jak definovat prokazatelnost. Výše uvedená definice je typickým příkladem „Hilbertova stylu“ kalkulu, který má mnoho různých axiomů, ale velmi málo pravidel odvození. Predikát „Gentzenova stylu“ se liší tím, že má velmi málo axiomů, ale mnoho pravidel odvození.

Metalogické věty logiky prvního řádu

Některé důležité metalogické věty jsou uvedeny níže v odrážkové formě.

Porovnání s jinými logikami

Většina z těchto logik jsou v určitém smyslu rozšíření logiky prvního řádu: zahrnují všechny kvantifikátory a logické operátory logiky prvního řádu se stejným významem. Lindström ukázal, že logika prvního řádu nemá žádná rozšíření (kromě sebe samé), která by splňovala jak kompaktní větu, tak směrem dolů Löwenheimovu-Skolemovu větu. Přesné vyjádření Lindströmovy věty vyžaduje výčet několika stránek technických podmínek, o nichž se předpokládá, že je logika splňuje; například změna symbolů jazyka by neměla znamenat žádný podstatný rozdíl v tom, které věty jsou pravdivé.

Logika prvního řádu, v níž žádná atomová věta neleží v rozsahu více než tří kvantifikátorů, má stejnou expresivní sílu jako vztahová algebra Tarského a Givanta (1987). Ukazují také, že FOL s primitivním uspořádaným párem a vztahová algebra zahrnující dva uspořádané párové projekční vztahy jsou rovnocenné.