I read a book which says that in Predicate Calculus, syntactic theorem proving is identical (complete and sound) with semantic entailment and this is very useful because it is easier to prove positive witnesses in natural deduction whereas when you seem to fail you better switch to semantic account to demonstrate a counter-example.Particularly Logic in computer science saysto show that    is valid, we need to provide a proof of  from .  Yet, how can we show that  is not a consequence of ? Intuitively,  this is harder; how can you possibly show that there is no proof of  something? You would have to consider every candidate proof and show  it is not one. Thus, proof theory gives a positive characterisation  of the logic; it provides convincing evidence for assertions like     is valid, but it is not very useful for establishing evidence  for assertions of the form    is not valid.Semantics, on the other hand, works in the opposite way. To show  that  is not a consequence of  is the easy bit: find a model in  which all _i are true, but  isnt. Showing that  is a consequence  of , on the other hand, is harder in principle. For propositional  logic, you need to show that every valuation (an assignment of truth  values to all atoms involved) that makes all _i true also makes   true. If there is a small number of valuations, this is not so bad.  However, when we look at predicate logic, we will find that there are  infinitely many valuations, called 'models' from hereon, to consider.  Thus, in semantics we have a negative characterisation of the logic.  We find establishing assertions of the form    ( is not a  semantic entailment of all formulas in ) easier than establishing    ( is a semantic entailment of ), for in the former case we need  only talk about one model, whereas in the latter we potentially have  to talk about infinitely many. All this goes to show that it is  important to study both proof theory and semantics. For example, if  you are trying to show that  is not a consequence of  and you have a  hard time doing that, you might want to change your strategy for a  while by trying to prove the validity of   . If you find a proof,  you know for sure that  is a consequence of . If you cant find a  proof, then your attempts at proving it often provide insights which  lead you to the construction of a counter example. The fact that proof  theory and semantics for predicate logic are equivalent is amazing,  but it does not stop them having separate roles in logic, each  meriting close study.I was sure that we can prove the opposite by proving   and wondered why do we need the entailment. Now I see that validity of the opposite has nothing to do with validity of affirmative statement. Thanks. What we need is the satisfaction of the , which says that there is a counterexample. We do not need the validity of . But why semantics instead of proof? Do you say that semantics is in patrimony of satisfaction whereas proof theory is dedicated to validity?I have mistakenly thought that not being able to prove  means that  is absurd and, thus, you can prove . But, this seems not to be the case.
Why  for affirmative predicates and  for negations?
terminology;logic;first order logic