{"entities":{"Q361872":{"pageid":363639,"ns":120,"title":"Item:Q361872","lastrevid":61286109,"modified":"2026-04-10T22:22:55Z","type":"item","id":"Q361872","labels":{"en":{"language":"en","value":"Negative translations not intuitionistically equivalent to the usual ones"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6199442"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$091F1EA8-E415-4328-B3C5-8FA681F1C733","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6cd49d31ed6598dafcb958dff75c6f76b4266ba2","datavalue":{"value":{"text":"Negative translations not intuitionistically equivalent to the usual ones","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q361872$02588CF3-8DD4-45F7-8101-12F63792E78A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"abb889e75d7133f09ce5d17bdc86a6a9e95276db","datavalue":{"value":"1284.03263","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$50E80938-B7BC-4809-B393-00707F1869E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e86e1216a92c4550f95799f0e9e6b17064108fc7","datavalue":{"value":{"entity-type":"item","numeric-id":361871,"id":"Q361871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$7739CC56-241A-4E2C-8322-17879C14B0D2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$5DFE8524-12BD-448F-9563-E69159E2ED42","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"108ede7b32300394ff9a1f5dd35fef9c8cf60c54","datavalue":{"value":{"time":"+2013-08-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q361872$9963C7EC-F77D-4E23-AE25-AD6A43032FFE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1cb3dd3ed2e18eacb5347fad941e6f99dbd6af6a","datavalue":{"value":"https://arxiv.org/abs/1011.0317","type":"string"},"datatype":"url"},"type":"statement","id":"Q361872$46531406-7657-4E5D-90A2-70E236315695","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"28b77bd49c740251256fd2e4ae120354550c7ca4","datavalue":{"value":"With the purpose of verifying the folklore conjecture that all negative translations of classical predicate logic into intuitionistic predicate logic are intuitionistically equivalent, the notion of ``negative translation'' is defined as one applying to any translation \\((-)^*\\) of formulas that satisfies: if \\(\\Gamma\\vdash A\\) classically, then \\(\\Gamma^*\\vdash A^*\\) intuitionistically (soundness); and, \\(\\vdash (A^* \\leftrightarrow A)\\) classically (characterization).  Then it is shown that there are (at least) two translations \\((-)^{N_1}\\) and \\((-)^{N_2}\\) that satisfy the above definition of negative translation, but are both not intuitionistically equivalent to Gentzen's negative translation \\((-)^G\\) (Theorem 8). The translation \\((-)^{N_1}\\) is defined by  \\[  A^{N_1} := A^G \\vee F,  \\]  for \\(F\\) a chosen formula such that \\(\\vdash \\neg F\\) classically, but \\(\\not\\vdash \\neg F\\) intuitionistically. For the same kind of \\(F\\), \\((-)^{N_2}\\) is defined as  \\[  A^{N_2} := A^G [F/\\bot],  \\]  where \\(A'[F/\\bot]\\) denotes the formula obtained by replacing all instances of \\(\\bot\\) in \\(A'\\) by \\(F\\). The translation \\((-)^{N_2}\\) is actually the well-known Dragalin-Friedman translation applied after Gentzen's translation, as shown in Proposition 11.  The method for establishing Theorem 8 is to choose as \\(F\\) one of the two classically (provable and) equivalent versions of Kuroda's conjecture (double negation shift -- DNS),  \\[  \\neg(\\neg\\forall x P(x) \\wedge \\forall x \\neg\\neg P(x)),  \\]   \\[  \\neg\\neg(\\forall x\\neg\\neg P(x) \\to \\neg\\neg\\forall x P(x)),  \\]  with one prefixing ``\\(\\neg\\)'' removed. The theorem then follows from the well-known fact that DNS is intuitionistically not provable.  In conclusion we can infer that the defined notion of ``negative translation'' is too permissive if one wants to keep thinking of all negative translations as being intuitionistically equivalent.  Besides the main result outlined above, the paper may also be of interest to researchers studying negative translations because of the elementary and detailed exposition.","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$4503F106-C24B-4DBC-9E53-830E45B64661","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2024ee1f8ee71a3310fa31760e649693800bdaab","datavalue":{"value":{"entity-type":"item","numeric-id":450949,"id":"Q450949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$F80B1D10-D0F2-4B5B-B27A-DEE69F499874","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"4dd17e948ef0e266d136e969bf8283741afbd898","datavalue":{"value":"03F25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$9A3EA496-0B20-4B83-9FAA-889D28E0FCF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$EE730D9F-5089-407F-9DE6-AB2E3D28A6F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c06e0874e30722381d620ef69fb36c407a01cb04","datavalue":{"value":"03B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$1B30FC59-E060-459E-A897-DDA62C1E5EFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$04130C55-6964-4D49-AC64-F5F50E21DD94","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f83c9b0cacdb3462cdd1b041d183be86b512d5aa","datavalue":{"value":"6199442","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$CB7C58A8-36A6-406E-A793-6901390BB392","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9c692898122c448c23e56ede0af47d931c8a809c","datavalue":{"value":"double negation translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$C04B8498-C9C1-4FEA-8EA3-5DD027B8AE2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"80a57277e70500c09036fc170a87496fb3fdc5b5","datavalue":{"value":"Friedman-Dragalin A-translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$C3068975-1B5F-4202-9343-97B6D6DEB37D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ffd3928aa1fd818bc1a8806528172e266ac8bcc","datavalue":{"value":"classical logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$CC9F1038-9F59-4C8B-9891-2CB1A405DBA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$6111CBB6-F402-4EF8-AED9-1E03093C5DCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab7456a6500678da2c11297409c3d94f7b6af242","datavalue":{"value":"minimal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$DA01B894-BC47-43CB-899D-9EEACF385832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b38afb6a1f73c2390a409095d16aa67e02f9e90","datavalue":{"value":"double negation shift","type":"string"},"datatype":"string"},"type":"statement","id":"Q361872$6E785E9D-FA26-487B-8EED-F15369C883CA","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$78FE62F9-E5C7-480F-B0AA-EDAEA8A327D4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1b850e771264c8db5b1c2d2dd7e177051d714c9d","datavalue":{"value":"W2018523347","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$F4F8D3C4-0FF9-4FDE-8025-B68688F8E1D6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f2a6052e0491ab074fb920d9114f8bf05a781f1","datavalue":{"value":{"entity-type":"item","numeric-id":5421788,"id":"Q5421788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$772AAA3D-DFF3-4120-963B-435CBB273083","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52ea8498461ad98c2c25d2d3ae72c43b05174e53","datavalue":{"value":{"entity-type":"item","numeric-id":5957850,"id":"Q5957850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$F9D47374-1C7F-4B9A-8467-630C883B1713","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b317402d8df7a3aba3d161c369223f65efae4fd","datavalue":{"value":{"entity-type":"item","numeric-id":4225148,"id":"Q4225148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$03DB7525-396E-4E41-AA94-58D800F2E0D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b77280232c8e48c811a6e0d7a252126cbfae47","datavalue":{"value":{"entity-type":"item","numeric-id":3937386,"id":"Q3937386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$EE818C3E-7AA1-4758-B90A-5F8F92D59180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a9fa29d85b0fa6bb92ccad434bdf75276ac6ee7","datavalue":{"value":{"entity-type":"item","numeric-id":580343,"id":"Q580343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$FF601BB8-0F78-4FDB-98C4-3DA03843C69B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ae07805a76a77b05d8f39024fc85ed8898d802a","datavalue":{"value":{"entity-type":"item","numeric-id":4774024,"id":"Q4774024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$71C95F16-F7FE-474C-8639-DBABA4B14B88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5124a39f12a6e4b215f2f99cc495a24e8ff91ad","datavalue":{"value":{"entity-type":"item","numeric-id":3753978,"id":"Q3753978"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$BC7B2C3D-8739-4671-B154-A8AE237914EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4abb670df6f5a721581efd6381b449049864bddb","datavalue":{"value":{"entity-type":"item","numeric-id":4939409,"id":"Q4939409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$1361D7A1-B029-4C09-9E34-235DF6B0BB47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62728de11085b2637852fd5b2e4cd2194b3b9d02","datavalue":{"value":{"entity-type":"item","numeric-id":923069,"id":"Q923069"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$D8333A18-126E-43FB-BC40-62570B3E03A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f5f4acd56522c4d0768c024603aed4365179f67","datavalue":{"value":{"entity-type":"item","numeric-id":5803251,"id":"Q5803251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$55C9EBD8-0C4D-4564-A3D7-3DAC31B46606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1bec9637dba5e8307ef3ad4b6a5c2e0405240f9","datavalue":{"value":{"entity-type":"item","numeric-id":3437042,"id":"Q3437042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$37260B12-499B-403A-BFF8-A5C236A7F86E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db7629881c3e7bd88e597d7e4f26d7cbdf6a97ce","datavalue":{"value":{"entity-type":"item","numeric-id":4240152,"id":"Q4240152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$A0E6E4F8-D2EC-4285-ABE8-081A45458CB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$3A948EB8-5C93-41F5-8A50-53E8A1F352BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d306fe5453e13dac5aace6f82668ff9863de3fd","datavalue":{"value":{"entity-type":"item","numeric-id":5904363,"id":"Q5904363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$B5FA8B6D-F614-4357-BEB2-BBC1EEA158E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c89d163ec2cfe20cdcef09243a785a3cf35ab8f","datavalue":{"value":{"entity-type":"item","numeric-id":5573940,"id":"Q5573940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q361872$1E32611C-7D30-4DEA-A420-B649485CD79E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4e238cd22d27844d0822dbb46b2d86b77e39fb0d","datavalue":{"value":"10.1007/S11225-011-9367-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q361872$4D0B648E-2175-4107-BF52-8AE085DB913B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4db4b79dec7ac775e490e66bd71a0c55c15e63c5","datavalue":{"value":{"entity-type":"item","numeric-id":4964696,"id":"Q4964696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"494c28934dd8d9c678397987742fa64ee583950c","datavalue":{"value":{"amount":"+0.8626089692115784","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q361872$934D5122-05BD-4A21-B4A1-90E5898CB442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e3db21f583ac0e09155b3d2c57606588a5291fb","datavalue":{"value":{"entity-type":"item","numeric-id":5499598,"id":"Q5499598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74aa3d8a32c31f7d88f10add7710d9f0477acc63","datavalue":{"value":{"amount":"+0.8588926792144775","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q361872$38437F72-E8C9-4065-A4AC-7E38FA236A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"88d5cd98e0a10d85bbe4e6263f5862cd277cf22c","datavalue":{"value":{"entity-type":"item","numeric-id":4981448,"id":"Q4981448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccc6748d855c205cf6f6a32ce386db9357975627","datavalue":{"value":{"amount":"+0.8565993905067444","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q361872$623F63FB-921F-4E75-973A-5938830F39CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec4663357b8fc5fd7c6d37f5792c4f5d07487ddc","datavalue":{"value":{"entity-type":"item","numeric-id":5111325,"id":"Q5111325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"850fcc247798e35d66fb4f3f16a09950b458a837","datavalue":{"value":{"amount":"+0.8257558345794678","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q361872$ECB7DF0E-9F91-4BD5-85E1-A13315D8D200","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e675133ee67b4d4d550551ea030551afcaada9d4","datavalue":{"value":{"entity-type":"item","numeric-id":3080095,"id":"Q3080095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"764c345fa4b7677405916bee6ab3b83290db59b4","datavalue":{"value":{"amount":"+0.8149059414863586","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q361872$7F064C1F-6AD8-4ADA-8368-42A0B0904249","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Negative translations not intuitionistically equivalent to the usual ones","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Negative_translations_not_intuitionistically_equivalent_to_the_usual_ones"}}}}}