Definitie van regels voor het vormen van Well Formed Formulas:

• Elke eenvoudige letter is een WFF.
• Het teken – gevolgd door om het even welke WFF is een WFF.
• Een open hakje gevolgd door een WFF gevolgd door één van de tekens ., v, →, ↔, gevolgd door en andere WFF gevolgd door een gesloten haakje is een WFF.

Uit deze regels kan je besluiten of een opeenvolging van tekens een juiste tekencombinatie heeft (maw of de opeenvolging de juiste syntax heeft)

• De keuze van axioma’s, dit is een klein aantal basiscombinaties waaruit de andere kunnen worden afgeleid:

• (p v p) → p
• q → (p v q)
• (p v q) → (q v p)
• (p v ( q v r)) →(q v ( p v r))
• (q → r) → ((p v q) → (p v r)

Door die axioma’s worden een aantal tekens impliciet gedefinieerd. Maar je hoeft die interpretatie niet te maken om de axioma’s correct te kunnen hanteren. Dat gebeurt namelijk door:

• De keuze van een aantal afleidingsregels die toelaten uit de axioma’s andere WFF’s af te leiden:

• Een regel voor de ‘substitutie van variabelen’ die toelaat een variabele te vervangen door een andere, op voorwaarde dat de vervanging consistent gebeurt door de hele formule heen.
• Een regel voor de afleiding die stelt dat uit p → q en p, q mag worden afgeleid.
• Een regel voor de ‘substitutie bij definitie’ die toelaat om een formule te vervangen door een andere formule die er equivalent mee is. Door deze regel wordt een aantal tekens expliciet gedefinieerd.