# 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

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.

-