Jazyk výrokové logiky
Abeceda jazyka výrokové logiky obsahuje:
- symboly pro výrokové proměnné:
- symboly pro logické konstanty:
- symboly pro výrokové spojky:
- pomocné symboly:
Nechť V je množina elementárních výroků (výrokových proměnných). Konečnou posloupnost prvků z množiny V, logických spojek a závorek nazýváme výroková formule (zkráceně jen formule), jestliže vznikla podle následujících pravidel (rekurzivní definice):
- Každá výroková proměnná (elementární výrok) je výroková formule.
- Jsou-li A, B výrokové formule, pak i jsou také výrokové formule.
- Nic jiného než to, co vzniklo pomocí konečně mnoha použití bodů 1 a 2, není výroková formule.
Podformule je souvislá část formule, která je sama formulí. Z pojmu podformule je patrné, že každá formule je svou podformulí. Chceme-li hovořit o podformulích, které jsou různé od původní formule, budeme používat název vlastní podformule. Všechny vlastní podformule formule jsou tedy .
Poznámka: Negace se nazývá unární spojka a ostatní se nazývají binární spojky. Výrokové proměnné značíme malými písmeny např. , formule můžeme značit velkými písmeny např. . Při zápisu negace díky silnější vazbě této negace vnější závorky neuvádíme.