There are several rules relating to each logical connective discussed in §2.1.1 - and we now focus on their application.

2.2.1 Soundness and Completeness
First, we must note that inference rules work in conjunction with a formal language (in this case propositional logic) to form what is referred to as a logical system. These must be both sound and complete with respect to their inference rules for their users to have any faith in their conclusions.

Soundness, also known as truth-preserving, is the property held by a logical system if its inference rules only derive new information that is valid under the formal languages’ semantics. More precisely, if we can derive a sentence b through (finite) application of inference rules to a knowledge base a (which we will abbreviate a |- b, pronounced "a syntactically entails b"), it must be the case that a |= b. [Note we have introduced some duality in our usage of the word ’entails’ - from now on we read a |= b as "a semantically entails b".]

Completeness, the converse of soundness, completeness is the property held if any sentence which is semantically entailed by a knowledge base a can be derived by (finite) application of the inference rules of a logical system - formally represented by a |= b => a |- b.
We can conclude that in a logical system possessing both properties, a |- b <=> a |= b and our two definitions of entailment are equivalent. We take advantage of this when constructing proofs in the program to follow.