|
|
[complicated mess of quotation-within-quotation, but this seems to be
Manna and Waldinger]
> Unless we have a philosophical commitment to intuitionism, maintaining
> constructiveness when it is not required can only make a proof system
> more cumbersome to use. We have seen that certain programs cannot be
> derived from their specifications in a constructive logic, but can be
> derived in a classical logic upon which minimal restrictions have been
> imposed ... ': Zohar Manna and Richard Waldinger, 'Constructive Logic
> considered Obstructive' (typescript, n.d.), 8.
There is a trick that comes out of the theorem-proving-on-top-of-Scheme
community that draws a completely different moral. You can extend the
Curry-Howard isomorphism to interpret classical logic; Peirce's law
ends up being the type of call-with-current-continuation. But this
isn't restricting classical logic, it's reinterpreting it.
============== j-c ====== @ ====== purr . demon . co . uk ==============
Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
<http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
|
|