Afleidingen

Afleidingsregels 

Absurde bewering

Notatie: ⊥
Synoniemen: falsum

Een negate ¬ψ ook kunnen opvatten als een implicatie ψ → ABSURD van ψ naar een absurde atomaire bewering ⊥ waaruit alles volgt.

Afleidbaar

Notatie: ∑ ⊢ ψ
Indien niet afleidbaar: ∑ ⊬ ψ

Een formule ψ heet afleidbaar uit een verzameling aannames ∑ als er een afleiding van ψ bestaat waarin aan het eind alleen nog aannames uit ∑ van kracht zijn.

Syntactisch consistent

Een verzameling formules Γ heet syntactisch consistent wanneer er geen formule ψ is waarvoor zowel Γ ⊢ ψ als Γ ⊢ ¬ψ.

Volledigheid

Als ∑ een formuleverzameling is en ψ een formule, dan geldt:
∑ ⊢ ψ ↔ ∑ ⊨ ψ