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?
 A: 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 ;-)
A: Type theory, meaning systems in textbooks and theorem provers such as the HOL family based on Church's type theory, are supersets of first order logic.  Modus ponens is usually a derived rule of inference, but is perfectly valid, as are other first order theorems and rules of inference.
Type theory though takes a different approach than set theory though, especially compared with ZFC. ZFC has only sets, and all variables range over sets, where in type theory variables, constants, and terms generally have types. Expressions are not syntactically valid unless function and argument types match up properly.
So a proof in type theory need not look any different than a proof in first order logic, though technically there should be type annotations at least on enough variables to determine the types of the terms in it.
