As usual, the easiest connective to deal with is conjuinction. Could the first invalid sequent in our hypothetical proof be the output of the rule ANDE, taking us from  A AND B  to A? No, because if the input sequent  X TS A AND B  is valid, then any interpretation satisfying all of X has to satisfy  A AND B  and so by the truth table for AND it has to satisfy A in particular, meaning that  X TS A  is also valid. By the same reasoning, so is  X TS B.

The case of ANDI is similar. Suppose  X STS A  and  Y STS B  both hold, and consider any interpretation satisfying everything in X ∪ Y. Since it satisfies X and Y, it satisfies both A and B, and therefore (by truth tables again) their conjunction  A AND B.  Hence, if the inputs to a step of ANDI are both valid, so is its output.

The rule IMPE is similarly easy. If  X STS A IMP B  and  Y STS A,  and I is an interpretation satisfying X ∪ Y, then I has to satisfy both  A IMP B  and A, and thus satisfies B as well; so  X, Y STS B.

Now suppose  X TS A IMP B  is invalid and comes by a step of IMPI from a sequent  X, A TS B . Since it is invalid, there must be an interpretation I which satisfies all formulae in X but fails to satisfy  A IMP B.  The only way for this to happen is for I to satisfy A but not satisfy B, which means that the input sequent  X, A TS B . is likewise invalid.

The rule NOTE cannot be the first to introduce an invalid sequent into a proof, since in order for its output  X, Y TS BAD  to be invalid, there has to be an interpretation I which satisfies everything in X ∪ Y. Obviously, I cannot satisfy both A and NOTA, so it also provides a counter-example showing that one of the two input sequents is invalid.

Nor can NOTI be the culprit, since if its input  X, A TS BAD  is valid, there is no interpretation satisfying all of X while also satisfying A. But that means that any interpretation which satisfies X must satisfy NOTA, so the output is also valid.

RAA does not require a separate argument, since it is merely NOTE and NOTI telescoped together, so it is covered by the above cases. NOTNOTE does need to be noted, but it is trivial because its input and output formulae are completely equivalent, so neither can follow validly from X unless the other does.

ORI is unproblematic. By inspection of the truth table, we see that if X  STS  A and I satisfies X, then I satisfies the disjunction  A OR B.  The same holds if the input formula is B.

The most complicated propositional rule is ORE. We may suppose all three of its input sequents are valid. That is,  X STS A OR B,   Y, A STS C,  and  Z, B STS C.  We need to show on these suppositions that the output is valid:  X, Y, Z STS C.  Consider, then, any interpretation giving the value 1 to every formula in X, Y or Z. Since this makes everything in X true it must make A OR B true, in which case by the truth table for 'or' it either gives A the value 1 or gives B the value 1. If it gives A the value 1 then it gives 1 to everything in Y and to A, so by the second of our three suppositions it gives 1 to C. Similarly, if it gives 1 to B, by the third supposition it gives 1 to C. Either way C gets the value 1. In sum, any interpretation verifying all of X, Y and Z verifies C which is what we want.

The inference encapsulated in the rule ALLE, that what is universally true is true in particular of whatever object is named by a term t, looks obviously valid, but in fact showing the semantic correctness of ALLE is less simple than it looks. Suppose, then, that there is an interpretation I on which the output sequent fails. That is, every formula in X is satisfied by I but A^t_v is not. We wish to show that ALLv A is also false for interpretation I. To obtain the truth value of ALLv A, we choose a name m which does not occur in A and find an m-variant of I in which of A^m_v is false. Unsurprisingly, the m-variant which falsifies A^m_v is I_[m←δ(t)]  where δ(t) is the object denoted by t in interpretation I. There are two cases to consider: either m is a sub-term of t, or it is not. If it is, then t does not occur in A, so the two formulae A^t_v and A^m_v are exactly the same except that one has m exactly where the other has t, so since the two terms denote the same thing, the values of the formulae are the same. If m is not a sub-term of t, then m is the only term in A^m_v whose denotation changes between I and I _[m←δ(t)] , so again it is clear that all subformulae of A^m_v have the same values in I_[m←δ(t)]  as the corresponding subformulae of A^t_v have in I. Since every formula in X is true for I but ALLv A is false for I, the input sequent is invalid as required.

Now consider the rule ALLI. Suppose m is a name which occurs in A but not in any formula in X. Let v be a variable not occurring in A. Suppose X does not semantically entail ALLv A^v_mso there is an interpretation I which is a model of X but for which ALLv A^v_mis false. By the modelling condition for the universal quantifier, this means that there is some m-variant J of I for which A is false. Since m does not occur in X, and I is a model of X, it follows that J is also a model of X. That is, there is an interpretation for which everything in X is true but A is false, showing that X does not (semantically) entail A.

SOMEI preserves validity in much the same way as ALLE. Suppose the input is valid: that is,  X STS A^t_v and suppose every formula in X is true for I. Choose m as before. Since A^t_v is true for I, A^m_vis true for I_[m←δ(t)]  which makes SOMEv A true for I. Since this holds for any interpretation satisfying X, we have  X STS SOMEv A.

For SOMEI, suppose the inputs are valid, and consider any interpretation I satisfying X and Y. Since  X  STS  SOMEv A^v_mthere is some m-variant J of I fopr which A is true. Since m does not occur anywhere in Y, all formulae in Y are true for J, but  Y, A  STS  B, so B is also true for J. The name m does not occur in B, so the value of m is irrelevant to B, which is therefore also true in I.