# Proofs, Implications, and Models

Fol­lowup to: Causal Reference

From a math pro­fes­sor’s blog:

One thing I dis­cussed with my stu­dents here at HCSSiM yes­ter­day is the ques­tion of what is a proof.

They’re smart kids, but com­pletely new to proofs, and they of­ten have ques­tions about whether what they’ve writ­ten down con­sti­tutes a proof. Here’s what I said to them.

A proof is a so­cial con­struct – it is what we need it to be in or­der to be con­vinced some­thing is true. If you write some­thing down and you want it to count as a proof, the only real is­sue is whether you’re com­pletely con­vinc­ing.

This is not quite the defi­ni­tion I would give of what con­sti­tutes “proof” in math­e­mat­ics—per­haps be­cause I am so used to iso­lat­ing ar­gu­ments that are con­vinc­ing, but ought not to be.

Or here again, from “An In­tro­duc­tion to Proof The­ory” by Sa­muel R. Buss:

There are two dis­tinct view­points of what a math­e­mat­i­cal proof is. The first view is that proofs are so­cial con­ven­tions by which math­e­mat­i­ci­ans con­vince one an­other of the truth of the­o­rems. That is to say, a proof is ex­pressed in nat­u­ral lan­guage plus pos­si­bly sym­bols and figures, and is suffi­cient to con­vince an ex­pert of the cor­rect­ness of a the­o­rem. Ex­am­ples of so­cial proofs in­clude the kinds of proofs that are pre­sented in con­ver­sa­tions or pub­lished in ar­ti­cles. Of course, it is im­pos­si­ble to pre­cisely define what con­sti­tutes a valid proof in this so­cial sense; and, the stan­dards for valid proofs may vary with the au­di­ence and over time. The sec­ond view of proofs is more nar­row in scope: in this view, a proof con­sists of a string of sym­bols which satisfy some pre­cisely stated set of rules and which prove a the­o­rem, which it­self must also be ex­pressed as a string of sym­bols. Ac­cord­ing to this view, math­e­mat­ics can be re­garded as a ‘game’ played with strings of sym­bols ac­cord­ing to some pre­cisely defined rules. Proofs of the lat­ter kind are called “for­mal” proofs to dis­t­in­guish them from “so­cial” proofs.

In mod­ern math­e­mat­ics there is a much bet­ter an­swer that could be given to a stu­dent who asks, “What ex­actly is a proof?”, which does not match ei­ther of the above ideas. So:

Med­i­ta­tion: What dis­t­in­guishes a cor­rect math­e­mat­i­cal proof from an in­cor­rect math­e­mat­i­cal proof—what does it mean for a math­e­mat­i­cal proof to be good? And why, in the real world, would any­one ever be in­ter­ested in a math­e­mat­i­cal proof of this type, or obey­ing what­ever good­ness-rule you just set down? How could you use your no­tion of ‘proof’ to im­prove the real-world effi­cacy of an Ar­tifi­cial In­tel­li­gence?

...
...
...

Con­sider the fol­low­ing syl­l­o­gism:

1. All kit­tens are lit­tle;

2. Every­thing lit­tle is in­no­cent;

3. There­fore all kit­tens are in­no­cent.

Here’s four math­e­mat­i­cal uni­verses, aka “mod­els”, in which the ob­jects col­lec­tively obey or di­s­obey these three rules:

There are some mod­els where not all kit­tens are lit­tle, like mod­els B and D. And there are mod­els where not ev­ery­thing lit­tle is in­no­cent, like mod­els C and D. But there are no mod­els where all kit­tens are lit­tle, and ev­ery­thing lit­tle is in­no­cent, and yet there ex­ists a guilty kit­ten. Try as you will, you won’t be able to imag­ine a model like that. Any model con­tain­ing a guilty kit­ten has at least one kit­ten that isn’t lit­tle, or at least one lit­tle en­tity that isn’t in­no­cent—no way around it.

Thus, the jump from 1 & 2, to 3, is truth-pre­serv­ing: in any uni­verse where premises (1) and (2) are true to start with, the con­clu­sion (3) is true of the same uni­verse at the end.

Which is what makes the fol­low­ing im­pli­ca­tion valid, or, as peo­ple would usu­ally just say, “true”:

“If all kit­tens are lit­tle and ev­ery­thing lit­tle is in­no­cent, then all kit­tens are in­no­cent.”

The ad­vanced main­stream view of logic and math­e­mat­ics (i.e., the main­stream view among pro­fes­sional schol­ars of logic as such, not nec­es­sar­ily among all math­e­mat­i­ci­ans in gen­eral) is that when we talk about math, we are talk­ing about which con­clu­sions fol­low from which premises. The “truth” of a math­e­mat­i­cal the­o­rem—or to not over­load the word ‘true’ mean­ing com­par­i­son-to-causal-re­al­ity, the val­idity of a math­e­mat­i­cal the­o­rem—has noth­ing to do with the phys­i­cal truth or falsity of the con­clu­sion in our world, and ev­ery­thing to do with the in­evita­bil­ity of the im­pli­ca­tion. From the stand­point of val­idity, it doesn’t mat­ter a fig whether or not all kit­tens are in­no­cent in our own uni­verse, the con­nected causal fabric within which we are em­bed­ded. What mat­ters is whether or not you can prove the im­pli­ca­tion, start­ing from the premises; whether or not, if all kit­tens were lit­tle and all lit­tle things were in­no­cent, it would fol­low in­evitably that all kit­tens were in­no­cent.

To para­phrase Mayor Daley, logic is not there to cre­ate truth, logic is there to pre­serve truth. Let’s illus­trate this point by as­sum­ing the fol­low­ing equa­tion:

x = y = 1

...which is true in at least some cases. E.g. ‘x’ could be the num­ber of thumbs on my right hand, and ‘y’ the num­ber of thumbs on my left hand.

Now, start­ing from the above, we do a lit­tle alge­bra:

 1 x = y = 1 start­ing premise 2 x2 = xy mul­ti­ply both sides by x 3 x2 - y2 = xy—y2 sub­tract y2 from both sides 4 (x + y)(x—y) = y(x—y) fac­tor 5 x + y = y can­cel 6 2 = 1 sub­sti­tute 1 for x and 1 for y

We have reached the con­clu­sion that in ev­ery case where x and y are equal to 1, 2 is equal to 1. This does not seem like it should fol­low in­evitably.

You could try to find the flaw just by star­ing at the lines… maybe you’d sus­pect that the er­ror was be­tween line 3 and line 4, fol­low­ing the heuris­tic of first mis­trust­ing what looks like the most com­pli­cated step… but an­other way of do­ing it would be to try eval­u­at­ing each line to see what it said con­cretely, for ex­am­ple, mul­ti­ply­ing out x2 = xy in line 2 to get (12) = (1 * 1) or 1 = 1. Let’s try do­ing this for each step, and then af­ter­ward mark whether each equa­tion looks true or false:

 1 x = y = 1 1 = 1 true 2 x2 = xy 1 = 1 true 3 x2 - y2 = xy—y2 0 = 0 true 4 (x + y)(x—y) = y(x—y) 0 = 0 true 5 x + y = y 2 = 1 false 6 2 = 1 2 = 1 false

Logic is there to pre­serve truth, not to cre­ate truth. When­ever we take a log­i­cally valid step, we can’t guaran­tee that the premise is true to start with, but if the premise is true the con­clu­sion should always be true. Since we went from a true equa­tion to a false equa­tion be­tween step 4 and step 5, we must’ve done some­thing that is in gen­eral in­valid.

In par­tic­u­lar, we di­vided both sides of the equa­tion by (x—y).

Which is in­valid, i.e. not uni­ver­sally truth-pre­serv­ing, be­cause (x—y) might be equal to 0.

And if you di­vide both sides by 0, you can get a false state­ment from a true state­ment. 3 * 0 = 2 * 0 is a true equa­tion, but 3 = 2 is a false equa­tion, so it is not al­low­able in gen­eral to can­cel any fac­tor if the fac­tor might equal zero.

On the other hand, adding 1 to both sides of an equa­tion is always truth-pre­serv­ing. We can’t guaran­tee as a mat­ter of logic that x = y to start with—for ex­am­ple, x might be my num­ber of ears and y might be my num­ber of fingers. But if x = y then x + 1 = y + 1, always. Logic is not there to cre­ate truth; logic is there to pre­serve truth. If a scale starts out bal­anced, then adding the same weight to both sides will re­sult in a scale that is still bal­anced:

I will re­mark, in some hor­ror and ex­as­per­a­tion with the mod­ern ed­u­ca­tional sys­tem, that I do not re­call any math-book of my youth ever once ex­plain­ing that the rea­son why you are always al­lowed to add 1 to both sides of an equa­tion is that it is a kind of step which always pro­duces true equa­tions from true equa­tions.

What is a valid proof in alge­bra? It’s a proof where, in each step, we do some­thing that is uni­ver­sally al­lowed, some­thing which can only pro­duce true equa­tions from true equa­tions, and so the proof grad­u­ally trans­forms the start­ing equa­tion into a fi­nal equa­tion which must be true if the start­ing equa­tion was true. Each step should also—this is part of what makes proofs use­ful in rea­son­ing—be lo­cally ver­ifi­able as al­lowed, by look­ing at only a small num­ber of pre­vi­ous points, not the en­tire past his­tory of the proof. If in some pre­vi­ous step I be­lieved x2 - y = 2, I only need to look at that sin­gle step to get the con­clu­sion x2 = 2 + y, be­cause I am always al­lowed to add y to both sides of the equa­tion; be­cause I am always al­lowed to add any quan­tity to both sides of the equa­tion; be­cause if the two sides of an equa­tion are in bal­ance to start with, adding the same quan­tity to both sides of the bal­ance will pre­serve that bal­ance. I can know the in­evita­bil­ity of this im­pli­ca­tion with­out con­sid­er­ing all the sur­round­ing cir­cum­stances; it’s a step which is lo­cally guaran­teed to be valid. (Note the similar­ity—and the differ­ences—to how we can com­pute a causal en­tity know­ing only its im­me­di­ate par­ents, and no other an­ces­tors.)

You may have read—I’ve cer­tainly read—some philos­o­phy which en­deav­ors to score points for counter-in­tu­itive cyn­i­cism by say­ing that all math­e­mat­ics is a mere game of to­kens; that we start with a mean­ingless string of sym­bols like:

$\forall x : (K(x) \rightarrow L(x)) \land (L(x) \rightarrow I(x))$

...and we fol­low some sym­bol-ma­nipu­la­tion rules like “If you have the string ‘A ∧ (A → B)’ you are al­lowed to go to the string ‘B’”, and so fi­nally end up with the string:

$\forall x: K(x) \rightarrow I(x)$

...and this ac­tivity of string-ma­nipu­la­tion is all there is to what math­e­mat­i­ci­ans call “the­o­rem-prov­ing”—all there is to the glo­ri­ous hu­man en­deavor of math­e­mat­ics.

This, like a lot of other cyn­i­cism out there, is need­lessly defla­tion­ary.

There’s a fam­ily of tech­niques in ma­chine learn­ing known as “Monte Carlo meth­ods” or “Monte Carlo simu­la­tion”, one of which says, roughly, “To find the prob­a­bil­ity of a propo­si­tion Q given a set of premises P, simu­late ran­dom mod­els that obey P, and then count how of­ten Q is true.” Stanis­law Ulam in­vented the idea af­ter try­ing for a while to calcu­late the prob­a­bil­ity that a ran­dom Can­field soli­taire lay­out would be solv­able, and fi­nally re­al­iz­ing that he could get bet­ter in­for­ma­tion by try­ing it a hun­dred times and count­ing the num­ber of suc­cess­ful plays. This was dur­ing the era when com­put­ers were first be­com­ing available, and the thought oc­curred to Ulam that the same tech­nique might work on a cur­rent neu­tron diffu­sion prob­lem as well.

Similarly, to an­swer a ques­tion like, “What is the prob­a­bil­ity that a ran­dom Can­field soli­taire is solv­able, given that the top card in the deck is a king?” you might imag­ine simu­lat­ing many 52-card lay­outs, throw­ing away all the lay­outs where the top card in the deck was not a king, us­ing a com­puter al­gorithm to solve the re­main­ing lay­outs, and count­ing what per­centage of those were solv­able. (It would be more effi­cient, in this case, to start by di­rectly plac­ing a king on top and then ran­domly dis­tribut­ing the other 51 cards; but this is not always effi­cient in Monte Carlo simu­la­tions when the con­di­tion to be fulfilled is more com­plex.)

Okay, now for a harder prob­lem. Sup­pose you’ve wan­dered through the world a bit, and you’ve ob­served the fol­low­ing:

(1) So far I’ve seen 20 ob­jects which have been kit­tens, and on the 6 oc­ca­sions I’ve paid a penny to ob­serve the size of some­thing that’s a kit­ten, all 6 kit­ten-ob­jects have been lit­tle.

(2) So far I’ve seen 50 ob­jects which have been lit­tle, and on the 30 oc­ca­sions where I’ve paid a penny to ob­serve the moral­ity of some­thing lit­tle, all 30 lit­tle ob­jects have been in­no­cent.

(3) This ob­ject hap­pens to be a kit­ten. I want to know whether it’s in­no­cent, but I don’t want to pay a cent to find out di­rectly. (E.g., if it’s an in­no­cent kit­ten, I can buy it for a cent, sell it for two cents, and make a one-cent profit. But if I pay a penny to ob­serve di­rectly whether the kit­ten is in­no­cent, I won’t be able to make a profit, since gath­er­ing ev­i­dence is costly.)

Your pre­vi­ous ex­pe­riences have led you to sus­pect the gen­eral rule “All kit­tens are lit­tle” and also the rule “All lit­tle things are in­no­cent”, even though you’ve never be­fore di­rectly checked whether a kit­ten is in­no­cent.

Fur­ther­more...

You’ve never heard of logic, and you have no idea how to play that ‘game of sym­bols’ with K(x), I(x), and L(x) that we were talk­ing about ear­lier.

But that’s all right. The prob­lem is still solv­able by Monte Carlo meth­ods!

First we’ll gen­er­ate a large set of ran­dom uni­verses. Then, for each uni­verse, we’ll check whether that uni­verse obeys all the rules we cur­rently sus­pect or be­lieve to be true, like “All kit­tens are lit­tle” and “All lit­tle things are in­no­cent” and “The force of grav­ity goes as the square of the dis­tance be­tween two ob­jects and the product of their masses”. If a uni­verse passes this test, we’ll check to see whether the in­quiry of in­ter­est, “Is the kit­ten in front of me in­no­cent?”, also hap­pens to be true in that uni­verse.

We shall re­peat this test a large num­ber of times, and at the end we shall have an ap­prox­i­mate es­ti­mate of the prob­a­bil­ity that the kit­ten in front of you is in­no­cent.

On this al­gorithm, you perform in­fer­ence by vi­su­al­iz­ing many pos­si­ble uni­verses, throw­ing out uni­verses that dis­agree with gen­er­al­iza­tions you already be­lieve in, and then check­ing what’s true (prob­a­ble) in the uni­verses that re­main. This al­gorithm doesn’t tell you the state of the real phys­i­cal world with cer­tainty. Rather, it gives you a mea­sure of prob­a­bil­ity—i.e., the prob­a­bil­ity that the kit­ten is in­no­cent—given ev­ery­thing else you already be­lieve to be true.

And if, in­stead of vi­su­al­iz­ing many imag­in­able uni­verses, you checked all pos­si­ble log­i­cal mod­els—which would take some­thing be­yond magic, be­cause that would in­clude mod­els con­tain­ing un­countably large num­bers of ob­jects—and the in­quiry-of-in­ter­est was true in ev­ery model match­ing your pre­vi­ous be­liefs, you would have found that the con­clu­sion fol­lowed in­evitably if the gen­er­al­iza­tions you already be­lieved were true.

This might take a whole lot of rea­son­ing, but at least you wouldn’t have to pay a cent to ob­serve the kit­ten’s in­no­cence di­rectly.

But it would also save you some com­pu­ta­tion if you could play that game of sym­bols we talked about ear­lier—a game which does not cre­ate truth, but pre­serves truth. In this game, the steps can be lo­cally pro­nounced valid by a mere ‘syn­tac­tic’ check that doesn’t re­quire us to vi­su­al­ize all pos­si­ble mod­els. In­stead, if the mere syn­tax of the proof checks out, we know that the con­clu­sion is always true in a model when­ever the premises are true in that model.

And that’s a math­e­mat­i­cal proof: A con­clu­sion which is true in any model where the ax­ioms are true, which we know be­cause we went through a se­ries of trans­for­ma­tions-of-be­lief, each step be­ing li­censed by some rule which guaran­tees that such steps never gen­er­ate a false state­ment from a true state­ment.

The way we would say it in stan­dard math­e­mat­i­cal logic is as fol­lows:

A col­lec­tion of ax­ioms X se­man­ti­cally im­plies a the­o­rem Y, if Y is true in all mod­els where X are true. We write this as X Y.

A col­lec­tion of ax­ioms X syn­tac­ti­cally im­plies a the­o­rem Y within a sys­tem S, if we can get to Y from X us­ing trans­for­ma­tion steps al­lowed within S. We write this as X Y.

The point of the sys­tem S known as “clas­si­cal logic” is that its syn­tac­tic trans­for­ma­tions pre­serve se­man­tic im­pli­ca­tion, so that any syn­tac­ti­cally al­lowed proof is se­man­ti­cally valid:

If X Y, then X Y.

If you make this idea be about proof steps in alge­bra do­ing things that always pre­serve the bal­ance of a pre­vi­ously bal­anced scale, I see no rea­son why this idea couldn’t be pre­sented in eighth grade or ear­lier.

I can at­test by spot-check­ing for small N that even most math­e­mat­i­ci­ans have not been ex­posed to this idea. It’s the stan­dard con­cept in math­e­mat­i­cal logic, but for some odd rea­son, the knowl­edge seems con­strained to the study of “math­e­mat­i­cal logic” as a sep­a­rate field, which not all math­e­mat­i­ci­ans are in­ter­ested in (many just want to do Dio­phan­tine anal­y­sis or what­ever).

So far as real life is con­cerned, math­e­mat­i­cal logic only tells us the im­pli­ca­tions of what we already be­lieve or sus­pect, but this is a com­pu­ta­tional prob­lem of supreme difficulty and im­por­tance. After the first thou­sand times we ob­serve that ob­jects in Earth grav­ity ac­cel­er­ate down­ward at 9.8 m/​s2, we can sus­pect that this will be true on the next oc­ca­sion—which is a mat­ter of prob­a­bil­is­tic in­duc­tion, not valid logic. But then to go from that sus­pi­cion, plus the ob­ser­va­tion that a build­ing is 45 me­ters tall, to a spe­cific pre­dic­tion of how long it takes the ob­ject to hit the ground, is a mat­ter of logic—what will hap­pen if ev­ery­thing we else we already be­lieve, is ac­tu­ally true. It re­quires com­pu­ta­tion to make this con­clu­sion trans­par­ent. We are not ‘log­i­cally om­ni­scient’ - the tech­ni­cal term for the im­pos­si­ble dream­like abil­ity of know­ing all the im­pli­ca­tions of ev­ery­thing you be­lieve.

The great virtue of logic in ar­gu­ment is not that you can prove things by logic that are ab­solutely cer­tain. Since log­i­cal im­pli­ca­tions are valid in ev­ery pos­si­ble world, “ob­serv­ing” them never tells us any­thing about which pos­si­ble world we live in. Logic can’t tell you that you won’t sud­denly float up into the at­mo­sphere. (What if we’re in the Ma­trix, and the Ma­trix Lords de­cide to do that to you on a whim as soon as you finish read­ing this sen­tence?) Logic can only tell you that, if that does hap­pen, you were wrong in your ex­tremely strong sus­pi­cion about grav­i­ta­tion be­ing always and ev­ery­where true in our uni­verse.

The great virtue of valid logic in ar­gu­ment, rather, is that log­i­cal ar­gu­ment ex­poses premises, so that any­one who dis­agrees with your con­clu­sion has to (a) point out a premise they dis­agree with or (b) point out an in­valid step in rea­son­ing which is strongly li­able to gen­er­ate false state­ments from true state­ments.

For ex­am­ple: Nick Bostrom put forth the Si­mu­la­tion Ar­gu­ment, which is that you must dis­agree with ei­ther state­ment (1) or (2) or else agree with state­ment (3):

(1) Earth-origi­nat­ing in­tel­li­gent life will, in the fu­ture, ac­quire vastly greater com­put­ing re­sources.

(2) Some of these com­put­ing re­sources will be used to run many simu­la­tions of an­cient Earth, aka “an­ces­tor simu­la­tions”.

(3) We are al­most cer­tainly liv­ing in a com­puter simu­la­tion.

...but un­for­tu­nately it ap­pears that not only do most re­spon­dents de­cline to say why they dis­be­lieve in (3), most are un­able to un­der­stand the dis­tinc­tion be­tween the Si­mu­la­tion Hy­poth­e­sis that we are liv­ing in a com­puter simu­la­tion, ver­sus Nick Bostrom’s ac­tual sup­port for the Si­mu­la­tion Ar­gu­ment that “You must ei­ther dis­agree with (1) or (2) or agree with (3)”. They just treat Nick Bostrom as hav­ing claimed that we’re all liv­ing in the Ma­trix. Really. Look at the me­dia cov­er­age.

I would se­ri­ously gen­er­al­ize that the main­stream me­dia only un­der­stands the “and” con­nec­tive, not the “or” or “im­plies” con­nec­tive. I.e., it is im­pos­si­ble for the me­dia to re­port on a dis­cov­ery that one of two things must be true, or a dis­cov­ery that if X is true then Y must be true (when it’s not known that X is true). Also, the me­dia only un­der­stands the “not” pre­fix when ap­plied to atomic facts; it should go with­out say­ing that “not (A and B)” can­not be re­ported-on.

Robin Han­son some­times com­plains that when he tries to ar­gue that con­clu­sion X fol­lows from rea­son­able-sound­ing premises Y, his col­leagues dis­agree with X while re­fus­ing to say which premise Y they think is false, or else say which step of the rea­son­ing seems like an in­valid im­pli­ca­tion. Such be­hav­ior is not only an­noy­ing, but log­i­cally rude, be­cause some­one else went out of their way and put in ex­tra effort to make it as easy as pos­si­ble for you to ex­plain why you dis­agreed, and you couldn’t be both­ered to pick one item off a mul­ti­ple-choice menu.

The in­spira­tion of logic for ar­gu­ment is to lay out a mod­u­lar de­bate, one which con­ve­niently breaks into smaller pieces that can ex­am­ined with smaller con­ver­sa­tions. At least when it comes to try­ing to have a real con­ver­sa­tion with a re­spected part­ner—I wouldn’t nec­es­sar­ily ad­vise a teenager to try it on their oblivi­ous par­ents—that is the great in­spira­tion we can take from the study of math­e­mat­i­cal logic: An ar­gu­ment is a suc­ces­sion of state­ments each allegedly fol­low­ing with high prob­a­bil­ity from pre­vi­ous state­ments or shared back­ground knowl­edge. Rather than, say, snow­ing some­one un­der with as much fury and as many de­mands for ap­plause as you can fit into sixty sec­onds.

Michael Vas­sar is fond of claiming that most peo­ple don’t have the con­cept of an ar­gu­ment, and that it’s pointless to try and teach them any­thing else un­til you can con­vey an in­tu­itive sense for what it means to ar­gue. I think that’s what he’s talk­ing about.

Med­i­ta­tion: It has been claimed that logic and math­e­mat­ics is the study of which con­clu­sions fol­low from which premises. But when we say that 2 + 2 = 4, are we re­ally just as­sum­ing that? It seems like 2 + 2 = 4 was true well be­fore any­one was around to as­sume it, that two ap­ples equaled two ap­ples be­fore there was any­one to count them, and that we couldn’t make it 5 just by as­sum­ing differ­ently.

Main­stream sta­tus.

Part of the se­quence Highly Ad­vanced Episte­mol­ogy 101 for Beginners

Next post: “Log­i­cal Pin­point­ing

Pre­vi­ous post: “Causal Refer­ence

• A proof is a so­cial con­struct – it is what we need it to be in or­der to be con­vinced some­thing is true. If you write some­thing down and you want it to count as a proof, the only real is­sue is whether you’re com­pletely con­vinc­ing.

Some philoso­phers of math­e­mat­ics (of­ten those who call them­selves “nat­u­ral­ists”) ar­gue that what we ought to be pay­ing at­ten­tion to in math­e­mat­ics is what math­e­mat­i­ci­ans ac­tu­ally do. If you look at it like this, you no­tice that very few math­e­mat­i­ci­ans ac­tu­ally pro­duce fully valid proofs in first-or­der logic, even when they’re prov­ing a new the­o­rem (al­though there are salu­tory at­tempts to change this, such as prov­ing lots of ex­ist­ing the­o­rems us­ing Coq).

The best en­cap­su­la­tion that I’ve heard of what math­e­mat­i­ci­ans ac­tu­ally do when they offer proofs is some­thing like:

You don’t have to provide a fully rigor­ous proof, you just have to con­vince me that you could do if you had to.

It seems pretty clear to me that this still in­di­cates that math­e­mat­i­ci­ans are re­ally in­ter­ested in the ex­is­tence of the for­mal proof, but they use a bunch of heuris­tics to figure out whether it ex­ists and what it is. Rather than math­e­mat­i­cal prac­tice show­ing us that the no­tion of proof is re­ally this more so­cial no­tion, and that there­fore the for­mal ver­sion is some­how off base.

• Another way of look­ing at it, would be to imag­ine what would hap­pen if we started writ­ing proofs in for­mal logic. Quite quickly, peo­ple would no­tice pat­terns of in­fer­ences that ap­peared again and again, and save space and time by en­cod­ing the pat­tern in a sin­gle state­ment which any­one could use, not ac­tu­ally an ad­di­tional ax­iom since it fol­lows from the oth­ers, but work­ing like one. If you do this a lot quite soon you would be al­most en­tirely us­ing short-cuts like this, and be­gin to no­tice higher-level pat­terns in the short-cuts you are us­ing. Keep ex­tend­ing this short-cut-gen­er­at­ing pro­cess un­til math­e­mat­i­cal pa­pers are ac­tu­ally of a re­motely read­able length, and you get some­thing that looks quite a lot like mod­ern math­e­mat­ics.

I’m not claiming this is what ac­tu­ally hap­pened, what ac­tu­ally hap­pened is a few hun­dred years ago math­e­mat­ics re­ally was as wishy-washy as you say it is, and peo­ple grad­u­ally re­al­ised what they should ac­tu­ally be do­ing, then skipped the stage of writ­ing 10000-page proofs in for­mal logic be­cause math­e­mat­i­ci­ans aren’t stupid and could see where the chain ended from there.

• I can at­test by spot-check­ing for small N that even most math­e­mat­i­ci­ans have not been ex­posed to this idea. It’s the stan­dard con­cept in math­e­mat­i­cal logic, but for some odd rea­son, the knowl­edge seems con­strained to the study of “math­e­mat­i­cal logic” as a sep­a­rate field, which not all math­e­mat­i­ci­ans are in­ter­ested in (many just want to do Dio­phan­tine anal­y­sis or what­ever).

I’m sur­prised by this claim. Most math­e­mat­i­ci­ans have at least some un­der­stand­ing of math­e­mat­i­cal logic. What you may be en­coun­ter­ing are peo­ple who sim­ply haven’t had to think about these is­sues in a while. But your use of Dio­phan­tine anal­y­sis, a sub­branch of num­ber the­ory, as your other ex­am­ple is a bit strange be­cause num­ber the­ory and alge­bra have be­come quite adept in the last few years at us­ing model the­ory to show the ex­is­tence of proofs even when one can’t point to the proof in ques­tion. The clas­si­cal ex­am­ple is the Ax-Grothendieck the­o­rem, Terry Tao dis­cusses this and some re­lated is­sues here. Similarly , Mochizuki’s at­tempted proof of the ABC con­jec­ture (as I very roughly un­der­stand it) re­quires del­i­cate work with mod­els.

• I’m not go­ing to say they haven’t been ex­posed to it, but I think quite few math­e­mat­i­ci­ans have ever de­vel­oped a ba­sic ap­pre­ci­a­tion and work­ing un­der­stand­ing of the dis­tinc­tion be­tween syn­tac­tic and se­man­tic proofs.

Model the­ory is, very rarely, suc­cess­fully ap­plied to solve a well-known prob­lem out­side logic, but you would have to sam­ple many ran­dom math­e­mat­i­ci­ans be­fore you could find one that could tell you ex­actly how, even if you re­stricted to only ask­ing math­e­mat­i­cal lo­gi­ci­ans.

I’d like to add that in the over­whelming ma­jor­ity of aca­demic re­search in math­e­mat­i­cal logic, the syn­tax-se­man­tics dis­tinc­tion is not at all im­por­tant, and syn­tax is sup­pressed as much as pos­si­ble as an in­con­ve­nient thing to deal with. This is true even in model the­ory. Now, it is of­ten needed to dis­cuss for­mu­las and the­o­ries, but a syn­tac­ti­cal proof need not ever be con­sid­ered. First-or­der logic is dom­i­nant, and the com­plete­ness the­o­rem (to­gether with sound­ness) shows that syn­tac­tic im­pli­ca­tion is equiv­a­lent to se­man­tic im­pli­ca­tion.

If I had to sum­ma­rize what mod­ern re­search in math­e­mat­i­cal logic is like, I’d say that it’s about in­creas­ingly elab­o­rate no­tions of com­plex­ity (of prob­lems or the­o­rems or some­thing else), and prov­ing that cer­tain things have cer­tain de­grees of com­plex­ity, or that the de­grees of com­plex­ity them­selves are laid out in a cer­tain way.

There are how­ever a healthy num­ber of lo­gi­ci­ans in com­puter sci­ence academia who care a lot more about syn­tax, in­clud­ing proofs. Th­ese could be called math­e­mat­i­cal lo­gi­ci­ans, but the two cul­tures are quite differ­ent.

(I am a math PhD stu­dent spe­cial­iz­ing in logic.)

• How about you sur­vey math­e­mat­i­ci­ans?

• This is meant to pre­sent a com­pletely stan­dard view of se­man­tic im­pli­ca­tion, syn­tac­tic im­pli­ca­tion, and the link be­tween them, as un­der­stood in mod­ern math­e­mat­i­cal logic. All de­par­tures from the stan­dard aca­demic view are er­rors and should be flagged ac­cord­ingly.

Although this view is stan­dard among the pro­fes­sion­als whose job it is to care, it is sur­pris­ingly poorly known out­side that. Try­ing to make a func­tion call to these con­cepts in­side your math pro­fes­sor’s head is likely to fail un­less they have knowl­edge of “math­e­mat­i­cal logic” or “model the­ory”.

Beyond clas­si­cal logic lie the ex­cit­ing fron­tiers of weird log­ics such as in­tu­ition­is­tic logic, which doesn’t have the the­o­rem ¬¬P → P. Th­ese stranger syn­taxes can im­ply en­tirely differ­ent views of se­man­tics, such as a syn­tac­tic deriva­tion of Y from X mean­ing, “If you hand me an ex­am­ple of X, I can con­struct an ex­am­ple of Y.”

I can’t ac­tu­ally re­call where I’ve seen some­one else say that e.g. “An alge­braic proof is a se­ries of steps that you can tell are lo­cally li­censed be­cause they main­tain bal­anced weights”, but it seems like an ob­vi­ous di­rect spe­cial­iza­tion of “syn­tac­tic im­pli­ca­tion should pre­serve se­man­tic im­pli­ca­tion” (which is definitely stan­dard). Similarly, I haven’t seen the illus­tra­tion of “Where does this first go from a true equa­tion to a false equa­tion?” used as a way of teach­ing the un­der­ly­ing con­cept, but that’s be­cause I’ve never seen the differ­ence be­tween se­man­tic and syn­tac­tic im­pli­ca­tion taught at all out­side of one rare sub­field of math­e­mat­ics. (AAAAAAAAAAAAHHHH!)

The idea that logic can’t tell you any­thing with cer­tainty about the phys­i­cal uni­verse, or that logic is only as sure as its premises, is very widely un­der­stood among Tra­di­tional Ra­tion­al­ists:

… as far as the laws of math­e­mat­ics re­fer to re­al­ity, they are not cer­tain; and as far as they are cer­tain, they do not re­fer to re­al­ity.

--Albert Einstein

• I can’t ac­tu­ally re­call where I’ve seen some­one else say that e.g. “An alge­braic proof is a se­ries of steps that you can tell are lo­cally li­censed be­cause they main­tain bal­anced weights”

The metaphor of a scale is at least a com­mon teach­ing tool for alge­bra: see 1, 2, 3.

• I was taught alge­bra with a scale in the sixth grade. We had lit­tle weights that said “X” on them and learned that you could add or take away “x” from both sides.

• Yeah, we were taught in ba­si­cally the ex­act same way—mov­ing around differ­ent col­ored weights on plas­tic print-outs of bal­ances. I’ll also note that this was a pub­lic (non-mag­net) school—a rea­son­ably good pub­lic school in the sub­urbs, to be sure, but not what I would think of as an es­pe­cially ad­vanced pri­mary ed­u­ca­tion.

I join lots of other com­menters as be­ing gen­uinely sur­prised that the con­tent of this post is un­der­stood so lit­tle, even by math­e­mat­i­ci­ans, as it all seemed pretty com­mon sense to me. In­deed, my in­stinc­tive re­sponse to the first med­i­ta­tion was al­most ex­actly what Eliezer went on to say, but I kept try­ing to think of some­thing else for a while be­cause it seemed too ob­vi­ous.

• GOOD. Espe­cially this one: http://​​www.how­tolearn.com/​​2011/​​02/​​de­mys­tify­ing-algebra

But I don’t re­call ever get­ting that in my classes. Also, the illus­tra­tion of “first step go­ing from true equa­tion to false equa­tion” I think is also im­por­tant to have in there some­where.

• “An alge­braic proof is a se­ries of steps that you can tell are lo­cally li­censed be­cause they main­tain bal­anced weights”, but it seems like an ob­vi­ous di­rect spe­cial­iza­tion of “syn­tac­tic im­pli­ca­tion should pre­serve se­man­tic im­pli­ca­tion”

Eliezer, I very much like your an­swer to the ques­tion of what makes a given proof valid, but I think your ex­pla­na­tion of what proofs are is severely lack­ing. To quote An­drej Bauer in his an­swer to the ques­tion “Is rigour just a rit­ual that most math­e­mat­i­ci­ans wish to get rid of if they could?”, treat­ing proofs as syntatic ob­jects “puts logic where anal­y­sis used to be when math­e­mat­i­ci­ans thought of func­tions as sym­bolic ex­pres­sions, prob­a­bly some­time be­fore the 19th cen­tury.” If the only im­por­tant thing about the steps of a proof are that they pre­serve bal­anced weights (or se­man­tic im­pli­ca­tion), then it shouldn’t be im­por­tant which steps you take, only that you take valid steps. Con­se­quently, it should be ei­ther non­sen­si­cal or ir­rele­vant to ask if two proofs are the same; the only im­por­tant prop­erty of a proof, math­e­mat­i­cally, val­idity (un­der this view). But this isn’t the case. Peo­ple care about whether or not proofs are new and origi­nal, and which meth­ods they use, and whether or not they help give a per­son in­tu­ition. Fur­ther­more, it is com­mon to prove a the­o­rem, and re­fer to a con­stant con­structed in that proof. (If the only im­por­tant prop­erty of a proof were val­idity, this should be an in­ad­mis­si­ble prac­tice.) Fi­nally, as we have only re­cently dis­cov­ered, it is fruit­ful to in­ter­pret proofs of equal­ity as paths in topolog­i­cal spaces! If a proof is just a se­ries of steps which pre­serve se­man­tic im­pli­ca­tion, we should be wary of mod­els which only per­mit con­tin­u­ous preser­va­tion of se­man­tic im­pli­ca­tion, but this in­ter­pre­ta­tion is pre­cisely the one which leads to ho­mo­topy type the­ory.

So while I like your an­swer to the ques­tion “What ex­actly is the differ­ence be­tween a valid proof and an in­valid one?”, I think proof-rele­vant math­e­mat­ics has a much bet­ter an­swer to the ques­tion you claimed to an­swer “What ex­actly is a proof?”

(By the way, I highly rec­comend An­drej Bauer’s an­swer to any­one in­ter­ested in elo­quent prose about why proof-rele­vant math­e­mat­ics and ho­mo­topy type the­ory are in­ter­est­ing.)

• My data point: as an un­der­grad­u­ate math­e­mat­i­cian at Oxford, the math­e­mat­i­cal logic course was one of the most pop­u­lar, and cer­tainly cov­ered most of this ma­te­rial. I guess I haven’t talked a huge num­ber of math­e­mat­i­ci­ans about logic, but I’d be pretty shocked if they didn’t know the differ­ence be­tween syn­tax and se­man­tics. YMMV.

• Another data point: in Cam­bridge the first course in logic done by math­e­mat­ics un­der­grad­u­ates is in third year. It cov­ers com­plete­ness and sound­ness of propo­si­tional and pred­i­cate logic and is quite pop­u­lar. But in third year peo­ple are already so spe­cial­ised that prob­a­bly way less than half of us take it.

• It ter­rifies me that I seem to be unique in hav­ing had pretty much all of this cov­ered in my high school’s stan­dard math cur­ricu­lum (not even an ad­vanced or op­tional class). Eliezer’s method of “find the point where it be­comes un­true” wasn’t stan­dard, but I think (p ~0.5) that my teacher went over it when I wrote a proof of 2=1 on the board. I knew he was a cool math teacher who made a point of tu­tor­ing flag­ging stu­dents, but I hadn’t re­al­ized he was this ex­cep­tional.

• Judg­ing just from your de­scrip­tion, he’s prob­a­bly more than two stan­dard de­vi­a­tions of ab­nor­mal.

Your cur­ricu­lum sounds at least a good deal above av­er­age, but the core prob­lem is that most “cur­ricula” are effec­tively noth­ing more than a list of things that teach­ers should make sure to men­tion, along with a sep­a­rate, dis­joint, of­ten not cor­re­lated list of things that will be “tested” in an exam.

I ex­pect many cur­ricula would con­tain a good deal of the good parts of tra­di­tional ra­tio­nal­ity and math­e­mat­ics, but there are many steps be­tween a list on one sheet of pa­per that each teacher must read once a year and ac­tual non-pass­word un­der­stand­ing be­com­ing com­mon­place among stu­dents.

I still have a copy of my Se­condary 4 (US 10th /​ high school sopho­more) cur­ricu­lum some­where, which my math teacher gave me se­cretly back then de­spite the threat of se­vere rep­ri­mand (our teach­ers were not even al­lowed to dis­close the ac­tual cur­ricu­lum—that’s how bad things of­ten are). We both ver­ified back then that not even half of what’s sup­posed to be cov­ered ac­cord­ing to this piece of pa­per ever ac­tu­ally gets taught in most classes. That teacher re­ally was that ex­cep­tional, but he only had so much time, split across sev­eral hun­dred stu­dents.

• Similarly, I haven’t seen the illus­tra­tion of “Where does this first go from a true equa­tion to a false equa­tion?” used as a way of teach­ing the un­der­ly­ing con­cept,

My mid­dle school alge­bra books dis­cussed this on a very ba­sic level. The prob­lem in the book would show the work of a fic­tional child who was try­ing to solve a math prob­lem and failing, and the real stu­dent would be told to iden­tify where the first one went wrong and how the prob­lem should have been solved in­stead.

I never saw it done with any­thing more com­pli­cated than alge­bra, though.

I’m not sure whether or not this is com­mon, ei­ther.

• How main­stream is the Monte Carlo meth­ods stuff, speci­fi­cally the kit­ten-ob­serv­ing ma­te­rial?

• In Hun­gary this (model the­ory and co.) is part of the stan­dard cur­ricu­lum for Math­e­mat­ics BSc. Or at least was in my time.

• to not over­load the word ‘true’ mean­ing com­par­i­son-to-causal-re­al­ity, the val­idity of a math­e­mat­i­cal theorem

Ok, de­duc­tively true things should be la­beled valid to avoid con­fu­sion with in­duc­tively true things. That’s an ex­cel­lent re­s­olu­tion of the over­load­ing of the word “true” in pop­u­lar ver­nac­u­lar.

But some­times you aren’t clear in ear­lier writ­ings about whether you are refer­ring to true or valid. For ex­am­ple, one mes­sage of Zero and One are not Prob­a­bil­ities is a so­phis­ti­cated restate­ment of the prob­lem of in­duc­tion. Still, I’m hon­estly un­cer­tain whether you in­tended a broader point. I mostly agree with what I un­der­stand, but there is some un­cer­tainty about what pre­cise rents are paid by these spe­cific be­liefs.

• Great post!

Try­ing to make a func­tion call to these con­cepts in­side your math pro­fes­sor’s head is likely to fail un­less they have knowl­edge of “math­e­mat­i­cal logic” or “model the­ory”.

Hrmm… I don’t think that’s right at all, at least for pro­fes­sors who teach proof-based classes. Do­ing proofs, in any area, re­ally does feel like go­ing from solid ground to new ground, only tak­ing steps that are guaran­teed to keep you from fal­ling into the lava. My mod­els of my math pro­fes­sors un­der­stand how an ar­gu­ment con­nects its premises to its con­clu­sions—but I haven’t got­ten into philo­soph­i­cal dis­cus­sions with them. My damned philos­o­phy pro­fes­sors, on the other hand, are the log­i­cally-rud­est peo­ple I’ve ever spo­ken to.

BTW,

Robin Han­son some­times com­plains that when he tries to ar­gue that con­clu­sion X fol­lows from rea­son­able-sound­ing premises Y, his col­leagues dis­agree with X while de­clin­ing to say which premise Y they think is false, or point­ing out which step of the rea­son­ing seems like an in­valid im­pli­ca­tion.

I parsed this as ”...his col­leagues dis­agree with X while de­clin­ing … or while point­ing out which step of the rea­son­ing seems like an in­valid im­pli­ca­tion”, which is the op­po­site of what you meant.

• Tried an edit.

Math pro­fes­sors cer­tainly un­der­stand in­stinc­tively what con­nects premises to con­clu­sions, or they couldn’t do alge­bra. It’s try­ing to talk about the pro­cess ex­plic­itly where the non-mod­ern-lo­gi­ci­ans start say­ing things like “proofs are ab­solutely con­vinc­ing, hence so­cial con­structs”.

• A math pro­fes­sor who failed to get a solid course in for­mal logic sounds un­likely… (If it’s not what you are say­ing, it’s not clear to me what that is.)

• I go to a Big Ten uni­ver­sity where the grad­u­ate-level se­quence in for­mal logic hasn’t been taught in six years.

• I never got a course in for­mal logic, and could prob­a­bly have been close to be­ing a math pro­fes­sor by now.

• Yes, well, the prob­lem is that many courses on “logic” don’t teach model the­ory, at least from what I’ve heard. Try it and see. I could’ve just been ask­ing the wrong math­e­mat­i­ci­ans—e.g. a young math­e­mat­i­cian vis­it­ing CFAR knew about model the­ory, but that it­self seems a bit se­lected. But the mod­ern courses could be bet­ter than the old courses! It’s been known to hap­pen, and I’d sure be happy to hear it.

(I’m pretty sure math­babe has been through a course on for­mal logic and so has Sa­muel R. Buss...)

• When I went to Rut­gers, the course on proof the­ory and model the­ory was taught by the philos­o­phy de­part­ment. (And it satis­fied my hu­man­i­ties re­quire­ment for grad­u­a­tion!)

• At Yale, the situ­a­tion is similar. I took a course on Gödel’s in­com­plete­ness the­o­rem and earned a hu­man­i­ties credit from it. The course was taught by the philos­o­phy de­part­ment and also in­cluded a seg­ment on the equiv­alence of var­i­ous no­tions of com­putabil­ity. Coolest hu­man­i­ties class ever!

I shud­der to think of what poli­tics were in­volved to clas­sify it as such, though.

• Prob­a­bly it was that a Phil pro­fes­sor wanted to teach the class, and no one cared to ar­gue. It’s not things like which classes are taught that are the big poli­ti­cal fights, to my knowl­edge; the fights are more of­ten about who gets the right to teach a topic of their choos­ing, and who doesn’t.

• Have you read the book of Marker? I love that thing to pieces.

• Robin Han­son some­times com­plains that when he tries to ar­gue that con­clu­sion X fol­lows from rea­son­able-sound­ing premises Y, his col­leagues dis­agree with X while de­clin­ing to say which premise Y they think is false, or point­ing out which step of the rea­son­ing seems like an in­valid im­pli­ca­tion.

I parsed this as ”...his col­leagues dis­agree with X while de­clin­ing … or while point­ing out which step of the rea­son­ing seems like an in­valid im­pli­ca­tion”, which is the op­po­site of what you meant.

I think the cor­rect syn­tax here is ”...his col­leagues dis­agree with X while de­clin­ing to say which premise..., or to point out which step...”, which links the two in­fini­tives “to say” and “to point out” to the verb “de­clin­ing”. ETA: The cur­rent edit works too.

• My damned philos­o­phy pro­fes­sors, on the other hand, are the log­i­cally-rud­est peo­ple I’ve ever spo­ken to.

Really? I find peo­ple who have done just first year philos­o­phy worse. Maybe I was lucky and had the two philos­o­phy pro­fes­sors who philoso­phize well.

• Ok, fair enough. My philos­o­phy pro­fes­sors were the log­i­cally-rud­est adults I’ve spo­ken to. Ac­tu­ally, that’s not even true. Rather, my philos­o­phy pro­fes­sors were the peo­ple I most hoped would have less than the stan­dard rude­ness, but did not at all.

An anec­dote: spring quar­ter last year, I tried to con­vince my philos­o­phy pro­fes­sor that logic pre­serves cer­tainty, but that we could (prob­a­bly) never be ab­solutely cer­tain that we had wit­nessed a cor­rect deriva­tion. He dodged, and in­stead ser­mo­nized about the his­tory of logic. At one point I men­tioned GEB, and he said, I quote, “Hofs­tadter is some­thing of a one trick pony”. Here, “one trick” refers to “self-refer­ence”. I was too flab­ber­gasted to re­spond po­litely.

• I was too flab­ber­gasted to re­spond po­litely.

I hope that means you re­frain from re­spond­ing at all. You can’t fix bro­ken high sta­tus peo­ple!

Wait. Oh bother. I try to do that all the time. But I at least tend to di­rect my efforts to­wards in­fluenc­ing the so­cial en­vi­ron­ment such that the in­cen­tives for se­cur­ing said sta­tus fur­ther are changed so that on the mar­gin the be­hav­ior of the high-sta­tus peo­ple (in­clud­ing, at times, log­i­cal rude­ness) is some­what al­tered. “Per­sua­sion” of a kind.

• Name three ways of you perform­ing said per­sua­sion.

• Name three ways of you perform­ing said per­sua­sion.

No. Not at this time. (I would pre­fer to be not be­lieved than to give ex­am­ples of this right now.)

• Ac­tu­ally it was more on the line of “give me prac­ti­cal ex­am­ples so I can ex­trap­o­late the rule bet­ter than from an ab­stract sum­mary”, but, sure, suit your­self.

• He dodged, and in­stead ser­mo­nized about the his­tory of logic

Or tried to tell you some­thing you didn’t get.

• Or tried to tell you some­thing you didn’t get.

From the de­scrip­tion TsviBT gives it is far more likely that the pro­fes­sor was stub­bornly ser­mo­niz­ing against a straw­man.

• If TsviBT failed to get some­thing, it is quite likely that from TsviBT ’s per­spec­tive the pro­fes­sor was waf­fling pointlessly, and that TsviBTs ac­count would re­flect that. We can­not ap­peal to TsviBT’s sub­jec­tive per­spec­tive as prov­ing the ob­jec­tive val­idity of it­self, can we?

• If TsviBT failed to get some­thing, it is quite likely that from TsviBT ’s per­spec­tive the pro­fes­sor was waf­fling pointlessly, and that TsviBTs ac­count would re­flect that. We can­not ap­peal to TsviBT’s sub­jec­tive per­spec­tive as prov­ing the ob­jec­tive val­idity of it­self, can we?

I can look at the spe­cific claim TsviBT says he made and eval­u­ate whether it is a true claim or a false claim. It hap­pens to be a true claim.

As­sum­ing you ac­cept the above claim then be­fore ques­tion­ing whether TsviBT failed to com­pre­hend you must first ques­tion whether what TsviBT says he said is what he ac­tu­ally said. It seems un­likely that he is ly­ing about what he said and also not es­pe­cially likely that he for­got what point he was mak­ing—it is some­thing etched firmly in his mind. It is more likely that the pro­fes­sor did not pay suffi­cient at­ten­tion to com­pre­hend than it is than that Tsvi did not say what he says he said. The former oc­curs far more fre­quently than I would pre­fer.

• Edit:

It hap­pens to be a true claim.

Is it? I think it’s a bit mis­lead­ing. Logic would pre­serve cer­tainty if there were any cer­tainty. But there prob­a­bly isnt. Maybe the prof was try­ing to make that point.

As­sum­ing you ac­cept the above claim then be­fore ques­tion­ing whether TsviBT failed to com­pre­hend you must first ques­tion whether what TsviBT says he said is what he ac­tu­ally said.

No, that isn;t the is­sue. TsviBT only offered a sub­jec­tive re­ac­tion to the pro­fes­sor’s words, not the words them­selves. We can­not judge from that whether the pro­fes­sor was rudely miss­ing his bir­lli­ant point, or mak­ing an even more bir­lli­ant ri­poste, the sub­teleties of which passed TsviBT by.

• I dis­agree re­gard­ing the ac­cu­racy of the claim as stated (you seem to be mak­ing the mis­take a pro­fes­sor may care­lessly make by con­sid­er­ing a differ­ent more triv­ial point). I also dis­agree that the alleged “brilli­ant ri­poste” could be ‘brilli­ant’ as more than an effec­tive so­cial move given that it moved to to a differ­ent point (as a ri­poste to the claim and not just an ap­pro­pri­ate sub­ject change) rather than ac­knowl­edg­ing the rather sim­ple tech­ni­cal cor­rec­tion.

You are giv­ing the pro­fes­sor the benefit of doubt that can not ex­ist with­out TsviBT’s claim of what he per­son­ally said be­ing out­right false.

• We don;t know that the ri­poste moved to a differnt point be­cause we weren;t there and do not have the profs words.

• We don;t know that the ri­poste moved to a differnt point be­cause we weren;t there and do not have the profs words.

It did one of mov­ing to a differ­ent point, agree­ing with TsviBT or be­ing out­right in­cor­rect. (Again fol­low­ing your as­sump­tion that it was, in fact, a ri­poste.) Mov­ing to a differ­ent point is the most likely (and most gen­er­ous) as­sump­tion.

(I have ex­pressed my point as much as I ought and most likely then some. It would be best for me to stop.)

• TsviBT ’s point was not out­right cor­rect,, which leads to fur­ther op­tions such as ex­pound­ing on a sub­tle er­ror.

• To be fair, Hoft­stadter is ba­si­cally a one-trick pony, in that he pub­lished one aca­dem­i­cally-rele­vant book and then more or less jumped straight to Pro­fes­sor Emer­i­tus in all but name, pub­lish­ing very lit­tle and in­ter­act­ing with academia even less.

• Just wish­ing I had read GEB sooner. Read­ing it now and it seems to be get­ting ru­ined by poli­tics.

• Poli­tics? I don’t un­der­stand how.

Also, above com­ment should in no way be taken as crit­i­cism of GEB. It’s great. It’s just that that’s pretty much all he has to his credit.

• I mean peo­ple want to tear chunks out of it for sta­tus rea­sons… …I think.

• An anec­dote: spring quar­ter last year, I tried to con­vince my philos­o­phy pro­fes­sor that logic pre­serves cer­tainty, but that we could (prob­a­bly) never be ab­solutely cer­tain that we had wit­nessed a cor­rect deriva­tion.

This does seem cor­rect as stated. I won­der if he de­liber­ately avoided the point to save face re­gard­ing a pre­vi­ous er­ror or, as Tim sug­gested, pat­tern matched to some­thing differ­ent.

• Rather, my philos­o­phy pro­fes­sors were the peo­ple I most hoped would have less than the stan­dard rude­ness, but did not at all.

Now that is far less sur­pris­ing and on av­er­age I can agree there (al­though I per­son­ally had ex­cep­tions!) It was the ab­solute scale that I per­haps ques­tioned.

• To be fair to the pro­fes­sor, con­flat­ing de­duc­tive and in­duc­tive rea­son­ing is a ba­sic er­ror that’s easy to pat­tern match.

• To be fair to the pro­fes­sor, con­flat­ing de­duc­tive and in­duc­tive rea­son­ing is a ba­sic er­ror that’s easy to pat­tern match.

To be fair to TsviBT it is pat­tern match­ing to the near­est pos­si­ble stupid thing that is per­haps the most an­noy­ing log­i­cal rude tac­tics there is (whether em­ployed de­liber­ately or in­stinc­tively ac­cord­ing to so­cial drives).

• FWIW, the un­der­grad­u­ate Philos­o­phy de­part­ment at South­ern Con­necti­cut State Univer­sity has at least 2 logic courses, and the “Philo­soph­i­cal logic” spe­cial top­ics course cov­ers ev­ery­thing here and then some in a lot of de­tail. The first half of the course goes through syn­tax and se­man­tics for propo­si­tional logic sep­a­rately, as well as the rele­vant the­o­rems that show how to link them up.

• Fi­nally, an Ein­stein quote used on the in­ter­net that isn’t ob­vi­ously false.

• I hap­pen to be study­ing model the­ory at the mo­ment. For any­one cu­ri­ous, when Eliezer say ‘If X ⊢ Y, then X ⊨ Y’ (that is, if a model proves a state­ment, that state­ment is true in the model), this is known as sound­ness. The con­verse is com­plete­ness, or more speci­fi­cally se­man­tic com­plete­ness, which says that if a state­ment is true in ev­ery model of a the­ory (in other words, in ev­ery pos­si­ble world where that the­ory is true), then there is a finite proof of the state­ment. In sym­bols this is ‘If X ⊨ Y, then X ⊢ Y’. Note that this no­tion of ‘com­plete­ness’ is not the one used in Gödel’s in­com­plete­ness the­o­rems.

• I plan to talk about this in some posts on sec­ond-or­der logic.

• Note that this no­tion of ‘com­plete­ness’ is not the one used in Gödel’s in­com­plete­ness the­o­rems.

Um, yes it is, I think. The in­com­plete­ness the­o­rems tell you that there are state­ments that are true (se­man­ti­cally valid) but un­prov­able, and hence they provide a coun­terex­am­ple to “If X |=Y then X |- Y”, i.e. the proof sys­tem is not com­plete.

EDIT: To all re­spon­dents: sorry, I was un­clear. Yes, I do re­al­ise that FOL is com­plete, but the same no­tion of com­plete­ness gen­er­al­ises to differ­ent proof sys­tems. The in­com­plete­ness the­o­rems show that the proof sys­tem for Peano ar­ith­metic is in­com­plete, in pre­cisely this way

• First-or­der logic is com­plete. There are no coun­terex­am­ples. Since the Godel sen­tence of a the­ory is not prov­able from the ax­ioms of a the­ory, it fol­lows (from com­plete­ness) that the Godel sen­tence must be false in some “non-stan­dard” mod­els of the ax­ioms.

You can read the first in­com­plete­ness the­o­rem as say­ing that there’s no way to come up with a finitely ex­press­ible set of ax­ioms that can prove all the truths of ar­ith­metic. This is not in con­flict with the com­plete­ness the­o­rem. The com­plete­ness the­o­rem tells us that if there were some finite (or re­cur­sively enu­mer­able) set of ax­ioms of ar­ith­metic such that the in­fer­ence to any truth of ar­ith­metic from those ax­ioms was se­man­ti­cally valid, then all truths of ar­ith­metic can be proven from that set of ax­ioms. The in­com­plete­ness the­o­rem tells us that the an­tecedent of this con­di­tional is false; it doesn’t deny the truth of the con­di­tional it­self.

• Right, I think the con­fu­sion was that I tend to think of the in­com­plete­ness the­o­rems as be­ing about sec­ond-or­der Peano ar­ith­metic, but it does give a some­what differ­ent re­sult for first-or­der.

• The in­com­plete­ness the­o­rems tell you that there are state­ments that are true (se­man­ti­cally valid) but un­prov­able, and hence they provide a coun­terex­am­ple to “If X |=Y then X |- Y”, i.e. the proof sys­tem is not com­plete.

This is not cor­rect. In first-or­der logic, there are no coun­terex­am­ples to “If X |=Y then X |- Y”—this is (equiv­a­lent to) Gödel’s com­plete­ness the­o­rem. Gödel’s in­com­plete­ness the­o­rem says that ev­ery first-or­der the­ory with an effec­tively enu­mer­able set of ax­ioms, and which in­cludes ar­ith­metic, con­tains some propo­si­tions which have nei­ther a proof nor a dis­proof. One typ­i­cally goes on to say that the un­de­cid­able propo­si­tion that the proof con­structs is true in the “usual model” of the nat­u­ral num­bers, but that is verg­ing on philos­o­phy. At any rate, the truth of the propo­si­tion is as­serted for only one par­tic­u­lar model of the ax­ioms of ar­ith­metic, not all pos­si­ble mod­els. By the com­plete­ness the­o­rem, an un­de­cid­able propo­si­tion must be true in some mod­els and false in oth­ers.

• I think you’re con­fus­ing syn­tax and se­man­tics your­self here. An un­de­cid­able propo­si­tion has no proof, that does not mean it is not se­man­ti­cally valid. So the sec­ond the­o­rem shows that for a con­sis­tent the­ory T, the state­ment ConT that T is con­sis­tent is not prov­able, but it is true in all mod­els.

• So the sec­ond the­o­rem shows that for a con­sis­tent the­ory T, the state­ment ConT that T is con­sis­tent is not prov­able, but it is true in all mod­els.

No, it isn’t. When T in­cludes ar­ith­metic, ConT is not prov­able in T (pro­vided that T is con­sis­tent, the usual back­ground as­sump­tion). There­fore by the com­plete­ness the­o­rem, there are mod­els of T in which ConT is false.

ConT can be in­for­mally read as “T is con­sis­tent”, and by as­sump­tion the lat­ter state­ment is true, but that is not the same as ConT it­self be­ing true in any model other than the unique one we think we are talk­ing about when we talk about the nat­u­ral num­bers.

• Okay, I think this is still be­cause I’m think­ing about the sec­ond-or­der logic re­sult. I just went and looked up the FOL stuff, and the in­com­plete­ness the­o­rem does give some weird re­sults in FOL! You’re quite right, you do get mod­els in which ConT is false.

I think my point still stands for SOL, though.

• No, not quite. The dis­tinc­tion is sub­tle, but I’ll try to lay it out.

there are state­ments that are true (se­man­ti­cally valid) but un­prov­able, and hence they provide a coun­terex­am­ple to “If X |=Y then X |- Y”

This is not the case. The prob­lem is with the ‘and hence’: ‘X ⊨ Y’ should not be read as ‘Y is true in X’ but rather ‘Y is true in ev­ery model of X’. There are state­ments which are true in the stan­dard model of Peano ar­ith­metic which are not en­tailed by it—that is, ‘Y is true in the stan­dard model of Peano ar­ith­metic’ is not the same as ‘PA ⊨ Y’. So this is not a coun­terex­am­ple.

Rather, the no­tion of ‘com­plete’ in the in­com­plete­ness the­o­rem is that a model is com­plete if for ev­ery state­ment, ei­ther the state­ment or its nega­tion is en­tailed by the model (and hence prov­able by se­man­tic com­plete­ness). Gödel’s in­com­plete­ness the­o­rem shows that no the­ory T con­tain­ing PA is com­plete in this sense; that is, there state­ments S which are true in T but not en­tailed by it (and so not prov­able). This is be­cause there are mod­els of T in which S is not true: that is, sys­tems in which ev­ery state­ment in T holds, but S does not. (Th­ese sys­tems have some ad­di­tional struc­ture be­yond that re­quired by T.)

Wikipe­dia may do a bet­ter job of ex­plain­ing this than I can at the mo­ment.

• I did mean “se­man­ti­cally valid” to be “true in all mod­els”, I was just think­ing about sec­ond-or­der Peano ar­ith­metic not first-or­der ;) I think it’s more nat­u­ral pre­cisely be­cause then it ex­actly does show in­com­plete­ness.

• I’ll at­tempt to clar­ify a lit­tle, if that’s alright. Given a par­tic­u­lar well-be­haved the­ory T, Gödel’s (first!) in­com­plete­ness the­o­rem ex­hibits a state­ment G that is nei­ther prov­able nor dis­prov­able in T—that is, nei­ther G nor ¬G is syn­tac­ti­cally en­tailed by T. It fol­lows by the com­plete­ness the­o­rem that there are mod­els of T in which G is true, and mod­els of T in which ¬G is true.

Now G is of­ten in­ter­preted as mean­ing “G is not prov­able in T”, which is ob­vi­ously true. How­ever, this in­ter­pre­ta­tion is an ar­ti­fact of the way we’ve care­fully con­structed G, us­ing a sys­tem of re­la­tions on Gödel num­bers de­signed to care­fully re­flect the prov­abil­ity re­la­tions on state­ments in the lan­guage of T. But these Gödel num­bers are el­e­ments of what­ever model of T we’re us­ing, and our as­sump­tion that the re­la­tions used in the con­struc­tion of G have any­thing to do with prov­abil­ity in T only ap­ply if the Gödel num­bers are from the usual, non-crazy model N of the nat­u­ral num­bers. There are un­usual, very-much-crazy mod­els of the nat­u­ral num­bers which are not N, how­ever, and if we’re us­ing one of those then our re­la­tions are un­in­tu­itive and wacky and have noth­ing at all to do with prov­abil­ity in T, and in these G can be true or false as it pleases. So when we say “G is true”, we ac­tu­ally mean “G is true if we’re us­ing the stan­dard model of the nat­u­ral num­bers, which may or may not even be a valid model of T in the first place”.

• The sim­plest way to ex­plain the differ­ence, is that Gödel’s com­plete­ness the­o­rem ap­plies to first or­der logic, whereas Gödel’s in­com­plete­ness the­o­rem ap­plies to sec­ond or­der logic.

• Right.

• The mo­ti­va­tion for the ex­tremely un­satis­fy­ing idea that proofs are so­cial is that no lan­guage—not even the for­mal lan­guages of math and logic—is self-in­ter­pret­ing. In or­der to un­der­stand a syl­l­o­gism about kit­tens, I have to un­der­stand the lan­guage you use to ex­press it. You could try to ex­plain to me the rules of your lan­guage, but you would have to do that in some lan­guage, which I would also have to un­der­stand. Un­less you as­sume some a pri­ori lin­guis­tic agree­ment, ex­plain­ing how to in­ter­pret your syl­l­o­gism, re­quires ex­plain­ing how to in­ter­pret the lan­guage of your ex­pla­na­tion, and ex­plain­ing how to in­ter­pret the lan­guage of that ex­pla­na­tion, and so on ad in­fini­tum. This is es­sen­tially the point Lewis Car­roll was mak­ing when he said that “A” and “if A then B” were not enough to con­clude B. You also need “if ‘A’ and ‘if A then B’ then B” and and so on and so on. You and I may un­der­stand that as im­plied already. But it is not log­i­cally nec­es­sary that we do so, if we don’t already un­der­stand the English lan­guage the same way.

This is, I think, the cen­tral point that Lud­wig Wittgen­stein makes in The Philo­soph­i­cal In­ves­ti­ga­tions and Re­marks on the Foun­da­tion of Math­e­mat­ics. It’s not your awe­some kit­ten pic­tures are prob­le­matic. You and I might well see the same phys­i­cal world, but not agree on how your syl­l­o­gism ap­plies to it. Along the same lines, Saul Kripke ar­gued that the state­ment 2+2=4 was prob­le­matic, not be­cause of any dis­agree­ment about the phys­i­cal world, but be­cause we could dis­agree about the mean­ing of the state­ment 2+2=4 in ways that no dis­cus­sion could ever nec­es­sar­ily clear up (and that it was there­fore im­pos­si­ble to re­ally say what the mean­ing of that sim­ple state­ment is).

In math and logic, this is typ­i­cally not much of a prob­lem. We gen­er­ally all read the state­ment 2+2=4 in a way that seems the same as the way ev­ery­one else reads it. But that is a fact about us as hu­mans with our par­tic­u­lar ed­u­ca­tion and cog­ni­tive abil­ities, not an in­trin­sic fea­ture of math or logic. Proof of your kit­ten syl­l­o­gism is so­cial in the sense that we agree so­cially on the mean­ing of the syl­l­o­gism it­self, but not be­cause states of af­fairs you rep­re­sent in your pic­tures are in any way so­cially de­ter­mined.

And if this is nor­mally much of an is­sue in math­e­mat­ics, it is in­cred­ibly prob­le­matic in any kind of meta­math­e­mat­i­cal or met­a­log­i­cal philos­o­phy—in other words, once we start try to ex­plain why math and logic must nec­es­sar­ily be true. The kep point is not that the world is so­cially con­structed, but that any at­tempt to talk about the world is so­cially con­structed, in a way that makes fi­nal, nec­es­sary judg­ments about its truth or falsity im­pos­si­ble.

• From my per­spec­tive, when I’ve ex­plained why a sin­gle AI alone in space would benefit in­stru­men­tally from check­ing proofs for syn­tac­tic le­gal­ity, I’ve ex­plained the point of proofs. Com­mu­ni­ca­tion is an or­thog­o­nal is­sue, hav­ing noth­ing to do with the struc­ture of math­e­mat­ics.

• I thought of a bet­ter way of putting what I was try­ing to say. Com­mu­ni­ca­tion may be or­thog­o­nal to the point of your ques­tion, but rep­re­sen­ta­tion is not. An AI needs to use an in­ter­nal lan­guage to rep­re­sent the world or the struc­ture of math­e­mat­ics—this is the crux of Wittgen­stein’s fa­mous “pri­vate lan­guage ar­gu­ment”—whether or not it ever at­tempts to com­mu­ni­cate. You can’t eval­u­ate “syn­tac­tic le­gal­ity” ex­cept within a par­tic­u­lar lan­guage, whose cor­re­spon­dence to the world is not given a mat­ter of logic (al­though it may be more or less use­ful prag­mat­i­cally).

• See my re­ply to Chap­pell here and the en­clos­ing thread: http://​​less­wrong.com/​​lw/​​f1u/​​causal_refer­ence/​​7phu

• If your point is that it isn’t nec­es­sar­ily use­ful to try to say in what sense our pro­ce­dures “cor­re­spond,” “rep­re­sent,” or “are about” what they serve to model, I com­pletely agree. We don’t need to ex­plain why our model works, al­though some the­ory may help us to find other use­ful mod­els.

But then I’m not sure see what is at stake when you talk about what makes a proof cor­rect. Ob­vi­ously we can have a valuable dis­cus­sion about what kinds of demon­stra­tion we should find con­vinc­ing. But ul­ti­mately the pro­ce­dure that guides our be­hav­ior ei­ther gives satis­fac­tory re­sults or it doesn’t; we were ei­ther right or wrong to be con­vinced by an ar­gu­ment.

• The math­e­mat­i­cal re­al­ist con­cept of “the struc­ture of math­e­mat­ics”—at least as sep­a­rate from the phys­i­cal world—is prob­le­matic once you can no longer de­scribe what that struc­ture might be in a non-ar­bi­trary way. But I see your point. I guess my re­sponse would be that the con­cept of “a proof”—which im­plies that you have demon­strated some­thing be­yond the pos­si­bil­ity of con­tra­dic­tion—is not what re­ally mat­ters for your pur­poses. Ul­ti­mately, how an AI ma­nipu­lates its rep­re­sen­ta­tions of the world and how it in­ter­nally rep­re­sents the world are in­ex­tri­ca­bly re­lated prob­lems. What mat­ters is how well the AI can pre­dict/​retro­d­ict/​ma­nipu­late phys­i­cal phe­nom­ena. Your AI can be a prag­ma­tist about the con­cept of “truth.”

• “I will re­mark, in some hor­ror and ex­as­per­a­tion with the mod­ern ed­u­ca­tional sys­tem, that I do not re­call any math-book of my youth ever once ex­plain­ing that the rea­son why you are always al­lowed to add 1 to both sides of an equa­tion is that it is a kind of step which always pro­duces true equa­tions from true equa­tions.”

I can now say that my K-12 ed­u­ca­tion was, at least in this one way, bet­ter than yours. I must have been 14 at the time, and the re­al­iza­tion that you can do that hit me like a ton of bricks, fol­lowed closely by an­other ton of bricks—choos­ing what to add is not gov­erned by the laws of math—you re­ally can add any­thing, but not ev­ery­thing is equally use­ful.

E.g., “solve for x, x+1=5”

You can choose to add −1 to the equa­tion, get­ting “x+1+-1=5+-1”, sim­plify both sides and get “x=4“ and yell “yay”, but you can also choose to add, say, 37, and get (af­ter sim­plifi­ca­tion) “x+38=42” which is still true, just not use­ful. My im­me­di­ate ques­tion af­ter that was “how do you know what to choose” and, long story short, 15 years later I pub­lished a math pa­per… :)

• I ab­solutely re­mem­ber be­ing taught that the rea­son we could add some­thing to both sides, sub­tract some­thing from both sides, di­vide or mul­ti­ply… was be­cause it pre­served the equal­ity. I think 7th grade. And when I helped my kids on the rele­vant math (they did not in­herit my “in­tu­itive ob­vi­ous­ness” gene) I would re­peat this over and over.

Of course we all want to blame the teacher or the course when we haven’t learned some­thing in the past, but I have seen too many peo­ple not learn things that I was re­peat­ing and em­pha­siz­ing and ex­plain­ing in as many ways as I could imag­ine or read, and still they didn’t get it. I think we have all head the ex­pe­rience of hav­ing some­one we were ex­plain­ing some­thing to fi­nally get it and ex­claim some­thing like “why didn’t you just tell me that in the first place.”

• I’d prob­a­bly be in­ter­ested in read­ing that pa­per, since I’ve never my­self figured it out and still have to (grudg­ingly) rely on the school-drilled method of “do more ex­er­cises and solve more prob­lems un­til it’s so painfully ob­vi­ous that it hurts”. AKA the we-have-no-idea-but-do-it-any­way method.

• My mat class pro­vided the sim­ple “how to choose” heuris­tic that you want X to be alone. So if you have “x+1″ on one side, you’ll need to sub­tract 1 to get it by it­self. X+1-1=5-1. X=4.

I can see how this wouldn’t get ex­plicit at­ten­tion, since I’d sus­pect it be­comes in­tu­itive af­ter a point, and you just don’t think to ask that ques­tion. I can’t see how one could get through even ba­sic alge­bra with­out de­vel­op­ing this in­tu­ition, though o.o

• Yes, clearly, a bit af­ter I asked, I learned how to use in­tu­ition, and at some point, it be­came rote. But the big­ger point is that this is a spe­cial case—in logic, and in math, there are a lot of truth-pre­serv­ing trans­for­ma­tions, and choos­ing a se­quence of trans­for­ma­tions is what do­ing math is. That in­ter­est­ing in­ter­face be­tween logic-as-rigid and math-as-some­thing-ex­plo­ra­tory is a big part of the fun in math, and what led me to do enough math that led to a pub­lished pa­per. Of course, af­ter that, I went into soft­ware en­g­ineer­ing, but I never for­got that ini­tial sen­sa­tion of “oh my god that is awe­some” the first time Moshe_1992 learned that there is no such thing as “mov­ing the 1 from one side of the equa­tion to the other” ex­cept as a high-level ab­strac­tion.

• I can’t see how one could get through even ba­sic alge­bra with­out de­vel­op­ing this in­tu­ition, though o.o

And yet so many do. Num­bers are hor­ribly scarce in this area, though. Some­times I get des­per­ate.

Anec­do­tally, I do re­mem­ber say­ing some­thing very similar to high school peers, in a man­ner that as­sumed they already un­der­stood it, and see­ing their face con­tort in ex­actly the same man­ner that it would have had I sud­denly meta­mor­phosed into a po­lar bear and started writ­ing all the equa­tions for fourier and laplace trans­forms us­ing trails of vol­canic ash in mid-air.

This was years af­ter ba­sic alge­bra had already been taught ac­cord­ing to the cur­ricu­lum, and we were now be­gin­ning pre-calcu­lus (i.e. last year of sec­ondary /​ high school here in québec, calcu­lus it­self is never touched in high school level courses).

• If you’re try­ing to find the value of x and there’s only one x in the equa­tion, it’s sim­ply a mat­ter of in­vert­ing ev­ery func­tion in the equa­tion from the out­side in. It’s harder if you have mul­ti­ple x’s be­cause you have to try to com­bine them in some rea­son­able way—and some­times you ac­tu­ally want to sep­a­rate them, e.g. “x^2 − 9 = 0” into “(x − 3)(x + 3) = 0″.

Solv­ing this prob­lem ap­pears equiv­a­lent to writ­ing a com­puter pro­gram to solve alge­braic equa­tions.

• For polyno­mial ex­pres­sions of the third or­der or lower in only one vari­able, the pro­cess is triv­ial. I be­lieve that in ev­ery gen­eral case for which a solu­tion is guaran­teed, there is also a triv­ial method which will always gen­er­ate such a solu­tion.

• There are closed form solu­tions to all cu­bic or quar­tic polyno­mial equa­tions, but they’re quite com­pli­cated. Do those solu­tions count as “triv­ial”?

• Are any de­ci­sions re­quired to be made in their im­ple­men­ta­tion? If so, they are non­triv­ial. If not, they are triv­ial.

I was say­ing that for ev­ery gen­eral case in which a zero of a polyno­mial is guaran­teed, there is a de­ter­minis­tic path to de­ter­mine what the guaran­teed ze­ros are.

• Hrm. Is there a short proof of this claim? It’s not com­pletely ob­vi­ous to me. How do you know there isn’t some set of n-th de­gree polyno­mi­als, for which there’s a non-con­struc­tive proof that they have roots, but where there isn’t any known al­gorithm for find­ing them?

I sup­pose you could always do nu­meric eval­u­a­tion with bi­sec­tion or some­such, since polyno­mi­als are smooth. But I think you’re say­ing some­thing more than “iter­a­tive nu­mer­i­cal meth­ods can find ze­ros of polyno­mi­als over one vari­able.” I also imag­ine that you don’t want to in­clude “ex­plore all pos­si­ble de­ci­sion trees” as a valid solu­tion method.

Part of my hes­i­ta­tion is that there are classes of equa­tion (not polyno­mial) for which it’s be­lieved that there aren’t effi­cient al­gorithms to find solu­tions. For in­stance, sup­pose we have a fixed g, k, n. There’s no known effi­cient tech­nique to find x such that g^x = k, mod n. (This is the dis­crete log­a­r­ithm prob­lem.) It seems think­able to me that there are similar cases over the re­als, but where you can’t do ex­haus­tive search.

• There ex­ist what is called non-alge­braic re­als, which can­not be de­scribed with any­thing other than the in­finite string of dec­i­mals they are.

• Yes. I’m aware of them. But that’s not quite the ques­tion here. The ques­tion was whether there were equa­tions that have solu­tions, that can be found, but where there’s no al­gorithm to do so. So by defi­ni­tion the num­bers of in­ter­est are defin­able in some way more suc­cinct than their in­finite rep­re­sen­ta­tion.

As a nit­pick: My un­der­stand­ing is that alge­braic just means a num­ber is the root of some polyno­mial equa­tion with ra­tio­nal co­effi­cients. But that’s not the same as “can­not be de­scribed ex­cept with an in­finite dec­i­mal string.” A num­ber might be de­scribed suc­cinctly while still be­ing tran­scen­den­tal. The nat­u­ral log­a­r­ithm base is tran­scen­den­tal—not alge­braic—but can be de­scribed suc­cinctly. It has a one-let­ter name (“e”) and a well known se­ries ex­pres­sion that con­verges quickly. I think you want to re­fer to some­thing like the non-com­putable re­als, not the non-alge­braic re­als.

• I only got K-8[\6] (I’m not a high­school dropout, thank you, I just never went in the first place) so I’ve got no idea what peo­ple learn when they’re 14.

• Homeschooled! The sta­tus-pre­serv­ing term is “home­schooled”!

• For the peo­ple who got Thiel Fel­low­ships, the sta­tus-pre­serv­ing term is “stopped-out”.

• Heck, at that level even “drop-out” works as a form of counter-sig­nal­ing.

• Homeschool­ing is what Chris­ti­ans do. I’m an au­to­di­dact.

• One thing that I’ve always wanted to ask you, but for some rea­son never have, is what kind of form your au­to­di­dac­tism took. Did you just read books (if so, what kind? Text­books?), did you get a tu­tor, did your par­ents help?

• Homeschooled! The sta­tus-pre­serv­ing term is “home­schooled”!

Homeschooled? That is sta­tus-pre­serv­ing? Really? I think I’d pre­fer “dropout”.

• “Homeschooled” is what you say to col­lege ad­mis­sions peo­ple.

“Dropout” im­plies that you’re not in­ter­ested in con­tin­u­ing your ed­u­ca­tion.

• If you con­sider the ideas of John Tay­lor Gatto, the 1991 New York State teacher of the year, re­gard­ing school­ing, you might hes­i­tate be­fore us­ing the word “school­ing” to mean some­thing cred­ible.

His per­spec­tive is that school­ing is not ed­u­ca­tion and can help or hin­der learn­ing (ex­plained un­der the head­ing “Learn­ing, School­ing, & Ed­u­ca­tion”). The crit­i­cisms he pro­vides in “Dumb­ing us Down” are pretty nasty. I gave the gist of it and linked to an on­line book pre­view here. I highly recom­mend read­ing at least the first chap­ter of that book.

• Yeah, I’ve read some of what he says. He’s right and he’s wrong; Amer­i­can pub­lic ed­u­ca­tion is in­deed de­signed to pro­duce work­ers, but we still have far more en­trepreneurs per cap­ita than, say, China.

• Hmmm. Not to ig­nore the fact that this es­sen­tially sidesteps my point that school should not nec­es­sar­ily be as­so­ci­ated with cred­i­bil­ity, but you’ve suc­ceeded in mak­ing me cu­ri­ous: what do you think the differ­ence is be­tween the US and China that would ex­plain that?

• Ac­tu­ally, I think I’m wrong on the facts here; The GEM 2011 Global Re­port has some ta­bles about this, but they don’t copy/​paste very well. The U.S. is ranked first in “early-stage en­trepreneurial ac­tivity” (per­centage of the pop­u­la­tion that owns or is em­ployed by a busi­ness less than three and a half years old) among na­tions char­ac­ter­ized as “in­no­va­tion-driven economies” (a cat­e­gory that in­cludes most of Europe, Ja­pan, and South Korea) at 12.3%, but “effi­ciency-driven economies” (which in­cludes China, most of Latin Amer­ica, and much of Eastern Europe) tend to have higher val­ues; China is listed at 24.0%,

• I think it’s a good thing you didn’t re­ceive more school­ing. I’m an au­to­di­dact, too. I wish I had em­barked on a self-ed­u­ca­tion jour­ney sooner. Rea­sons.

• Nick Bostrom put forth the Si­mu­la­tion Ar­gu­ment, which is that you must dis­agree with ei­ther state­ment (1) or (2) or else agree with state­ment

Given sev­eral other as­sump­tions, some em­piri­cal, some about an­thropic rea­son­ing.

• Right. Most poe­ple dis­agree with the premise “Be­ing in a simu­la­tion is/​can be made to be in­dis­t­in­guish­able from re­al­ity from the point of view of the simulee.”

Edit: And by most peo­ple, I mean my anal­y­sis of why I in­tu­itively re­ject the con­clu­sion, not any dis­cus­sion with other, let alone 3.6+ billion peo­ple or statis­ti­cally rep­re­sen­ta­tive sam­pling, etc.

• Yes, and this isn’t nec­es­sar­ily due to naive ‘no mere simu­la­tion could feel so real’-type think­ing ei­ther. Once can make a de­cent ar­gu­ment that the only known method of mak­ing a simu­la­tion that can fool mod­ern physics labs would be to simu­late the en­tire planet and much of sur­round­ing space at the level of quan­tum me­chan­ics, which is com­pu­ta­tion­ally in­tractable even with ma­ture nan­otech. Well, that or have an SI con­stantly tin­ker­ing with ev­ery­one’s per­cep­tions to make them think ev­ery­thing looks cor­rect, but then you have to sup­pose that such en­tities have noth­ing more in­ter­est­ing to do with their run­time.

• I once de­scribed a 240 GHz waveg­uide-struc­ture ra­dio re­ceiver I had built as a “com­pre­hen­sive analogue simu­la­tion of Maxwell’s equa­tions in­cor­po­rat­ing re­al­is­tic as­sump­tions about the con­duc­tivity of real ma­te­ri­als used in waveg­uide man­u­fac­ture.” Although this simu­la­tion was in­sanely ac­cu­rate, it was much more difficult to a) change pa­ram­e­ters in this simu­la­tion and b) mea­sure/​calcu­late the re­sults of this simu­la­tion than with the more tra­di­tional digi­tal simu­la­tions of Maxwell’s equa­tions we had available.

• Another pos­si­bil­ity would be to build simu­lated per­ceivers whose per­cep­tions are sys­tem­at­i­cally dis­torted in such a way that they will fail to no­tice the gaps in the simu­lated en­vi­ron­ment, I sup­pose. Which would not re­quire con­stant de­liber­ate in­ter­ven­tion by an in­tel­li­gence.

• Be­fore you build that, just to prac­tice your skills you can build some code that will take a blurry pic­ture and with ex­tremely high ac­cu­racy show what the pic­ture would have looked like had the cam­era been in fo­cus. This prob­lem would of course be much eas­ier than know­ing that you had built a simu­la­tion with holes in it but man­aged to cor­rect for the ab­sence of in­for­ma­tion in the simu­la­tion in a way that was ac­tu­ally sim­pler than fix­ing the simu­la­tion in the first place.

I think you might run in to limits based on con­sid­er­a­tions of in­for­ma­tion the­ory that make both tasks pos­si­ble, but if you start with the image re­con­struc­tion prob­lem you will save a lot of effort.

• Be­fore you build that, just to prac­tice your skills you can build some code that will take a blurry pic­ture and with ex­tremely high ac­cu­racy show what the pic­ture would have looked like had the cam­era been in fo­cus.

This has now been done—to a first ap­prox­i­ma­tion, at least.

• The prob­lem with that pro­gram is that the in­for­ma­tion was already there. The in­for­ma­tion may have been scat­tered in a semi-ran­dom pat­tern, but it was still there to be re­or­ga­nized. In this hy­po­thet­i­cal simu­la­tion, there is a lack of in­for­ma­tion. And while you can undo ran­dom­iza­tion to recre­ate a blurred image, you can­not cre­ate in­for­ma­tion from noth­ing.

How­ever, the hu­man brain does have some in­ter­est­ing traits which might make it pos­si­ble for hu­mans to think they are see­ing some­thing with­out cre­at­ing all the in­for­ma­tion such a thing would pos­sess. The neo­cor­tex has mul­ti­ple lev­els. Lower lev­els de­tect things like ab­sence and pres­ence of light, which higher lev­els turn into lines and curves, which even higher lev­els turn into shapes, which even­tu­ally get in­ter­preted as a spe­cific face (the brain has clusters of a few hun­dred neu­rons re­spon­si­ble for ev­ery face we have mem­o­rized). All you would have to do to make a hu­man brain think they saw some­one would be to stim­u­late the top few hun­dred neu­rons, the bot­tom ones need not be given in­for­ma­tion. Imag­ine a gen­eral tel­ling his troops to move some­where. Each troop car­ries out an ac­tion, tells their su­pe­rior, who gives their su­pe­rior a gen­er­al­iza­tion, who gives their su­pe­rior a gen­er­al­iza­tion, un­til the gen­eral gets one mes­sage “Move go­ing fine”. To fool the gen­eral (hu­man) into think­ing the move is go­ing fine (in­ter­act­ing with some­thing), you don’t need to forge the en­tire chain of events (simu­late ev­ery quark), you just need to give them the mes­sage say­ing ev­ery­thing is go­ing great (stim­u­late those few hun­dred neu­rons). And then when the ma­trix per­son looks closer, the Ma­trix Lords just forge the lower lev­els tem­porar­ily.

The prob­lem with this is is it does not match the prin­ci­ple “Hu­mans simu­lat­ing old earth to get in­for­ma­tion”. It would not be giv­ing the fu­ture hu­mans any new in­for­ma­tion they hadn’t cre­ated, be­cause they would have to fake that in­for­ma­tion. They wouldn’t learn any­thing. It is pos­si­ble to fool hu­mans in that way, but the only pos­si­ble use would be for the pur­pose of fool­ing some­one. And that would re­quire some se­ri­ous sadism. So there is a sce­nario in which hu­mans have the com­pu­ta­tional power and al­gorithms to make you live in a simu­la­tion you think is real, but have no rea­son to do so.

• The origi­nal hy­po­thet­i­cal was to cre­ate a simu­lated agent that merely fails to no­tice a gap. New in­for­ma­tion does not need to be added for this; in­for­ma­tion from around the gap merely needs to be av­er­aged out to cre­ate what ap­pears to be not-a-gap (much as hu­man sight doesn’t have a visi­ble hole in the blind spot).

Now, if the in­tent was to cover the gap with some­thing spe­cific, then your ar­gu­ment would ap­ply. If, how­ever, the in­tent is to sim­ply cover up the gap with the most eas­ily calcu­lated non-gap data, then it be­comes pos­si­ble to do so. (Note that it may still re­main pos­si­ble, in such cir­cum­stances, to dis­cover the gap in­di­rectly).

• Well, given that the al­ter­na­tive ebrownv was con­sid­er­ing was on­go­ing tin­ker­ing dur­ing run­time by a su­per­in­tel­li­gence, it’s not quite clear what my abil­ity to build such code has to do with any­thing.

There’s also a big differ­ence, even for a su­per­in­tel­li­gence, be­tween build­ing a sys­tem­at­i­cally de­luded ob­server, build­ing a sys­tem­at­i­cally de­luded high-pre­ci­sion ob­server, and build­ing a guaran­teed sys­tem­at­i­cally de­luded high-pre­ci­sion ob­server. I’m not sure more than the former is needed for the sce­nario ebrownv had in mind.

Sure, it might no­tice some­thing weird one in a mil­lion times, but one can prob­a­bly count on so­cial forces to pre­vent such anoma­lous per­cep­tions from be­ing taken too se­ri­ously, es­pe­cially if one patches the simu­la­tion promptly on the rare oc­ca­sions when it doesn’t.

• Most poe­ple dis­agree with the premise “Be­ing in a simu­la­tion is/​can be made to be in­dis­t­in­guish­able from re­al­ity from the point of view of the simulee.”

I am sur­prised to hear this. What is your ba­sis for claiming that this is the premise most peo­ple ob­ject to?

Also, if you are aware of or fa­mil­iar with this ob­jec­tion—would you mind ex­plain­ing the fol­low­ing ques­tions I have re­gard­ing it?

1. What rea­son is there to sus­pect that a simu­lated me would have a differ­ent/​dis­t­in­guish­able ex­pe­rience from real me?

2. What rea­son is there to sus­pect that if there were differ­ences be­tween simu­lated and real life, that a simu­lated life would be aware of those differ­ences? That is, even if it is dis­t­in­guish­able—I have only ex­pe­rienced one kind of life and can’t say if my to­tally dis­t­in­guish­able ex­pe­rience of life is that of a simu­lated life or a real one.

3. A magic su­per com­puter from the fu­ture will be able to simu­late one atom with ar­bi­trary ac­cu­racy—right? A su­per-enough com­puter will be able to simu­late many atoms in­ter­act­ing with ar­bi­trary ac­cu­racy. If this su­per com­puter is pre­cisely simu­lat­ing all the atoms of an empty room con­tain­ing a sin­gle hu­man be­ing (brain in­cluded). If this simu­la­tion is hap­pen­ing—how could the simu­lated be­ing pos­si­bly have a differ­ent ex­pe­rience than its real coun­ter­part in an empty room? Atom­i­cally speak­ing ev­ery­thing is iden­ti­cal.

Maybe ques­tions 1 and 3 are similar—but I’d ap­pre­ci­ate if you (or some­one else) could en­lighten me re­gard­ing these is­sues.

• What rea­son is there to sus­pect that a simu­lated me would have a differ­ent/​dis­t­in­guish­able ex­pe­rience from real me?

As some­one who has writ­ten lots of simu­la­tions, there are a few rea­sons.

1) The simu­la­tion de­liber­ately sim­plifies or changes some things from re­al­ity. At min­i­mum, when “noise” is re­quired an al­gorithm is used to gen­er­ate num­bers which have many of the prop­er­ties of ran­dom num­bers but a) are not in fact ran­dom, b) are usu­ally much more ac­cu­rately de­scribed by a par­tic­u­lar math­e­mat­i­cal dis­tri­bu­tion than would any mea­sure­ments of the ac­tual noise in the sys­tem be.

2) The simu­la­tion ac­ci­den­tally sim­plifies/​changes LOTS of things from re­al­ity. A brain simu­la­tion at the neu­ron level is likely to simu­late ob­served vari­a­tions us­ing a noise gen­er­a­tor, when these vari­a­tions arise from a) a ream of de­tailed mo­tions of in­di­vi­d­ual ions and b) quan­tum in­ter­ac­tions. The claim is gen­er­ally made that one can simu­late at a more and more de­tailed level AND GET TO THE ENDPOINT where the simu­la­tion is “perfect.” The get­ting to the end­point claim is not only un­proven, but highly sus­pect. At ev­ery level of physics we have in­ves­ti­gated so far, we have always found a deeper level. Fur­ther, the equa­tions of mo­tions at these deep­est lay­ers are not known in com­plete de­tail. So even if we can get to an end­point, we have no rea­son to be­lieve we have got­ten to the end­point in any given simu­la­tion. At some point, we are no longer com­pute bound, we are knowl­edge bound.

3) There is a great in­sight in soft­ware that “if it isn’t tested, its bro­ken.” How do you even test a supremely deep simu­la­tion of your­self? If there are fea­tures of your­self you are still learn­ing, you can’t test for them. Un­til you com­pre­hen­sievly com­pre­hend your­self, you can never know that a simu­la­tion was com­pre­hen­sively similar.

Even some­thing as sim­ple as a coin toss simu­la­tion is likely to be “wrong” in de­tail. Per­haps you know the coin toss you are ac­tu­ally simu­lat­ing has .500 or even .500000000 prob­a­bil­ity of giv­ing heads (where num­ber of ze­ros rep­re­sents ac­cu­racy to which you know it.) But what is your con­fi­dence that the true ex­pec­ta­tion is 0.5 with a google­plex ze­ros fol­low­ing (or 3^^3 ze­ros to pre­tend to try to fit in here) is the ex­per­i­men­tal fact? Even 64 ze­ros would be a bitch to prove. And what are the chances that your simu­la­tion gets a ’true ex­pec­ta­tion” of 0.5 with even 64 ze­ros af­ter it? With the coin toss, the var­i­ance might SEEM triv­ial, but con­sider the same un­cer­tainty in the hu­man. You need to pre­dict my next post keystroke for keystroke, which nec­es­sar­ily in­cludes a pre­dic­tion of whether I will eat an egg for break­fast or a bowel of ce­real be­cause the posts I read while eat­ing de­pend on that. And so on and so on.

My claim is that the ex­is­tence of an end­point in fi­nally get­ting the simu­la­tion com­plete is at best vastly be­yond our knowl­edge (and not in a com­pute bound way) and at worst sim­ply un­know­able for a ream of good rea­sons. My es­ti­mate of the prob­a­bil­ity that a simu­la­tion will ever be re­li­ably known is < 0.01%.

Now we may get to a much eas­ier place: good enough to con­vince oth­ers. That some­one can write a simu­la­tion of me that can­not be dis­t­in­guished from me by peo­ple who know me is a much lower bar than that the simu­lat­ino feels the same as me to it­self. To con­vince oth­ers, the simu­la­tion may not even have to be con­scious, for ex­am­ple. But you are go­ing to have to build your simu­la­tion in to a fat hu­man body good enough to fool my wife, and give it a va­ri­ety of ner­vous and per­son­al­ity di­s­or­ders that cause it to come up with digs that are deeply dis­turb­ing to her to do even that.

At some point, the com­pre­hen­sive difficulty of a prob­lem has to open the ques­tion: is it rea­son­able to sweep this un­der the rug by ap­peal­ing to an un­known fu­ture of much greater ca­pa­bil­ity than we have now, or is do­ing that a hu­man bias we may need to avoid?

• I think enough peo­ple are non-re­duc­tion­ist/​ma­te­ri­al­ist to have doubt about whether a simu­la­tion can be said to have ex­pe­riences. And we don’t ex­actly have demon­stra­tion of this at this time, do we? I mean, in the ex­am­ple cited, Cv­i­liza­tion PC games, there aren’t in­di­vi­d­u­als there to have ex­pe­riences (un­less one counts the ai which is run­ning the en­tire fac­tion), rather there are some blips in databases in­cre­ment­ing the num­ber of units here or there, or rais­ing the pop­u­la­tion from an ab­stract 6 to 7. I don’t think peo­ple will be able to take simu­la­tion the­ory se­ri­ously un­til they have per­sonal in­ter­ac­tion with a con­vinc­ing ai.

That’s prob­a­bly as much an an­swer as I can give for any of the quest­sions, other than that I don’t see why we can as­sume that magic su­per com­put­ers are plau­si­ble. Re­lated, I don’t know if I trust my in­tu­ition or rea­son­ing as to whether an in­finite simu­la­tion will re­sem­ble re­alty in ev­ery way (as­sum­ing the su­per­com­puter is run­ning equa­tions and databases, etc, rather than ac­tu­ally re­con­stuct­ing a uni­verse atom by atom or some­thing).

It feels like you’re ask­ing me to be­lieve that a map is the same as the ter­ri­tory if it is a good enough map. I know that’s just an anal­ogy, but I have a hard time com­pre­hend­ing the sen­tence that “re­al­ity is the solu­tion to/​ equa­tions and noth­ing more” (as op­posed to even “re­al­ity is pre­dictable by equa­tions”).

This is prob­a­bly not the LW ap­proved an­swer, but then, I did say most peo­ple and not most LW-ers.

• I don’t un­der­stand sub­jec­tive ex­pe­rience very well, so I don’t know if a simu­la­tion would have it. I know that an adult hu­man brain does, and I’m pretty sure a rock doesn’t, but there are other cases I’m much less cer­tain about. Mice, for ex­am­ple.

• Also, 2 seems to im­ply there’s a rea­son to do his­tor­i­cal simu­la­tions with­out the knowl­edge of the simulees, and to thus effec­tively have billions of sen­tient be­ings lead sub­op­ti­mal mis­er­able lives with­out their con­sent.

• If the pro­ject is gov­ern­ment-funded, and the gov­ern­ment is any con­ceiv­able di­rect de­scen­dent of our cur­rent forms of gov­ern­ment, then this seems like the de­fault re­sult.

When was the last time you didn’t hear a re­li­gious con­ser­va­tive claim “But they’re not re­ally al­ive, they’re just ma­chines, they don’t have a soul!” or some similar ar­gu­ment (or the short­hand “Who cares? They’re just robots, not liv­ing things.”) when­ever the sub­ject of re­verse ma­chine ethics (i.e. how we treat com­put­ers, robots and AIs and whether they should be happy or some­thing) came up?

• There’s already some effort be­ing done in that di­rec­tion. If sen­tient ex­trater­res­trial life­forms could at least be con­sid­ered le­gal an­i­mals, what of our own hu­man-made crea­tures?

I also don’t see the point of mak­ing his­tor­i­cal simu­la­tions of that kind in the first place. It strikes me as un­nec­es­sar­ily com­plex and costly.

Fi­nally, if we’ve reached that level of de­vel­op­ment so that vir­tual con­structs mis­take them­selves for con­scious, one would think hu­mans would have de­vel­oped their use as councelors, pets, com­pany, and so on, and would have come to value them as “more than ma­chines”, not be­cause it’s true, but be­cause they want it to be. We hu­mans have a lot of trou­ble fulfilling each other’s emo­tional needs, and, if ma­chines were able to do it bet­ter, we’d prob­a­bly re­fuse to ac­knowl­edge their love, af­fec­tion, es­teem, trust, and so on, as lies.

On the other hand, we might also want to be­lieve that they aren’t “real peo­ple” so that we can mi­suse, abuse and de­stroy them when­ever that’s con­ve­nient, like we used to do with slaves and pros­ti­tutes. It cer­tainly raises in­ter­est­ing ques­tions, and I can’t pre­sume to know enough about hu­man psy­chol­ogy (or fu­ture AI de­vel­op­ment) to con­fi­dently make a pre­dic­tion one way or an­other.

• vir­tual con­structs mis­take them­selves for conscious

My brain just folded in on it­self and van­ished. Or at least in simu­la­tion it did. I think you may have stated a basilisk, or at least one that works on my self-simu­la­tion.

I used to think I was con­scious, but then I re­al­ized I was mis­taken.

Who­ever it was that said “I err, there­fore I am” didn’t know what he was talk­ing about… be­cause he was wrong in think­ing he was even con­scious!

• I used to won­der what con­scious­ness could be, un­til you all shared its qualia with me.

You know, we could sim­ply ask; “What would con­vince us that the simu­lated hu­mans are not con­scious?” “What would con­vince us that we our­selves are not con­scious?” Be­cause, oth­er­wise, “un­con­scious ho­mun­culi” are ba­si­cally the same as P-Zom­bies, and we’re mak­ing a use­less dis­tinc­tion.

Nev­er­the­less, it is pos­si­ble for a ma­chine to be mis­taken about be­ing con­scious. Make it un-con­scious (in some mean­ingful way), but make it un­able to dis­t­in­guish con­scious from un­con­scious, and bias its judg­ment to­wards qual­ify­ing it­self as con­scious. Ba­si­cally, the “mis­take” would be in its defi­ni­tion of con­scious­ness.

• I used to think I was con­scious, but then I re­al­ized I was mis­taken.

Den­nett ac­tu­ally be­lieves some­ht­ing like that about phe­nom­e­nal con­scious­ness.

[Den­nett:] Th­ese ad­di­tions are perfectly real, but they are … not made of fig­ment, but made of judg­ment. There is noth­ing more to phe­nomenol­ogy than that [Otto:] But there seems to be! [Den­nett:] Ex­actly! There seems to be phe­nomenol­ogy. That’s a fact that the het­erophe­nome­nol­o­gist en­thu­si­as­ti­cally con­cedes. But it does not fol­low from this un­de­ni­able, uni­ver­sally at­tested fact thatth ere re­ally is phe­nomenol­ogy. This is the crux. (Den­nett, 1991, p. 366)

• Er… can I get the cliff’s notes on the jar­gon here?

• (nods) There’s an amus­ing bit in a John Var­ley novel along these lines, where our hero asks a cut­ting-edge su­per­com­puter AI whether it’s gen­uinely con­scious, and it replies some­thing like “I’ve been ex­plor­ing that ques­tion for a long time, and I’m still not cer­tain. My cur­rent work­ing the­ory is that no, I’m not—nor are you, in­ci­den­tally—but I am not yet con­fi­dent of that.” Our hero thinks about that an­swer for a while and then takes a nap, IIRC.

• I also don’t see the point of mak­ing his­tor­i­cal simu­la­tions of that kind in the first place. It strikes me as un­nec­es­sar­ily com­plex and costly.

Cal­ibra­tion test: How many poli­cies that have been en­forced by gov­ern­ments wor­ld­wide would you have made the same claim for? How many are cur­rently still be­ing en­forced? How many are cur­rently in plan­ning/​dis­cus­sion/​vot­ing/​etc. but not yet im­ple­mented?

In my own, not see­ing the point and this be­ing un­nec­es­sar­ily com­plex and costly, com­bined with the fact that it’s some­thing peo­ple dis­cuss as op­posed to any ran­dom other pos­si­ble hy­poth­e­sis, makes it just as valid a can­di­date for gov­ern­ment sig­nal­ing and sta­tus-gam­ing as many other types of poli­cies.

How­ever, to clar­ify my own po­si­tion: I agree that the sec­ond premise im­plies some sort of mo­tive for run­ning such a simu­la­tion with­out car­ing for the lives of the minds in­side it, but I just don’t think that the part about hav­ing billions of “merely simu­lated” mis­er­able lives would be of much con­cern to most peo­ple with a mo­tive to do it in the first place.

As ev­i­dence, I’ll point to the many naive an­swers to coun­ter­fac­tual mug­gings of the form “If you don’t give me 100\$ I’ll run a trillion simu­lated copies of you and tor­ture them im­mensely for billions of sub­jec­tive years.” “Yeah, so what? They’re just simu­la­tions, not real peo­ple.”

It cer­tainly raises in­ter­est­ing ques­tions, and I can’t pre­sume to know enough about hu­man psy­chol­ogy (or fu­ture AI de­vel­op­ment) to con­fi­dently make a pre­dic­tion one way or an­other.

I’d be care­ful here about con­strain­ing your thoughts to “Either mag­i­cal tiny green buck-toothed AK47-wield­ing gob­lins yel­ling ‘Wa­zooomba’ ex­ist, or they don’t, right? So it’s about 50-50 that they do.” I’m not quite sure if there even is any schel­ling point in-be­tween.

• I can’t say that any policy comes to mind at this point. In my coun­try the norm has always been to claim for more gov­ern­ment in­ter­ven­tion and higher di­rect taxes, not less. If any­thing, I find gov­ern­ment spend­ing cuts are the ones that tend to be ir­ra­tionally im­ple­mented and make a mess of perfectly ser­vice­able ser­vices, and I always see those as a threat. The pri­vate sec­tor is the one in charge of frivoli­ties, lux­u­ries and un­nec­es­sary stuff that peo­ple still want to spend money on, as long as it isn’t pub­lic dimes. [I’ve been down­voted over ex­press­ing this kind of opinion in the past; if you have differ­ent opinions that con­sider these to be blatantly stupid, I’ll still humbly re­quest that you re­frain from do­ing that. Please.].

It’s only some­thing peo­ple dis­cuss be­cause, as far as I can tell from the su­perfi­cial data I’ve col­lected so far, some in­tel­lec­tual hip­ster de­cided it would be amus­ing to pose a dis­turb­ing and un­falsifi­able hy­poth­e­sis, and see how peo­ple re­acted to it and ar­gued against it. As far as I’m con­cerned, un­til there’s any ev­i­dence at all that this re­al­ity is not the origi­nal, it sim­ply doesn’t make sense to pro­mote the hy­poth­e­sis to our at­ten­tion.

That coun­ter­fac­tual mug­ging would at least give me pause. Though I think my re­sponse would be more long the lines of at­tempt­ing pre-emp­tive use of po­ten­tially lethal force than sim­ply pay­ing the bribe. That sort of dan­ger­ous, geno­ci­dal mad­man shouldn’t be al­lowed ac­cess to a com­puter.

I didn’t im­ply that there are only two ways this can go, but the hy­poth­e­sis space and the state of cur­rent ev­i­dence is such that I can’t see any spe­cific hy­poth­e­sis be­ing pro­moted to my at­ten­tion, so I’m stick­ing with the de­fault “this is the origi­nal re­al­ity” un­til ev­i­dence shows up to make me con­sider oth­er­wise.

• I’d be care­ful here about con­strain­ing your thoughts to “Either mag­i­cal tiny green buck-toothed AK47-wield­ing gob­lins yel­ling ‘Wa­zooomba’ ex­ist, or they don’t, right? So it’s about 50-50 that they do.” I’m not quite sure if there even is any schel­ling point in-be­tween.

Com­plex­ity-based pri­ors solve that prob­lem. Mag­i­cal tiny green buck-toothed AK47-wield­ing gob­lins yel­ling ‘Wa­zooomba’ are com­plex, so, in the ab­sence of ev­i­dence that they do ex­ist, you’re jus­tified in con­clud­ing that they don’t. ;)

• I can at­test by spot-check­ing for small N that even most math­e­mat­i­ci­ans have not been ex­posed to this idea.

I can tes­tify that in differ­en­tial ge­om­e­try, al­most no­body knows this idea (I cer­tainly didn’t back in that part of my ca­reer). But also no­body re­ally thought as proofs as mean­ingless sym­bol ma­nipu­la­tions; the mod­els in ge­om­e­try are so in­tu­itively vivid, it feels you are ac­tu­ally ex­plor­ing a real pla­tonic realm.

(that’s why I found logic so hard: you had to fol­low the proofs, and in­tu­ition wasn’t re­li­able)

• Be­fore I read the rest of the post, I’d like to note that those pic­tures are adorable. I sincerely hope we’ll be see­ing more an­i­mal car­toons like that in the fu­ture.

• (Au­di­atur et al­tera pars is the im­pres­sive Latin name of the prin­ci­ple that you should clearly state your premises.)

That’s not what I thought it means. My un­der­stand­ing was that it’s some­thing like: “all par­ties should be heard”, and it’s more of a le­gal thing…

http://​​en.wikipe­dia.org/​​wiki/​​Audi_al­teram_partem

• I’m not an ex­pert at Latin, but from what I can tell the vast ma­jor­ity of re­sources on the in­ter­net side with Klao’s in­ter­pre­ta­tion, and its Google trans­la­tion seems much closer to the wikipe­dia ver­sion.

• Mmkay. Page up­dated.

• Your ac­count of “proof” is not ac­tu­ally an al­ter­na­tive to the “proofs are so­cial con­structs” de­scrip­tion, since these are ad­dress­ing two differ­ent as­pects of proof. You have fo­cused on the stan­dard math­e­mat­i­cal model of proofs, but there is a sep­a­rate so­ciolog­i­cal ac­count of how pro­fes­sional math­e­mat­i­ci­ans prove things.

Here is an ex­am­ple of the lat­ter from Thurston’s “On Proof and Progress in Math­e­mat­ics.”

When I started as a grad­u­ate stu­dent at Berkeley, I had trou­ble imag­in­ing how I could “prove” a new and in­ter­est­ing math­e­mat­i­cal the­o­rem. I didn’t re­ally un­der­stand what a “proof” was.

By go­ing to sem­i­nars, read­ing pa­pers, and talk­ing to other grad­u­ate stu­dents, I grad­u­ally be­gan to catch on. Within any field, there are cer­tain the­o­rems and cer­tain tech­niques that are gen­er­ally known and gen­er­ally ac­cepted. When you write a pa­per, you re­fer to these with­out proof. You look at other pa­pers in the field, and you see what facts they quote with­out proof, and what they cite in their bibliog­ra­phy. You learn from other peo­ple some idea of the proofs. Then you’re free to quote the same the­o­rem and cite the same cita­tions. You don’t nec­es­sar­ily have to read the full pa­pers or books that are in your bibliog­ra­phy. Many of the things that are gen­er­ally known are things for which there may be no known writ­ten source. As long as peo­ple in the field are com­fortable that the idea works, it doesn’t need to have a for­mal writ­ten source.

At first I was highly sus­pi­cious of this pro­cess. I would doubt whether a cer­tain idea was re­ally es­tab­lished. But I found that I could ask peo­ple, and they could pro­duce ex­pla­na­tions and proofs, or else re­fer me to other peo­ple or to writ­ten sources that would give ex­pla­na­tions and proofs. There were pub­lished the­o­rems that were gen­er­ally known to be false, or where the proofs were gen­er­ally known to be in­com­plete. Math­e­mat­i­cal knowl­edge and un­der­stand­ing were em­bed­ded in the minds and in the so­cial fabric of the com­mu­nity of peo­ple think­ing about a par­tic­u­lar topic. This knowl­edge was sup­ported by writ­ten doc­u­ments, but the writ­ten doc­u­ments were not re­ally pri­mary.

I think this pat­tern varies quite a bit from field to field. I was in­ter­ested in ge­o­met­ric ar­eas of math­e­mat­ics, where it is of­ten pretty hard to have a doc­u­ment that re­flects well the way peo­ple ac­tu­ally think. In more alge­braic or sym­bolic fields, this is not nec­es­sar­ily so, and I have the im­pres­sion that in some ar­eas doc­u­ments are much closer to car­ry­ing the life of the field. But in any field, there is a strong so­cial stan­dard of val­idity and truth. …

• The great virtue of valid logic in ar­gu­ment, rather, is that log­i­cal ar­gu­ment ex­poses premises, so that any­one who dis­agrees with your con­clu­sion has to (a) point out a premise they dis­agree with or (b) point out an in­valid step in rea­son­ing which is strongly li­able to gen­er­ate false state­ments from true state­ments.

This is false as a de­scrip­tion of how math­e­mat­ics is done in prac­tice. If I am con­fronted with a pur­ported the­o­rem and a messy com­pli­cated “proof”, there are ways I can re­fute it with­out ei­ther challeng­ing a premise or a spe­cific step.

• If I find a coun­terex­am­ple to the claimed the­o­rem, read­ers prob­a­bly won’t need to dive into the proof to find a spe­cific mis­step.

• if the the­o­rem con­tra­dicts some well-es­tab­lished re­sult, it’s prob­a­bly wrong. (This is closely re­lated to the above)

• If a pur­ported proof falls into a pat­tern of proof that is known not to work, that is also suffi­cient grounds for ra­tio­nally dis­miss­ing it. (This came up dur­ing the dis­cus­sion of Vi­nay De­o­lal­ikar’s pur­ported P != NP proof—most of the pro­fes­sion­als were ex­tremely skep­ti­cal once it be­came clear that the proof didn’t seem to evade the known limi­ta­tions of so-called nat­u­ral proofs.)

• I will re­mark, in some hor­ror and ex­as­per­a­tion with the mod­ern ed­u­ca­tional sys­tem, that I do not re­call any math-book of my youth ever once ex­plain­ing that the rea­son why you are always al­lowed to add 1 to both sides of an equa­tion is that it is a kind of step which always pro­duces true equa­tions from true equa­tions.

Would the av­er­age 9-year old be able to un­der­stand such a math book? (For that mat­ter, would the av­er­age teacher of 9-year-olds?)

• http://​​www.wired.com/​​geek­dad/​​2012/​​06/​​drag­onbox/​​all/​​ Well, Dragon Box sug­gests that a five year old can get at least the ba­sic idea, so I’d deeply hope a 9 year old could grasp it more ex­plic­itly.

• As I un­der­stand the ar­ti­cle, the game pri­mar­ily teaches how the rules can be used to solve for some­thing and sec­on­dar­ily it teaches the rules. It doesn’t seem to teach at all why the rules are the way they are. That’s ac­tu­ally, IMHO, the biggest is­sue with the game.

• Yes and no, re­spec­tively.

• It seems like a fairly sim­ple no­tion. So my pre­dic­tion is yes.

• My pre­dic­tion to the first one is yes, if they are also taught the right pre­req­ui­sites. My pre­dic­tion to the lat­ter is strongly no. They have too much at stake to change their ways that much.

• What is a valid proof in alge­bra? It’s a proof where, in each step, we do some­thing that is uni­ver­sally al­lowed, some­thing which can only pro­duce true equa­tions from true equa­tions, and so the proof grad­u­ally trans­forms the start­ing equa­tion into a fi­nal equa­tion which must be true if the start­ing equa­tion was true. Each step should also—this is part of what makes proofs use­ful in rea­son­ing—be lo­cally ver­ifi­able as al­lowed, by look­ing at only a small num­ber of pre­vi­ous points, not the en­tire past his­tory of the proof.

Note that this doesn’t re­ally solve the same prob­lem that the quotes in the in­tro­duc­tion are try­ing to solve. Proofs need to be valid and con­vinc­ing. The ‘valid’ part is ex­plained in the above. But the defi­ni­tion of the ‘con­vinc­ing’ part is hid­den in the phrase ‘lo­cally ver­ifi­able’. It is not clear what lo­cally ver­ifi­able means, so this sim­ply leaves open that part of the defi­ni­tion.

Put differ­ently, you could still define

lo­cally ver­ifi­ablethe math­e­mat­i­ci­ans who read it can cor­rectly as­sess whether this step is valid

which is the so­cial ap­proach; or

lo­cally ver­ifi­able the math­e­mat­i­cian who wrote it is ca­pa­ble of trans­form­ing the step into a se­quence of steps that are valid ac­cord­ing to a for­mal proof system

which is ar­guably the proper ver­sion of the sym­bolic ap­proach. Both would fit with the ex­pla­na­tion above.

(I’m not claiming that leav­ing this part open makes it a worth­less defi­ni­tion, just that it can’t be fairly com­pared to the open­ing quotes, as those are, in fact, try­ing to define the con­vinc­ing part. They’re at­tempts (not nec­es­sar­ily good ones) at solv­ing a strictly harder prob­lem.)

• I will re­mark, in some hor­ror and ex­as­per­a­tion with the mod­ern ed­u­ca­tional sys­tem, that I do not re­call any math-book of my youth ever once ex­plain­ing that the rea­son why you are always al­lowed to add 1 to both sides of an equa­tion is that it is a kind of step which always pro­duces true equa­tions from true equa­tions.

I had a similar ex­pe­rience. When I took Alge­bra I, I un­der­stood that you could add, sub­tract, mul­ti­ply, and di­vide (non-zero) some value to both sides of the equa­tion and it would still be true. I re­mem­ber at one point I was work­ing on solv­ing an equa­tion that re­quired tak­ing the square root of both sides, and I won­dered, “Are you al­lowed to do that?”

It wasn’t un­til years later that I figured it out: you’re al­lowed to perform any func­tion on both sides of the equa­tion, be­cause both sides rep­re­sent the same value. For any func­tion, if a = b, f(a) = f(b).

In this con­text, you’re not al­lowed to di­vide by 0 be­cause di­vi­sion by 0 is not a func­tion. Mul­ti­pli­ca­tion by zero is a func­tion, but ev­ery real in­put maps to an out­put of 0; the func­tion is not a one-to-one func­tion, and thus not in­vert­ible.

• I re­mem­ber at one point I was work­ing on solv­ing an equa­tion that re­quired tak­ing the square root of both sides, and I won­dered, “Are you al­lowed to do that?”

Yes, but you have to watch out, be­cause of the an­noy­ing fact that sqrt(x^2) doesn’t equal x when x is nega­tive. It’s easy to look at x^2 = y, “take the square root of both sides”, and end up with x = sqrt(y) with­out re­al­iz­ing that you left out a step that is not always truth-pre­serv­ing.

• Strictly speak­ing, “take the square root of both sides” is not always a truth-pre­serv­ing op­er­a­tion, so you should re­ally use “take the +/​- square root of both sides” in­stead.

• “Take the square root of both sides” is always a truth-pre­serv­ing op­er­a­tion, but sub­se­quently sim­plify­ing sqrt(x^2) to x is not.

So when you take the square root of both sides in, e.g., x^2=25, you re­ally get sqrt(x^2)=5. Sim­plify­ing that to x=5 is where you lose gen­er­al­ity.

• sqrt(x^2)=5 or −5, along with an in­finite num­ber of com­plex val­ues.

• sqrt(x^2)=5 or −5, along with an in­finite num­ber of com­plex values

No. Even in the com­plex plane there are only two pos­si­ble square roots. More­over, if one wants to sqrt to be a func­tion one needs a con­ven­tion, hence we definite sqrt to be the non-nega­tive square root when it ex­ists.

• You could define sqrt as a multi-val­ued func­tion, in which case, when you ap­ply it to x^2 = 25, you will get +/​-x = +/​-5, but you don’t have to. We can take the pos­i­tive square root (which is what peo­ple usu­ally mean) and get sqrt(x^2)=sqrt(25)=5, and the op­er­a­tion is truth-pre­serv­ing. sqrt(x^2) then sim­plifies to |x|.

Com­plex num­bers are a bit trick­ier, but you don’t get “an in­finite num­ber of com­plex val­ues”. Even over the com­plex num­bers, the only square roots of 25 are 5 and −5. In gen­eral, there are two pos­si­ble square roots, and the pop­u­lar one to take is the one with pos­i­tive real part. So ev­ery­thing I said above is still true, ex­cept sqrt(x^2) doesn’t sim­plify nicely—it’s no longer equal to |x|. So when you take square roots of com­plex num­bers it’s prob­a­bly bet­ter to go the multi-val­ued func­tion ap­proach with the +/​-.

• Squar­ing is not truth-pre­serv­ing (Although I think rais­ing to any power not an even num­ber is, at least for real num­bers). Why would even roots be truth-pre­serv­ing?

• What? For any func­tion f, if x=y, then f(x) = f(y). Squar­ing is a func­tion. Do you mean some­thing else by truth-pre­serv­ing?

Squar­ing can in­tro­duce truth into a false­hood. For ex­am­ple, if we write −5 = 5, that’s false, but we square both sides and get 25=25, and that’s true. Fur­ther­more, squar­ing doesn’t pre­serve the truth of an in­equal­ity: −5 < 3, but 25 > 9.

• Ah- if you don’t define the (prin­ci­ple) square root to be the in­verse of squar­ing, the ap­par­ent con­tra­dic­tion goes away.

I con­cluded that you wanted to be able to pre­serve false­hood as well. Squar­ing pre­serves false­hood in the do­main of the non­nega­tive re­als, ex­actly like mul­ti­pli­ca­tion and di­vi­sion by pos­i­tive val­ues does.

• The great virtue of valid logic in ar­gu­ment, rather, is that log­i­cal ar­gu­ment ex­poses premises, so that any­one who dis­agrees with your con­clu­sion has to (a) point out a premise they dis­agree with or (b) point out an in­valid step in rea­son­ing which is strongly li­able to gen­er­ate false state­ments from true state­ments.

Fur­ther to that, there is an ad­van­tage to the maker of an ar­gu­ment, in that they have to make ex­plicit as­sump­tions they may not have re­al­ised they were mak­ing. Speak­ing of imo­plicit as­sump­tions...

For ex­am­ple: Nick Bostrom put forth the Si­mu­la­tion Ar­gu­ment, which is that you must dis­agree with ei­ther state­ment (1) or (2) or else agree with state­ment (3):

(1) Earth-origi­nat­ing in­tel­li­gent life will, in the fu­ture, ac­quire vastly greater com­put­ing re­sources.

(2) Some of these com­put­ing re­sources will be used to run many simu­la­tions of an­cient Earth, aka “an­ces­tor simu­la­tions”.

(3) We are al­most cer­tainly liv­ing in a com­puter simu­la­tion.

(3) is not en­tailed by the con­junc­tion of (1) and (2). You also need to as­sume some­thing like “the kind of con­scious­ness we have is com­pu­ta­tion­ally simu­la­ble”. If that is false, no amount of com­put­ing power will make the ar­gu­ment work.

• Law of Iden­tity. If you “perfectly simu­late” An­cient Earth, you’ve in­vented a time ma­chine and this is the ac­tual An­cient Earth.

If there’s some differ­ence, then what you’re simu­lat­ing isn’t ac­tu­ally An­cient Earth, and in­stead your com­puter hard­ware is liter­ally the god of a uni­verse you’ve cre­ated, which is a fact about our uni­verse we could de­tect.

• A simu­la­tion con­sists of an in­ner part that is be­ing simu­lated and an outer part that is do­ing the simu­lat­ing. How­ever perfect the in­ner part is, it is not the same as the his­toric event be­cause the his­toric event did not have the outer part. There is also the is­sue that in some cases a thing’s his­tory is taken to be part of it iden­tity. A perfect replica of the Mona Lisa cre­ated in a lab­o­ra­tory would not be the Mona Lisa, since part of the iden­tity of The Mona Lisa is its hav­ing been painted by Leonardo.

• How­ever perfect the in­ner part is, it is not the same as the his­toric event be­cause the his­toric event did not have the outer part.

False. The outer part is ir­rele­vant to the in­ner part in a perfect simu­la­tion. The outer part can ex­ert no causal in­fluence, or you won’t get a perfect re­ply of the origi­nal event’s pre­sumed lack of outer part.

There is also the is­sue that in some cases a thing’s his­tory is taken to be part of it iden­tity.

A thing’s his­tory causes it. If you aren’t simu­lat­ing it prop­erly, that’s your prob­lem. A perfect simu­la­tion of the Mona Lisa was in fact painted by Leonardo, prov­able in all the same ways you claim the origi­nal was.

• False. The outer part is ir­rele­vant to the in­ner part in a perfect simu­la­tion.

You can­not claim that such a perfect simu­la­tion liteally just is go­ing back in time, be­cause back in time there was no outer part. The claim is du­bi­ous for other rea­sons.

The outer part can ex­ert no causal in­fluence, or you won’t get a perfect re­ply of the origi­nal event’s pre­sumed lack of outer part.

The outer part can ex­ert what­ever in­fluence it likes, so long as it is no de­tectable from within. A com­puter must “in­fluence” the pro­gramme it is run­ning, even if the pogramme can­not tell how deeply nested in simu­la­tion it is .

. A perfect simu­la­tion of the Mona Lisa was in fact painted by Leonardo, prov­able in all the same ways you claim the origi­nal was.

A perfect simu­la­tion of the ML was in fact simu­lated and not painted by Leonardo. Sup­pose some­one made a perfect copy and took it into the Lou­vre in the mid­dle of the night. Then they walk out..with a ML un­der their arm. We don’t know whether or not they have been swapped. We would not then say there are two origi­nal ML’s , we would say there are two ver­sions of the ML, one of which si the real one,, but we don’t know which.

• You can­not claim that such a perfect simu­la­tion liteally just is go­ing back in time, be­cause back in time there was no outer part.

You’re not jus­tified in as­sert­ing that, for the same rea­son that your copy in a (cor­rect, ac­cu­rate) simu­la­tion of the mo­ment when you wrote the com­ment would not be jus­tified in as­sert­ing it. You can’t tell there’s no outer part of the uni­verse, be­cause if you could then it would be a part of the uni­verse. Your simu­la­tion can’t tell there’s no outer part to its (simu­lated) uni­verse, be­cause then the simu­la­tion wouldn’t be cor­rect and ac­cu­rate.

There are tur­tles all the way down.

• I am jus­tified in as­sert­ing that simu­la­tion is not, in prin­ci­ple, time travel. I may not be jus­tifieid in as­sert­ing that I am not cur­rently in a simu­la­tion. That is a differ­ent is­sue.

• How­ever perfect the in­ner part is, it is not the same as the his­toric event be­cause the his­toric event did not have the outer part.

False. The outer part is ir­rele­vant to the in­ner part in a perfect simu­la­tion.

You can­not claim that such a perfect simu­la­tion liter­ally just is go­ing back in time, be­cause back in time there was no outer part.

I am jus­tified in as­sert­ing that simu­la­tion is not, in prin­ci­ple, time travel.

You are of course right about this state­ment. It’s not time travel (for “nor­mal” defi­ni­tions of time travel), since no­body ac­tu­ally trav­eled through time within one of the uni­verses.

But the pre­cise claim seems to me to have shifted be­tween an­swers, or at least the way we in­ter­preted them did at each step.

With re­spect to whether or not the simu­lated event is the same as the past event in the uni­verse host­ing the simu­la­tion, I’d say the mat­ters are less clear. First, the ques­tion is some­what un­clear: nei­ther the simu­lated par­ti­ci­pants nor the his­tor­i­cal ones can tell if there’s a out­side uni­verse simu­lat­ing their own’s. So the ques­tion is not quite counter-fac­tual, but nei­ther is it about a known (or even know­able) fact. For both the simu­lated and the his­tor­i­cal ob­servers, the pres­ence or ab­sence of an ex­ter­nal uni­verse is perfectly hy­po­thet­i­cal (or perfectly non-testable, as­sum­ing a perfect-enough simu­la­tion).

Any “prop­erty” of the events (the his­tor­i­cal and the simu­lated one) that can be com­pared will give the an­swer “equal”. You (the “real” you) can’t say, for ex­am­ple, “there is an out­side-simu­lated-uni­verse ob­server of the simu­lated event, but there was no out­side-his­tor­i­cal-uni­verse ob­server of the his­tor­i­cal event, so the two events are dis­tinct”, be­cause you can’t (by the as­sump­tion that the simu­la­tion was perfect enough) have any ev­i­dence in fa­vor of the em­pha­sized part of the state­ment.

I think this is some­thing similar to that be­tween clas­si­cal and con­struc­tivist logic. That is, the an­swer de­pends on if your defi­ni­tion of same­ness (“same events” in this case) is that

a) Every prop­erty can be shown to be iden­ti­cal, or

b) No prop­erty can be shown to be dis­tinct.

If it’s (a), then you can’t jus­tify say­ing that the two events are not the same, nor can you jus­tify say­ing that they are the same, be­cause there are prop­er­ties that can­not be com­pared, so you can’t find out if they’re the same.

If it’s (b), then it fol­lows from the as­sump­tions that the two events are the same. (I take “How­ever perfect the in­ner part is” to mean that it could be perfect enough that no ob­ser­va­tion made in the simu­lated uni­verse is (or even the stronger ver­sion, could be) able to give in­for­ma­tion about the simu­lat­ing uni­verse’s pres­ence.)

In the (b) case, note that (the his­tor­i­cal) you can’t use your knowl­edge of the simu­la­tion to get around this. If the simu­la­tion is run for long enough, it will it­self con­tain in its fu­ture a you simu­lat­ing its own his­tory, etc. Even if you stop the simu­la­tion be­fore it reaches that point, you can’t claim that its timeline is shorter than yours, be­cause it might be restarted in your fu­ture (and po­ten­tially catch up).

Of course, you can run a perfect simu­la­tion of an event and then in­ter­vene in the simu­la­tion in a way you re­mem­ber to be differ­ent from your past. But I don’t know if you can de­sign a change that would not re­quire you to run the simu­la­tion in­finitely long, so as to make sure its fu­ture doesn’t con­tain some­one like you (i.e., that there’s no weird con­se­quence of your change that leads to a simu­lated you that has the same mem­o­ries as the his­tor­i­cal you at the point when you made the simu­la­tion di­verge, be­cause he doesn’t re­mem­ber his his­tory cor­rectly). Even if you turn the simu­la­tion off, I think that as long as you re­mem­ber enough about it to be jus­tified in mak­ing this kind of claims about it, it could be restarted in your fu­ture.

• With re­spect to whether or not the simu­lated event is the same as the past event in the uni­verse host­ing the simu­la­tion, I’d say the mat­ters are less clear.

I think it is clear enough. “Is” us­ally means “is ob­jec­tively”, not “ap­pears to be so from the per­spec­tive of a sub­ject”. It has been stipu­lated that there is a state of the uni­vere S1 fol­lowed by a sub­se­quent state S2 that in­cludes a simu­la­tion of the state S1. That is enough to show, not only that no travel has oc­cured, but that the state of the uni­verse S1 has not been recre­ated be­cause the state of the uni­verse at T2 is S2 and S2 =/​= S1.

First, the ques­tion is some­what un­clear: nei­ther the simu­lated par­ti­ci­pants nor the his­tor­i­cal ones can tell if there’s a out­side uni­verse simu­lat­ing their own’s.

That in­volves a shift from what is go­ing on to what seems to be.

So the ques­tion is not quite counter-fac­tual, but nei­ther is it about a known (or even know­able) fact.

The origi­nal sce­nario sim­ply stipu­lated that cer­tain things were hap­pen­ing, so where does knowa­biliy come in?

Any “prop­erty” of the events (the his­tor­i­cal and the simu­lated one) that can be com­pared will give the an­swer “equal”.

But that is ir­rele­vant, be­cause the origi­nal sce­nario stipu­lates that they are not.

• With re­spect to whether or not the simu­lated event is the same as the past event in the uni­verse host­ing the simu­la­tion, I’d say the mat­ters are less clear.

I think it is clear enough. “Is” us­ally means “is ob­jec­tively”, not “ap­pears to be so from the per­spec­tive of a sub­ject”. It has been stipu­lated that there is a state of the uni­vere S1 fol­lowed by a sub­se­quent state S2 that in­cludes a simu­la­tion of the state S1. That is enough to show, not only that no travel has oc­cured, but that the state of the uni­verse S1 has not been recre­ated be­cause the state of the uni­verse at T2 is S2 and S2 =/​= S1.

(Em­pha­sis mine.)

I think that is the root of our dis­agree­ment. I don’t think you’re sup­posed to just ac­cept the “usual” mean­ing of the word “is” when you’re dis­cussing un­usual situ­a­tions, and in this par­tic­u­lar case I thought we were do­ing just that. (I.e., I thought we were us­ing an un­usual sce­nario to ex­plore the pos­si­ble mean­ings of “equal­ity”, rather than us­ing a cer­tain mean­ing of “equal­ity” to ex­plore an un­usual sce­nario. That was just my thought, I don’t mean you’re wrong if you were ar­gu­ing a differ­ent is­sue, just that we failed to agree what we are talk­ing about.)

My read­ing of the origi­nal sce­nario agrees with the ital­i­cised part of your sum­mary, but not the rest. My claim is not that S2 equals S1, but that the simu­la­tion of S1 con­tained in S2 (call it S1b), could con­tain an event (call it Eb) that is equal with an event E con­tained in S1 that pre­cedes the run­ning of S2, for some use­ful defi­ni­tions of “equal” and choices of E. Note that the origi­nal sce­nario doesn’t say that there is no S0 in which S1 is a simu­la­tion.

(I also sug­gested the stronger claim that, given a good enough simu­la­tion, it could also be pos­si­ble for S1b to ac­tu­ally equal S1, though our uni­verse might not al­low the cre­ation of a “good enough” simu­la­tion. Or, more pre­cisely, that there are use­ful mean­ings of “equal­ity” that al­low such sce­nar­ios, and even that there might not be a con­sis­tent mean­ing for “equal” that don’t al­low this in any pos­si­ble uni­verse.)

I think the root of your dis­agree­ment is an un­stated as­sump­tion that “Sy fol­lows (in time) Sx” im­plies “Sy =/​= Sx”. That is usu­ally true, but I don’t think it should be ac­cepted with­out jus­tifi­ca­tion in un­usual cases, such as those con­tain­ing time loops or (al­most-)perfect simu­la­tions (which could mean the same thing for some kinds of uni­verses).

• for some use­ful defi­ni­tions of “equal”

But what’s the mileage in the claim that you have an ap­prox­i­mate re­pro­ducion of a mo­ment in time? A bat­tel re-enac­ment or his­tor­i­cal move would cound for some val­ues of “ap­prox­i­mate”. That’s a long way from time travel.

I think the root of your dis­agree­ment is an un­stated as­sump­tion that “Sy fol­lows (in time) Sx” im­plies “Sy =/​= Sx”. That is usu­ally true,

If you are say­ing Sx and Sy are uni­ver­sal states, then you would need a simu­la­tor that some­how sac­ri­fices it­self to in gen­er­at­ing the simu­lated state.

• If you are a simu­la­tion, then the kind of con­scious­ness you think you have is by defi­ni­tion simu­la­ble. Right down to your simu­lated scep­ti­cism that it is pos­si­ble.

But it doesn’t have to be simu­la­ble from within the simu­la­tion...

• If you are a simu­la­tion, then the kind of con­scious­ness you think you have is by defi­ni­tion simu­la­ble. Right down to your simu­lated scep­ti­cism that it is pos­si­ble.

My dis­agree­ments with (3) are that (1) is not cer­tain to im­ply suffi­cient com­put­ing re­sources for such a pro­ject, and (2) is pure spec­u­la­tion not sup­ported by com­pel­ling rea­sons for our de­scen­dants to do it.

I agree that if (1) is true to the ex­tent that such enor­mous re­sources were available and not needed for any­thing more im­por­tant, and (2) is true to the ex­tent that > 10^6 such to­tal plane­tary simu­la­tions were car­ried out, then that would qual­ify for (3) be­ing true as stated. ( 1.0 − 1.0e-6 is ac­cept­able for me as “al­most cer­tainly”). I just think the premises are bul­lshit, that’s all.

• Note that a proper simu­la­tion in step (2) would in­clude a num­ber of simu­la­tions of simu­la­tions, and each of those would in­clude a num­ber of simu­la­tions of simu­la­tions of simu­la­tions. It’s not merely the num­ber of simu­la­tions that the base-re­al­ity does that’s im­por­tant; it’s also the num­ber of lay­ers of simu­la­tion within that.

For ex­am­ple, with only three lay­ers of simu­la­tion, if each hu­man­ity (simu­lated or not) at­tempts to simu­late its own past just 100 times, then that will re­sult in 10^6 third-layer simu­la­tions (1010100 simu­la­tions al­to­gether).

• The prob­lem with re­cur­sive simu­la­tions is that the amount of available com­pu­tro­n­ium de­creases ex­po­nen­tially with level.

• If you are a simu­la­tion, then the kind of con­scious­ness you think you have is by defi­ni­tion simu­la­ble. Right down to your simu­lated scep­ti­cism that it is pos­si­ble.

But one can’t as­sume that is the case in or­der to prove the premise.

• Nor can you as­sume that is not the case to ar­gue against be­ing in­side a simu­la­tion. Spec­u­la­tions about whether con­scious­ness can be simu­lated are no help ei­ther way. If you’re be­ing simu­lated you don’t have any base re­al­ity to perform ex­per­i­ments on to de­cide what things are true. You don’t even have a testable model of what you might be be­ing simu­lated on.

So, de­cid­ing be­tween two log­i­cally con­sis­tent but in­com­pat­i­ble hy­pothe­ses that you can’t di­rectly test, you’re down to Oc­cam’s Ra­zor, which I think favours base re­al­ity rather than a simu­lated uni­verse.

• I agree with all of that. But Bostrom’s ar­gu­ment is a bad choice for EY’s pur­poses, be­cause the flaws in it are sub­tle and not re­ally a case of any one premise be­ing plumb wrong.

• It has been claimed that logic and math­e­mat­ics is the study of which con­clu­sions fol­low from which premises. But when we say that 2 + 2 = 4, are we re­ally just as­sum­ing that? It seems like 2 + 2 = 4 was true well be­fore any­one was around to as­sume it, that two ap­ples equalled two ap­ples be­fore there was any­one to count them, and that we couldn’t make it 5 just by as­sum­ing differ­ently.

• My two cents:

“2 + 2 = 4” is not the same type of state­ment as, say, “sugar dis­solves in wa­ter”. The state­ment “sugar dis­solves in wa­ter” refers to a fact about the world; there are ex­per­i­ments we can perform that would ver­ify that state­ment.

The state­ment “2 + 2 = 4”, on the other hand, doesn’t re­fer to a fact about the world; it refers to a truth-pre­serv­ing trans­for­ma­tion that can be ap­plied to facts about the world. It al­lows us to trans­form “I have 2 + 2 ap­ples” into “I have 4 ap­ples”, and “he is 4 years old” to “he is 2 + 2 years old”, and so on.

What do the sym­bols “2”, “4“, and “+” mean here? Well, they mean a differ­ent thing in each con­text. In one con­text, “2” means “two ap­ples”, “4“ means “four ap­ples”, and “X + Y” means “X ap­ples, and also Y sep­a­rate ap­ples”. In the other, “2” means “two years ear­lier”, “4″ means “four years ear­lier”, and “X + Y” means “X years ear­lier than the time that was Y years ear­lier”.

Why do we use the same sym­bols with differ­ent mean­ings? Be­cause there hap­pens to be a set of truth-pre­serv­ing trans­for­ma­tions—the ring ax­ioms—that can be ap­plied to all of these differ­ent mean­ings. Since they obey the same ax­ioms, they also obey the trans­for­ma­tion “2 + 2 = 4”, which is just a com­pos­ite of ax­ioms.

• Come to think of it, ap­ples don’t ac­tu­ally satisfy the ring ax­ioms. In par­tic­u­lar, if you have at least one ap­ple, there is no num­ber of ap­ples I can give you such that you no longer have any ap­ples.

• In fancy math-talk, we can say ap­ples are a semi­mod­ule over the semiring of nat­u­ral num­bers.

• You can add two bunches of ap­ples through the well-known “glom­ming-to­gether” op­er­a­tion.

• You can mul­ti­ply a bunch of ap­ples by any nat­u­ral num­ber.

• Mul­ti­pli­ca­tion dis­tributes over both nat­u­ral-num­ber ad­di­tion and glom­ming-to­gether.

• Mul­ti­pli­ca­tion-of-ap­ples is as­so­ci­a­tive with mul­ti­pli­ca­tion-of-num­bers.

• 1 is an iden­tity with re­gard to mul­ti­pli­ca­tion-of-ap­ples.

You could quib­ble that there is a finite sup­ply of ap­ples out there, so that (3 ap­ples) + (all the ap­ples) is un­defined, but this model ought to work well enough for small col­lec­tions of ap­ples.

• Ap­ples (and other finite sets of con­crete ob­jects) form a semiring.

• Nor is it ob­vi­ous how mul­ti­pli­ca­tion of ap­ples should work. Ap­ples might be con­sid­ered an in­finite cyclic abelian monoid, if you like, but it’s beside the point—the point is that once you know what ax­ioms they satisfy, you now know a whole bunch of stuff.

• Well, if you have a row of 3 ap­ples, and you get an­other three rows, you’ll have 9 ap­ples. But mul­ti­ply­ing 3 ap­ples by 3 ap­ples would re­sult in 9 ap­ples^2; and I don’t know what those look like.

• In par­tic­u­lar, if you have at least one ap­ple, there is no num­ber of ap­ples I can give you such that you no longer have any ap­ples.

Sure there is, as long as you re­al­ize that “give” and “take” are the same ac­tion. Giv­ing −1 ap­ples is just tak­ing 1 ap­ple.

• Num­ber of ap­ples isn’t closed un­der tak­ing.

If you wish to satisfy the ring ax­ioms from scratch, you must first in­vent the econ­omy...

• Does an ap­ple com­posed of an­ti­mat­ter still count as an ap­ple? If I add that to the origi­nal ap­ple, I get a big ex­plo­sion and lots of en­ergy fly­ing around, but nei­ther ap­ple ac­tu­ally re­mains af­ter­wards.

• Well, strictly speak­ing we don’t di­rectly as­sume that 2+2=4. We have some ba­sic as­sump­tions about count­ing and ad­di­tion, and it fol­lows from these that 2+2=4. But that doesn’t re­ally avoid the ob­jec­tion, it just moves it down the chain.

Can I change these as­sump­tions? Well, firstly it bears say­ing that if I do, I’m not re­ally talk­ing about count­ing or ad­di­tion any more, in the same way that if I define “beaver” to mean “300 ton sub-Sa­haran lizard”, I’m not re­ally talk­ing about beavers.

So sup­pose I change my as­sump­tions about count­ing and ad­di­tion such that it came out that 2+2=5. Would that mean that two ap­ples added to two ap­ples made five ap­ples? Ob­vi­ously not. It would mean that two ap­ples added to two ap­ples made five ap­ples, where the starred words re­fer to al­tered con­cepts.

• Any­way, I pre­fer to see 2+2=4 as de­riv­ing from set the­ory, rather than ar­ith­metic. Set the­ory has its for­mal rules, and some ver­sion of 2+2=4 is one of them.

The ques­tion is, do we find things in our world that can be use­fully mod­el­led by set the­ory? We can. For a start, there seem to be many ob­jects that have per­sis­tence—cups, trees and planets don’t gen­er­ally split or mul­ti­ply in the course of a con­ver­sa­tion. Also, we can use­fully group ob­jects to­gether by their prop­er­ties, and it is of­ten use­ful to ig­nore their differ­ences. Two similar look­ing trees are likely to do similar kinds of things in similar situ­a­tions (ie in­duc­tion over classes of ob­jects is not com­pletely use­less).

So two cups of wa­ter plus two cups of sugar makes four cups—as long as we’re in­ter­ested in cups, not in the differ­ence be­tween sugar and wa­ter. Two elms and two oaks make four trees—as long as we’re in­ter­est in trees in gen­eral, and as long as we aren’t think­ing on the scale of decades, and as long there isn’t a guy with a chain­saw and an itchy trig­ger finger.

In fact, set the­ory is so use­ful about so many things in the world, that we ab­stract it to a uni­ver­sal truth − 2+2=4 in so many differ­ent cir­cum­stances, that sim­ply 2+2=4.

So we can’t make two ap­ples plus two ap­ples equal five ap­ples (at least not in a few sec­onds) be­cause ap­ples, in the way that we use the term, and on the time scales that we use the term, are ob­jects that obey the ax­ioms of set the­ory.

• Not ex­actly on sub­ject, but the num­bers up to 5 seem wired into our brain, so in effect, 2+2=4 be­fore you were old enough to know what “2” was.

• Two cups of wa­ter plus two cups of sugar does not equal four cups of sugar wa­ter. ;)

• All the premises nec­es­sary to prove that 2+2=4 can be found in the defi­ni­tions of 2, 4, + and =. Add in some defi­ni­tions from set the­ory, and you get sizeof(X)=2 && sizeof(Y)=2 and dis­joint(X,Y) |- sizeof(X u Y)=4. The trick­ier as­sump­tions are in con­vert­ing from op­er­a­tions on ap­ples to op­er­a­tions on sets. This iso­mor­phism is en­tailed by the count­ing al­gorithm; if there’s no per­son around to count them, then when we said “there are two ap­ples” we were talk­ing about a coun­ter­fac­tual in which some­thing did run the count­ing al­gorithm. (Note that the ab­stract count­ing al­gorithm as­sumes a perfectly-re­li­able tag­ging of counted and not-counted-yet ob­jects, and a perfectly re­li­able in­cre­ment­ing num­ber; a count made by a hu­man has nei­ther of these things, so some­times counted_as(25,000)+counted_as(25,000gp) = counted_as(50,001).)

• This doesn’t seem di­rectly rele­vant to the med­i­ta­tion. Are you say­ing that, yes, it is an as­sump­tion, be­cause it’s an ar­gu­ment from defi­ni­tion? Be­cause I guess that would be re­spon­sive, but the more in­ter­est­ing ques­tion is whether or not those defi­ni­tions of 2, 4, +, and = can be known to cor­re­spond to the ex­ter­nal world through more than just our as­sump­tions.

• We might mean many things by “2 + 2 = 4”. In PA: “PA |- SS0 + SS0 = SSSS0″, and so by sound­ness “PA |= SS0 + SS0 = SSSS0” In that sense, it is a log­i­cal tru­ism in­de­pen­dent of peo­ple count­ing ap­ples. Of course, this is clearly not what most peo­ple mean by “2+2=4″, if for no other rea­son than peo­ple did num­ber the­ory be­fore Peano.

When ap­plied to ap­ples, “2 + 2 = 4” prob­a­bly is meant as: “ap­ples + the world |= 2 ap­ples + 2 ap­ples = 4 ap­ples”. the truth of which de­pends on the na­ture of “the world”. It seems to be a cor­rect state­ment about ap­ples. Tech­ni­cally I have not checked this prop­erty of ap­ples re­cently, but when I con­sider plac­ing 2 ap­ples on a table, and then 2 more, I think I can re­move 4 ap­ples and have none left. It seems that if I re­quire 4 ap­ples, it suffices to find 2 and then 2 more. This is also true of en­velopes, pa­per­clips, M&M’s and other ob­jects I use. So I gen­er­al­ise a law like be­havi­our of the world that “2 things + 2 things makes 4 things, for or­di­nary sorts of things (eg. ap­ples)”.

At some level, this is part of why I care about things that PA en­tails, rather than an ar­bi­trary sym­bol game; it seems that PA is a log­i­cal struc­ture that ex­tracts lawlike be­havi­our of the world. If I as­sumed a differ­ent sys­tem, I might get “2+2=5”, but then I don’t think the sys­tem would cor­re­spond to the be­havi­ours of ap­ples and M&M’s that I want to gen­er­al­ise.

(On the other hand, PA clearly isn’t enough; it seems to me that strength­ened finite Ram­sey is true, but PA doesn’t show it. But then we get into ZFC /​ sec­ond or­der ar­ith­metic, and then sys­tems at least as strong as PA_or­di­nal, and still lose be­cause there are no in­finite de­scend­ing chains in the or­di­nals)

• 2, +, 2, =, and 4 are just defi­ni­tions. What they are defi­ni­tions for de­pends on the un­der­ly­ing rep­re­sen­ta­tion (2 might be a defi­ni­tion for S(S(0)) in PA, { {} , {{}} } in ZF set the­ory, or two ap­ples in school) but what re­ally mat­ters is that there ex­ists a ho­mo­mor­phism be­tween all our rep­re­sen­ta­tions.

$H\_\{school\}\(2 apples\$%20+%5E{school}%20H_{school}(2%20ap­ples)%20=%20H_{school}(2%20ap­ples%20+%202%20ap­ples))

Even bet­ter, there’s gen­er­ally an in­verse ho­mo­mor­phism back the real world.

$4 apples = H\_\{school\}^\{\-1\}\( H\_\{PA\}\(S\(S\(0\$)))%20+%20H_{school}%5E{-1}(%20H_{ZF}(\{%20\{\}%20,%20\{\{\}\}%20\})))

We can con­vert be­tween any of our rep­re­sen­ta­tions while pre­serv­ing the struc­ture of the re­la­tion­ships be­tween the ob­jects in our rep­re­sen­ta­tions. What we have dis­cov­ered is not that “2 + 2 = 4” was always true but that any pos­si­ble equiv­a­lent rep­re­sen­ta­tion is an in­her­ent prop­erty of the uni­verse.

“2 + 2 = 5” just lacks a ho­mo­mor­phism to any other use­ful rep­re­sen­ta­tions of re­al­ity based on our com­mon defi­ni­tions.

• This is a tricky one...here’s my at­tempt:

One does not have to di­rectly as­sume that 2 + 2 = 4. Note that all of the fol­low­ing state­ments cor­rectly de­scribe first-or­der logic (given the ap­pro­pri­ate defi­ni­tions of 2, 3, and 4):

• ∀x ∀y ((x + y) + 1 = x + (y + 1)) ⊢ (2 + 1) + 1 = 2 + (1 + 1)

• (2 + 1) + 1 = 2 + (1 + 1) ⊢ 3 + 1 = 2 + (1 + 1)

• 3 + 1 = 2 + (1 + 1) ⊢ 4 = 2 + (1 + 1)

• 4 = 2 + (1 + 1) ⊢ 4 = 2 + 2

• 4 = 2 + 2 ⊢ 2 + 2 = 4

So ∀x ∀y ((x + y) + 1 = x + (y + 1)) ⊢ 2 + 2 = 4 (in the con­text of first-or­der logic). By the sound­ness the­o­rem for first-or­der logic, then, ∀x ∀y ((x + y) + 1 = x + (y + 1)) ⊨ 2 + 2 = 4. (i.e. In all mod­els where “∀x ∀y ((x + y) + 1 = x + (y + 1))” is true, “2 + 2 = 4″ is also true.)

So, yes, an as­sump­tion is be­ing made, and that as­sump­tion is “∀x ∀y ((x + y) + 1 = x + (y + 1))”. To eval­u­ate the plau­si­bil­ity of that as­sump­tion, we now must spec­ify a do­main of dis­course, the mean­ing of ‘+’, and the mean­ing of ‘1’. Eliezer means to (I hope!) spec­ify the nat­u­ral num­bers, ad­di­tion, and one, re­spec­tively. Ad­di­tion over the nat­u­ral num­bers is it­self an ab­strac­tion of mov­ing differ­ent quan­tities of dis­crete non-micro­scopic ob­jects (like ap­ples) next to each other, and ob­serv­ing the quan­tity af­ter that. Now we can eval­u­ate the plau­si­bil­ity of “∀x ∀y ((x + y) + 1 = x + (y + 1))”, or, to trans­late into English, “If you take a group of y ob­jects and move it next to a group of x ob­jects, and then move one more ob­ject next to that newly formed group of ob­jects, and then ob­serve the quan­tity, then you will ob­serve the same quan­tity as if you take a group of y ob­jects and move 1 more ob­ject next to it, and then move that newly formed group of ob­jects next to a group of x ob­jects, and ob­serve the quan­tity, no mat­ter what the origi­nal num­bers x and y are.” (So sym­bolic lan­guage is use­ful af­ter all....) We ob­serve ev­i­dence for that state­ment ev­ery day! It is a be­lief that pays rent in terms of an­ti­ci­pated ex­pe­rience. So, yes, we could as­sume differ­ently, but we would be do­ing so in the face of moun­tains of ev­i­dence point­ing in the other di­rec­tion, and with some­thing to pro­tect, that won’t do.

Notes:

• How do we know the sound­ness the­o­rem for first-or­der logic is true? For one thing, we ob­serve in­duc­tive ev­i­dence for it all the time (the rules of first-or­der logic are in­cred­ibly in­tu­itive, see page 51 (PDF page 57) of A Primer for Logic and Proof for an enu­mer­a­tion), just as we see in­duc­tive ev­i­dence for “∀x ∀y ((x + y) + 1 = x + (y + 1))” all the time. We can also use math­e­mat­i­cal in­duc­tion (on the length of a de­duc­tion) to prove the sound­ness the­o­rem, but this prob­a­bly won’t con­vince some­one who is skep­ti­cal of even first-or­der logic.

• It might be helpful to think of (X ⊨ Y) as mean­ing P(Y|X) = 1.

• Yes, we are mak­ing an as­sump­tion, and yes, (if it is true) it was true well be­fore any­one was around to as­sume it, and yes, mak­ing a differ­ent as­sump­tion does not change it’s truth value. That’s part of what “as­sump­tion” means in this sense.

• The fact that if we put any two ob­jects into the same (pre­vi­ously empty) bas­ket as any other two ob­ject we will in this bas­ket have four ob­jects is true be­fore we can make any defi­ni­tions. But the state­ment 2 + 2 = 4 does not make any sense be­fore we have in­vented: (a) the nu­mer­als 2 and 4, (b) the sym­bol for ad­di­tion + and (c) the sym­bol for equal­ity =. When we have in­vented mean­ings for these sym­bols (sym­bols as things we use in for­mal ma­nipu­la­tions are quite differ­ent from words and were in­vented quite late, much later than we started to ac­tu­ally solve prob­lems math­e­mat­i­cally) we have to show that they cor­re­spond to our in­tu­itive mean­ing of putting things into bas­kets and count­ing them, but if they do they will also satisfy, say the Peano ax­ioms for the nat­u­ral num­bers, which are the ax­ioms we tend to start from to prove state­ments like 2+2=4 or “there are in­finitely many prime num­bers”.

If we were to as­sume differ­ently such that 2+2 =5, then our no­tion of + and = would not cor­re­spond to the no­tions of adding ob­jects to a bas­ket and count­ing them. This is be­cause we could walk through our proof step by step (as de­scribed in this post) to find the first line where we write down some­thing that is not true for our usual no­tion of adding ap­ples, there we would have an as­sump­tion or a rule of in­fer­ence that was as­sumed in this new the­ory but which does not cor­re­spond to ap­ple com­par­i­son.

• When peo­ple say “2+2=4”, what do they mean? Well, “=” is a stan­dard sym­bol in logic (IIRC it can be de­rived from purely syn­tac­ti­cal rules). But 2 and 4 and + aren’t stan­dard; they are defined as part of the model you’re work­ing with. For in­stance, if your model is boolean alge­bra, there are no 2 or 4, there are only ‘true’ and ‘false’, and “2+2=4” isn’t valid or in­valid, it’s syn­tac­ti­cally mean­ingless.

Depend­ing on the model you choose, the sen­tence “2+2=4” may be true (as for the Peano in­te­gers), or un­defined (as for boolean alge­bra), or even false (ex­change the usual mean­ings of the strings “2“ and “4”). The lat­ter case would be hu­man-per­verse but math­e­mat­i­cally-sound. But once you choose a a model, ev­ery sen­tence—in­clud­ing “2+2=4”—is ei­ther a log­i­cal truth (is valid) or it is not.

Now, there are some stan­dard (in the sense of widely used) mod­els where 2 and 4 and + are used as sym­bols. Th­ese in­clude the in­te­gers, the real num­bers, etc. Usu­ally when peo­ple say “2+2=4”, they are think­ing of one of these. And in these stan­dard mod­els, “2+2=4″ is in­deed a log­i­cal truth.

So given a model, we are not as­sum­ing 2+2=4. Our choice of a stan­dard model dic­tates that “2+2=4” is true, with­out ex­tra as­sump­tions. A differ­ent model might dic­tate that “2+2=4″ is false, or un­defined.

But we are rely­ing on our shared as­sump­tion about what model we’re talk­ing about—which is a differ­ent kind of as­sump­tion; it’s not about whether “2+2=4” is true (valid), but about what the string means—how to read it. It’s similar to the as­sump­tion that we’re speak­ing English, rather than a differ­ent lan­guage in which all the words just hap­pen to mean some­thing else.

• My re­sponse, be­fore read­ing the other re­sponses, is that this is not a mat­ter of as­sump­tion but of defi­ni­tion; the sym­bols ‘2’, ‘+’, ‘=’ and ‘4’ have been defined in such a way that 2+2=4 is a true state­ment. (The im­por­tant sym­bol, here, is + in my view: 2, 4 and = are such ba­sic op­er­a­tions that it’s near cer­tain that there would have been some sym­bol with those mean­ings. + is pretty ba­sic, but to my mind less ba­sic—it’s not the only way to com­bine two quan­tities).

This could be seen as tak­ing the defi­ni­tions of 2, 4, = and + as premises and the truth of the state­ment 2+2=4 as a con­clu­sion. The con­clu­sion (2+2=4) fol­lows from the premises whether any­one’s around to pos­tu­late the premises or not; that re­mains true of any log­i­cal state­ment. So, similarly, if all kit­tens are lit­tle, and if all lit­tle things are in­no­cent, then it re­mains true that all kit­tens are in­no­cent whether any­one has ever con­sid­ered that chain of logic be­fore or not.

• It has been claimed that logic and math­e­mat­ics is the study of which con­clu­sions fol­low from which premises. But when we say that 2 + 2 = 4, are we re­ally just as­sum­ing that? It seems like 2 + 2 = 4 was true well be­fore any­one was around to as­sume it, that two ap­ples equaled two ap­ples be­fore there was any­one to count them, and that we couldn’t make it 5 just by as­sum­ing differ­ently.

I think it’s an as­sump­tion, de­pend­ing on what you mean when you say some­thing is an as­sump­tion. It seems to us like “2 + 2 = 4”, but if we as­sumed differ­ently then it would seem like “2 + 2 = 5“. We seem to have jus­tifi­ca­tions to point to to be­lieve that “2 + 2 = 4”, but if we as­sumed that “2 + 2 = 5” then we would also seem to have jus­tifi­ca­tions for that point of view.

I per­son­ally have no prob­lem with this and will con­tinue to fol­low my cur­rent be­liefs.

• claiming that most peo­ple don’t have the con­cept of an ar­gu­ment, and that it’s pointless to try and teach them any­thing else un­til you can con­vey an in­tu­itive sense for what it means to argue

This is some­thing I can ob­serve ev­ery­day in my life. Prob­a­bly I am less lucky then other guys and in my sur­round­ing there are not that much “re­spected part­ners” who are able to listen and not rudely im­me­di­ately dis­agree. So yes, it seems like most peo­ple don’t have the con­cept of a proper ar­gu­ment. But that way I also did not have thsi con­cept for a long time. We all learn and change. The eas­iest way is to say “peo­ple are rude and dumb and there is no point in try­ing to change them”. But in real life one can­not just change his sur­round­ing, change the lo­ca­tion, change the work and col­leagues, change friends. If you want to have more “re­spected part­ners”—try to ed­u­cate those you already have.

• A con­clu­sion which is true in any model where the ax­ioms are true, which we know be­cause we went through a se­ries of trans­for­ma­tions-of-be­lief, each step be­ing li­censed by some rule which guaran­tees that such steps never gen­er­ate a false state­ment from a true state­ment.

I want to add that this idea jus­tifies ma­te­rial im­pli­ca­tion (“if 2x2 = 4, then sky is blue”) and other counter-in­tu­itive prop­er­ties of for­mal logic, like “you can prove any­thing, if you as­sume a con­tra­dic­tion/​false state­ment”.

Usual way to show the lat­ter goes like this:

1) As­sume that “A and not-A” are true

2) Then “A or «pigs can fly»” are true, since A is true

3) But we know that not-A is true! There­fore, the only way for “A or «pigs can fly»” to be true is to make «pigs can fly» true.

4) There­fore, pigs can fly.

The steps are clear, but this seems like cheat­ing. Even more, this feels like a strange, alien in­fer­ence. It’s like putting your keys in a pocket, pop­ping your­self on the head to in­duce short-term mem­ory loss and then us­ing your in­abil­ity to re­mem­ber keys’ where­abouts to win a poli­ti­cal de­bate. That isn’t how hu­mans usu­ally rea­son about things.

But the thing is, for­mal logic isn’t about rea­son­ing about things. For­mal logic is about pre­serv­ing the truth; and if you as­sumed “A and not-A”, then there is noth­ing left to pre­serve.

How Wikipe­dia puts it:

An ar­gu­ment (con­sist­ing of premises and a con­clu­sion) is valid if and only if there is no pos­si­ble situ­a­tion in which all the premises are true and the con­clu­sion is false.

• I would sug­gest that the most likely rea­son for log­i­cal rude­ness—not tak­ing the mul­ti­ple-choice—is that most ar­gu­ments be­yond a cer­tain level of so­phis­ti­ca­tion have more un­stated premises than they have stated premises.

And I sus­pect it’s not easy to iden­tify un­stated premises. Not just the ones you don’t want to say, be­lief-in-be­lief sort of things, but ones you as an ar­guer sim­ply aren’t suffi­ciently skil­led to de­scribe.

As an ex­am­ple:

For ex­am­ple: Nick Bostrom put forth the Si­mu­la­tion Ar­gu­ment, which is that you must dis­agree with ei­ther state­ment (1) or (2) or else agree with state­ment (3):

In the given sum­mary (which may not ac­cu­rately de­scribe the full ar­gu­ment; for the pur­poses of the demon­stra­tion, it doesn’t mat­ter ei­ther way), Mr. Bostrom doesn’t note that, pre­sum­ably, the num­ber of po­ten­tial simu­lated earths im­mensely out­num­bers the num­ber of non­si­mu­lated earths as a re­sult of his ear­lier state­ments. But that premise doesn’t nec­es­sar­ily hold!

If the in­verse of the chances of an Earth reach­ing simu­la­tion-level progress with­out some­how self-ex­ter­mi­nat­ing or be­ing ex­ter­mi­nated (say, 1 in 100) is lower than the av­er­age num­ber of Earth-simu­la­tions that so­ciety runs (so less than 100), then the bal­ance of po­ten­tial earths does not match the un­stated premise… in uni­verses suffi­ciently large for mul­ti­ple Earths to ex­ist (See? A po­ten­tial hid­den premise in my pro­posal of a hid­den premise! Th­ese things can be tricky).

And if most ar­guers aren’t good at dis­cern­ing hid­den premises, then ar­guers can feel like they’re fal­ling into a trap: that there must be a premise there, hid­den, but undis­cov­ered, that pro­vides a more se­ri­ous challenge to the ar­gu­ment than they can muster. And with that pos­si­bil­ity, an av­er­age ar­guer might want to sim­ply be quiet on it, ex­pect­ing a more skil­led ar­guer to dis­cern a hid­den premise that they couldn’t.

That doesn’t seem rude to me, but hum­ble; a con­ces­sion of lack of in­di­vi­d­ual skill when faced with a suffi­ciently so­phis­ti­cated ar­gu­ment.

• Truth pre­serv­ing logic is part of a fam­ily of ax­iom sys­tems called Mo­dal log­ics. In my hum­ble opinion I think that Truth pre­serv­ing logic isn’t the most in­ter­est­ing; I think the most in­ter­est­ing logic is the Proof or Jus­tifi­ca­tion pre­serv­ing logic, and com­ing in at a close sec­ond, the break-even-bet­ting-on-prob­a­bil­is­tic-out­comes logic.

Clas­si­cal logic is the com­mon name for truth pre­serv­ing logic, In­tu­ition­ist logic for jus­tifi­ca­tion pre­serv­ing and Bayesian rea­son­ing for the last one.

• Great post, Eliezer. I’ve seen all of this be­fore, but never all in one place, and not ex­plained so clearly.

I was go­ing to write a long story about how I be­came in­ter­ested in math, but it would take too much time, and I doubt many peo­ple would care. So, I’ll ab­bre­vi­ate it: Num­ber Munch­ers → “How can I solve an alge­bra prob­lem in which there are “x”s on both sides of the equals sign?” → An ob­ses­sion with pi (I had over 500 dec­i­mal places mem­o­rized at one point.) → Learn­ing some eas­ier calcu­lus for fun in 9th grade → An ob­ses­sion with prime num­bers → Me­ta­math , and then there were many things af­ter that, too, but in­ter­act­ing with the idea of for­mal proof ver­ifi­ca­tion us­ing a com­puter is what forced me into much greater math­e­mat­i­cal ma­tu­rity.

Edit: For­mat­ting is­sues, sorry.

• My [un­in­formed] in­ter­pre­ta­tion of math­e­mat­ics is that it is an ab­strac­tion of con­cepts which do ex­ist in this world, which we have ob­served like we might ob­serve grav­ity. We then go on to in­fer things about these ab­stract con­cepts us­ing proofs.

So we would ob­serve num­bers in many places in na­ture, from which we would make a model of num­bers (which would be an ab­stract model of all the things which we have ob­served fol­low­ing the rules of num­bers), and from our model of num­bers we could in­fer prop­er­ties of num­bers (much like we can in­fer things about a fal­ling ball from our model of grav­ity), and these in­fer­ences would be “proofs” (and thank­fully, be­cause num­bers are so much sim­pler than most things, we can list all our as­sump­tions and have perfect in­for­ma­tion about them, so our in­fer­ences are in­deed proofs in the sense that we can be pretty damn cer­tain of them).

But it seems like a com­mon view that math­e­mat­ics has some sort of spe­cial place in the uni­verse, above the laws of physics. I’m not a math­e­mat­i­cian, so it is not un­likely that there is some­thing I don’t know which takes down my view. But I’d be glad to know what it is.

• Most of this is old, but up­voted for the last cou­ple para­graphs.

• The re­jec­tion of the defi­ni­tion of proofs as “mere” sym­bol ma­nipu­la­tion is as in­sight­ful as the re­jec­tion of physics as the study of fun­da­men­tal par­ti­cles or of neu­rol­ogy as the study of neu­rons in the brain.

Your emo­tional ap­peal is about as mov­ing (and non­sen­si­cal) as “It is not pos­si­ble that all hu­man in­tel­li­gence, com­plex­ity, and emo­tion could be de­scribed by the mere atoms mak­ing up the neu­rons in our brains. What of the hu­man heart and soul?”

The fact is that com­pletely rigor­ous for­mal proofs are nec­es­sary to ap­proach cer­tain prob­lems. It is not be­cause cer­tain math­e­mat­i­ci­ans are “cyn­i­cal” but be­cause the ap­proach of treat­ing proofs as “mere” sym­bol ma­nipu­la­tions bears fruit. But this does not in­val­i­date the higher level pic­ture that you are so at­tached to, just as the rel­a­tivis­tic and quan­tum the­o­ries did not in­val­i­date New­ton’s.

• What, speci­fi­cally, did Eliezer say in this post that you dis­agree with?

• You may have read—I’ve cer­tainly read—some philos­o­phy which en­deav­ors to score points for counter-in­tu­itive cyn­i­cism by say­ing that all math­e­mat­ics is a mere game of to­kens; that we start with a mean­ingless string of sym­bols like: …and we fol­low some sym­bol-ma­nipu­la­tion rules like “If you have the string ‘A ∧ (A → B)’ you are al­lowed to go to the string ‘B’”, and so fi­nally end up with the string: …and this ac­tivity of string-ma­nipu­la­tion is all there is to what math­e­mat­i­ci­ans call “the­o­rem-prov­ing”—all there is to the glo­ri­ous hu­man en­deavor of math­e­mat­ics.

• Also, read through this thread. I’m pretty sure Eliezer’s in agree­ment with you.

Now, ex­actly how was this post a mov­ing and non­sen­si­cal emo­tional ap­peal?

• I don’t con­sider the post to be an emo­tional ap­peal, just the phrase “and this ac­tivity of string-ma­nipu­la­tion is all there is to what math­e­mat­i­ci­ans call “the­o­rem-prov­ing”—all there is to the glo­ri­ous hu­man en­deavor of math­e­mat­ics.” I mean, there is es­sen­tially no con­tent there. Just a rough out­line of a philos­o­phy, and then not even a le­gi­t­i­mate at­tack on it, just a “if they are right, then math­e­mat­ics doesn’t seem glo­ri­ous to me any longer!”

• Then this should have been your origi­nal com­ment. In­ci­den­tally, if you ap­proved of the rest of the post, then praise-first style, as ex­em­plified here and here, for rea­sons (partly) speci­fied here, would have been more ap­pro­pri­ate.

• I agree that math­e­mat­i­cal sym­bols are in­her­ently mean­ingless. I doubt Eliezer would dis­agree with that.

Math­e­mat­i­ci­ans do as­sign mean­ing to sym­bols while work­ing, though. See this com­ment for an ex­am­ple.

• Yeah, when it starts with “You may have read philos­o­phy try­ing to score points by say­ing”, it doesn’t mean the writer en­dorses it.

• I’m sorry if I wasn’t clear. I en­dorse the “cyn­i­cal view” that math­e­mat­ics is fun­da­men­tally sym­bol ma­nipu­la­tion. Fun­da­men­tal in the sense that math­e­mat­ics as we cur­rently know it can be com­pletely de­scribed by sym­bol ma­nipu­la­tion with­out hav­ing to re­sort to no­tions such as “in­tu­ition.” Eliezer, ap­par­ently, dis­agrees with this philos­o­phy on the grounds that it is rob­bing math­e­mat­ics of some­thing which he finds aes­thet­i­cally pleas­ing.

• You seem to be ar­gu­ing that math­e­mat­ics is all syn­tax and no se­man­tics. I shall re­fer you to Gödel num­ber­ing, as well as the re­cur­sion the­o­rem.

• Un­countabil­ity is an idea that skep­tics/​ra­tio­nal­ists/​less-wrongers should treat with a grain of salt.

In­side of a par­tic­u­lar sys­tem, you might add an ad­di­tional sym­bol, “i”, with the as­sumed defi­ni­tional prop­erty that “i times i plus one equals zero”. This is how we make com­plex num­bers. We might similarly add “in­finity”, with an as­sumed defi­ni­tional prop­erty that “in­finity plus one equals in­finity”. Depend­ing on the laws that we’ve already as­sumed, this might form a con­tra­dic­tion or cause ev­ery­thing to col­lapse, but in some situ­a­tions it’s a rea­son­able thing to do. This new sym­bol, “in­finity” can be defi­ni­tion­ally large in mag­ni­tude with­out be­ing large in in­for­ma­tion con­tent—bits or bytes re­quired to com­mu­ni­cate it.

A spe­cific generic mem­ber of an un­countable set is in­finitely large in in­for­ma­tion con­tent—that means it would take in­finite time to com­mu­ni­cate at finite band­width, in­finite vol­ume to store at finite in­for­ma­tion den­sity. It is ut­terly im­prac­ti­cal.

It is rea­son­able (be­cause it is true) to be­lieve that ev­ery math­e­mat­i­cal ob­ject that a math­e­mat­i­cian has ever ma­nipu­lated was of finite in­for­ma­tion con­tent. The set of all ob­jects of finite in­for­ma­tion con­tent is merely countable, not un­countable.

What I’m try­ing to say is: Don’t worry about un­countabil­ity. It isn’t phys­i­cal and it isn’t prac­ti­cal. Math­e­mat­i­ci­ans may be in love with it (Hilbert’s fa­mous quote: “No one shall ex­pel us from the Par­adise that Can­tor has cre­ated.”), but the con­cept is a bit like that “in­finite” sym­bol—in­finite in mag­ni­tude, not in in­for­ma­tion con­tent.

• I strongly recom­mend that, if you haven’t already, you learn enough in­tro­duc­tory calcu­lus to un­der­stand what it means to take the limit of an ex­pres­sion as a vari­able ap­proaches in­finity. You are mak­ing a com­mon mis­take here by con­flat­ing your in­tu­itive un­der­stand­ing about in­finity with its mean­ing in stric­ter math­e­mat­i­cal con­texts.