Jazyk výrokové logiky, formule

Jazyk výrokové logiky obsahuje:

• symboly pro prvotní formule
• logické spojky
• závorky

Formule výrokové logiky (výroková formule) je každá posloupnost symbolů z jazyka výrokové logiky, které vznikne aplikací následujících pravidel
(definice indukcí):

• Každá prvotní formule je výroková formule
• Jsou-li a výrokové formule, pak jsou i výrokové formule
• Každý řetězec symbolů sestavený podle pravidel 1. a 2. v konečně mnoha krocích je formule výrokové logiky

Podformule formule je taková její část, která je sama formulí.
Přitom uvažujeme formule i s vnějšími závorkami - tedy u formule není její podformule