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 the working mathematician.

A long time ago mathematicians thught 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. Logicians tell 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 concieve 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.

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.

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.

Perhaps, before I actually, answer the question asked, I can explain why it makes sense to think of "proofs" as "elements of propositions".

A long time ago mathematicians thught of functions as symbolic expression, and many high-school students and beginning undergraduates still think of them that way. But modern mathematics has gone far beyond such a naive view. For instance, 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 the structure of $L(V,W)$ 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. Logicians tell 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.

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 concieve of an entire space of proofs as a single mathematical entity, let us call it a type.

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.

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 the working mathematician.

A long time ago mathematicians thught 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. Logicians tell 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 concieve 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.

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.