It is not that these statements are "not generally valid", but that they are not included within the axiom system used by H. If we attempt to include them, there will be a new statement of the same kind which is not included.
Obviously such statements will be true if H's axiom system is true, and in that sense they are always valid.
It is not that these statements are "not generally valid"
The intended meaning of valid in my post is "valid step in a proof" in the given formal system. I reworded the offending section.
Obviously such statements will be true if H's axiom system is true, and in that sense they are always valid.
Yes, and one also has to be careful with the use of the word "true". There are models in which the axioms are true, but which contain counterexamples to Provable(#φ) → φ.
I'm very confused about something related to the Halting Problem. I discussed this on the IRC with some people, but I couldn't get across what I meant very well. So I wrote up something a bit longer and a bit more formal.
The gist of it is, the halting problem lets us prove that, for a specific counter example, there can not exist any proof that it halts or not. A proof that it does or does not halt, causes a paradox.
But if it's true that there doesn't exist a proof that it halts, then it will run forever searching for one. Therefore I've proved that the program will not halt. Therefore a proof that it doesn't halt does exist (this one), and it will eventually find it. Creating a paradox.
Just calling the problem undecidable doesn't actually solve anything. If you can prove it's undecidable, it creates the same paradox. If no Turing machine can know whether or not a program halts, and we are also Turing machines, then we can't know either.
Now here is the weird and confusing part. If the above is a valid proof, then H will eventually find it. It searches all proofs, remember?
Fortunately, H will never find your argument because it is not a correct proof. You rely on hidden assumptions of the following form (given informally and symbolically):
= 27d567bc2d48d9f40e9ccc20ea370b15)
If φ is provable, then φ holds.
Provable(#φ) → φ
where #φ denotes the Gödel number of the proposition φ.
Statements of these form are generally not provable. This phenomenon is known as Löb's theorem - featured in Main back in 2008.
You use these invalid assumptions to eliminate the first two options from Either H returns true, or false, or loops forever. For example, if H returns true, then you can infer that "FF halts on input FF" is provable, but that does not contradict FF does not halt on input FF.
From Falsehoods Programmers Believe About Names:
anything someone tells you is their name is — by definition — an appropriate identifier for them.
There should be a list of false things people coming from common law jurisdictions believe about how choice of identity works on the rest of the globe.
Korean academy in Guatemala
I notice that I am confused. What, exactly, is a Korean academy doing halfway around the world? Were you teaching people-who-speak-Korean English in a Spanish-speaking country?
Should this be surprising? I briefly worked at a French school in Hungary: the guy who taught Spanish was Mexican, the girl who taught English was American, and so on. A Korean living in Guatemala still needs to learn English.
Sorry, this was an useless post so now it's gone
"How useful is my contribution, given what others are already doing?What will happen if I don't do it?What are the chances of success, and how good would success be?" - Giving What We Can newsletter
looked up monotone voice on google, and found that it has a positive, redeeming side – attractiveness.
My friends tell me that my face is pretty scarred. Research shows that facial scars are attractive. By the word scar, researchers mean healed cut. My friends mean acne hole.
Not all monotone voices are created equal. I'd be really surprised if "autistic" monotone and a "high-status" monotone would refer to the same thing.
Thank you for this insightful and comprehensive reply!
I have a follow-up question: Would ultrafinitist arithmetic still be incomplete due to Gödel’s incompleteness theorem?
I believe that an ultrafinitist arithmetic would still be incomplete. By that I mean that classical mathematics could prove that a sufficiently powerful ultrafinitist arithmetic is necessarily incomplete. The exact definition of "sufficiently powerful", and more importantly, the exact definition of "ultrafinitistic" would require attention. I'm not aware of any such result or on-going investigation.
The possibility of an ultrafinitist proof of Gödel's theorem is a different question. For some definition of "ultrafinitistic", even the well-known proofs of Gödel's theorem qualify. Mayhap^1 someone will succed where Nelson failed, and prove that "powerful systems of arithmetic are inconsistent". However, compared to that, Gödel's 1st incompleteness theorem, which merely states that "powerful systems of arithmetic are either incomplete or inconsistent", would seem rather... benign.
^1 very unlikely, but not cosmically unlikely
Can't the set of effectively representable numbers be inductive if we decide that "the smallest number not effectively representable" does not effectively represent a number?
"The smallest positive integer not definable in under twelve words" isn't an effective representation of a number any more than "The number I'm thinking of" or "Potato potato potato potato potato" are.
Sure, that's exactly what we have to do, on pain of inconsistency. We have to disallow representation schemas powerful enough to internalise the Berry paradox, so that "the smallest number not definable in less than 11 words" is not a valid representation. Cf. the various set theories, where we disallow comprehension schemas strong enough to internalise Russell's paradox, so that "the set of all sets that don't contain themselves" is not a valid comprehension.
Nelson thought that, similarly to how we reject "the smallest number not effectively representable" as an invalid representation, we should also reject e.g. "3^^^3" as an invalid representation; not because of the Berry paradox, but because of a different one, one that he ultimately could not establish.
Nelson introduced a family of standardness predicates, each one relative to a hyper-operation notation (addition, multiplication, exponentiation, the ^^-up-arrow operation, the ^^^-up-arrow notation and so on). Since standardness is not a notion internal to arithmetic, induction is not allowed on these predicates (i. e. '0' is standard, and if 'x' is standard then so is 'x+1', but you cannot use induction to conclude that therefore everything is standard).
He was able to prove that the standardness of n and m implies the standardness of n+m, and that of n×m. However, the corresponding result for exponentiation is provably false and the obstruction is non-associativity. What's more, even if we can prove that 2^^d is standard, this does not mean that the same holds for 2^^(d+1).
At this point, Nelson attempted to prove that an explicit recursion of super-exponential length does not terminate, thereby establishing that arithmetic is inconsistent, and vindicating ultrafinitism as the only remaining option. His attempted proof was faulty, with no obvious fix. Nelson continued looking for a valid proof until his death last September.
Wearing a vibrating compass anklet for a week. It improved my navigational skills tremendously.
I bought a NorthPaw last year but got very little out of it. I wondered if perhaps my local environment is simply not navigationally challenging enough; what sort of place were you using your haptic compass?
Mainly in the city of Edinburgh, HW campus and the Lothians. It worked well inside college buildings with non-trivial layouts as well.
Important question: do you usually travel by car? I can't drive, so my main methods of transportation were public transport and walking.
Him: Airports would be an issue, but it's easy to prove the magnets are there and be on your way. I had a single N52 grade 3mmx1mm disk magnet in the 3rd finger of my left hand.
As far as MRI's i was going to have a medical bracelet made, directing the doctor to a note that says "magnetic implants in fingers, please remove if MRI is necessary" or if I was going in myself, I'd just tell them. Then I'd keep the magnets and have them re-implanted later.
And I saw the guy with the ring. The sensation is nothing compared to an implant into the somatosensory nerve cluster.
me: Can you say more about what it felt like to have it?
him: That would be like describing blue to a blind person.
me: You still haven't replaced it right? So what does it feel like to not have it now?
him: I've pretty much gone back to normal. It's been over a year. I still need to find a viable coating.
What else would you like to ask him about?
Thanks! If still possible, I'd like to ask the following:
Who performed the insertion procedure? How long does it take to heal?
An N52 is very strong. Did you experience any unexpected negative side-effects while handling everyday objects (weight training, smartphones, et c.)?
Apart from the ring, have you tried achieving the same thing externally (i.e. without an implant)? Do you think it would be possible to "come close"?
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
I'm not sure that my paradox even requires the proof system to prove it's own consistency.
But regardless, even if removing that does resolve the paradox, it's not a very satisfying resolution. Of course a crippled logic can't prove interesting things about Turing machines.
Your argument requires the proof system to prove it's own consistency. As we discussed before, your argument relies on the assumption that the implication
is available for all φ. If this were the case, your theory would prove itself consistent. Why? Because you could take the contrapositive
and substitute "0=1" for φ. This gives you
The premise "0≠1" holds. Therefore, the consequence "0=1 is not provable" also holds. At this point your theory is asserting its own consistency: everything is provable in an inconsistent theory.
You might enjoy reading about the Turing Machine proof of Gödel's first incompleteness theorem, which is closely related to your paradox.