wbot - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Wrap Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > wbot		Structured version

Syntax Definition wbot 1

Description: Bottom, the unit of ⅋. In the resource interpretation, this represents an impossibility. Characterized by ax-ibot 4 and ax-ebot 5.

**Assertion**
Ref	Expression
wbot	wff ⊥

This syntax is primitive. The first axiom using it is ax-ibot 4.

Colors of variables: wff var nilad