Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question

2 Answers 2

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 ;-)

share|improve this answer
    
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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.