On 2/13/2014 8:40 PM, Russell Standish wrote:
I had a look at your SANE paper, which is the main paper where you describe
your work that you published since your thesis. I can sort of see you
saying something a bit like the above on page 11 "Now DU [sic - should
be UD in English] is emulated platonistically by the verifiable
propositions of arithmetic. They are equivalent to sentences of the
form ``if exists n such that P(n)'' with P(n) decidable."
That is actually rather confusing. Obviously a UD executes all proofs
of all true Sigma 1 sentences, but I think what you are trying to say that
all programs executed by the UD correspond to a proof of some true
Sigma 1 sentence. Is that obvious? I didn't get that when I read the SANE paper
originally, only got it in context of your statements above.
How can that be? Many programs executed by the UD are non-halting, just loops. Can they
be considered to correspond to a proof?
Brent
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
