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?

  • 1
    $\begingroup$ This sounds like a question about (pure) logic rather than computer science. It might be better to ask it on math.stackexchange.com. $\endgroup$ – Tsuyoshi Ito Sep 20 '10 at 1:18
  • 6
    $\begingroup$ I'd argue otherwise. Logic is one of the fundamental ingredients in theoretical computer science, especially the so-called Theory B track. $\endgroup$ – Dave Clarke Sep 20 '10 at 7:53
  • $\begingroup$ @supercooldave: I agree that logic is a fundamental ingredient in computer science, but I had guessed that this question would be answered more satisfactorily on math.stackexchange.com rather than here. That was before you posted an answer, of course. $\endgroup$ – Tsuyoshi Ito Sep 20 '10 at 10:40
  • 2
    $\begingroup$ @Tsuyoshi: I have heard that there are more logicians employed in computer science departments than in any other department, with logicians in logic departments being a positively rare breed. $\endgroup$ – Charles Stewart Sep 20 '10 at 13:13
  • 2
    $\begingroup$ @Suresh: We've seen a rise in theory-B over the last week. $\endgroup$ – Charles Stewart Sep 20 '10 at 18:40

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.


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.


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.

  • 1
    $\begingroup$ You wrote: "Whether or not the proposed semantics corresponds to one's intuitive notion of deduction is a philosophical matter." We could replace the word "semantics" in this sentence by "proof rules" and get the following sentence: Whether or not the proposed proof rules correspond to one's intuitive notion of deduction is a philosophical matter. My point here is that the specification of proof rules is a form of defining semantics. $\endgroup$ – Martin Sep 20 '10 at 12:21
  • 1
    $\begingroup$ By specifying formal semantics and then proving the soundness and completeness with respect to this semantics, we have only shown that the semantics and proof rules are consistent, but it does not make the proof rules more "true", then if we had justified them directly using the intuitive notion of proof. $\endgroup$ – Martin Sep 20 '10 at 12:22
  • $\begingroup$ I disagree with what you say in the second paragraph. If we had defined syllogism to be sound and complete, we surely would have invented some other calculi and then shown that they can proof exactly the same statments as the syllogisms (i.e. they are sound and complete with reference to syllogisms). But surely, some logicians and philosophers would have come along and argued that the syllogisms are not enough. At the latest, Boole and Frege would have extended the set of rules, and Gentzen would have just as well invented his ND. $\endgroup$ – Martin Sep 20 '10 at 12:22
  • 1
    $\begingroup$ Regarding your first comment. Indeed, proof rules do define a logic and can in themselves be seen as a semantics. Indeed, it is quite common in programming language research that the semantics of a programming language are defined in a similar fashion (namely, via operational semantics). So your point is valid. On the other hand, work on semantics tries to find an absolute, non-operational meaning for the formula in the logic, one which is independent of the means of performing deduction. $\endgroup$ – Dave Clarke Sep 20 '10 at 12:51
  • 1
    $\begingroup$ @Martin, your responses to the answers people are posting seem "soft" and "unscientific" to me. Of course we don't need semantics, if by "need" you mean "is it in theory possible to re-derive all mathematical theorems from bizzare-but-provably-equivalent unsemantical logic L." But it's nice to have models! Models can be computer programs we want to verify, distributed systems we want to simulate, or ordered structures we can play Ehrenfeucht-Fraisse games over to prove P=FO(LFP). My question to you: can you name any computer science advantage to working with logics without semantics? $\endgroup$ – Aaron Sterling Sep 20 '10 at 13:34

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.