df-zero - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > df-zero		Structured version

Definition df-zero 130

Description: Zero is the dual of Top.

**Assertion**
Ref	Expression
df-zero	⊦ (0 ⧟ ~ ⊤)

**Detailed syntax breakdown of Definition df-zero**
Step	Hyp	Ref	Expression
1		wzero 129	. 2 wff 0
2		wtop 29	. . 3 wff ⊤
3	2	wneg 3	. 2 wff ~ ⊤
4	1, 3	wlb 55	1 wff (0 ⧟ ~ ⊤)

Colors of variables: wff var nilad

This definition is referenced by: (None)