2
$\begingroup$

In type theory there is a type $\mathrm{Prop}$ that contains every proposition, so $p\colon\mathrm{Prop}$ (in words, "$p$ is of type $\mathrm{Prop}$") where $p$ is a proposition. In all type theories I have seen, any proposition $p$ is treated as a type whose terms are its proofs. I find that unnatural because I don't think it is satisfying to identify a propositions (such as $\forall m\colon \mathbb{N}. \forall n\colon \mathbb{N}. m+n = n+m$) with the collection of its proofs.

So here is my question:

Are there (HOL) type theories that do not treat propositions as types? Do you can give some references?

Improve this question
$\endgroup$
4
  • $\begingroup$ Have you looked up Tarski universes (as opposed to Russell universes)? $\endgroup$
    – Zhen Lin
    Sep 17, 2015 at 14:04
  • $\begingroup$ I don't see the relation to my question ... $\endgroup$
    – newNameRandomDigga
    Sep 17, 2015 at 14:34
  • $\begingroup$ Prop, as you describe it, is a Russell universe, albeit a "small" one. $\endgroup$
    – Zhen Lin
    Sep 17, 2015 at 14:47
  • $\begingroup$ From treating $p$ as a type, it doesn't follow that $p$ is identified with the collection of its proofs. In general, a type is not identified with the collection of terms of that type; they're treated separately in the formal system. So the unnatural consequence doesn't necessarily follow from treating $p$ as a type. $\endgroup$
    – Andy Manion
    Sep 17, 2015 at 23:25

2 Answers 2

Reset to default
6
$\begingroup$

Before I actually answer the question asked, let me try to explain one way of thinking about proofs as elements of propositions. It is not the only way, but it should appeal to a mathematician with a taste for abstraction.

A long time ago mathematicians thought of functions as symbolic expressions, and many high-school students and beginning undergraduates still think of them that way. This sort of thinking had some unfortunate consequences. For example, it was sometimes assumed that every function can be differentiated because every expression one wrote down could obviously be differentiated symbolically.

Modern mathematics has gone far beyond such a naive view of functions. Today you take it for granted to say things like "let $V$ and $W$ be any Banach spaces and consider the space $L(V,W)$ of continuous linear functions from $V$ to $W$". A mathematician from the past would have a hard time understanding what this means because he would be used to thinking only about a single function at a time (but $L(V,W)$ is an entire space of functions), and the only concrete expression denoting a map $V \to W$ that he could actually write down would be $x \mapsto 0$.

Now let us consider the situation with proofs. Traditional logic tells us that proofs are syntactic entities: sequences (or trees) of statements each of which is an axiom or a consequence of the previous ones. Mathematicians do not study proofs at all, at least not in the same way that they study numbers, curves, and other mathematical objects. They mostly think about one proof at a time. Our understanding of proofs is where our understanding of functions was a couple of centuries ago.

When type theory says that "the elements of a proposition are its proofs" you should read that as "let us consider spaces of abstract proofs", just like we consider spaces of abstract functions. A function need not be an expression, and a proof need not be a sequence (or a tree) of statements. Once this is accepted we are able to conceive of an entire space of proofs as a single mathematical entity (a type), and then we can think of constructions of such entities, and so on.

Alfred Tarski's cylindrical algebras are another example of how proofs in first-order logic can be made abstract.

I can express my point with an equation: $$\frac{\text{mathematical logic}}{\text{type theory}} = \frac{\text{Newton's calculus}}{\text{functional analysis}}.$$ This equation is wrong in many respects, but I hope it communicates the point I am trying to make.

Finally, to answer your question: Church's theory of types is classical and has the type bool of truth values which are not proofs. It is used by the HOL family of proof assistants.

Improve this answer
$\endgroup$
1
$\begingroup$

In Altenkirch, McBride and Swiestra's "Observational Equality, Now!", the propositional fragment is carefully carved out and for any given p : Prop, you have a type of proofs Prf p (denoted with fancy brackets in the paper).

This gives you the opportunity to ask more from Prop (e.g. that all the proofs of a given proposition should be considered equal).

Improve this answer
$\endgroup$
2
  • $\begingroup$ @Myshkin: re your edit, the use of code formatting instead of $\LaTeX$ in this answer may have been a deliberate preference. Since type theories are often used as programming languages (e.g. Coq, Agda), some people like to borrow the syntax of such languages when discussing type theory. The $\LaTeX$ is fine too, but in future, I would suggest not “correcting” code formatting in type theory like one does in other contexts. $\endgroup$
    – Peter LeFanu Lumsdaine
    Oct 18, 2015 at 12:08
  • $\begingroup$ @PeterLeFanuLumsdaine Thanks, I hadn't considered it that way. I've reverted the edit. $\endgroup$
    – Myshkin
    Oct 18, 2015 at 12:14

Your Answer

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

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