Talk:Friedman translation

Logical automorphism

EmilJ: I can see how it is one might call the A-trans a self-interpretation, but to me that seems like a strange way of looking at it, especially as it only applies to a subclass of intuitionistic formulae. I'd really prefer to call it a mapping on formulae/proofs. Has Friedman called it a self-interpretation? I don't have the paper to hand to check. — Charles Stewart (talk) 12:33, 30 April 2009 (UTC)

It is a mapping on formulas which preserves provability, and that is exactly the definition of an interpretation. I have no idea what you mean by "only applies to a subclass of intuitionistic formulae", that's just not true. I can't find Friedman explicitly calling it an interpretation in the paper, but he writes "the double negation of Gödel is used to interpret PA within HA" (emph. mine) and (speaking about his translation) "an elementary syntactic argument in the same sense that the double negation translation is". — Emil J. 12:58, 30 April 2009 (UTC)

Re: scope of translation: I was letting myself be distracted, despite your hint, by its application, where A,B are Sigma-0-1. I don't dispute that it is an interpretation, only how cogent that fact is. Double-negation translations are normally talked of as interpretations not of intuitionistic logic, but of classical logic, although they are equally interpretations of intuitionistic logic in the sense you describe.

I don't see any harm in observing that it is an interpretation, but I think it is distracting to put that in the definition in the lede. — Charles Stewart (talk) 13:08, 30 April 2009 (UTC)

I do not insist on calling it an interpretation, a mapping on formulas or something like that would do. However, I consider it a fundamental matter of comprehension that the lead should start by saying what the Friedman translation is, not what it is used for. — Emil J. 13:17, 30 April 2009 (UTC)

I'm happy with this, and how the lede stands. — Charles Stewart (talk) 11:51, 3 May 2009 (UTC)