Logic

What do derivation systems in a formal logical language tell us about logic? Or about the propositions in the proof? Are their purpose only to show us that a particular proof or argument can be demonstrated using that particular language? IN other words, why do we have derivations in formal logic ... what is their grand purpose?

Comments

Logic is about what follows from what. But what follows from what isn't always obvious (or else, e.g., pure maths would be a lot easier than it is). So we need ways of demonstrating unobvious entailments.

And a standard way of doing this is to show how we can get from the given premisses to the intended conclusion by a sequence of small steps, each of which is guaranteed to be truth-preserving. If we can break down the big inferential leap from premisses to conclusion into smaller inferential moves, each one of which is evidently valid, that shows the big leap is valid too.

Now all this applies equally to informal reasoning -- e.g. derivations or proofs in informal mathematics -- and to formally tidied-up reasoning alike. There's nothing mysterious then about derivations in formal logic. They just do in a regimented way, in some tightly constrained formal language, the sort of thing we usually do in a less regimented way. And given a formal version of a proof, we can read back an informal, ordinary-language version of the proof (at the risk of prolixity and getting tangled with quirks of the vernacular).

For more about the notion of a proof or derivation, and about the relation between informal and formalized versions, see any introductory logic text. E.g. my An Introduction to Formal Logic (Ch. 5 on proofs, Ch. 7 on why we might want to go formal).

Peter always gets to these before I do. I agree with what he says, but will add a couple points.

First, modern logic emerges in the work of Gottlob Frege, one of whose contributions was the first formal system of logic. Frege is explicit about his motivations. Here's a passage from his paper "On Mr Peano's Conceptual Notation and My Own", from 1897:

"I became aware of the need for a concpetual notation [formal language] when I was looking for the fundamental principles upon which the whole of mathematics rests. ...For an investigation such as I have in mind here, it is not sufficient just for us to convince ourselves of the truth of a conclusion, as we are usually content to do in mathematics; on the contrary, we must also be made aware of what it is that justifies our conviction, and upon what primitive laws it is based. For this are required fixed guiding-lines, along which the deductions are to run; and in verbal languages these are not provided. If we try to list all the laws governing the inferences which occur when arguments are conducted in the usual way, we find an almost unsurveyable multitude which apparently has no precise limits. The reason for this, obviously, is that these inferences are composed of simpler ones. And hence it is easy for something to intrude which is not of a logical nature and which consequently ought to be specified as an axiom. This is where the difficulty of discerning the axioms lies: for this the inferences have to be resolved into their simple components."

So Frege's motivation was this: We want to know on exactly which assumptions a given theorem rests. But, even if we specify our assumptions clearly in advance, how we be sure some other, as yet unspecified assumption has not tacitly been made somewhere along the way? Answer: We can be sure, if we carry out our argument in a formal language and clearly specify the forms of inference we are going to use in such a way that it is always possible to tell, on purely formal grounds, whether we have indeed reasoned in accordance with those rules.

Nowadays, people rarely carry out arguments in formal systems---except for students in logic classes. But that does not mean that formal argument has become any less important. It is, rather, that we have a developed a good sense for what such reasoning is like, and we can usually tell pretty well when an informal argument could or could not be carried out in such a system. But when things become unclear, then people who are interested in the sort of question in which Frege was interested---logicians---do start formalizing things, if not to the same degree Frege did, then at least to some degree. I've recently had to do just that sort of thing myself in a study of the question what sorts of principles are involved in "semantic" consistency proofs.

One other point. Both in Peter's remarks and in my preceding remarks, the focus is primarily on what logicians call "soundness": Formal arguments can be used to establish the validity of inferences, because what is formally derivable really does follow. There are other things to be said about the significance of completeness: the fact that all valid first-order inferences can be derived using an appropriate set of formal rules. This is extremely important to the study of the notion of computation as it relates to formal theories. Peter's other book, An Introduction to Gödel's Theorems, is a nice introduction to that material.

Read another response by Peter Smith, Richard Heck

Read another response about Logic