Skip to main content
Proof Assistants Beta

Return to Answer

added 76 characters in body
Source Link
xuq01
xuq01
  • 136
  • 5

Let me answer this question tangentially: while in our world the LEM may seem an unobjectionable and harmless principle, there are "worlds" where the LEM is false.

In the normal mathematical world, we just assume that some things exist. For example, piecewise functions exist: I can define a function $f : \mathbb{R} \rightarrow \mathbb{R}$ by $f(x) = 0$ if $x \leq 0$, $f(x) = x$ if $x > 0$. We can decide the equality ofGiven any two real numbers $a$ and $b$, precisely one of $a < b$, $a = b$ or $a > b$ is true. Some functions are provably discontinuous. Noncomputable functions from $\mathbb{N}$ to $\mathbb{N}$ exist and cam be defined. Everything seems perfectly normal, right?

But this is not the only "mathematical world" that existexists. There are other mathematical worlds out there. There is a world where all functions from $\mathbb{R}$ to $\mathbb{R}$ are not only continuous but smooth; however, of course this necessitates that piecewise functions could not exist. There is a world where all functions $\mathbb{N} \rightarrow \mathbb{N}$ are computable, and this necessitates that the Busy Beaver and other non-computable functions are undefinable. Of course, all of these nice properties necessitate that the LEM fails to hold.

More formally speaking, the mathematical worlds I've been talking about are the concept of (elemantary) toposes. Each topos has an internal language, where mathematics can be conducted; depending on your topos, however, the internal language may validate or fail to validate statements that may seem bonkers.

Now, by the Curry-Howard correspondence, each of the internal languages could be used as a programming language. This is the beginnings of type theory. In some of them, there exist oracles for things that are not explicitly computable, and the law of excluded middle is just one of them. Recall that the LEM has the type: $\forall P : \mathtt{Prop}, P \vee \neg P$; by Curry-Howard, it is a function that, when given a proposition $P$, returns either a proof that either $P$ is true or that $\neg P$ is true. Of course, it is impossible to write down the definition of this function via recursion, which can be done in any topos with enough structure (if it were possible, then all toposes admit the LEM, which is not the case!). But still we can allow this principle as a function that defines itself.

So, LEM and Curry-Howard are not really directly related. It's not right to think of Curry-Howard as a specific statement, but rather as a broad principle. In some toposes, the internal language actually does allow you to write functions to decide whether a Turing machine halts - they just aren't computable in the usual sense. Meanwhile there are a plethora of reasons why internal functions in toposes can fail to be computable, again in the usual sense, and the LEM is just one of them; it is nothing special.

If you want to learn more about this subject, I suggest reading Mac Lane & Moerdijk's Sheaves in Geometry and Logic, which is a fantastic introduction to topos theory. Also, you may be interested in the effective topos.

Let me answer this question tangentially: while in our world the LEM may seem an unobjectionable and harmless principle, there are "worlds" where the LEM is false.

In the normal mathematical world, we just assume that some things exist. For example, piecewise functions exist: I can define a function $f : \mathbb{R} \rightarrow \mathbb{R}$ by $f(x) = 0$ if $x \leq 0$, $f(x) = x$ if $x > 0$. We can decide the equality of two real numbers. Some functions are provably discontinuous. Noncomputable functions from $\mathbb{N}$ to $\mathbb{N}$ exist. Everything seems perfectly normal, right?

But this is not the only "mathematical world" that exist. There are other mathematical worlds out there. There is a world where all functions from $\mathbb{R}$ to $\mathbb{R}$ are not only continuous but smooth; however, this necessitates that piecewise functions could not exist. There is a world where all functions $\mathbb{N} \rightarrow \mathbb{N}$ are computable, and this necessitates that the Busy Beaver and other non-computable functions are undefinable. Of course, all of these nice properties necessitate that the LEM fails to hold.

More formally speaking, the mathematical worlds I've been talking about are the concept of (elemantary) toposes. Each topos has an internal language, where mathematics can be conducted; depending on your topos, however, the internal language may validate or fail to validate statements that may seem bonkers.

Now, by the Curry-Howard correspondence, each of the internal languages could be used as a programming language. This is the beginnings of type theory. In some of them, there exist oracles for things that are not explicitly computable, and the law of excluded middle is just one of them. Recall that the LEM has the type: $\forall P : \mathtt{Prop}, P \vee \neg P$; by Curry-Howard, it is a function that, when given a proposition $P$, returns either a proof that either $P$ is true or that $\neg P$ is true. Of course, it is impossible to write down the definition of this function via recursion, which can be done in any topos with enough structure (if it were possible, then all toposes admit the LEM, which is not the case!). But still we can allow this principle as a function that defines itself.

So, LEM and Curry-Howard are not really directly related. It's not right to think of Curry-Howard as a specific statement, but rather as a broad principle. In some toposes, the internal language actually does allow you to write functions to decide whether a Turing machine halts - they just aren't computable in the usual sense. Meanwhile there are a plethora of reasons why internal functions in toposes can fail to be computable, again in the usual sense, and the LEM is just one of them; it is nothing special.

If you want to learn more about this subject, I suggest reading Mac Lane & Moerdijk's Sheaves in Geometry and Logic, which is a fantastic introduction to topos theory. Also, you may be interested in the effective topos.

Let me answer this question tangentially: while in our world the LEM may seem an unobjectionable and harmless principle, there are "worlds" where the LEM is false.

In the normal mathematical world, we just assume that some things exist. For example, piecewise functions exist: I can define a function $f : \mathbb{R} \rightarrow \mathbb{R}$ by $f(x) = 0$ if $x \leq 0$, $f(x) = x$ if $x > 0$. Given any two real numbers $a$ and $b$, precisely one of $a < b$, $a = b$ or $a > b$ is true. Some functions are provably discontinuous. Noncomputable functions from $\mathbb{N}$ to $\mathbb{N}$ exist and cam be defined. Everything seems perfectly normal, right?

But this is not the only "mathematical world" that exists. There are other mathematical worlds out there. There is a world where all functions from $\mathbb{R}$ to $\mathbb{R}$ are not only continuous but smooth; however, of course this necessitates that piecewise functions could not exist. There is a world where all functions $\mathbb{N} \rightarrow \mathbb{N}$ are computable, and this necessitates that the Busy Beaver and other non-computable functions are undefinable. Of course, all of these nice properties necessitate that the LEM fails to hold.

More formally speaking, the mathematical worlds I've been talking about are the concept of (elemantary) toposes. Each topos has an internal language, where mathematics can be conducted; depending on your topos, however, the internal language may validate or fail to validate statements that may seem bonkers.

Now, by the Curry-Howard correspondence, each of the internal languages could be used as a programming language. This is the beginnings of type theory. In some of them, there exist oracles for things that are not explicitly computable, and the law of excluded middle is just one of them. Recall that the LEM has the type: $\forall P : \mathtt{Prop}, P \vee \neg P$; by Curry-Howard, it is a function that, when given a proposition $P$, returns either a proof that either $P$ is true or that $\neg P$ is true. Of course, it is impossible to write down the definition of this function via recursion, which can be done in any topos with enough structure (if it were possible, then all toposes admit the LEM, which is not the case!). But still we can allow this principle as a function that defines itself.

So, LEM and Curry-Howard are not really directly related. It's not right to think of Curry-Howard as a specific statement, but rather as a broad principle. In some toposes, the internal language actually does allow you to write functions to decide whether a Turing machine halts - they just aren't computable in the usual sense. Meanwhile there are a plethora of reasons why internal functions in toposes can fail to be computable, again in the usual sense, and the LEM is just one of them; it is nothing special.

If you want to learn more about this subject, I suggest reading Mac Lane & Moerdijk's Sheaves in Geometry and Logic, which is a fantastic introduction to topos theory. Also, you may be interested in the effective topos.

Source Link
xuq01
xuq01
  • 136
  • 5

Let me answer this question tangentially: while in our world the LEM may seem an unobjectionable and harmless principle, there are "worlds" where the LEM is false.

In the normal mathematical world, we just assume that some things exist. For example, piecewise functions exist: I can define a function $f : \mathbb{R} \rightarrow \mathbb{R}$ by $f(x) = 0$ if $x \leq 0$, $f(x) = x$ if $x > 0$. We can decide the equality of two real numbers. Some functions are provably discontinuous. Noncomputable functions from $\mathbb{N}$ to $\mathbb{N}$ exist. Everything seems perfectly normal, right?

But this is not the only "mathematical world" that exist. There are other mathematical worlds out there. There is a world where all functions from $\mathbb{R}$ to $\mathbb{R}$ are not only continuous but smooth; however, this necessitates that piecewise functions could not exist. There is a world where all functions $\mathbb{N} \rightarrow \mathbb{N}$ are computable, and this necessitates that the Busy Beaver and other non-computable functions are undefinable. Of course, all of these nice properties necessitate that the LEM fails to hold.

More formally speaking, the mathematical worlds I've been talking about are the concept of (elemantary) toposes. Each topos has an internal language, where mathematics can be conducted; depending on your topos, however, the internal language may validate or fail to validate statements that may seem bonkers.

Now, by the Curry-Howard correspondence, each of the internal languages could be used as a programming language. This is the beginnings of type theory. In some of them, there exist oracles for things that are not explicitly computable, and the law of excluded middle is just one of them. Recall that the LEM has the type: $\forall P : \mathtt{Prop}, P \vee \neg P$; by Curry-Howard, it is a function that, when given a proposition $P$, returns either a proof that either $P$ is true or that $\neg P$ is true. Of course, it is impossible to write down the definition of this function via recursion, which can be done in any topos with enough structure (if it were possible, then all toposes admit the LEM, which is not the case!). But still we can allow this principle as a function that defines itself.

So, LEM and Curry-Howard are not really directly related. It's not right to think of Curry-Howard as a specific statement, but rather as a broad principle. In some toposes, the internal language actually does allow you to write functions to decide whether a Turing machine halts - they just aren't computable in the usual sense. Meanwhile there are a plethora of reasons why internal functions in toposes can fail to be computable, again in the usual sense, and the LEM is just one of them; it is nothing special.

If you want to learn more about this subject, I suggest reading Mac Lane & Moerdijk's Sheaves in Geometry and Logic, which is a fantastic introduction to topos theory. Also, you may be interested in the effective topos.