Jazyk výrokové logiky

Abeceda jazyka výrokové logiky obsahuje:

1. symboly pro výrokové proměnné:
2. symboly pro logické konstanty:
3. symboly pro výrokové spojky:
4. 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):

1. Každá výroková proměnná (elementární výrok)  je výroková formule.
2. Jsou-li A, B výrokové formule, pak i jsou také výrokové formule.
3. 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.

Úlohy k procvičení