Wikidata:Property proposal/implies

implies

Originally proposed at Wikidata:Property proposal/Natural science

   Done: generalization of (P7719) (Talk and documentation)

Description	statement whose truth is implied by this statement
Represents	logical implication (Q7881229)
Data type	Item
Domain	item of type proposition (Q108163)
Allowed values	item of type proposition (Q108163)
Example 1	generalized Poincaré conjecture (Q5532452) → Poincaré conjecture (Q203586)
Example 2	Szpiro's conjecture (Q829242) → Fermat's Last Theorem (Q132469)
Example 3	Tate conjecture (Q7687975) → Standard Conjectures on Algebraic Cycles (Q7598336)
Source	used in https://en.wikipedia.org/wiki/Template:Infobox_mathematical_statement (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 jobs	ideally migrating the data from existing mathematical statement infoboxes: https://en.wikipedia.org/w/index.php?title=Special%3AWhatLinksHere&target=Template%3AInfobox+mathematical+statement&namespace=0

Motivation

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)

Discussion

•  Support. Nomen ad hoc (talk) 18:05, 24 November 2019 (UTC).
•  Support David (talk) 15:16, 25 November 2019 (UTC)
•  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)

• @ArthurPSmith, A3nm: some previous discussion here: Wikidata:Property_proposal/Implies_(necessary_condition). − Pintoch (talk) 09:26, 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)

Opensofias
Tobias1984
Arthur Rubin
Cuvwb
TomT0m
Physikerwelt
Lymantria
Bigbossfarin
Infovarius
Helder
PhilMINT
Malore
Lore.mazza51
Wikisaurus
The Anome
The-erinaceous-one
Daniel Mietchen
Haansn08
Xenmorpha
John Samuel
Jeremy Dover
Toni 001
Bocardodarapti
Duckmather
HTinC23
fgnievinski

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)
•  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)
•  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)
•  Support --opensofias (talk) 15:10, 10 December 2019 (UTC)
•  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: generalization of (P7719). − Pintoch (talk) 07:02, 12 December 2019 (UTC)