1
$\begingroup$

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, 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 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$?

Improve this question
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – xavierm02
    Sep 15, 2017 at 15:38
  • 2
    $\begingroup$ This is not a research-level question. I will address it if you move it to cs.stackexchange.com. $\endgroup$
    – Andrej Bauer
    Sep 16, 2017 at 12:05

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.