<p>I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a decidable type theoretic language.</p>

<p>To my understanding, a constructivist foundation would require that an inequality could be proven only by exhibiting, say, a $n:\mathbb{N}$ such that $a + n = b$ to prove that $a \leq b$ for $a, b \in \mathbb{Z}$. </p>

<p>This is indeed the example of a "dependent pair type" on <a href="https://en.wikipedia.org/wiki/Dependent_type#Systems_of_the_lambda_cube" rel="nofollow noreferrer">Wiki</a>, which represents the first-order theorem:</p>

<p>$a \leq b \iff \Sigma\mathbb{N}(\lambda n \to a + n = b)$</p>

<p>But what exactly is going on here? How are we allowed to put a function from $n$ to a proposition, $a + n = b)$ into our type formula? If you see <a href="https://cstheory.stackexchange.com/questions/18962/formalizing-the-theory-of-finite-sets-in-type-theory">this</a> post also, the first answer has an "if then else" conditional in their type formula!</p>

<p>Moreover, if wanted to wanted to prove an equality $a = b$ where $a$ and $b$ are mathematical terms like polynomials, there would not be any model $n$ to choice from as above - so how would we do it? Usually, in a regular undergraduate mathematics course, we might try a proof by contradiction. Maybe try showing that we any inhabitants of $a$ and $b$ will be such that $ a - b = 0$?</p>

CC BY-SA 3.0
2017-09-15T15:38:40.133Z
The $\Sigma$ type is often interpreted as follows: an element of $\Sigma_{x:A}B$ is a pair $(t,u)$ where $t$ is of type $A$ and $u$ is of type $B[t/x]$. But sometimes, you want to make the fact that $B$ depends on $x$ explicit. And you write $\Sigma_{A}(\lambda x.B(x))$ instead of $\Sigma_{x:A}B$, and $B(t)$ instead of $B[t/x]$. So your example could also be written $a\le b\iff \Sigma_{x:\mathbb N}a+n=b$. | The if then else in the type is because we have dependent types: since the type can depend on terms (including some input), you can't know exactly what it is before knowing said terms.
xavierm02
CC BY-SA 3.0
2017-09-16T12:05:11.547Z
This is not a research-level question. I will address it if you move it to cs.stackexchange.com.
Andrej Bauer
<type-theory><set-theory><constructive-mathematics><curry-howard>
Equality Theorems with Type Theoretic Proof
Krpcannon
# Equality Theorems with Type Theoretic Proof

(Asked by: username_0 on 2017-09-15)

I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a decidable type theoretic language.

To my understanding, a constructivist foundation would require that an inequality could be proven only by exhibiting, say, a $n:\mathbb{N}$ such that $a + n = b$ to prove that $a \leq b$ for $a, b \in \mathbb{Z}$.

This is indeed the example of a "dependent pair type" on [Wiki](https://en.wikipedia.org/wiki/Dependent_type#Systems_of_the_lambda_cube), which represents the first-order theorem:

$a \leq b \iff \Sigma\mathbb{N}(\lambda n \to a + n = b)$

But what exactly is going on here? How are we allowed to put a function from $n$ to a proposition, $a + n = b)$ into our type formula? If you see [this](https://cstheory.stackexchange.com/questions/18962/formalizing-the-theory-of-finite-sets-in-type-theory) post also, the first answer has an "if then else" conditional in their type formula!

Moreover, if wanted to wanted to prove an equality $a = b$ where $a$ and $b$ are mathematical terms like polynomials, there would not be any model $n$ to choice from as above - so how would we do it? Usually, in a regular undergraduate mathematics course, we might try a proof by contradiction. Maybe try showing that we any inhabitants of $a$ and $b$ will be such that $ a - b = 0$?

**Tags:** type-theory, set-theory, constructive-mathematics, curry-howard
> **Comments:**
> **username_1**: The $\Sigma$ type is often interpreted as follows: an element of $\Sigma_{x:A}B$ is a pair $(t,u)$ where $t$ is of type $A$ and $u$ is of type $B[t/x]$. But sometimes, you want to make the fact that $B$ depends on $x$ explicit. And you write $\Sigma_{A}(\lambda x.B(x))$ instead of $\Sigma_{x:A}B$, and $B(t)$ instead of $B[t/x]$. So your example could also be written $a\le b\iff \Sigma_{x:\mathbb N}a+n=b$. | The if then else in the type is because we have dependent types: since the type can depend on terms (including some input), you can't know exactly what it is before knowing said terms.  
> **username_2**: This is not a research-level question. I will address it if you move it to cs.stackexchange.com.  

---

## 0 answers

