Return to Question

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. ... The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.

Edit 2: The last sentence is not precise and Reid Barton has an excellent comment on what I was actually thinking.

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory:

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. … The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.

Edit 2: The last sentence is not precise and Reid Barton has an excellent comment on what I was actually thinking.

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. ... The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. ... The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.

Edit 2: The last sentence is not precise and Reid Barton has an excellent comment on what I was actually thinking.

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. ... The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$.

Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory

Given a formula C, there is a translation giving a formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is classically derivable. ... The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.