Matrix semantics for a propositional proof system

A logical matrix specifies truth values, designated values, and operations interpreting the primitive connectives. To prove nonderivability from an axiom set, it suffices that every axiom instance is designated and every inference rule preserves designation, while the proposed conclusion is not designated under some valuation. The primitive connective symbols need not receive their intended classical meanings: preservation by the displayed rules is what makes the syntactic obstruction valid. Rules with discharged assumptions, such as a deduction theorem for propositional logic, must also preserve consequence for arbitrary assumption sets.

Take ordinary material logical implication on $\{0,1\}$, designate $1$, and interpret negation by the constant-zero operation $N$. Then $A\to (B\to A)$ and $(NB\to A)\to (NA\to B)$ are always designated, and modus ponens rule and logical implication discharge preserve consequence. But $(NB\to NA)\to (A\to B)$ is false for $A=1,B=0$. Thus the first two schemes and the deduction rule do not derive the last scheme. This detects the loss of a genuine classical-negation principle even though all the displayed schemes are tautologies under the usual classical negation.