Reguła wnioskowania

Niech ${\displaystyle E}$ będzie dowolnym zbiorem.

Regułą wnioskowania w ${\displaystyle E}$ jest dowolna relacja ${\displaystyle r\subseteq \wp (E)\times E,}$ dla której ${\displaystyle \emptyset \not \in {\textrm {dm}}(r).}$

Jeśli ${\displaystyle r}$ jest regułą wnioskowania w ${\displaystyle E,}$ to ${\displaystyle \langle \Pi ,e\rangle \in r}$ nazywamy sekwentem tej reguły. Zbiór ${\displaystyle \Pi }$ nazywamy zbiorem przesłanek tego sekwentu, a ${\displaystyle e}$ jego wnioskiem.

Reguła jest finitarna, jeśli przesłanki jej sekwentów są zawsze skończone.

• dowód w systemie formalnym
• system formalny