Wikidata:Property proposal/implies

From Wikidata
Jump to navigation Jump to search


Originally proposed at Wikidata:Property proposal/Natural science

   Done: implies (P7719) (Talk and documentation)
Descriptionstatement whose truth is implied by this statement
Representslogical implication (Q7881229)
Data typeItem
Domainitem of type proposition (Q108163)
Allowed valuesitem of type proposition (Q108163)
Example 1Generalized Poincaré conjecture (Q5532452)Poincaré conjecture (Q203586)
Example 2Szpiro's conjecture (Q829242)Fermat's Last Theorem (Q132469)
Example 3Tate conjecture (Q7687975)Standard conjectures on algebraic cycles (Q7598336)
Sourceused in (argument "consequences" gives "implies" facts, arguments "generalizations" and "implied by" give reverse "implies" facts, argument "equivalent to" gives "implies" facts in both directions
Robot and gadget jobsideally migrating the data from existing mathematical statement infoboxes:


The mathematical statement infobox on Wikipedia has fields for statements implied by another statement, or which imply another statement. I'd like to be able to use this property on Wikidata. In terms of constraints, the property is transitive (if A implies B and B implies C then A implies C), and it may make sense to create the reverse property "implied by". This property could make sense also outside of mathematics, if we have items about non-mathematical statements. A3nm (talk) 08:52, 24 November 2019 (UTC)


  • Symbol support vote.svg Support. Nomen ad hoc (talk) 18:05, 24 November 2019 (UTC).
  • Symbol support vote.svg Support David (talk) 15:16, 25 November 2019 (UTC)
  • Pictogram voting comment.svg Comment Don't we already have a property that does this? I'm sure I remember at least a property proposal along these lines before. On the proposal itself, aren't there often contexts/conditions or other theorems that are usually there as part of an implication? Or would this only be for where one conceptually completely subsumes the other? ArthurPSmith (talk) 20:48, 25 November 2019 (UTC)
@ArthurPSmith: I'm thinking of cases when one completely subsumes the other, e.g., Generalized Poincaré conjecture (Q5532452) vs Poincaré conjecture (Q203586). --A3nm (talk) 13:34, 28 November 2019 (UTC)
Thanks @Pintoch: for the pointers! I guess I hadn't realized that there is indeed some leeway in how you formally define that something is a consequence of something else. How about "A implies B" means "B has an extremely short proof when assuming A"? I understand that's a bit subjective if you look closely... but I'm thinking there should really be some semantic link between Generalized Poincaré conjecture (Q5532452) and Poincaré conjecture (Q203586)... --A3nm (talk) 13:34, 28 November 2019 (UTC)
We can probably also accept the fuzziness of this notion - after all most Wikidata properties are not defined mathematically. I don't think anyone is pretending we can build a proof assistant on top of Wikidata anyway! We could perhaps require references on these statements (to claim that A implies B, provide a reference to a source which derives B from A)… − Pintoch (talk) 16:04, 28 November 2019 (UTC)

Arthur Rubin
Nomen ad hoc
Pictogram voting comment.svg Notified participants of WikiProject Mathematics

  • Pinging project to make sure we get enough eyeballs on this. − Pintoch (talk) 20:11, 9 December 2019 (UTC)
  • Let's take for example string theory (Q33198). It requires supersymmetry (Q193442) to hold. Yet supersymmetry does not require string theory, if I am not mistaken. So one could state Q33198 implies (P?) Q193442− PhilMINT (talk) 21:35, 9 December 2019 (UTC)
  • Pictogram voting comment.svg Comment I tend to oppose this proposal. Are we aware that all proven theorems imply each other and that all proposition (Q108163) are implied by a false one like Mertens conjecture (Q2600201) - which is indeed disproven? Lymantria (talk) 21:52, 9 December 2019 (UTC)
    • Yes, it is clear that we cannot give this property a mathematical meaning, but there seems to be interest in an intuitive version of it. Just like most other Wikidata properties, actually! − Pintoch (talk) 13:14, 11 December 2019 (UTC)
  • Symbol support vote.svg Support. I'm not active on Wikidata, but there are cases in mathematics in which "A implies B" is really appropriate, not just "B is obvious from A" (for sufficiently weird values of "obvious"). Examples include Axiom of Choice implies Axiom of dependent choice (when we are talking about different models of w:set theory), and normal implies regular (for different topological spaces). (Please feel free to change my examples to {{Q}} entries.) Arthur Rubin (talk) 22:04, 9 December 2019 (UTC)
  • Symbol support vote.svg Support --opensofias (talk) 15:10, 10 December 2019 (UTC)
  • Pictogram voting comment.svg Comment this now looks reasonably well supported, so I will create this property soon. − Pintoch (talk) 13:14, 11 December 2019 (UTC)

@ديفيد عادل وهبة خليل 2, Nomen ad hoc, ArthurPSmith, Arthur Rubin, A3nm, Lymantria: @Opensofias, PhilMINT: ✓ Done: implies (P7719). − Pintoch (talk) 07:02, 12 December 2019 (UTC)