Axiom ax-init 7

Description: The init rule. This innocent-looking rule looks similar to the Law of Excluded Middle in classical logic, but don't be fooled. This allows us to turn any deduction into its dual by simply performing operations on the ~ 𝜑 side and flipping it around to get the reverse implication. This is analogous to using modus tollens in classical logic, but it's especially useful in linear logic because it allows each operator to be defined as its dual with all of the deductions negated and backwards.

Assertion

Ref	Expression
ax-init	⊦ (~ 𝜑 ⅋ 𝜑)

Detailed syntax breakdown of Axiom ax-init

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wneg 3	. 2 wff ~ 𝜑
3	2, 1	wmd 2	1 wff (~ 𝜑 ⅋ 𝜑)

This axiom is referenced by:  nebot  20  dnid  23  dned  24  itopi  41  mdm1s  73  mdm2s  74  id  77  dnis  78  dnes  79  acm1s  84  acm2s  85  nems  86  dflb2s  92  mdco  108  md1  113  abs1  178