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 says
to 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 ψ isn’t. 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 can’t 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.
