Ben, OK, that is a pretty good answer. I don't think I have any questions left about your philosophy :).
Some comments, though. > hmmm... you're saying the halting is provable in some more powerful > axiom system but not in Peano arithmetic? Yea, it would be provable in whatever formal system I used to prove the undecidability in the first place. (Probably PA plus an axiom asserting "PA is consistent".) > The thing is, a Turing machine is not a real machine: it's a mathematical > abstraction. A mathematical abstraction only has meaning inside a certain > formal system. So, the "Turing machine inside the Peano arithmetic > system" would neither provably halt nor not-halt ... the "Turing machine > inside > some other formal system" might potentially provably halt... Basically, I see this this as a "no" to my original "Do you think there is a truth of the matter" question. After all, if we need more definitions to determine the truth of a statement, then surely the statement's truth without the additional context is undefined. Take-home message for me: "Yes, Ben really is a constructivist." > > But the question is what does this mean about any actual computer, > or any actual physical object -- which we can only communicate about clearly > insofar as it can be boiled down to a finite dataset. What it means to me is that "Any actual computer will not halt (with a correct output) for this program". An actual computer will keep crunching away until some event happens that breaks the metaphor between it and the abstract machine-- memory overload, power failure, et cetera. This does not seem to me to depend on the formal system that we choose. Argument: very basic axioms fill in all the positive facts, and will tell us that a Turing machine halts when such is the case. Any additional axioms are attempts to fill in the negative space, so that we can prove some Turing machines non-halting. It seems perfectly reasonable to think hypothetically about the formal system that has *all* the negative cases filled in properly, even though this is impossible to actually do. This system is the "truth of the matter". So, when we choose a formal system to reason about Turing machines with, we are justified in choosing the strongest one available to us (more specifically, the strongest one we suspect to be consistent). > > The use of the same term "machine" for an observable object and a > mathematical > abstraction seems to confuse the issue. Sure. Do you have a preferred term? I can't think of any... > > -- Ben > > ________________________________ > agi | Archives | Modify Your Subscription ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
