# TezlaKoil

Karma: 147
• In a topolog­i­cal space, defining

1. X ∨ Y as X ∪ Y

2. X ∧ Y as X ∩ Y

3. X → Y as Int( X^c ∪ Y )

4. ¬X as Int( X^c )

does yield a Heyt­ing alge­bra. This means that the un­der­stand­ing (but not the ex­pla­na­tion) of /​u/​cousin_it checks out: re­mov­ing the bor­der on each nega­tion is the “right way”.

No­tice that un­der this in­ter­pre­ta­tion X is always a sub­set of ¬¬X.:

1. Int(X^c) is a sub­set of X^c; by defi­ni­tion of Int(-).

2. Int(X^c)^c is a su­per­set of X^c^c = X; since tak­ing com­ple­ments re­verses con­tain­ment.

3. Int( Int(X^c)^c ) is a su­per­set of Int(X) = X; since Int(-) pre­serves con­tain­ment.

But Int( Int(X^c)^c ) is just ¬¬X. So X is always a sub­set of ¬¬X.

How­ever, in many cases ¬¬X is not a sub­set of X. For ex­am­ple, take the Eu­clidean plane with the usual topol­ogy, and let X be the plane with one point re­moved. Then ¬X = Int( X^c ) = ∅ is empty, so ¬¬X is the whole plane. But the whole plane is ob­vi­ously not a sub­set of the plane with one point re­moved.

• You can get a clearer-if-still-im­perfect sense from con­trast­ing up­votes on par­allel,

I’m fairly cer­tain that P(dis­agrees with blargtroll | dis­agrees with your pro­posal) >> P(agrees with blargtroll | dis­agrees with your pro­posal), sim­ply be­cause blargtroll’s coun­ter­ar­gu­ment is weak and its fol­lowups re­veal some anger man­age­ment is­sues.

For ex­am­ple, I would down­vote both your pro­posal and blargtroll’s coun­ter­ar­gu­ment if I could—and by the Typ­i­cal Mind heuris­tic so would ev­ery­one else :)

That said, I think you’re right in that this would not have re­ceived suffi­ciently many down­votes to be­come in­visi­ble.

• Thanks for giv­ing a name to this phe­nomenon.

In­deed, it would not sur­prise me if some peo­ple ac­tu­ally want hedge drift to oc­cur. They don’t ac­tu­ally try to pre­vent their claims from be­ing mi­s­un­der­stood.

It’s much worse. In my ex­pe­rience as an aca­demic, most de­part­ments sim­ply pre-hedge-drift their press re­leases. Science jour­nal­ists don’t—and are of­ten not qual­ified to—read and com­ment on the ac­tual pa­pers, all they have to work with is the press re­lease.

• I mean na­tion­al­ized, as in the dis­tri­bu­tion of to­bacco prod­ucts (im­ports, whole­sale, re­tail) is han­dled by com­pa­nies that may or may not have been pri­vate at some point, but are now prop­erty of the state.

What do you mean by na­tion­al­iz­ing?

• The weight of ev­i­dence best demon­strates that con­trol mea­sures have thus far been quite uniformly pos­i­tive.

I see. The black mar­ket effects are well-doc­u­mented, but I am not fa­mil­iar with ev­i­dence which shows that con­trol mea­sures have any mea­surable effects on pub­lic health. Where could I find that data?

• Dagon’s points are very good. There’s an­other as­pect as well:

Tobacco im­port and dis­tri­bu­tion (and in some cases, pro­duc­tion) are already na­tion­al­ized in many coun­tries, es­pe­cially in the EU. Na­tional gov­ern­ments try to im­pose ar­tifi­cial scarcity (wind­ing down op­er­a­tions, tax in­creases, fixed pric­ing), and this makes the statis­tics look bet­ter—offi­cially mon­i­tored to­bacco sales de­crease.

Ar­tifi­cial scarcity can­not last: a black mar­ket of RYO to­bacco, and home-made cigarettes of du­bi­ous ori­gin is always ready to serve cus­tomer de­mands. In the end, the health effects of na­tion­al­iz­ing the to­bacco in­dus­try, and wind­ing down op­er­a­tions, can eas­ily be nega­tive.

• I bet if you phrase the ques­tion as “your brain is de­stroyed and recre­ated 5 min­utes later”, most peo­ple out­side LW an­swer no. I guess this might be an­other in­stance of brain func­tions in­ac­tive vs lack of abil­ity to have ex­pe­riences.

• In row 8 of the table, P(D) should be re­placed by P(~D).

• In a ster­il­ized and sealed jar, jam made with­out sugar can last for years. Once you ac­tu­ally open the jar, you have about 7 days to eat it, and you bet­ter keep it re­friger­ated. You don’t need the sugar for thick­en­ing—the pectin in the fruit thick­ens jam just fine.

How­ever, if you don’t add any sweet­ener, the re­sult will be very sour.

Source: been mak­ing my own jam for years, had plenty of time to ex­per­i­ment.

• I’m not sure that my para­dox even re­quires the proof sys­tem to prove it’s own con­sis­tency.

Your ar­gu­ment re­quires the proof sys­tem to prove it’s own con­sis­tency. As we dis­cussed be­fore, your ar­gu­ment re­lies on the as­sump­tion that the im­pli­ca­tion

``````If “φ is prov­able” then “φ”
Prov­able(#φ) → φ
``````

is available for all φ. If this were the case, your the­ory would prove it­self con­sis­tent. Why? Be­cause you could take the contrapositive

``````If “φ is false” then “φ is not prov­able”
¬φ → ¬Prov­able(#φ)
``````

and sub­sti­tute “0=1” for φ. This gives you

``````if “0≠1” then “0=1 is not prov­able”
¬0=1 → ¬Prov­able(#(0=1))
``````

The premise “0≠1” holds. There­fore, the con­se­quence “0=1 is not prov­able” also holds. At this point your the­ory is as­sert­ing its own con­sis­tency: ev­ery­thing is prov­able in an in­con­sis­tent the­ory.

You might en­joy read­ing about the Tur­ing Ma­chine proof of Gödel’s first in­com­plete­ness the­o­rem, which is closely re­lated to your para­dox.

• It is not that these state­ments are “not gen­er­ally valid”

The in­tended mean­ing of valid in my post is “valid step in a proof” in the given for­mal sys­tem. I re­worded the offend­ing sec­tion.

Ob­vi­ously such state­ments will be true if H’s ax­iom sys­tem is true, and in that sense they are always valid.

Yes, and one also has to be care­ful with the use of the word “true”. There are mod­els in which the ax­ioms are true, but which con­tain coun­terex­am­ples to `Prov­able(#φ) → φ`.

• Now here is the weird and con­fus­ing part. If the above is a valid proof, then H will even­tu­ally find it. It searches all proofs, re­mem­ber?

For­tu­nately, H will never find your ar­gu­ment be­cause it is not a cor­rect proof. You rely on hid­den as­sump­tions of the fol­low­ing form (given in­for­mally and sym­bol­i­cally):

`````` If φ is prov­able, then φ holds.
Prov­able(#φ) → φ
``````

where #φ de­notes the Gödel num­ber of the propo­si­tion φ.

State­ments of these form are gen­er­ally not prov­able. This phe­nomenon is known as Löb’s the­o­remfea­tured in Main back in 2008.

You use these in­valid as­sump­tions to elimi­nate the first two op­tions from Either H re­turns true, or false, or loops for­ever. For ex­am­ple, if H re­turns true, then you can in­fer that “FF halts on in­put FF” is prov­able, but that does not con­tra­dict FF does not halt on in­put FF.

• From False­hoods Pro­gram­mers Believe About Names:

any­thing some­one tells you is their name is — by defi­ni­tion — an ap­pro­pri­ate iden­ti­fier for them.

There should be a list of false things peo­ple com­ing from com­mon law ju­ris­dic­tions be­lieve about how choice of iden­tity works on the rest of the globe.

• Should this be sur­pris­ing? I briefly worked at a French school in Hun­gary: the guy who taught Span­ish was Mex­i­can, the girl who taught English was Amer­i­can, and so on. A Korean liv­ing in Gu­atemala still needs to learn English.

• looked up mono­tone voice on google, and found that it has a pos­i­tive, re­deem­ing side – at­trac­tive­ness.

My friends tell me that my face is pretty scarred. Re­search shows that fa­cial scars are at­trac­tive. By the word scar, re­searchers mean healed cut. My friends mean acne hole.

Not all mono­tone voices are cre­ated equal. I’d be re­ally sur­prised if “autis­tic” mono­tone and a “high-sta­tus” mono­tone would re­fer to the same thing.

• I be­lieve that an ul­tra­fini­tist ar­ith­metic would still be in­com­plete. By that I mean that clas­si­cal math­e­mat­ics could prove that a suffi­ciently pow­er­ful ul­tra­fini­tist ar­ith­metic is nec­es­sar­ily in­com­plete. The ex­act defi­ni­tion of “suffi­ciently pow­er­ful”, and more im­por­tantly, the ex­act defi­ni­tion of “ul­tra­fini­tis­tic” would re­quire at­ten­tion. I’m not aware of any such re­sult or on-go­ing in­ves­ti­ga­tion.

The pos­si­bil­ity of an ul­tra­fini­tist proof of Gödel’s the­o­rem is a differ­ent ques­tion. For some defi­ni­tion of “ul­tra­fini­tis­tic”, even the well-known proofs of Gödel’s the­o­rem qual­ify. May­hap^1 some­one will succed where Nel­son failed, and prove that “pow­er­ful sys­tems of ar­ith­metic are in­con­sis­tent”. How­ever, com­pared to that, Gödel’s 1st in­com­plete­ness the­o­rem, which merely states that “pow­er­ful sys­tems of ar­ith­metic are ei­ther in­com­plete or in­con­sis­tent”, would seem rather… be­nign.

^1 very un­likely, but not cos­mi­cally unlikely

• Sure, that’s ex­actly what we have to do, on pain of in­con­sis­tency. We have to dis­al­low rep­re­sen­ta­tion schemas pow­er­ful enough to in­ter­nal­ise the Berry para­dox, so that “the small­est num­ber not defin­able in less than 11 words” is not a valid rep­re­sen­ta­tion. Cf. the var­i­ous set the­o­ries, where we dis­al­low com­pre­hen­sion schemas strong enough to in­ter­nal­ise Rus­sell’s para­dox, so that “the set of all sets that don’t con­tain them­selves” is not a valid com­pre­hen­sion.

Nel­son thought that, similarly to how we re­ject “the small­est num­ber not effec­tively rep­re­sentable” as an in­valid rep­re­sen­ta­tion, we should also re­ject e.g. “3^^^3″ as an in­valid rep­re­sen­ta­tion; not be­cause of the Berry para­dox, but be­cause of a differ­ent one, one that he ul­ti­mately could not es­tab­lish.

Nel­son in­tro­duced a fam­ily of stan­dard­ness pred­i­cates, each one rel­a­tive to a hy­per-op­er­a­tion no­ta­tion (ad­di­tion, mul­ti­pli­ca­tion, ex­po­nen­ti­a­tion, the ^^-up-ar­row op­er­a­tion, the ^^^-up-ar­row no­ta­tion and so on). Since stan­dard­ness is not a no­tion in­ter­nal to ar­ith­metic, in­duc­tion is not al­lowed on these pred­i­cates (i. e. ‘0’ is stan­dard, and if ‘x’ is stan­dard then so is ‘x+1’, but you can­not use in­duc­tion to con­clude that there­fore ev­ery­thing is stan­dard).

He was able to prove that the stan­dard­ness of n and m im­plies the stan­dard­ness of n+m, and that of n×m. How­ever, the cor­re­spond­ing re­sult for ex­po­nen­ti­a­tion is prov­ably false and the ob­struc­tion is non-as­so­ci­a­tivity. What’s more, even if we can prove that 2^^d is stan­dard, this does not mean that the same holds for 2^^(d+1).

At this point, Nel­son at­tempted to prove that an ex­plicit re­cur­sion of su­per-ex­po­nen­tial length does not ter­mi­nate, thereby es­tab­lish­ing that ar­ith­metic is in­con­sis­tent, and vin­di­cat­ing ul­tra­fini­tism as the only re­main­ing op­tion. His at­tempted proof was faulty, with no ob­vi­ous fix. Nel­son con­tinued look­ing for a valid proof un­til his death last Septem­ber.