|
|
Stephen Harris wrote:
> Alan Smaill wrote:
> > "Charlie-Boo" <shymathguy@xxxxxxxxx>
> >> Alan Smaill, Charlie-Boo:
> >>> 129.215.101.90:1001/publications/PICTworkingpapers/WP38.pdf
> Content of footnotes:
>
> 38. MacKenzie, Donald, Negotiating arithmetic, constructing proof:
> the sociology of mathematics and information technology. download.pdf
> Now consider
> the principum tertii exclusi [law of excluded middle]: It claims that
> every supposition is either true or false; in mathematics this means
> that for every supposed imbedding of a system into another, satisfying
> certain given conditions, we can either accomplish such an imbedding by
> a construction, or arrive by a construction at the arrestment of the
> process which would lead to the imbedding.
No, it means your universal set (or the range of every map) consists of
two elements.
> We have seen that certain
> programs cannot be derived from their specifications in a constructive
> logic,
So Curry and Howard (and all of their advocates) are liars? I see.
> 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.
You left out the addendum (you must have read from an earlier edition):
'Ongoing research shows that Computationally Based Logics, however,
hold promise to overcome this limitation and actually formally derive
every possible program, in the sense that for every recursive function
a program that computes that function is derived.'
(I first personally showed Richard Waldinger and Zohar Manna early
results from a Computationally Based Logic in the 1980's at their
Stanford offices. Richard had long hair, was somewhat shy, and
delighted in showing me pictures of his family that covered the wall in
front of his desk. Zohar was heavy set and very gentlemanly and
jovial. I told him that athletes get so much pubicity, but
intellectuals such as ourselves are recognized only by a small minority
of the population. He agreed and joked, "But I don't want to be on the
cover of scandal magazines!" All 3 of us got a good laugh at that.)
C-B
|
|