# mapping simple first oreder problems to type theory

Since Peano axioms expressed in type theory doesn't seem to be going anywhere, here is a simpler question:

How would I map simple first order systems to an equivalent type theoretic notation.

Specificly:

for all x, isman(x) then ismortal(x)

isman(Socrates)

prove:

ismortal(Socrates)

and what would a type theoretic proof look like?

-

I am not sure of what kind of proofs you are looking for (there is a very little context in your post). Below is some approach, but as I am not really working in type theory, take it with a pinch of salt, it might not be even representative of standard proofs in that area.

Let $\mathtt{IsMan}(x)$ and $\mathtt{IsMortal}(x)$ be structures that depend on type $x$. Then $$\forall x.\ \mathtt{IsMan}(x) \to \mathtt{IsMortal}(x) \tag{1}$$ is a valid type, that is the type of functions that convert structures of $\mathtt{IsMan}(x)$ to structures $\mathtt{IsMortal}(x)$ for any type $x$. If we know that $(1)$ is true, then we know that it is inhabited, that is, there exists $f$ of type $(1)$. Then, given an element $a$ of type $\mathtt{IsMan(Socrates)}$ we can construct element $f(a)$ of type $\mathtt{IsMortal(Socrates)}$ and we are done.

I hope this helps ;-)

-
This looks like a pretty standard first order representation. I may steal your formatting for my post. –  user833970 Mar 26 '13 at 3:47
@user833970 It does, but the proof is different (funcion application versus modus ponens). Also, my impression is that a lot of type theory is just plain logic, so it might not be much different for you. Still, I like proofs using Curry-Howard correspondence, because one can easily see where the implications come from, something like a "flow of truth" ;-) (here the "pipe" was the function $f$). –  dtldarek Mar 26 '13 at 8:07