Logic And Programs

Posté par alpheccar le08 Jan 2007 à 20:11 CEST

One month ago I did not know a lot about logic : just truth tables for some connectives. But, for some time I have been having fun with Haskell and it finally convinced me to use some of my spare time to learn about logic. Of course, you can code in Haskell without knowing a lot about logic, the Curry-Howard isomorphism and all that but it is much more fun to code in Haskell if you know a bit about logic.

So, thanks to my Christmas vacations, and the fact that being French I have long vacations :-), I read a few papers about logic : classical, intuitionistic, modal, linear etc... This post is an attempt to summarize what I think I have understood and I hope it may be useful to other newbies too.

What is logic ?

There are several logics and since they are all using the word "logic" I assumed there was really something in common between them. So, my first question was : what is logic ?

I thought it was related to the connectives. Perhaps "logics" are the formal theories which have in common a basic set of connectives. But, it looks wrong since linear logic is using a different set.

Tarskian Semantic

So, logic is perhaps related to truth. It is the Tarskian semantic of logic. Logic is the study of arguments which are preserving truth. But, I have a problem with this way of defining logic. Indeed, you need a model to interpret your logical sentences and define what is true in that model. But, to define a model you need set theory. But set theory is using logic for its own formalization. So, it looks like a vicious circle. And some logics are multi-valued so generalizing the meaning of "truth".

Moreover, there is an element of omniscience in this approach to logic since it is not constructive. You know some properties are true but you cannot give an example of object satisfying the property.

This approach is very useful, I agree. Model theory is full of cool results but it cannot be the fundamental justification for logic. What is logic and why it is so important to us human beings ?

Heyting semantic

So, another idea is to look at an internal justification for logic instead of looking at an external one. We are no more focusing on what is true since it is very difficult to define what is "truth". We prefer to look at what is provable and we try to do it in such a way that the omniscience element (inherited from the Tarskian view of logic) is removed. It is the intuitionistic logic. But what is a proof ? Is it just a derivation in a formal system and in that case why choosing one rather than another ?

Some people are trying to justify the choice based on symetry of the rules. But, it is no more a good argument than trying to justify superstring theory because of its cool mathematics. If logic is restricted to some category of formal systems then it means they must have something special.

Initially, logic is coming from the language as a formalization of some thought processes. What we see is that some subset of our conscious thoughts can be captured in a set of formal rules. That subset can be formalized because it is about the manipulation of symbols following some rules where the modus ponens is playing a key role.

So, my guess is : the fundamental reason for saying that a formal system is a logic is its computational content and I am going to explain what it means. It is the only way I can make sense of the word "logic".

The corollary is that some "logics" should not be called logics since they do not respect the fundamental properties which are allowing to give a computational content to the logic rules.

I am not a philosopher and this definition of logic is clearly not without problems. But, I have not found any other good definition which is satisfying me.

Some other people are just defining a logic as a preorder where the implication connective is the preorder between propositions. This approach is based upon a categorical point of view. And, you also want to define an equivalence of proof which is not easy for classical logic or modal logics.

Natural deduction

So, let's assume that being a logic just means that there is a computational content in the formal system and let's see what it could mean.

When I was in high school, they explained to me the implication connective with a truth table and I could not make sense of it.

For me, => was related to proofs but I could not see how. It was not natural to me. Natural deduction is a syntax which is assumed to represent a proof in a way which is more natural and corresponding to the practise.

For instance:

We have two hypothesis from which we can deduce a conclusion involving the AND connective.

Then, the natural deduction rule for => is:

Which means that you can replace a proof of B from hypothesis A with A => B

A => B is a summary of the fact that somewhere you was able to prove B from A.

A is between bracket because A is a temporary hypothesis that you can use only locally to prove B. As soon as it is done, you discharge A which is no more available and you just remember that B can be proved from A.

Then, if you can prove A somewhere else in your proof, you'll be able to prove B with:

Which is just a way to "call" the subproof of B from A and use it in this special case. Hey ! It looks like a function call !

The first two rules are introduction rules (for ^ and =>) : we build a compound expression from subcomponents. The last rule is an elimination rule.

Obviously, if I am writing:

it is just equivalent to

I do not need to make this detour by A => B. In short, if I use my function only once, I may not need to define a function and can just inline it.

Proof normalisation

So, we see that when an introduction rule is followed by an elimination rule for the same connective then there is a possible simplification.

A normal proof is a proof where no more simplification is possible. Do we always have a normal proof ? If yes the system is strongly normalizing. Is the normal form unique ? If yes, the system of rules has the Church-Rosser property.

It depends on how the temporary hypothesis are used. In classical logic, you can reuse the temporary hypothesis as many times as you want to prove B (even 0 times). In relevant logic you are not allowed to use it zero times. In affine logic, you are not allowed to use it more than once. In linear logic, the hypothesis can be used only once.

The Church-Rosser property is not true for classical logic. So, the simplification process will lead to different normal forms according to how the simplification is done. In linear logic or intuitionistic one, the Church-Rosser property is satisfied and you get only one answer.

On the meaning of being constructive

This process of simplification, of normalisation of the proof, is looking like the process of reduction of a lambda expression. The computational content of the logic is here. So we may say that the classical logic is not a logic since it is not giving a unique result through this simplification process ? It is but with an element of indeterminacy. It is indeed possible to extend the lambda calculus with an erratic choice operator so that the proof simplification of classical logic has an equivalent in the lambda calculus world.

Another way to connect the classical logic to lambda calculus is to restrict the simplifications that can be done on a proof. Then, you are dropping some information (some normal forms are not generated) but you remove the indeterminacy. One way to do that is to introduce a continuation operator as will be explained by sigfpe soon.

If there are many logics (according to my crazy definition) it is because there are many way to restrict the pure untyped lambda calculus to avoid the non terminating forms. So a logic would be a computational process where all programs are terminating.

Modal logics

The system of introduction/elimination of classical logic can be reduced to remove its non constructive aspect and we get intuitionistic logic. But, the system can also be extended to express modalities. A truth can be relative to some world : a truth can be relative to the time, or it can be relative to some possible state that can be reached from the current ones. Modality logics are formalizing this idea of world dependent truth. There are several modal logics. Too many ones ?

In fact, it is perhaps wrong to use the word logic for these formal systems. It is not obvious if we have the normalisation property in all of them (I have not found any paper confirming it. Just some doubts in some papers).

And, they are strongly related to coalgebra. For instance, you can define a temporal logic from the coalgebra used to specify a system : like streams, state machines ...

Interrogations

• How crazy is my definition of logic ? How wrong ?
• If I am not wrong, Church-Rosser is a property of the presentation of a system of rules. So, what does it imply for classical logic ? Do we have some presentation for which the property is true ? Then what does it mean for the non constructivity of classical logic ?
• What's the status of the fix point operator on the logic side ?

Post scriptum

This is a blog so don't expect a high level of rigor. I know that many parts of this post are fuzzy, unclear or wrong. I am just trying to communicate an idea, a way of looking at logic which is different from what an outsider may know about the topic.

So, to correct my mistakes, or my bad summary, here are some references:

Classical logic and Curry Howard

• Classical Logic is better than Intuitionistic Logic: A Conjecture about Double-Negation Translations

• Classical Logic and Computation

• Call-by-value is dual to call-by-name

Intuitionistic logic

• History of constructivism in the 20th century

Natural deduction and sequent calculus

• Proof Theory and Philosophy

  Pas de tags