A puzzle: How can one rigorously construct Self-PA as recursively axiomatized first order theory in the language of PA?
Larry_D'Anna
Karma: 81
simon: Let me explain some of the terminology here, because that may be where the confusion lies.
A scentence is a finite string symbols that satisfies a certain set of syntactic constraints.
A theory is a (possibly infinite) set of sentences. PA is a theory.
A proof from a theory T is a finite set of sentences, each of which is either an element of T, or follows from the ones before according to a fixed set of rules.
The notation PA + X, where X is a sentences is just the union of PA and {X}.
The notation PA |- Y means that a proof from PA that ends in Y exists.
Now I have left out some technical details, like what exactly are the syntactic constraints on sentences, and what is the fixed set of rules for proofs, but we have enough to say what the deduction theorem means. It says
PA + X |- Y ⇒ PA |- “X → Y”
or in english: if there is a proof from the theory PA + X to the scentence Y, then there is a proof from PA alone that X->Y.
So, you see, the deduction theorem is really just a technical lemma. It meerly shows that (in one particular way) our technical definition of a first order proof behaves the way it ought to.
Now on to Lob’s theorem, which says that if PA |- “◻C → C” then PA |- “C”. Now in general if you want to prove PA |- A implies that PA |- B, one way to do it is to write a first order proof inside of PA that starts with A and ends with B. But that is not what is going on here. Instead we start with a proof of “◻C->C” and do something totally different than a first order proof inside of PA in order to come up with a proof that PA |- C.
Psy-Kosh: There are two points of view of where the flaw is.
My point view is that the flaw is here:
“Löb’s Theorem shows that, whenever we have ((◻C)->C), we can prove C. Applying the Deduction Theorem to Löb’s Theorem gives us, for all C: ((◻C)->C)->C”
Because, in fact Lob’s Theorem is: (PA |- “◻C → C”) ⇒ (PA |- “C”) and the Deduction theorem says (PA + X |- Y) ⇒ (PA |- “X->Y”). We don’t have PA + X proving anything for any X. The deduction theorem just doesn’t apply. The flaw is that the informal prose just does not accurately reflect the actual math.
Eliezer’s point of view (correct me if I’m wrong) is that in the cartoon, we have 10 steps all of the form “PA proves ….” They each follow logically from the ones that came before. So they look like a proof inside of PA. And if they were a proof inside of PA then the deduction theorem would apply, and his contradiction would go through. So the flaw is that while all of the steps are justified, one of them is only justified from outside of PA. And that one is step 8.
Both of these views are correct.
Brian Jaress:
I think if you used Lob’s Theorem correctly, you’d have something like: if PA |- []C → C then PA |- C [Lob] PA |- ([]C → C) → C [Deduction]
This is incorrect because the if-then is outside of PA. The deduction theorem does not apply.
“I just tested and anecdotally confirmed a hypothesis made with very little data: I suspected that neither Douglas Knight nor Larry D’Anna, the two who pinpointed 8 as the critical step, would be among the objectors to my metaethics. (Either of them can torpedo this nascent theory by stating otherwise.)”
I like your metaethics just fine.
Psy-Kosh: No that isn’t the problem. If there is a proof that 1=2, then 1=2. If there isn’t, then 1=2. Either way 1=2. The problem is the mixing of meta-levels / inappropriate use of the deduction theorem / tacit assumption that ◻a → ◻b is the same as “a → b”.
Sebastian Hagen: no ◻X is PA |- “X”. My best guess as to what Eliezer meant by “interpret the smiley face as saying..” is that he meant to interpret the cartoonproof as a proof from the assumption “(◻C → C)” to the conclusion “C”, rather than a proof from “◻(◻C → C)” to “◻C”.
Eliezer: “Larry, interpret the smiley face as saying:
PA + (◻C → C) |-”
OK ignoring the fact that this is exactly what it doesn’t say, I suppose we could notice that every step is surrounded at the top by a happy-face-says, so, if we may be inclined to think we can take those off and get a proof inside PA, starting with “◻C → C” as a hypothesis. Lets see what happens.
◻L <-> ◻(◻L → C)
◻C → C
ok these are our hypothesis.
◻(◻L->C) → (◻◻L → ◻C)
Modus Ponens works in PA, fine
◻L → (◻◻L → ◻C)
ordinary MP
◻L → ◻◻L
if PA can prove it, then PA can prove it can prove it
◻L → ◻C
ordinary MP
◻L → C
ordinary MP
◻(◻L → C)
ARGH WHAT ARE YOU DOING. THERE IS NO RULE OF FIRST ORDER LOGIC THAT ALLOWS YOU TO DO THIS. TO SAY “if i can prove X then i can prove i can prove X” STEPS OUTSIDE OF FIRST ORDER LOGIC YOU LOSE.
◻L
ordinary MP
10 C
ordinary MP
Eliezer: “Why doesn’t the given proof of Lob’s Theorem, the steps 1-10, show that PA + “◻C → C” |- C?”
That’s just not what it says. The hypothesis in step 2 isn’t “◻C → C” it’s “◻(◻C → C)”. I suppose if the Hypothesis were “◻C → C” we could try to find where it breaks. Step 7 is the only step that depends on 2 so it has to be there. Translating the amusing cartoons, we have
◻(◻C → C)
◻(◻L → ◻C)
◻(◻L → C)
Lets say that instead we have
2′. ◻C → C
Well what are we supposed to do with it? We’re stuck. Just because ◻C → C doesn’t mean that PA can prove it.
Robert: “You can only say (((◻C)->C)->(◻C))”
No that’s not right. The theorem says that if PA proves “◻C → C” then PA proves C. so that’s ◻(◻C → C) → ◻C.
The flaw is that the deduction theorem does not cross meta levels. Eliezer says “Löb’s Theorem shows that, whenever we have ((◻C)->C), we can prove C.” and goes on to claim that (◻C->C)->C. But he’s intentionally failed to use quotes and mixed up the meta levels here. Lob’s Theorem does not give us a proof in first order logic from ((◻C)->C) to C. It gives us a proof that if there is a proof of ((◻C)->C) then there is a proof of C. Which is an entirely diffirent thing altogether.
Eliezer: “Any supposed analysis that does not tell you to mention a particular step, is inexact at best, and more probably mistaken.”
I’m pretty sure my answer was completely correct. Care to point out the inexactness/mistakes?
oops that should be “what the deduction theorem really says”
The flaw is the instant you used the deduction theorem. You used it to go from
PA |- “◻C → C” → PA |- “C”
to
PA |- “(◻C->C) → C”
What the induction theorem really says is
T + X |- Y implies T |- “X → Y”
so what you really would have needed to apply the deduction theorm would have been
PA + “◻C → C” |- C
do I win?
Roko: What the heck does morality have to do with category theory at all?
A related sense of “arbitrary”, which is common in math and CS, is “could be anything, and will probably be chosen specifically to annoy you”.
wikipedia on nets:
net or Moore-Smith sequence is a generalization of a sequence, intended to unify the various notions of limit and generalize them to arbitrary topological spaces.
Virge: Why is it “not the point”? In this discussion we are talking about differences in moral computation as implemented within individual humans. That the blind idiot’s global optimization strategy defines homosexuality as a defect is of no relevance.
well because we’re trying to characterize the sort of psychological diversity that can exist within our species. And this psychological unity argument is saying “we’re all the same, except for a mix of one-step changes”. This means that any complex adaptation in any human is in almost all humans. The exceptions being: sexual dimorphism, and the fact that certain individuals are “defective”, in the sense that one of their complex adaptations is broken. So if you’re arguing against this position and saying: look at homosexuals, they are different but not broken, then you aren’t talking about the same kind of “broken”. I’m not arguing that we should make base any moral judgment on evolution’s silly ideas of what’s broken. I’m just arguing that homosexuals don’t serve as a counterexample to the idea of psychological unity.
Virge: I wasn’t claiming a complex adaptation. I was claiming “other computations that could exhibit a superficial unity, but with a broad spread.”
I think you’re right here. But hopefully the spread is not so much that we could not come to agree if we “knew more, thought faster, were more the people we wished we were, and had grown up farther together.”
An example that gives me hope that this could be true is Vengeance. We seem to be born with a terminal value saying that it is good to see our enemies suffer. In terms of explicit moral argument, if not in deeds, we have mostly come to agree that it is wrong to take vengeance; even though some of us came from cultures that once reveled in it; even though some of us may be more naturally inclined towards it.
When you do Bayesian updates, the specific values of your initial priors become less important as you gather more evidence. The evidence piles up exponentially, and you need exponentially bad priors to keep the wrong answer in the face of it. Perhaps our moral debates are similar. Perhaps the “broad spread” is not so great that we cannot come to agree, if we consider enough evidence, if we hear enough arguments. Psychological unity does not prove that this is so, but without psychological unity, there would be no reason to hope it is possible.
Roko: I think Eliezer has explicitly stated that he is a realist.
Virge: The argument for psychological unity is that, as a sexually reproducing species, it is almost impossible for one gene to rise in relative frequency if the genes it depends on are not already nearly universal. So the all the diversity within any species at any given time consists of only one-step changes; no complex adaptations. The one exception of course is that males can have complex adaptations that females lack, and vice versa.
So, with respect to your specific examples:
Homosexuals: sexual preference certainly is a complex adaptation, but obviously one that differs between males and females. Homosexuals just got the wrong sexual preference for their equipment. And it doesn’t do any good to say that they aren’t defective. They aren’t defective from a human, moral point of view, but that’s not the point. From evolutions view, there’s hardly anything more defective, except perhaps a fox that voluntarily restrains it’s own breeding.
Stanford Prison Experiment, Psychopaths: I’m not sure if I see where the complex adaptation is here. Some people have more empathy, some less. Even if the difference is supposed to be genetic, there seem to be a lot of these flexible parameters in our genome. Empathy-level could be like skin-color, height, hairiness, etc. We all have the machinery to compute empathy (we all have the same complex adaptation), but it’s used more often, or carries more influence in some people and less in others. Those that totally lack empathy are like albinos. They have the genes that are supposed to code for empathy, but they’re broken.
Of course you are right that empirical data on this question is needed. But absent that, we have what looks like a strong theoretical argument for psycological unity.
Will Pearson: Why not just treat them as pure functions in the State monad?
Richard: You were correct. That is indeed the strongest pro-life argument I’ve ever read. And although it is quite wrong, the error is one of moral reasoning and not merely factual.
Richard: Abortion isn’t a moral debate. The only reason people disagree about it is because some of them don’t understand what souls are made of, and some of them do. Abortion is a factual debate about the nature of souls. If you know the facts, the moral conclusions are indisputable and obvious.
simon:
It is a theorem about PA, although everything the statement and the proof of it can be expressed in PA if you like, in which case it is a theorem inside of PA about PA. There’s no contradiction there, as long as you have everything quoted properly.
That’s a valid deduction, but I don’t think it’s a step that anyone has written down in this thread before. It’s not clear to me where you are going with it.
We use 10 steps, 9 of which are proofs inside of PA, and one of which is the fact that if PA |- X then PA |- “PA |- X”.