Why do we need formal semantics for predicate logic?

Question

Consider this question solved. I will not pick a best answer as all of them have contributed to my understanding of the topic.

Im unsure what benefit we have by formally defining the semantics of predicate logic. But I do see value in having a formal proof calculus. My point is that we would not need formal semantics to justify the inference rules of proof calculi.

We could define a calculus that mimicks the "laws of thought", i.e. the rules of inference that have been used by mathematicians for hundreds of years to proof their theorems. Such a calculus already exists: natural deduction. Then we would define this calculus to be sound and complete.

This can be justified by realising that the formal semantics of predicate logic is just a model. The appropriateness of the model can only be justified intuitively. Thus, by showing that natural deduction is sound and complete with reference to the formal semantics does not make natural deduction more "true". It would be just as good if we would directly justify the rules of natural deduction intuitively. The detour using formal semantics gives us nothing.

Then, having defined natural deduction to be sound and complete, we could show the soundness and completeness of other calculi by showing that the proofs they produce can be translated to natural deduction and vice versa.

Are my reflections above correct? Why is it important to prove the soundness and completeness of proof calculi by reference to formal semantics?

Answer 1

A minor comment, and a more serious answer.

First, it doesn't make sense to declare a natural deduction system complete by fiat. Natural deduction is interesting precisely because it has a natural internal notion of consistency and/or completeness -- namely, cut-elimination. This is a fantastic theorem, and IMO fully justifies attempts to give purely proof-theoretic semantics (and by the CH correspondence, it likewise justifies the use of operational methods in programming language semantics). But this is interesting precisely because it offers a more refined notion of getting the logic right than consistency. Taking the proof theoretic road means you'll have to do more work, but in exchange you get stronger results.

However, it happens that sometimes the logic per se takes a secondary role. We may begin with a (family of) models, and then look for ways of talking syntactically about them, using a logic. The soundness and completeness of a logic with respect to a family of models indicates that the logic really does capture everything both interesting and true you can say about the class of models. A concrete example of when models are more interesting than the logical theories occurs in program analysis and model checking. There, the usual thing to do is to take your model to be the execution of a program, and the logic to be some fragment of temporal logic. The propositions you can say in these languages are (deliberately) not terribly exciting -- e.g., null pointer dereferences never occur -- but it's the fact that it applies to actual program runs that gives it interest.

Answer 2

I'll just add another perspective to augment the above responses. First, these reflections are worthwhile, and many people have had similar ideas. In philosophy this is sometimes called "proof-theoretic semantics", appealing to work by Nuel Belnap, Dag Prawitz, Michael Dummett and others in the 60s and 70s, who themselves appeal back to Gentzen's work on natural deduction. Per Martin-Löf and Jean-Yves Girard also seem to propose variants of this position in their writings. And speaking very broadly, in programming languages this is the "syntactic approach to type soundness".

The thing is that even if you accept that the rules of logic do not need a separate semantic interpretation, it's not very interesting/useful to say that they are self-justified and leave it at that. The question is what a formal semantics accomplishes, and whether it's possible to achieve the same with fewer detours. However, the project of unifying model theory with analytic proof theory is important but still unresolved, being actively pursued along many different fronts including categorical logic, game semantics, and Girard's "ludics". For example, in addition to what Charles mentioned, another qualitative benefit of having models is the ability to provide concrete counterexamples to non-theorems, and the questions is how to make sense of this in a "direct" approach. For one ludics-inspired answer, see "On the meaning of logical completeness" by Michele Basaldella and Kazushige Terui.

Answer 3

A formal semantics provide a direct meaning of the terms in the calculus independently of the syntactic proof rules for manipulating them. Without a formal semantics how can you state whether or not the rules of deduction are correct (soundness) or whether you have enough of them (completeness)?

There have been "laws of thought" proposed before natural deduction came about. Aristotle's syllogisms were one such collection. If we had define them to be sound and complete we'd perhaps still be using them today, rather than developing more advanced logical techniques. The point being, if the syllogisms completely captures the laws of thought, why would we need to devise any further logics. What if they were in fact inconsistent? Having a semantics along with the formal proof calculus and the soundness and completeness proofs connecting them provides a measuring stick for judging the value of such a reasoning system. It would no longer stand in isolation.

Whether or not the proposed semantics corresponds to one's intuitive notion of deduction is a philosophical matter. Consider the difference between classical and intuitionistic logic, the essence of which is whether the law of excluded middle ($X\lor \neg X$) should be considered logically valid. Vast amounts of almost religious work has gone into arguing the validity of intuitionistic logic (see Intuitionism). So we cannot even agree on whether the a single notion of deduction makes sense. Beall and Greg Restall even go as far as arguing that we should accept that there is no one true logic and adopt a pluralistic attitude, using the most appropriate logic for the occasion. Given the plethora of logics available to computer scientists (linear logic, separation logic, higher-order constructive logic, many modal logics, all in classical and intuitionistic varieties), adopting a pluralistic attitude is something most of us probably haven't given a second thought, because logics are a tool to solve a particular problem and we try to select the most appropriate one. A formal semantics is one way of judging the appropriateness of the logic.

Another reason for having a formal semantics is that there are more logics than predicate calculus. Many of these logics are designed to reason about a particular kind of system. (I'm thinking about modal logics). Here the class of systems is known and the logic comes later (although, historically, this is also not true). Again, soundness tells us whether the axioms of the logic correctly capture the "behaviour" of the system, and completeness tells us whether we have enough axioms. Without a semantics, how would we know whether the rules of deduction are sufficient and not nonsense?

One example logic which was defined purely syntactically and work is still ongoing to provide it with a formal semantics is BAN logic for reasoning about cryptographic protocols. The logical inference rules seem reasonable, so why provide a formal semantics? Unfortunately, BAN logic can be used to prove that a protocol is correct, yet attacks on such protocols may exist. The deduction rules are therefore wrong, at least with respect to the expected semantics.

Answer 4

I agree with supercooldave, but there's another, more pragmatic reason for wanting more than some set or other of inference rules that characterise a logic: a given set of inference rules tends not to be good for answering the kind of problems faced when putting the logic to use.

If you have a logic specified by a list of axioms and couple of rules as a Hilbert system, it's usually going to be hard work to figure out how to prove a given theorem in the system, and without a theoretical insight, you are not going to be able to prove that a given proposition cannot be proven in the system. Traditional models are good for proving properties that hold for the whole logic by induction.

Four kinds of tools are useful to solve problems that most logicians want to solve, arranged from least to most semantic:

1. Hilbert-style systems are good for characterising the logical consequence relation of a logic, and they are usually good for categorising several logics, such as rival modal logics;
2. Tableau systems are good for formalising decision algorithms. Typically if a logic is decidable, one can find a terminating tableau system as a decision algorithm, and if not one can find a potentially non-terminating tableau system that provides a semi-decision procedure. If one wants to show an upper bound on the complexity of decidability (i.e., the complexity class of a logic), tableau systems are generally the first place one looks.
3. Analytic proof theories, such as Gentzen's natural deduction and sequent calculus, give representations of proofs that are good for reasoning, and offer the notion of analytic proof, which is useful for proving useful properties such as interpolation for a theory.
4. Tarski-style model theories are often even better for reasoning about logics, because they nearly completely abstract away from the syntactic details of the logic. In modal logic and set theory, they are so much better at delivering the results that those logicians tend to have very limited interest in tableau and analytic proof theory.

Since supercooldave mentioned intuitionistic logic: without the rule of the excluded middle, model theory becomes much more complicated, and analytic proof theories become more important, typically the semantics of choice. Algebraic techniques, such as category theory, become preferred for abstracting away from syntactic complexity.