Re: What is a proof, exactly?

From: Jasper Stein (J.J.Stein.Stein_at_cs.cs.ru.ru.nl.nl)
Date: 12/02/04 

Date: Thu, 02 Dec 2004 16:56:38 +0000

Josh Purinton wrote:

> In article <992b156f.0411232355.74c1829c@posting.google.com>,
> George Greene <greeneg@cs.unc.edu> wrote:
>> [A proof] can't be required and empty at the same time. It can't at
>> the same time be both necessarily present AND absent.
>
> Good point. I was trying to say that x is a theorem just when
> ProofPredicate(prf,x) is true, and ProofPredicate may be such that it is
> true for those arguments even if prf is something that we might consider
> empty, such as is the empty list or the empty tree.
>
>> [...] FS(.,.) is never a proof of anything. That is NOT the sort of
>> thing that a proof can be.
>
> Right; that was sloppy of me. I should have written ``nil might be a
> valid proof of "5=5"'' (according to my (idiosyncratic?) definition of a
> formal system as a ``"finitistic" function FS(Prf,x) that distinguishes
> valid proofs of x from invalid proofs of x'').

This is somewhat strange - does this mean that one (formal) proof can prove
several things? At least I suppose that if <> proves 5=5 then it also
proves e.g. 27=27.

(It seems that I'm missing some of the posts to the newsgroup - I haven't
seen George Greene's original post)

Jasper 

-- 
The problem with having an open mind is that people toss in garbage

Relevant Pages

  • Re: What is a proof, exactly?
    ... Josh Purinton wrote: ... >> the same time be both necessarily present AND absent. ... > empty, such as is the empty list or the empty tree. ... seen George Greene's original post) ...
    (sci.logic)
  • Re: HD no longer recognizable by XP pro once used in XP Home
    ... actually, made the first reply to the original post, suggesting the ... If it were cloning an empty disk, ... offering poor advice to try a program like TestDisk before going ... through the trouble of imaging a drive. ...
    (alt.comp.hardware.pc-homebuilt)
  • Re: HD no longer recognizable by XP pro once used in XP Home
    ... actually, made the first reply to the original post, suggesting the use ... If it were cloning an empty disk, ... that case i would reccomend making an image ASAP- in fact, ... offering poor advice to try a program like TestDisk before going ...
    (alt.comp.hardware.pc-homebuilt)
  • Re: HD no longer recognizable by XP pro once used in XP Home
    ... It was you who poked your beak in. ... original post. ... If it were cloning an empty disk, ... I did not complain about their ...
    (alt.comp.hardware.pc-homebuilt)
  • Re: Einstein summation notation (was: question of style)
    ... should also print one when they are all empty. ... If you want an absent string to work differently than a present one, ... If all the constituents are absent, then page_parts is the empty list, ...
    (comp.lang.python)