J Thomas: "How is that useful?"

I'm just answering your question

"Can you prove that if PA proved 6 was a prime number then 6 would be a prime number? How would you do it?"

I'm not stating that proving implications with false antecedent is particularly useful, just that it is valid. Also aside from 6 being prime it is true that for any sentence phi, ZF |- "if PA |- phi then phi", but that ZF cannot even say, yet alone prove that "forall phi. if PA |- phi then phi". But it can prove "forall phi. if PA |- phi then N |= phi".

"But Larry, PA does not actually say that 6 is prime, and 6 is not prime."

Well of course 6 isn't prime. But if PA said it was, then it would be. There's nothing invalid about proving that A -> B if you know ~A. It's just not very useful. But for a somewhat less vacuous example, let RH be the riemann hypothesis. Then if PA |- RH then RH is true and if PA |- ~RH then RH is false. At least one of these implications has a false hypothesis, but they are both perfectly valid.

J Thomas:

Once more through the mill. If PA proves that 6 is a prime number, then 6 is really a prime number. Can you prove that if PA proved 6 was a prime number then 6 would be a prime number? How would you do it?

If PA |- "forall x y . x * y = 6 => |x|=1 || |y|=1" then N |= "forall x y . x * y = 6 => |x|=1 || |y|=1" (N = the natural numbers equiped with + and *) so for all x and y in N, N |= ",x * ,y = 6 => |,x|=1 || |,y|=1" (where ,x means a constant symbol for x) if x*y = 6 then N |= ",x * ,y = 6" so therefore N |= "|,x|=1 || |,y|=1" thus either N |= "|,x| = 1" or N |= "|,y| = 1" thus either |x|=1 or |y|=1 therefore we have that if x*y = 6 then either |x| = 1 or |y| = 1 therefore 6 is prime therefore if PA |- "6 is prime" then 6 is actually prime

Of course it is also a meta-theorem that for any sentence phi in the language of PA that

ZF |- "PA |- phi => phi_omega"

where phi_omega is phi relativeized to the finite ordinals.

Caledonian: That's relativism, right there - the idea that rightness is not only socially determined, but individually socially determined.

What!? That's just not what I said at all.

Richard: It seems to me that asking how is it that the word 'right' came to refer to rightness is like asking why 'green' means green, instead of meaning zebra.

The fact is that there is some concept that we've been calling "right", and though we don't exactly know what we mean by it, we're pretty certain it means something, and in some cases we know it when we see it.

It strikes me as unfair to accuse Eliezer of having his own private meaning of "right" that isn't in accordance with the common one, because hasn't endorsed a criterion or decision procedure for 'right', he hasn't tried to define it, he hasn't made clearly-wrong claims about it like "murder is right", he really hasn't said much of anything about the object-level practical meaning of 'right'. He has mostly just discussed certain meta-level features of the concept, such as the fact that isn't all-possible-minds-universal, and the idea that one who explicitly thinks "If i think X is right, then X is right" can think that anything is right.

Roko:

Eliezer decides to start using the symbol "c" to denote the real number 3*10^8.

No, he has continuously refused to spell out an explicit description of morality, because it admits no concise description. When Eliezer writes a list of values ending with "etcetera" he's saying (in your analogy) "c is 3*10^8, up to one significant digit".

Richard:

but others have pointed out that this reference fact is fixed by means of a seemingly 'relative' procedure

I think you are mixing meta-levels here. The seemingly relative procedure is used to describe morality in blog posts, not to chose what morality is in the first place.

Roko: It certainly is possible to opine that 22 is prime. Watch this:

22 is prime!

See, I did it. If you claim murder is right, then you aren't talking about something other than right, you are just making false statements about right.

@Roko

Also, Echoing Jadagul: as most people use the words, you're a moral relativist

Honestly I do not understand how you can continue calling Eliezer a relativist when he has persistently claimed that what is right doesn't depend on who's asking and doesn't depend on what anyone thinks is right.

Is anyone who does not believes in universally compelling arguments a relativist?

Is anyone who does not believe that morality is ontologically primitive a relativist?

Is anyone who does not believe that morality admits a concise description a relativist?

With these distinctions in mind, I hope my intent will be clearer, when I say that although I am human and have a human-ish moral framework, I do not think that the fact of acting in a human-ish way licenses anything.

hah. I was wondering what this Lob stuff had to do with morality.

good job on an excellent post.

simon:

To argue that a proof is being made concluding ?C using the assumption ?(◻C -> C) given the theory PA, to which proof we can apply the deduction theorem to get (PA |- "?(◻C -> C) -> ?C") (i.e. my interpretation of Löb's Theorem)

OK so the question marks are boxes right? In that case then yes, PA |- "?(?C -> C) -> ?C". This is OK. The contradiction comes if PA |- "(?C->C)->C". But morally this doesn't have anything to do with the deduction theorem. PA proves Lob because everything in the proof of Lob is expressible inside of PA.

Like I said before, the deduction theorem is really just a technical lemma. If I'm doing ordinary mathematics (not logic), and I assume X, and prove Y, and then say "ok well now I've proved X -> Y", then I have not used the deduction theorem, because I'm writing a proof, not explicitly reasoning about proofs. The deduction theorem lies a meta level up, where we have a explicit, specific, technical definition of what constitutes a proof, and we are trying to prove theorems from that definition.

But the proof uses an additional assumption which is the antecedent of an implication, and comes to a conclusion which is the consequent of the implication. To get the implication, we must use the deduction theorem or something like it, right?

Nope, we are using an ordinary principle of mathematical reasoning. The deduction theorem says that if you have a proof that uses this principle and is otherwise first-order, you can convert it into a pure first order proof.

Is this fact a theorem of first order logic without any additional assumptions, or is it merely a theorem of PA? I admit I don't know, as I'm not very familiar with first order logic, but it intuitively seems to me that if first order logic were powerful enough on its own to express concepts like "PA proves X" it would probably be powerful enough to express arithmetic, in which case the qualification in Gödel's theorem that it only applies to theories that express arithmetic would be superfluous.

First order logic without any additional assumptions can't even express concepts like like PA. So, yea; that's why Gödel's theorem has that qualification, because there are plenty first order theories that are simple enough that they can't express integers.