Reguła wnioskowania

Niech $E$ będzie dowolnym zbiorem.

Regułą wnioskowania w $E$ jest dowolna relacja $r\subseteq \mathrm{\wp }(E)\times E,$ dla której $\mathrm{\varnothing }\in ̸\text{dm}(r).$

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

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

Zobacz też

• dowód w systemie formalnym
• system formalny