Dobře utvořená formule

Šablona:Upravit Dobře utvořená formule, zkráceně DUF, často jednoduše formule, je v matematické logice, výrokové logice a predikátové logice prvního řádu konečná posloupnost symbolů z dané abecedy, která je částí nějakého formálního jazyka.

Formální jazyk lze identifikovat množinou formulí v jazyce. Formule je syntaktický objekt, kterému lze přiřadit sémantický význam pomocí interpretace. Formule jsou klíčovými objekty výrokové a predikátové logiky.

Úvod

Klíčové je postavení formulí ve výrokové a predikátové logice např. v predikátové logice prvního řádu. V těchto kontextech je formule řetězec symbolů φ, pro který má smysl se ptát, „je φ pravdivý?“, jakmile jsou všechny volné proměnné v φ instanciovány. Ve formální logice mohou být důkazy reprezentovány posloupností formulí s určitými vlastnostmi, tak že poslední člen posloupnosti je formule, která se dokazuje.

Ačkoli se termín „formule“ může používat pro zapsané značky (například na papíře nebo na tabuli), je přesněji chápána jako posloupnost symbolů, přičemž značky jsou symbolickou instancí formule. Toto rozlišování mezi vágním pojmem „vlastnosti“ a induktivně definovaným pojmem „dobře utvořené formule“ má kořeny ve Weylově článku „Über die Definitionen der mathematischen Grundbegriffe“ z roku 1910.Šablona:Sfn Stejná formule může být tedy zapsána více způsoby, a formule může být v principu tak dlouhá, že ji ve fyzickém světě není možné vůbec zapsat.

Formule samy jsou syntaktické objekty. Jejich význam je dán jejich interpretací. Například ve výrokové formuli může být každá výroková proměnná interpretována jako konkrétní propozice, takže celá formule vyjadřuje vztah mezi těmito propozicemi. Formule nemusí být interpretována, aby byla považována za formuli.

Výrokový počet

Šablona:Podrobně Formule výrokové logiky, také nazývané výrokové formule, jsou výrazy např. $(A\wedge (B\vee C))$. Jejich definice vychází z libovolně zvolené množiny V výrokových proměnných. Abeceda sestává ze symbolů z V, symbolů výrokových spojek a závorek „(“ a „)“, o nichž se předpokládá, že nejsou ve V. Formulemi budou řetězce symbolů) nad touto abecedou induktivně definované takto:

• Každá výroková proměnná je sama o sobě formulí.
• Pokud φ je formule, pak ¬φ je formule.
• Pokud φ a ψ jsou formule, a • je libovolná binární spojka, pak (φ • ψ) je formule. Na místě • mohou být logické spojky, např. ∨, ∧, → nebo ↔ (případně i jiné).

Tuto definici je možné také zapsat jako formální gramatiku v Backusově–Naurově formě, za předpokladu, že množina proměnných je konečná:

<alpha set> ::= p | q | r | s | t | u | ... (libovolná konečná množina výrokových proměnných)
<form> ::= <alpha set>| ¬<form>| (<form>∧<form>) | (<form>∨<form>) | (<form>→<form>) | (<form>↔<form>)

Použitím této gramatika posloupnost symbolů

(((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s))

je formule, protože je gramaticky správná. Posloupnost symbolů

((p → q)→(qq))p))

není formule, protože nevyhovuje gramatice.

Složité formule může být obtížný číst, například kvůli přílišnému používání závorek. Tento problém lze zmírnit, zavedením pravidel priority (podobné prioritám) matematických operátorů, což znamená, že některé operátory vážou své operandy těsněji než ostatní. Obvykle se používají priority (od nejsilněji po nejméně vázající) 1. ¬   2. →  3. ∧  4. ∨. Pak formule

(((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s))

může být zkráceně zapsána

p → q ∧ r → s ∨ ¬q ∧ ¬s

To je však pouze konvence používaná pro zjednodušení psaných reprezentací formule. Pokud by priority byly jiné, například spojky by byly zleva doprava asociativní jejich priority by byly následující: 1. ¬   2. ∧  3. ∨  4. →, pak stejnou formuli jako je výše (bez závorek) by bylo možné přepsat jako

(p → (q ∧ r)) → (s ∨ (¬q ∧ ¬s))

Predikátová logika

Definice formule v v logice prvního řádu $𝒬𝒮$ je vztažena k signatuře dané teorie. Tato signatura udává konstantní symboly, predikátové symboly a funkční symboly dané teorie, spolu s aritami funkcí a predikátových symbolů.

Definice formule se skládá z několika složek. Nejprve je rekurzivně definována množina termů. Termy jsou neformálně výrazy, které reprezentují objekty z domény diskurzu.

1. Libovolná proměnná je term.
2. Libovolný konstantní symbol ze signatury je term
3. výraz tvaru f(t₁,...,t_n), kde f je n-ární funkční symbol, a t₁,...,t_n jsou termy, je opět term.

Dalším krokem je definovat atomické formule.

1. Pokud t₁ a t₂ jsou termy, pak t₁=t₂ je atomická formule
2. Pokud R je n-ární predikátový symbol, a t₁,...,t_n jsou termy, pak R(t₁,...,t_n) je atomická formule

Nakonec definujeme množinu formulí jako nejmenší množinu, která obsahuje atomické formule, a je vytvořena podle následujících pravidel:

1. $\mathrm{\neg }\varphi$ je formule, když $\varphi$ je formule
2. $(\varphi \wedge \psi )$ a $(\varphi \vee \psi )$ jsou formule, když $\varphi$ a $\psi$ jsou formule;
3. $\mathrm{\exists }x\varphi$ je formule, když $x$ je proměnná a $\varphi$ je formule;
4. $\mathrm{\forall }x\varphi$ je formule, když $x$ je proměnná a $\varphi$ je formule (alternativně, $\mathrm{\forall }x\varphi$ by mohlo být definováno jako zkratka pro $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }\varphi$).

Pokud formule neobsahuje $\mathrm{\exists }x$ ani $\mathrm{\forall }x$, pro jakoukoli proměnnou $x$, pak se nazývá Šablona:Kotvaformule bez kvantifikátorů. Existenční formule je formule začínající posloupností existenčních kvantifikátorů, za nimiž následuje formule bez kvantifikátorů.

Atomické a otevřené formule

Atomická formule je formule, které neobsahuje žádné logické spojky ani kvantifikátory, tedy formule, která nemá žádné striktní podformule. Přesný tvar atomických formulí závisí na uvažovaném formálním systému; například ve výrokové logice jsou atomickými formulemi výroková proměnné. V predikátové logice jsou atomickými formulemi predikátové symboly spolu se svými argumenty, přičemž každý argument je Term.

Někteří autoři používají název otevřená formule pro formuli, která neobsahuje kvantifikátory. Tento pojem není opakem pojmu uzavřené formule.

Uzavřené formule

Uzavřená formule, také základní formule nebo sentence, je formule, ve které se nevyskytují žádné volné proměnné. Pokud A je formule jazyka prvního řádu, ve které mají proměnné Šablona:Math volné výskyty, pak A, před níž stojí Šablona:Math je univerzální uzávěr formule A.

Vlastnosti formulí

• Formule A v jazyce $𝒬$ je logicky platná, pokud je splněna pro každou interpretace $𝒬$.
• Formule A v jazyce $𝒬$ je splnitelná, pokud je splněna pro nějakou interpretaci $𝒬$.
• Formule A jazyka aritmetiky je rozhodnutelná, pokud reprezentuje rozhodnutelnou množinu, tj. pokud existuje efektivní metoda, která, je-li dána substituce volných proměnných A, říká, že buď je dokazatelná výsledná instance A nebo její negace.

Terminologie

V dřívějších pracích o matematické logice (například od A. Churche) termín formule znamenal libovolný řetězec symbolů, a dobře utvořené formule byly ty řetězce, které se řídí pravidly správné tvorby formulí.

Někteří autoři prostě říkají formule. Moderní užití (zvláště v kontextu matematické informatiky s matematickým softwarem jako jsou model checkery, automatizované a interaktivní dokazovače vět) mají tendenci používat pojem formule pouze pro algebraický koncept a otázku zda, jde o dobře utvořenou formuli, tj. konkrétní řetězcové reprezentace formulí (použití toho či onoho symbolu pro spojky a kvantifikátory, použití té či oné konvence závorkování, použití prefixové nebo infixové notace, atd.) považovat pouze za problémy zápisu.

Anglický výraz pro „dobře utvořenou formuli“ (Šablona:Cizojazyčně) a jeho zkratka wff vyslovovaná [[[:Šablona:IPA]]], [[[:Šablona:IPA]]] nebo [[[:Šablona:IPA]]] se dostaly i do populární kultury. WFF je součástí esoterické slovní hříčky použité v názvu akademické hry „WFF 'N PROOF: The Game of Modern Logic“, kterou vytvořil Layman Allen v době svého působení na Yale Law School (později byl profesorem na Michiganské univerzitě). Název souboru her určeného k výuce principů symbolické logiky pro děti (v prefixové (polské) notaci) je ozvěnou nesmyslného slova „whiffenpoof“, které se používá jako „bojový pokřik“ na Yaleově univerzitě a které se objevilo v písni „The Whiffenpoof Song“ skupiny „The Whiffenpoofs“.

Odkazy

Reference

Šablona:Překlad*Šablona:Citace periodika

• Šablona:Citace monografie
• Šablona:Citace periodika
• Šablona:Citace monografie
• Šablona:Citace monografie
• Šablona:Citace monografie
• Šablona:Citace monografie
• Šablona:Citace monografie
• Šablona:Citace monografie
• Šablona:Citace monografie

Související články

• Základní výraz
• Korektně definovaný
• Formální jazyk

Externí odkazy

• Well-Formed Formula for First Order Predicate Logic – obsahuje krátký kvíz v jazyce Java
• Well-Formed Formula at ProvenMath