Talk:Double-negation translation

(Redirected from Talk:Gödel–Gentzen negative translation)
Latest comment: 9 years ago by 77.169.36.17 in topic Glivenko's Theorem

Weaker?

edit

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 (talkcontribs) 12:40, 25 February 2009 (UTC)Reply

This is wrong. Consider the formula  , where P is a unary predicate. Then   is the formula  , which is not intuitionistically valid. — Emil J. 14:18, 25 February 2009 (UTC)Reply
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 (talkcontribs) 16:14, 25 February 2009 (UTC)Reply
In propositional logic,   is equivalent to  , and   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   translation, and only then introduce the general inductive definition of   for first-order logic. — Emil J. 16:49, 25 February 2009 (UTC)Reply
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)Reply

Rework article into Double-negation translation

edit
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)Reply

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)Reply

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)Reply

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)Reply
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)Reply
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

edit

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)Reply

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)Reply