What could be the use of Modern Logic?

[Speakpigeon]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

What about computers? Well, same thing, I think. I did a fair amount of programmation in the past and never had to go beyond the basic laws of conjunction, disjunction and negation. You don't need to study modern logic to do that stuff.

So, I'm looking for examples you'd be aware of where modern logic is used for practical applications, and beyond the basics.

Thanks,
EB

 

[steve_bank]

Same answer as before. Logic is imbedd3ed everywhere in daily speech and analysis.

The form of a syllogism is usually not explicitly stated, that is for learning in class or some specific cases.. Part of the class I took in logic involved reading material and picking out the syllogism, and determining if the argument was valid. I am certainly not unique among peers, but with practice and experience the logical analysis of arguments became second nature without having to go through a series of conscious formal steps.

The skill is in picking out the propositions and conclusions in general arguments. Lawyers get paid to analyze logic and create logic.

Whenever I made a presentation to sell an idea to a group, the underlying reasoning was based on logic that could withstand scrutiny.

 

[Juma]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

What about computers? Well, same thing, I think. I did a fair amount of programmation in the past and never had to go beyond the basic laws of conjunction, disjunction and negation. You don't need to study modern logic to do that stuff.

So, I'm looking for examples you'd be aware of where modern logic is used for practical applications, and beyond the basics.

Thanks,
EB

What is this thing you call ”modern logic”? Can you give an explicit example of something in modern logic that you think isnt used in ”real world”(what ever that is supposed to mean)?

Here is a nice text on what modern logic really is.
http://jarda.peregrin.cz/mybibl/PDFTxt/613.pdf

 

[Speakpigeon]

Same answer as before. Logic is imbedd3ed everywhere in daily speech and analysis.

The form of a syllogism is usually not explicitly stated, that is for learning in class or some specific cases.. Part of the class I took in logic involved reading material and picking out the syllogism, and determining if the argument was valid. I am certainly not unique among peers, but with practice and experience the logical analysis of arguments became second nature without having to go through a series of conscious formal steps.

The skill is in picking out the propositions and conclusions in general arguments. Lawyers get paid to analyze logic and create logic.

Whenever I made a presentation to sell an idea to a group, the underlying reasoning was based on logic that could withstand scrutiny.

It seems to me you effectively, if only implicitly, agree here with what I say in the OP:

As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

If you don't agree with what I say in this quote, can you make your disagreement explicit?
EB

 

[Speakpigeon]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

What about computers? Well, same thing, I think. I did a fair amount of programmation in the past and never had to go beyond the basic laws of conjunction, disjunction and negation. You don't need to study modern logic to do that stuff.

So, I'm looking for examples you'd be aware of where modern logic is used for practical applications, and beyond the basics.

Thanks,
EB

What is this thing you call ”modern logic”?

The expression of "modern logic" seems perfectly identified to me:

Modern Logic
https://en.wikipedia.org/wiki/History_of_logic#Rise_of_modern_logic

A number of features distinguish modern logic from the old Aristotelian or traditional logic, the most important of which are as follows: Modern logic is fundamentally a calculus whose rules of operation are determined only by the shape and not by the meaning of the symbols it employs, as in mathematics. Many logicians were impressed by the "success" of mathematics, in that there had been no prolonged dispute about any truly mathematical result. C.S. Peirce noted that even though a mistake in the evaluation of a definite integral by Laplace led to an error concerning the moon's orbit that persisted for nearly 50 years, the mistake, once spotted, was corrected without any serious dispute. Peirce contrasted this with the disputation and uncertainty surrounding traditional logic, and especially reasoning in metaphysics. He argued that a truly "exact" logic would depend upon mathematical, i.e., "diagrammatic" or "iconic" thought. "Those who follow such methods will ... escape all error except such as will be speedily corrected after it is once suspected". Modern logic is also "constructive" rather than "abstractive"; i.e., rather than abstracting and formalising theorems derived from ordinary language (or from psychological intuitions about validity), it constructs theorems by formal methods, then looks for an interpretation in ordinary language. It is entirely symbolic, meaning that even the logical constants (which the medieval logicians called "syncategoremata") and the categoric terms are expressed in symbols.

There's no substantial ambiguity there I think. It's true that the expression covers a very large area, but so do the terms "mathematics", "science", "physics", etc.

Can you give an explicit example of something in modern logic that you think isnt used in ”real world”(what ever that is supposed to mean)?

I think I already explained. As I understand it, the logic people need is really their intuitive sense of logic, i.e., broadly, syllogistic logic or maybe a little bit more than that. Modern science was already well established before Modern Logic could possibly be of any practical use somewhere around the 1930's. So, people don't need Modern logic at all, not even scientists I think, except for the convenience of the symbolic language it provides when people have to consider the more complicated formulae.

Still, maybe I wrong on this, which is why I'm calling on the expertise other people around here may have on this issue.

Here is a nice text on what modern logic really is.
http://jarda.peregrin.cz/mybibl/PDFTxt/613.pdf

Yes, interesting, but irrelevant. Look at the extract of Wiki article I provided above. It's more than good enough.
EB

 

[Juma]

The expression of "modern logic" seems perfectly identified to me:

Modern Logic
https://en.wikipedia.org/wiki/History_of_logic#Rise_of_modern_logic

A number of features distinguish modern logic from the old Aristotelian or traditional logic, the most important of which are as follows: Modern logic is fundamentally a calculus whose rules of operation are determined only by the shape and not by the meaning of the symbols it employs, as in mathematics. Many logicians were impressed by the "success" of mathematics, in that there had been no prolonged dispute about any truly mathematical result. C.S. Peirce noted that even though a mistake in the evaluation of a definite integral by Laplace led to an error concerning the moon's orbit that persisted for nearly 50 years, the mistake, once spotted, was corrected without any serious dispute. Peirce contrasted this with the disputation and uncertainty surrounding traditional logic, and especially reasoning in metaphysics. He argued that a truly "exact" logic would depend upon mathematical, i.e., "diagrammatic" or "iconic" thought. "Those who follow such methods will ... escape all error except such as will be speedily corrected after it is once suspected". Modern logic is also "constructive" rather than "abstractive"; i.e., rather than abstracting and formalising theorems derived from ordinary language (or from psychological intuitions about validity), it constructs theorems by formal methods, then looks for an interpretation in ordinary language. It is entirely symbolic, meaning that even the logical constants (which the medieval logicians called "syncategoremata") and the categoric terms are expressed in symbols.

There's no substantial ambiguity there I think. It's true that the expression covers a very large area, but so do the terms "mathematics", "science", "physics", etc.

Can you give an explicit example of something in modern logic that you think isnt used in ”real world”(what ever that is supposed to mean)?

I think I already explained. As I understand it, the logic people need is really their intuitive sense of logic, i.e., broadly, syllogistic logic or maybe a little bit more than that. Modern science was already well established before Modern Logic could possibly be of any practical use somewhere around the 1930's. So, people don't need Modern logic at all, not even scientists I think, except for the convenience of the symbolic language it provides when people have to consider the more complicated formulae.

Still, maybe I wrong on this, which is why I'm calling on the expertise other people around here may have on this issue.

Here is a nice text on what modern logic really is.
http://jarda.peregrin.cz/mybibl/PDFTxt/613.pdf

Yes, interesting, but irrelevant. Look at the extract of Wiki article I provided above. It's more than good enough.
EB

I dont think your wikipedia extract is informative in this case.
I was asking for something more specific: as calculus for mathematics. What corresponding area in modern logic do you not see any use for?

 

[Copernicus]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

What about computers? Well, same thing, I think. I did a fair amount of programmation in the past and never had to go beyond the basic laws of conjunction, disjunction and negation. You don't need to study modern logic to do that stuff.

So, I'm looking for examples you'd be aware of where modern logic is used for practical applications, and beyond the basics.

Thanks,
EB

I'm not sure why you exclude symbolic operators like conjunction, disjunction, and negation from "modern logic", but the general answer to your question would be "lots of things". It depends on what your needs are. If you do any kind of calculation with symbols, then the study of symbolic logic can give you important basic skills in that department. You ask a very general question, so it might be helpful to provide more specifics on what kind of "uses" you think would provide a helpful answer.

 

[Speakpigeon]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

What about computers? Well, same thing, I think. I did a fair amount of programmation in the past and never had to go beyond the basic laws of conjunction, disjunction and negation. You don't need to study modern logic to do that stuff.

So, I'm looking for examples you'd be aware of where modern logic is used for practical applications, and beyond the basics.

Thanks,
EB

I'm not sure why you exclude symbolic operators like conjunction, disjunction, and negation from "modern logic",

Do I? No, I don't think I do. Well, I'm sure I don't. Still, If you think I do, you should exhibit a quote of the offending bit.

but the general answer to your question would be "lots of things". It depends on what your needs are. If you do any kind of calculation with symbols, then the study of symbolic logic can give you important basic skills in that department. You ask a very general question, so it might be helpful to provide more specifics on what kind of "uses" you think would provide a helpful answer.

Regarding symbolic logic, I see using logical symbols, even proficiently, as not necessarily indicative of using modern logic beyond the basics, i.e. beyond what most people do using their intuitive sense of logic, i.e. beyond syllogistic logic. Using a symbolic language to express logical relations is obviously very convenient, helpful and effective but that in itself doesn't necessarily mean anybody is going to use it to express anything more than trivial logical relations.

Regarding uses, any use would do as long as it is clearly more than what people do relying on their intuitive sense pf logic. Logic is potentially of universal application, and all areas of application would be of interest here. There are obvious areas where you could expect higher rates of use, like mathematics, physics, computing, philosophy etc. Yet, many people did well in all these areas even before any specific method of formal logic was made publicly available. People did without formal logic prior to its introduction at the beginning of the 20th century and I suspect they have kept doing without it after that. And, of course, mathematics was well on its way before the inception of formal logic.

So, symbolic logic certainly helps but is it really necessary? And if so, do you have any specific examples?
EB

 

[Speakpigeon]

I dont think your wikipedia extract is informative in this case.

You specifically asked what it is I called "Modern Logic". That's what the Wikipedia extract describes.

I was asking for something more specific: as calculus for mathematics.

All areas seem concerned, but examples in any specific area would do.

What corresponding area in modern logic do you not see any use for?

Whatever method is used to deduce the truth of such propositions as statements, formulas, theorems etc.. And a method would be a small number of rules of inference.
EB

 

[Juma]

You specifically asked what it is I called "Modern Logic". That's what the Wikipedia extract describes.



All areas seem concerned, but examples in any specific area would do.

What corresponding area in modern logic do you not see any use for?

Whatever method is used to deduce the truth of such propositions as statements, formulas, theorems etc.. And a method would be a small number of rules of inference.
EB

It seems to me that people have already told how they use modern logic but each time you dismiss them
By deckaring that that wasnt what you asked for. Thus I will only ask you one mire time: specify some soecific that
You deem part of modern logic and then we can see if we find if that is used or not.

 

[steve_bank]

From the wiki page I have no idea what 'modern logic' means. It is a convoluted mish mash of abstraction's. Philosophers talking about logic. It looks like modern logic refers to logic in math based in Abstract Algebra. Symbolic Logic has a number of forms.

Logic in language is limited to AND, OR, NOR, If THEN..etc. How you frame context is hand waving IMO. It would take me a few weeks to wade through the wiki page and follow up to get a complete picture. I'm guessing Modern Logic equates to Symbolic Logic, which has wide application in many areas. Not just science.

 

[Copernicus]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that...

I'm not sure why you exclude symbolic operators like conjunction, disjunction, and negation from "modern logic", but the general answer to your question would be "lots of things". It depends on what your needs are. If you do any kind of calculation with symbols, then the study of symbolic logic can give you important basic skills in that department. You ask a very general question, so it might be helpful to provide more specifics on what kind of "uses" you think would provide a helpful answer.

Do I? No, I don't think I do. Well, I'm sure I don't. Still, If you think I do, you should exhibit a quote of the offending bit.

See the bolded part in what you said above. The syntax and semantics of those operators are formally defined in "modern logic". Those are low level basic operators, but computer scientists need to be able to prove that their formalisms work as advertised. They need formal logic for that. No "modern logic", no compiler. In fact, some high level programming languages are modeled after logical notation. LISP and its derivatives use lambda operators.

but the general answer to your question would be "lots of things". It depends on what your needs are. If you do any kind of calculation with symbols, then the study of symbolic logic can give you important basic skills in that department. You ask a very general question, so it might be helpful to provide more specifics on what kind of "uses" you think would provide a helpful answer.

Regarding symbolic logic, I see using logical symbols, even proficiently, as not necessarily indicative of using modern logic beyond the basics, i.e. beyond what most people do using their intuitive sense of logic, i.e. beyond syllogistic logic. Using a symbolic language to express logical relations is obviously very convenient, helpful and effective but that in itself doesn't necessarily mean anybody is going to use it to express anything more than trivial logical relations.

That really depends on the "anybody" you are thinking about. Certainly, the proverbial "man in the street" doesn't need formal logic to live his life, but it is essential to a number of specialized disciplines. Again, like all the others responding to you, I don't quite get what kind of "use" you have in mind. There are lots of uses for formal proofs, but not everyone needs to use them.

Regarding uses, any use would do as long as it is clearly more than what people do relying on their intuitive sense pf logic. Logic is potentially of universal application, and all areas of application would be of interest here. There are obvious areas where you could expect higher rates of use, like mathematics, physics, computing, philosophy etc. Yet, many people did well in all these areas even before any specific method of formal logic was made publicly available. People did without formal logic prior to its introduction at the beginning of the 20th century and I suspect they have kept doing without it after that. And, of course, mathematics was well on its way before the inception of formal logic.

So, symbolic logic certainly helps but is it really necessary? And if so, do you have any specific examples?
EB

I don't think anyone expects formal or mathematical logic to be of use to non-specialists, but you seem to be asking how it could be useful to non-specialists. You yourself just listed fields in which you think formal logics might be useful, but then you seemed to casually dismiss the role of such logics on the ground that people outside of those fields wouldn't need them. If you are asking what practical use formal logic has in our everyday lives, I suppose it is reasonable to dismiss it as non-essential. So is calculus and quantum mechanics, for that matter. Most of us get by without having a lot of practical use for them.

 

[Speakpigeon]

What's the use of Modern Logic?

My view is that modern logic is effectively useless. As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

I'm not sure why you exclude symbolic operators like conjunction, disjunction, and negation from "modern logic",

Do I? No, I don't think I do. Well, I'm sure I don't. Still, If you think I do, you should exhibit a quote of the offending bit.

See the bolded part in what you said above.

I still don't see that I "exclude symbolic operators like conjunction, disjunction, and negation from "modern logic"" as you implied.

Whenever you have the time.

The syntax and semantics of those operators are formally defined in "modern logic".

Good, but were the dictionary definitions of English words necessary for the English to start to speak English to each other and to start to communicate in English and work together effectively?

As I said in same post, formal logic is very convenient and helpful:

Using a symbolic language to express logical relations is obviously very convenient, helpful and effective but that in itself doesn't necessarily mean anybody is going to use it to express anything more than trivial logical relations.

So, symbolic logic certainly helps but is it really necessary?

Formal logic is very convenient and helpful, but is it is ever necessary?

Those are low level basic operators, but computer scientists need to be able to prove that their formalisms work as advertised. They need formal logic for that. No "modern logic", no compiler. In fact, some high level programming languages are modeled after logical notation. LISP and its derivatives use lambda operators.

These are practical considerations. You get fired if you don't know the language and economic actors compete with one another so that in the end you have to be effective and to achieve that you have to use formal logic. Yes, I know that.
EB

 

[Speakpigeon]

Again, like all the others responding to you, I don't quite get what kind of "use" you have in mind.

Answer in same post:

Regarding uses, any use would do as long as it is clearly more than what people do relying on their intuitive sense pf logic. Logic is potentially of universal application, and all areas of application would be of interest here.

There are lots of uses for formal proofs

Answer in same post:

And if so, do you have any specific examples?

EB

 

[Speakpigeon]

Same answer as before. Logic is imbedd3ed everywhere in daily speech and analysis.

The form of a syllogism is usually not explicitly stated, that is for learning in class or some specific cases.. Part of the class I took in logic involved reading material and picking out the syllogism, and determining if the argument was valid. I am certainly not unique among peers, but with practice and experience the logical analysis of arguments became second nature without having to go through a series of conscious formal steps.

The skill is in picking out the propositions and conclusions in general arguments. Lawyers get paid to analyze logic and create logic.

Whenever I made a presentation to sell an idea to a group, the underlying reasoning was based on logic that could withstand scrutiny.

It seems to me you effectively, if only implicitly, agree here with what I say in the OP:

As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

If you don't agree with what I say in this quote, can you make your disagreement explicit?
EB

 

[steve_bank]

Same answer as before. Logic is imbedd3ed everywhere in daily speech and analysis.

The form of a syllogism is usually not explicitly stated, that is for learning in class or some specific cases.. Part of the class I took in logic involved reading material and picking out the syllogism, and determining if the argument was valid. I am certainly not unique among peers, but with practice and experience the logical analysis of arguments became second nature without having to go through a series of conscious formal steps.

The skill is in picking out the propositions and conclusions in general arguments. Lawyers get paid to analyze logic and create logic.

Whenever I made a presentation to sell an idea to a group, the underlying reasoning was based on logic that could withstand scrutiny.

It seems to me you effectively, if only implicitly, agree here with what I say in the OP:

As I see it, humans do use logic, but only use very basic logic, i.e. syllogistic logic, like all men are mortal, Socrates is a man, therefore Socrates is mortal. You don't need modern logic to understand that.

If you don't agree with what I say in this quote, can you make your disagreement explicit?
EB

It could not be more explicit. you have used that retort once too many times. One trick poney, but maybne that is too deep.

 

[Speakpigeon]

It seems to me you effectively, if only implicitly, agree here with what I say in the OP:


If you don't agree with what I say in this quote, can you make your disagreement explicit?
EB

It could not be more explicit. you have used that retort once too many times. One trick poney, but maybne that is too deep.

Declining to answer a perfectly legitimate question is just as telling.

No information is information.

ECONOMIC ASPECTS OF SUSTAINABLE DEVELOPMENT IN CROATIA
http://www.un.org/esa/agenda21/natlinfo/countr/croatia/eco.htm

No information is available.

No information is information.

EB

 

[Phil Scott]

I'm only aware of one important use for formal logic, and that is formal verification. This is the field where you want to prove some mathematical theorem, or prove that a computer system behaves as it should, but it's not feasible to write out the proof by hand, or, if you tried, the proof would end up so convoluted that it would be very difficult to be sure that it doesn't contain a mistake somewhere.

Instead, you can write a computer program that is designed to represent propositions given in a formal logic, and check that arguments made from these propositions meet syntactic requirements for validity: in other words, you write a proof checker for formal logic. You then work with the computer to build your hideously complex proof, feed it through the verification program, and thus become absolutely convinced that the final conclusion is sound.

Famous successes for this include the verification that the SeL4 microkernel is bug-free, that the CompCert compiler compiles C code according to specification, and that Kepler's conjecture is a mathematical theorem.

These results went through in verifiers for formal logics that are a good deal more sophisticated than Boolean logic, and indeed, first-order logic. The SeL4 proof and Kepler's Theorem were in the simply typed lambda calculus. CompCert is in an even more powerful theory called the calculus of constructions.

 

[Copernicus]

I'm not sure why you exclude symbolic operators like conjunction, disjunction, and negation from "modern logic",

Do I? No, I don't think I do. Well, I'm sure I don't. Still, If you think I do, you should exhibit a quote of the offending bit.

See the bolded part in what you said above.

I still don't see that I "exclude symbolic operators like conjunction, disjunction, and negation from "modern logic"" as you implied.

Whenever you have the time.

My point was only that those operators receive precise definitions within formal logic (what you and a few others call "modern logic"), whereas they do not in less formal approaches. You seemed to think that they didn't need to be assigned meaning. Semantics is actually important. However, belaboring this point really isn't. So, if you don't get it, I'm fine with that.

The syntax and semantics of those operators are formally defined in "modern logic".

Good, but were the dictionary definitions of English words necessary for the English to start to speak English to each other and to start to communicate in English and work together effectively?

I never said they were. However, it is a false equivalence to think of the semantics of formal symbolic systems as equivalent to the semantics of natural language. Natural language dictionaries only inform you of word senses in common usage. They don't prescribe usage, although many people try to use them for that purpose. And they never actually give comprehensive descriptions of word meanings, only concise heuristic statements. The semantics of logical and mathematical operators are not descriptions, but ironclad comprehensive prescriptions of usage. Truth tables exhaustively describe meanings.

As I said in same post, formal logic is very convenient and helpful:

Using a symbolic language to express logical relations is obviously very convenient, helpful and effective but that in itself doesn't necessarily mean anybody is going to use it to express anything more than trivial logical relations.

So, symbolic logic certainly helps but is it really necessary?

Formal logic is very convenient and helpful, but is it is ever necessary?

Necessary for what? You seem to have built up a straw man in your mind over what everyone thinks logic is good for. I don't think that I'm the only commentator here with that impression. Everyone else seems to have trouble grasping your implicit sense of necessity. Logic is a method for calculating truth consistency across a set of propositions. There are important applications for that in mathematics, computer science, philosophy, linguistics, and a host of other fields of study that require precise calculations. These are far from "trivial logical relations". Nobody is claiming that formal logic is needed to buy a hot dog or drive a car.

Those are low level basic operators, but computer scientists need to be able to prove that their formalisms work as advertised. They need formal logic for that. No "modern logic", no compiler. In fact, some high level programming languages are modeled after logical notation. LISP and its derivatives use lambda operators.

These are practical considerations. You get fired if you don't know the language and economic actors compete with one another so that in the end you have to be effective and to achieve that you have to use formal logic. Yes, I know that.
EB

Good. Then maybe you are on the path to answering your own question. There are necessary applications. You just have to figure out why some jobs require logic. Maybe you don't think that jobs which need precise logical tools in research and engineering projects are important, but it turns out that those doing the hiring do.

 

[Speakpigeon]

I'm only aware of one important use for formal logic, and that is formal verification. This is the field where you want to prove some mathematical theorem, or prove that a computer system behaves as it should, but it's not feasible to write out the proof by hand, or, if you tried, the proof would end up so convoluted that it would be very difficult to be sure that it doesn't contain a mistake somewhere.

Instead, you can write a computer program that is designed to represent propositions given in a formal logic, and check that arguments made from these propositions meet syntactic requirements for validity: in other words, you write a proof checker for formal logic. You then work with the computer to build your hideously complex proof, feed it through the verification program, and thus become absolutely convinced that the final conclusion is sound.

Famous successes for this include the verification that the SeL4 microkernel is bug-free, that the CompCert compiler compiles C code according to specification, and that Kepler's conjecture is a mathematical theorem.

These results went through in verifiers for formal logics that are a good deal more sophisticated than Boolean logic, and indeed, first-order logic. The SeL4 proof and Kepler's Theorem were in the simply typed lambda calculus. CompCert is in an even more powerful theory called the calculus of constructions.

Thanks, Phil, I'll try to have a close look into that. If you had a few links you think could help I would appreciate it!
EB