wnu - Linear Logic Proof Explorer

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

Syntax Definition wnu 206

Description: Creation operator. Creates and scopes a new channel x. It also has a dual ~ νx~ 𝜑, which has a meaning I don't quite understand.

**Hypotheses**
Ref	Expression
wph	wff 𝜑
vx	var x

**Assertion**
Ref	Expression
wnu	wff νx𝜑

This syntax is primitive. The first axiom using it is ax-int 208.

Colors of variables: wff var nilad