Mix
From LLWiki
The usual notion of is the binary version of the rule but a nullary version also exists.
Binary
rule
The rule is equivalent to
:
They are also equivalent to the principle :
Nullary
rule
The rule is equivalent to
:
The nullary acts as a unit for the binary one:
If π is a proof which uses no rule and no weakening rule, then (up to the simplification of the pattern
above into nothing) π is either reduced to a
rule or does not contain any
rule.