= 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.
Back to article page
