Dobře utvořená formule

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. 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

Podrobnější informace naleznete v článku Výroková logika.

Formule výrokové logiky, také nazývané výrokové formule, jsou výrazy např. $(A\land (B\lor 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 ${\mathcal {QS}}$ 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. $\neg \phi$ je formule, když $\phi$ je formule
2. $(\phi \land \psi )$ a $(\phi \lor \psi )$ jsou formule, když $\phi$ a $\psi$ jsou formule;
3. $\exists x\,\phi$ je formule, když $x$ je proměnná a $\phi$ je formule;
4. $\forall x\,\phi$ je formule, když $x$ je proměnná a $\phi$ je formule (alternativně, $\forall x\,\phi$ by mohlo být definováno jako zkratka pro $\neg \exists x\,\neg \phi$).

Pokud formule neobsahuje $\exists x$ ani $\forall x$, pro jakoukoli proměnnou $x$, pak se nazývá formule 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

Podrobnější informace naleznete v článku Atomická 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

Podrobnější informace naleznete v článku Sentence (logika).

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é v₁, …, v_n volné výskyty, pak A, před níž stojí ∀v₁ ⋯ ∀v_n je univerzální uzávěr formule A.

Vlastnosti formulí

• Formule A v jazyce ${\mathcal {Q}}$ je logicky platná, pokud je splněna pro každou interpretace ${\mathcal {Q}}$.
• Formule A v jazyce ${\mathcal {Q}}$ je splnitelná, pokud je splněna pro nějakou interpretaci ${\mathcal {Q}}$.
• 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“ (well-formed formula) a jeho zkratka wff vyslovovaná [wuːf], [wɪf] nebo [wef] 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

V tomto článku byl použit překlad textu z článku Well-formed formula na anglické Wikipedii.*ALLEN, Layman E., 1965. Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games. Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council. Roč. 30, čís. 1, s. 29–41. 

• BOOLOS, George; BURGESS, John; JEFFREY, Richard, 2002. Computability and Logic. 4. vyd. [s.l.]: Cambridge University Press. ISBN 978-0-521-00758-0. 
• EHRENBERG, Rachel. He's Positively Logical. www.umich.edu. University of Michigan, Spring 2002. Dostupné v archivu pořízeném dne 2009-02-08. 
• ENDERTON, Herbert, 2001. A mathematical introduction to logic. 2. vyd. Boston, MA: Academic Press. ISBN 978-0-12-238452-3. 
• GAMUT, L.T.F., 1990. Logic, Language, and Meaning, Volume 1: Introduction to Logic. [s.l.]: University Of Chicago Press. ISBN 0-226-28085-3. 
• HODGES, Wilfrid, 2001. The Blackwell Guide to Philosophical Logic. [s.l.]: Blackwell. Dostupné online. ISBN 978-0-631-20692-7. 
• HOFSTADTER, Douglas, 1980. Gödel, Escher, Bach: An Eternal Golden Braid. [s.l.]: Penguin Books. ISBN 978-0-14-005579-5. 
• KLEENE, Stephen Cole, 2002. Mathematical logic. New York: Dover Publications. ISBN 978-0-486-42533-7. 
• RAUTENBERG, Wolfgang, 2010. A Concise Introduction to Mathematical Logic. 3. vyd. New York: Springer Science & Business Media. ISBN 978-1-4419-1220-6. DOI 10.1007/978-1-4419-1221-3. 
• WEYL, Hermann, 1910. Definitions of Fundamental Mathematical Concepts. Překlad Stephen Pollard. [s.l.]: [s.n.]. Dostupné online. (anglicky) 

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

Portály: Filosofie | Matematika