Dobře vytvořený vzorec - Well-formed formula

V matematické logiky , výrokové logice a predikátové logiky , je dobře tvarovaná formule , zkráceně WFF nebo wff , často prostě formule , je konečná posloupnost ze symbolů z určitého abecedy , která je součástí formálního jazyka . Formální jazyk lze identifikovat pomocí sady vzorců v daném jazyce.

Vzorec je syntaktický objekt, kterému lze pomocí interpretace dát sémantický význam . Dvě klíčová použití vzorců jsou v propoziční logice a predikátové logice.

Úvod

Klíčové použití vzorců je v propoziční logice a predikátové logice, jako je logika prvního řádu . V těchto kontextech je vzorec řetězec symbolů φ, pro který má smysl ptát se „je φ pravdivý?“, Jakmile byly vytvořeny instance libovolných volných proměnných v φ. Ve formální logice mohou být důkazy reprezentovány sekvencemi vzorců s určitými vlastnostmi a je prokázán konečný vzorec v sekvenci.

Ačkoli výraz „vzorec“ může být použit pro psané značky (například na kousku papíru nebo tabuli), je přesněji chápán jako sled symbolů, které jsou vyjádřeny, přičemž značky jsou tokenovou instancí vzorce. Stejný vzorec tedy může být napsán vícekrát a vzorec může být v zásadě tak dlouhý, že jej nelze ve fyzickém vesmíru napsat vůbec.

Samotné vzorce jsou syntaktické objekty. Jsou jim dány významy interpretacemi. Například v propozičním vzorci lze každou výrokovou proměnnou interpretovat jako konkrétní výrok, takže celkový vzorec vyjadřuje vztah mezi těmito výroky. Vzorec nemusí být interpretován, ale je třeba jej považovat pouze za vzorec.

Výrokový počet

Vzorce výrokového počtu , nazývané také výrokové vzorce , jsou výrazy jako . Jejich definice začíná s libovolným výběrem nastaveného V z výrokových proměnných . Abeceda sestává z písmen V, spolu se symboly pro výrokové spojky a závorky „(“ a „)“, z nichž všechny se předpokládá, že není v V . Vzorce budou určitými výrazy (tj. Řetězci symbolů) nad touto abecedou. ${\ displaystyle (A \ land (B \ lor C))}$

Vzorce jsou indukčně definovány takto:

• Každá výroková proměnná je sama o sobě vzorcem.
• Pokud φ je vzorec, pak ¬φ je vzorec.
• Pokud φ a ψ jsou vzorce a • je libovolná binární spojka, pak (φ • ψ) je vzorec. Zde • by mohly být (ale nejsou omezeny na) obvyklé operátory ∨, ∧, → nebo ↔.

Tuto definici lze také psát jako formální gramatiku ve formě Backus – Naur za předpokladu, že množina proměnných je konečná:

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> | ¬<form> | (<form>∧<form>) | (<form>∨<form>) | (<form>→<form>) | (<form>↔<form>)

Pomocí této gramatiky je posloupnost symbolů

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

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

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

není vzorec, protože neodpovídá gramatice.

Složitý vzorec může být obtížně čitelný, například kvůli množení závorek. Ke zmírnění tohoto posledního jevu se mezi operátory předpokládají pravidla priority (podobná standardnímu matematickému pořadí operací ), čímž jsou některé operátory závaznější než jiné. Například za předpokladu, že přednost (od nejvíce závazné po nejméně závaznou) 1. ¬ 2. → 3. ∧ 4. ∨. Pak vzorec

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

lze zkrátit na

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

Toto je však pouze konvence používaná ke zjednodušení písemného vyjádření vzorce. Pokud by se předpokládalo, že priorita je asociativní zleva doprava, v následujícím pořadí: 1. ¬ 2. ∧ 3. ∨ 4. →, pak by stejný vzorec výše (bez závorek) byl přepsán jako

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

Predikátová logika

Definice vzorce v logice prvního řádu je relativní k podpisu dané teorie. Tento podpis specifikuje konstantní symboly, predikátové symboly a funkční symboly dané teorie spolu s aritami funkčních a predikátových symbolů. ${\ displaystyle {\ mathcal {QS}}}$

Definice vzorce má několik částí. Nejprve je sada termínů definována rekurzivně. Termíny, neformálně, jsou výrazy, které představují objekty z oblasti diskurzu .

1. Jakákoli proměnná je termín.
2. Jakýkoli konstantní symbol z podpisu je termín
3. výraz tvaru f ( t ₁ ,…, t _n ), kde f je n -ary funkční symbol, a t ₁ ,…, t _n jsou termíny, je opět termínem.

Dalším krokem je definování atomových vzorců .

1. Pokud se t ₁ a t ₂ jsou termíny pak t ₁ = t ₂ je atomická formule
2. Pokud R je n -ary predikátový symbol a t ₁ ,…, t _n jsou termíny, pak R ( t ₁ , ..., t _n ) je atomový vzorec

Nakonec je sada vzorců definována jako nejmenší sada obsahující sadu atomových vzorců, takže platí:

1. ${\ displaystyle \ neg \ phi}$ je vzorec, když je vzorec ${\ displaystyle \ phi}$
2. ${\ displaystyle (\ phi \ land \ psi)}$ a jsou vzorce, když a jsou vzorce; ${\ displaystyle (\ phi \ lor \ psi)}$${\ displaystyle \ phi}$${\ displaystyle \ psi}$
3. ${\ displaystyle \ existuje x \, \ phi}$ je vzorec, pokud je proměnná a je vzorec; ${\ displaystyle x}$${\ displaystyle \ phi}$
4. ${\ displaystyle \ forall x \, \ phi}$ je vzorec, když je proměnná a je vzorec (alternativně lze definovat jako zkratku pro ). ${\ displaystyle x}$${\ displaystyle \ phi}$${\ displaystyle \ forall x \, \ phi}$${\ displaystyle \ neg \ existuje x \, \ neg \ phi}$

Pokud vzorec nemá žádné výskyty nebo pro libovolnou proměnnou , pak se nazývá bez kvantifikátoru . Existenciální vzorec je vzorec začínající sekvencí existenční kvantifikace následuje Kvantifikátor bez vzorce. ${\ displaystyle \ existuje x}$${\ displaystyle \ forall x}$${\ displaystyle x}$

Atomové a otevřené vzorce

Atomická formule je vzorec, který neobsahuje žádné logické spojky ani quantifiers nebo ekvivalentně vzorec, který nemá žádné přísné subformulas. Přesná forma atomových vzorců závisí na uvažovaném formálním systému; pro výrokovou logiku jsou například atomové vzorce výrokovými proměnnými . Pro predikátovou logiku jsou atomy predikátové symboly spolu s jejich argumenty, přičemž každý argument je termín .

Podle určité terminologie je otevřený vzorec vytvořen kombinací atomových vzorců pouze pomocí logických spojek, s výjimkou kvantifikátorů. To se nesmí zaměňovat s neuzavřeným vzorcem.

Uzavřené vzorce

Uzavřená formule , i kostru vzorec nebo věta , je vzorec, ve kterém nejsou žádné volné výskyty jakékoliv proměnné . Pokud je vzorec prvního řádu jazyk, ve kterém jsou proměnné v ₁ , ..., V _n mají volné výskyty, pak předchází v ₁ ⋯ V _n je uzávěr A . ${\ displaystyle \ forall}$${\ displaystyle \ forall}$

Vlastnosti použitelné pro vzorce

• Vzorec v jazyce, který je platný , pokud je to pravda pro každého výkladu o . ${\ displaystyle {\ mathcal {Q}}}$${\ displaystyle {\ mathcal {Q}}}$
• Vzorec v jazyce, který je splnitelná , jestliže je pravda, nějaký výklad o . ${\ displaystyle {\ mathcal {Q}}}$${\ displaystyle {\ mathcal {Q}}}$
• Vzorec A jazyka aritmetiky je rozhodnutelný, pokud představuje rozhodnutelnou množinu , tj. Pokud existuje účinná metoda, která vzhledem k nahrazení volných proměnných A říká, že buď výsledná instance A je prokazatelná, nebo její negace je .

Používání terminologie

V dřívějších pracích o matematické logice (např. Church ) se vzorce vztahovaly k jakýmkoli řetězcům symbolů a mezi těmito řetězci byly dobře formulované vzorce řetězce, které se řídily pravidly formování (správných) vzorců.

Několik autorů jednoduše říká vzorec. Moderní zvyklosti (zejména v kontextu počítačové vědy s matematickým softwarem, jako jsou modely modelů , automatizované věty , interaktivní věty ) mají tendenci zachovat pojem vzorce pouze algebraický koncept a ponechat otázku dobře formovatelnosti , tj. konkrétní řetězcové vyjádření vzorců (použití tohoto nebo toho symbolu pro spojovací výrazy a kvantifikátory, použití této nebo té závorkové konvence , použití polské nebo infixové notace atd.) jako pouhý notační problém.

I když se výraz dobře formulovaný vzorec stále používá, tito autoři jej nutně nepoužívají v rozporu se starým smyslem pro vzorec , který v matematické logice již není běžný.

Výraz „dobře formulované vzorce“ (WFF) se vkradl také do populární kultury. WFF je součástí esoterické slovní hříčky používané ve jménu akademické hry „ WFF 'N PROOF : The Game of Modern Logic“, kterou napsal Layman Allen, vyvinuté na Právnické fakultě Yale (později byl profesorem na University of Michigan ). Sada her je navržena tak, aby učila děti principům symbolické logiky (v polské notaci ). Jeho jméno je ozvěnou whiffenpoof , je nesmysl slovo používá jako fandit na Yale University vyrobený populární v The Whiffenpoof Song a The Whiffenpoofs .

Viz také

• Základní výraz

Poznámky

Reference

• Allen, Layman E. (1965), „Towards Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games“, Mathematical Learning: Report of a Conference Sponzored by the Committee on Intellective Processes Research of the Social Science Research Council , Monographs of Společnost pro výzkum vývoje dětí, 30 (1): 29–41
• Boolos, George ; Burgess, John; Jeffrey, Richard (2002), Computability and Logic (4th ed.), Cambridge University Press , ISBN   978-0-521-00758-0
• Ehrenberg, Rachel (jaro 2002). „Je pozitivně logický“ . Michigan dnes . Michiganská univerzita. Archivovány od originálu dne 2009-02-08 . Citováno 2007-08-19 .
• Enderton, Herbert (2001), Matematický úvod do logiky (2. vydání), Boston, MA: Academic Press , ISBN   978-0-12-238452-3
• Gamut, LTF (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic , University Of Chicago Press, ISBN   0-226-28085-3
• Hodges, Wilfrid (2001), „Classical Logic I: First-Order Logic“, Goble, Lou (ed.), The Blackwell Guide to Philosophical Logic , Blackwell, ISBN   978-0-631-20692-7
• Hofstadter, Douglas (1980), Gödel, Escher, Bach: Věčný zlatý cop , Penguin Books , ISBN   978-0-14-005579-5
• Kleene, Stephen Cole (2002) [1967], Mathematical logic , New York: Dover Publications , ISBN   978-0-486-42533-7 , MR   1950307
• Rautenberg, Wolfgang (2010), Stručný úvod do matematické logiky (3. vyd.), New York : Springer Science + Business Media , doi : 10,1007 / 978-1-4419-1221-3 , ISBN   978-1-4419-1220-6

externí odkazy

• Dobře vytvořený vzorec pro predikátovou logiku prvního řádu - obsahuje krátký kvíz Java .
• Dobře formulovaný vzorec na ProvenMath