The Purpose is to build a Machine for Logic that is
able to prove that a Logical Consequence is correct.
The problem is when one wants to build a machine to proof this, one has to consider all interpretations which takes a lot of time. In practice one does this by avoiding this.
So one need to create a mechanical method for solving logical Problems.
In order to this one has to come up with a syntactical method not a semantic method. One has to implement logical Consequence simply be a syntactical method, a so called Calculus. For this logical Calculus two things must be proven. First the Correctness that every syntactic entailment also must be a semantic entailment. Vice versa one has to prove the Completeness that all Semantic Entailments on the same hand must be syntactic Entailments, then one can also use the syntactic Entailments method for the Semantic Entailment.
Theory (knowledge base) T, i.e. T ⊨ F, if
all models of T are also models of F