Substructural Logic: Understanding the roles of Weakening and Contraction I am trying to understand the "structural" rules of logic, and how  relaxing/adding certain these rules gives rise to different types of logic (linear, affine, etc.)
The rules are 


*

*Exchange: $$\left(\Gamma_1, x_1, x_2, \Gamma_2\longrightarrow p\right)\longrightarrow\left(\Gamma_1, x_2, x_1, \Gamma_2\longrightarrow p\right)$$

*Weakening: $\forall x$,
$$\left(\Gamma\longrightarrow p\right)\longrightarrow \left(\Gamma, x\longrightarrow p\right)$$

*Contraction
$$\left(\Gamma, x, x \longrightarrow p\right)\longrightarrow \left(\Gamma, x \longrightarrow p\right)$$
According to David Walker in Substructural Type Systems (page 5)


*

*Linear type systems ensure that every variable is used exactly once by allowing exchange but not weakening or contraction.

*Affine type systems ensure that every variable is used at most once by allowing exchange and weakening, but not contraction

I'm confused by the phrasing "not allowing" certain rules. I've given it some thought, and it seems to me that to achieve the listed properties, it has to mean we explicitly take their negations $p\rightarrow \overline{q}$, not just give up the axiom $p\rightarrow q$
Am I correct here, or is it simply that we just have to give up the "$p\rightarrow q$" form of these statements?

 A: You are using confusing notation. You are using $\longrightarrow$ for two different things and then, arguably, conflating it with $\to$ which is a third thing. A more common notation, using weakening as an example, would be $$\dfrac{\Gamma\vdash p}{\Gamma,x\vdash p}$$ or $$\dfrac{\Gamma\implies p}{\Gamma,x\implies p}$$
The first thing to note is that these are rules, not axioms. They show you how given one derivation (e.g. a derivation of $\Gamma\vdash p$), you can extend it to a longer derivation (e.g. a derivation of $\Gamma,x\vdash p$). A proof system as a whole will be a collection of such rules. A (conditional) proof of a formula is then a derivation which ends in that formula and which will need to start at some rules that have no premises, e.g. $\dfrac{}{\Gamma,p\vdash p}$.
All that is being said is that we're removing some of these rules as options. That means derivations can't use them. You then consider what derivations you can still make which will give you a (potentially) smaller set of provable formulas. Derivations are tree-like mathematical structures. Removing rules just changes what trees you can make.
As an analogy, if you don't have flour, this (potentially) limits what you can cook. It doesn't mean that it is now impossible to cook anything for which you have a recipe that involves flour. Maybe you have an alternate recipe that doesn't use flour. Maybe you can produce your own flour. Maybe you couldn't follow any of the recipes using flour even if you did have flour. 
