Talk:Double-negation translation

Weaker?

This article used to state that the Gödel–Gentzen negative translation of a formula is weaker than the original formula in intuitionistic logic, i.e. that intuitionistic logic proves φ → φ^N for any φ.[1] Is this an inaccurate statement? —Preceding unsigned comment added by Classicalecon (talk • contribs) 12:40, 25 February 2009 (UTC)

This is wrong. Consider the formula $\phi =\neg \forall x\,P(x)$, where P is a unary predicate. Then $\phi \to \phi ^{N}$ is the formula $\neg \forall x\,P(x)\to \neg \forall x\,\neg \neg P(x)$, which is not intuitionistically valid. — Emil J. 14:18, 25 February 2009 (UTC)

That's correct. However, the φ → φ^N property seems to hold for propositional logic. IMO we should add a propositional logic section to keep track of these results. —Preceding unsigned comment added by Classicalecon (talk • contribs) 16:14, 25 February 2009 (UTC)

In propositional logic, $\phi ^{N}$ is equivalent to $\neg \neg \phi$, and $\phi \to \neg \neg \phi$ is an intuitionistic tautology, so indeed, the property then trivially holds. A section on propositional logic could be useful. In fact, I think it would be better for didactic purposes to start with a section on the simple propositional $\neg \neg \phi$ translation, and only then introduce the general inductive definition of $\phi ^{N}$ for first-order logic. — Emil J. 16:49, 25 February 2009 (UTC)

When I created the article, I used the word "weaker" informally, to just mean "does not imply the original formula". I am glad this oversight was clarified later, since that is not what most people would mean by "weaker". — Carl (CBM · talk) 02:45, 26 February 2009 (UTC)

Rework article into Double-negation translation

The following discussion is closed. Please do not modify it. Subsequent comments should be made in a new section. A summary of the conclusions reached follows.

Consensus is to merge in Glivenko's theorem and rename to Double-negation translation. Non-admin closure. Note: I didn't perform this merge, awaiting expertise to actually do the merge. --KarlB (talk) 01:54, 1 July 2012 (UTC)

---

I'm inclined to think it would make most sense to rework this article to something like Double-negation translation, that can deal with this, the Kolmogorov, and the Kuroda translations on an equal footing, and allow Glivenko's theorem to be merged here. The article would then be better placed to talk about the ingredients, i.e. the relevant logical equivalences, that form the basis of these translations. Thoughts? — Charles Stewart (talk) 08:48, 24 April 2009 (UTC)

Having noticed that the first section falsely claims that double-negating propositional formulae, I think it is plain that the topics above are best treated together, as indeed all is done by all the modern treatments I am aware of. I've put a mege notice on the article: my proposal is first to merge Glivenko's theorem into this article, and then to move the merged article to Double-negation translation. — Charles Stewart (talk) 09:21, 30 April 2009 (UTC)

I completely support this. As other commentators have noted, the page should have a section covering the propositional case anyway, i.e. Glivenko's theorem. In my view, it would actually be more historically and logically accurate to call the translation Glivenko-Godel or Glivenko-Godel-Gentzen negative translation (GGG-translation?), but this is not common practice today.Computationalist (talk) 22:49, 29 October 2010 (UTC)

I completely support the renaming to Double-negation translation which is the concept to be presented, Gödel's and Gentzen's translations are just instances of the concept. Glivenko is known to be the original source for propositional logic (to intuitionistic propositional calculus) and Kolmogorov "On the principle of tertium non datur" (1925) the oldest source (though Gödel and Gentzen were probably unaware of) for the double-negation translation of first-order logic (to the minimal fragment of intuitionistic first-order logic). I have no strong opinion regarding the article Glivenko's theorem. If it can get its clear own section in the renamed page, the merge is fine for me. --Hugo Herbelin (talk) 09:56, 17 April 2011 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

Glivenko's Theorem

I am not an expert in this subject at all, but on this page it says that Glivenko's theorem is:

T ⊢ φ classically if and only if T ⊢ ¬¬φ intuitionistically.

Shouldn't this be:

T ⊢ φ classically if and only if T* ⊢ ¬¬φ intuitionistically,

where T* = { ¬¬θ | θ in T }? 77.169.36.17 (talk) 22:10, 12 February 2015 (UTC)

Or actually, Glivenko's theorem is just CPL ⊢ φ if and only if IPL ⊢ φ, the abovementioned statement can be derived with ¬¬φ → ¬¬ψ = ¬¬( φ → ψ ) and ¬¬φ ∧ ¬¬ψ = ¬¬( φ ∧ ψ ). 77.169.36.17 (talk) 14:24, 16 February 2015 (UTC)