Re: Han's startling new set theory.

cbrown@xxxxxxxxxxxxxxxxx wrote:
> But then the verification process is not a verification of some
> statement of PA; it is a verification that the physical device indeed
> does obey the axioms we originally posited.

I think it's a verification of both. Of course, the match between the
axioms and the actual behaviour is where I'd look first if something
went wrong.

I'd be seriously weirded out if I couldn't find a discrepancy in that
step, and nor could a bunch of highly respected people. Weirded out
in a sense like winning the lottery twice in a row.


> So the prediction "for any p, q, |2*p^2 - q^2| > 0", when verified on a
> physical device such as a compuetr, is a prediction that the computer
> obeys PA - not that the above statement is "true" (for whatever values
> of "true" apply currently :)).

It will usually be, but I don't think it *must* be. I'm not 100%
convinced that PA is sound (even if it's consistent). Just 99.9+% :)

Finding out that a theorem of PA happens to be false would fall into
that <0.1% category. (Plus a hefty dose of unlikelihood for it being
discovered in *my* life)


- Tim
.

Relevant Pages

  • Re: Hans startling new set theory.
    ... >>> It makes the testable prediction that for all positive integers p,q, ... The assumption is that the physical device operates ... But then the verification process is not a verification of some ... does obey the axioms we originally posited. ...
    (sci.math)
  • Re: Kresss Probability Trilogy Qs
    ... A rigorous proof is completely formal. ... Goedel says that this system will not generate all truths, ... Of course there's still the question of where the axioms come from. ... have no real verification behind them, and then James on the other side ...
    (rec.arts.sf.science)
  • Re: Deep Thoughts # 7: A New Kind of Mathematics
    ... Consider Boyer and Moore's paper, ... the idea of writing software to prove HP and generate axioms. ... They never do present a verification of what they call a formal ... Journal of the ACM foolish to publish what amounts to something less ...
    (sci.logic)
  • Re: Deep Thoughts # 7: A New Kind of Mathematics
    ... Consider Boyer and Moore's paper, ... the idea of writing software to prove HP and generate axioms. ... They never do present a verification of what they call a formal ... Journal of the ACM foolish to publish what amounts to something less ...
    (sci.math)
  • Compiling MSIL to Native Code - bypassing verification
    ... During the verification process, MSIL code is examined in an attempt to ... verification inspects code to determine whether the MSIL has ... type-safe code, and it passes only code that is type safe. ... generate incorrect MSIL that would lead to a violation of the type ...
    (microsoft.public.dotnet.languages.vb)
Quantcast