Has somebody worked out a typed higher order logic? I mean something like type theory but not with this intuitionistic touch. Is there a natural deduction system for this logic?
$\begingroup$
$\endgroup$
1
asked Sep 16, 2015 at 15:53
-
6$\begingroup$ "Type theory in classical logic" sounds like a description of Russell and Whitehead's "Principia Mathematica" and lots of simplifications and variations. Also, to get classical type theory from your favorite intuitionistic type theory, you could just add the law of the excluded middle as an axiom. If neither of those observations answers your first question, then you should probably clarify the question. $\endgroup$– Andreas BlassCommented Sep 16, 2015 at 17:01
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
Russell & Whiteheads theory is perhaps a bit on the heavy side, but here are some references to support Andreas Blass' comment:
An early formulations of classical higher-order logic was given by Alonzo Church in A formulation of the Simple Theory of Types, see also the Princeton Encyclopedia of Philosophy entry on Church's Type Theory.
Proof assistants from the HOL family typically use classical type theories similar to those of Church, see for instance HOL light, see this HOL Light overview for a quick description of the underlying type theory.
In general most kinds of intuitionistic type theory are agnostic about excluded middle and you can simply turn them into classical theories by postulating excluded middle.
answered Sep 16, 2015 at 21:58
$\begingroup$
$\endgroup$
From the viewpoint of semantics, higher order intuitionistic logic is what you get from the internal logic of an (elementary) topos.
For classical higher-order logic, take a boolean topos.