In his recent Dwarkesh Patel interview, Musk is pretty clear about why he wants to go to the moon: he wants to build a ton of solar panels to capture more of the sun's energy, its easier to launch from the moon than from the earth, and the moon has plenty of silicon ^[1] . He is also pretty clear that he wants to build datacenters in orbit. I don't think we need to speculate to get answers here.

1. Also, it keeps things interesting for the simulator gods. ↩︎

Wrong conclusions are inevitable and commonplace. Godel's Theorems apply to all formalisms.

A tangent, but Godel's incompleteness theorems simply show that for sufficiently powerful formal systems:

1. There are statements which are true, but unprovable
2. If the system is consistent, "this system is consistent" is such a statement.

Neither of which show that all formal systems are unsound. That is, if a statement is provable in a formal system, the corresponding property is true in all models of that formal system. So this point is not correct because of Godel (though it could be practically correct for other reasons, such as the world being complicated).

I don't know the reading list for the 17th yet, but will try to publish it on Wednesday, much sooner than typical, for your sake!

Here is the claimed Gorard's "alien logic system" in the linked tweet

I had Claude chew on this for a bit, and Claude determined that this proof system was the trivial one (ie ∀a,b:a=b) by writing a script in SPASS (an automatic theorem prover) to try to prove this statement.

--------------------------SPASS-START-----------------------------
Input Problem:
1[0:Inp] || equal(skc2,skc3)** -> .
2[0:Inp] ||  -> equal(op(op(u,v),op(v,u)),v)**.
3[0:Inp] ||  -> equal(op(op(u,v),v),op(v,op(v,u)))**.
4[0:Inp] ||  -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
 This is a unit equality problem.
 This is a problem that has, if any, a non-trivial domain model.
 The conjecture is ground.
 Axiom clauses: 3 Conjecture clauses: 1
 Inferences: IEqR=1 ISpR=1 ISpL=1 
 Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 
 Extras    : Input Saturation, No Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1
 Precedence: op > skc3 > skc2 > skc1 > skc0
 Ordering  : KBO
Processed Problem:

Worked Off Clauses:

Usable Clauses:
1[0:Inp] || equal(skc3,skc2)** -> .
2[0:Inp] ||  -> equal(op(op(u,v),op(v,u)),v)**.
3[0:Inp] ||  -> equal(op(op(u,v),v),op(v,op(v,u)))**.
4[0:Inp] ||  -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
	Given clause: 1[0:Inp] || equal(skc3,skc2)** -> .
	Given clause: 2[0:Inp] ||  -> equal(op(op(u,v),op(v,u)),v)**.
	Given clause: 3[0:Inp] ||  -> equal(op(op(u,v),v),op(v,op(v,u)))**.
	Given clause: 15[0:Rew:3.0,14.0,2.0,14.0] ||  -> equal(op(u,op(u,v)),op(v,op(v,u)))*.
	Given clause: 4[0:Inp] ||  -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
	Given clause: 11[0:SpR:3.0,2.0] ||  -> equal(op(op(u,op(u,v)),op(u,op(v,u))),u)**.
	Given clause: 16[0:SpR:15.0,2.0] ||  -> equal(op(op(op(u,v),u),op(v,op(v,u))),u)**.
SPASS V 3.9 
SPASS beiseite: Proof found.
Problem: collapse.dfg 
SPASS derived 171 clauses, backtracked 0 clauses, performed 0 splits and kept 96 clauses.
SPASS allocated 85510 KBytes.
SPASS spent	0:00:00.08 on the problem.
		0:00:00.03 for the input.
		0:00:00.02 for the FLOTTER CNF translation.
		0:00:00.00 for inferences.
		0:00:00.00 for the backtracking.
		0:00:00.01 for the reduction.


Here is a proof with depth 3, length 23 :
1[0:Inp] || equal(skc3,skc2)** -> .
2[0:Inp] ||  -> equal(op(op(u,v),op(v,u)),v)**.
3[0:Inp] ||  -> equal(op(op(u,v),v),op(v,op(v,u)))**.
4[0:Inp] ||  -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
14[0:SpR:2.0,3.0] ||  -> equal(op(op(u,v),op(op(u,v),op(v,u))),op(u,op(u,v)))**.
15[0:Rew:3.0,14.0,2.0,14.0] ||  -> equal(op(u,op(u,v)),op(v,op(v,u)))*.
16[0:SpR:15.0,2.0] ||  -> equal(op(op(op(u,v),u),op(v,op(v,u))),u)**.
17[0:SpR:15.0,2.0] ||  -> equal(op(op(u,op(u,v)),op(op(v,u),v)),op(v,u))**.
34[0:SpR:4.0,2.0] ||  -> equal(op(op(u,op(v,op(w,u))),op(w,op(v,op(u,v)))),op(v,op(w,u)))**.
49[0:SpR:4.0,2.0] ||  -> equal(op(op(u,op(op(op(v,u),u),v)),v),u)**.
63[0:Rew:3.0,49.0] ||  -> equal(op(op(u,op(op(u,op(u,v)),v)),v),u)**.
128[0:SpR:16.0,3.0] ||  -> equal(op(op(u,op(u,v)),op(op(u,op(u,v)),op(op(v,u),v))),op(v,op(u,op(u,v))))**.
145[0:SpR:3.0,16.0] ||  -> equal(op(op(op(u,op(u,v)),op(v,u)),op(u,op(u,op(v,u)))),op(v,u))**.
168[0:Rew:17.0,128.0] ||  -> equal(op(op(u,op(u,v)),op(v,u)),op(v,op(u,op(u,v))))**.
171[0:Rew:168.0,145.0] ||  -> equal(op(op(u,op(v,op(v,u))),op(v,op(v,op(u,v)))),op(u,v))**.
173[0:Rew:34.0,171.0] ||  -> equal(op(u,op(u,v)),op(v,u))**.
174[0:Rew:173.0,15.0] ||  -> equal(op(u,op(u,v)),op(u,v))**.
194[0:Rew:173.0,63.0] ||  -> equal(op(op(u,op(op(v,u),v)),v),u)**.
209[0:Rew:173.0,174.0] ||  -> equal(op(u,v),op(v,u))*.
228[0:Rew:173.0,194.0,209.0,194.0,173.0,194.0,173.0,194.0,209.0,194.0] ||  -> equal(op(u,v),u)**.
229[0:Rew:228.0,2.0] ||  -> equal(op(u,v),v)**.
234[0:Rew:228.0,229.0] ||  -> equal(u,v)*.
235[0:UnC:234.0,1.0] ||  -> .
Formulae used in the proof : conjecture0 axiom1 axiom0 axiom2

--------------------------SPASS-STOP------------------------------

Therefore I think its quite likely that many of the supposedly rich alien axiom systems Gorard found are actually just trivial almost-contradictory systems which are hard to prove the triviality of. It also explains why he couldn't "make sense" of the system. There is nothing to make sense of.

I think the content and arguments in the possessed machines are not very good, the prose is ok but it would read as too self important and AI slop on a less distinguished webpage. I think that many people were charmed by how respectable and nice the website looked and so were willing to give the writing and arguments much more leeway when sharing the page (if they read it at all).

Edit: I believe this because I notice it is popular, and I noticed this dynamic in myself, I felt I wanted the article to be deep and interesting, but also that if I thought about telling the arguments to a skeptical observer very few of them would stand up to scrutiny.

Yeah, the possessed machines is a very good example of how important good web design is.

If you are to make claims like this, at least make arguments. This isn't twitter.

Caro is extremely comprehensive and will write small mini-books on the history of every significant institution or person LBJ ever touched. That means that The Master of the Senate begins in like 1810 and gives a complete history of the Senate up until LBJ is elected into the body.

I would be interested in someone analyzing when the constitution would permit a private citizen to take up arms against a sitting government (if any such circumstance exists).

To my knowledge, the interpretation which comes closest is Insurrectionist theory which interprets the right to bear arms as including the right of citizens to use them to defend against an oppressive government. There are apparently more explicit statements of this right in the preambles to some first-state constitutions, as well as the declaration of independence.

It should not be surprising that nobody has yet won on such a case in court though, and practically speaking you don't have this right ^[1] .

My understanding has been that even if you are arrested unlawfully by a police officer, you can't use proportional force (as you would if you were assaulted by a non-police-officer), since the perspective of the government is that it is the judiciary's right to determine whether an arrest is or isn't lawful, not the citizen's.

1. Except implicitly the founders themselves, who of course supported the right to revolution. Or at least supported that right for themselves. But originalism has never been a popular (or coherent) constitutional philosophy. ↩︎

Yeah I meant "most" where the others we're comparing are the 9 justices and one Marshal at most.