Property talk:P7719
Documentation
the subject statement in particular gives this object statement, or the truth of this object statement is implied by the truth of the subject statement
| Represents | logical implication (Q7881229) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Data type | Item | |||||||||
| Domain | proposition (Q108163) or algorithm (Q8366) | |||||||||
| Example | law of cosines (Q164321) → Pythagorean theorem (Q11518) | |||||||||
| Lists |
| |||||||||
| Proposal discussion | Proposal discussion | |||||||||
| Current uses |
| |||||||||
| Search for values |
List of violations of this constraint: Database reports/Constraint violations/P7719#Entity types
List of violations of this constraint: Database reports/Constraint violations/P7719#Scope, SPARQL
Change label to clarify usage edit
Notified participants of WikiProject Mathematics
This property looks like it could use some love. It only has 13 uses right now. I think it is hard to use because it is vaugely defined and combines two different concepts that are not (formally) what mathematicians mean by "implies". Looking through the uses [1], I see that P7719 is most often used in cases where a statement A is a more general statement of B, which (informally) means A"implies"B. Alternatively, P7719 is used occasionally as "proof""has conclusion""conclusion" (this usage is only on proofs of Fermat's little theorem (Q467602) and Proofs of Fermat's theorem on sums of two squares (Q16249614), as far as I see).
Before I found this property, I was considering making a new "is generalization of" property to model A"is generalization of"B, but P7719 is already filling that roll. Thus, I propose that we relabel P7719 to "is generalization of" (or "generalizes"), move "implies" to an alias, and split off usages in the form "proof""has conclusion""conclusion" into to a new, dedicated "conlusion" property (or find another way to model that relationship).
@A3nm, Pintoch, ArthurPSmith, PhilMINT, Lymantria: You all contributed to the property proposal so I want to bring you into the loop. The-erinaceous-one (talk) 07:18, 15 September 2020 (UTC)
- I just noticed one more type of usage: axiom of choice (Q179692)generalization of (P7719)equivalent of the axiom of choice (Q4478785) uses P7719 to mean "equivalent to" (i.e. Q179692 implies Q4478785 and Q4478785 implies Q179692). In this cases, P7719 is actually used in the mathematical sense of "implies" because the implication goes both ways we get that Q179692 is true if and only if Q4478785 is true. I don't know how often that use case occurs, but I thought I'd mention it; perhaps it merits a property too (or maybe said to be the same as (P460) can be used). The-erinaceous-one (talk) 07:28, 15 September 2020 (UTC)
- Hi The-erinaceous-one, what you are proposing makes complete sense to me. In fact maybe the "implies" relationship should be reserved to axioms (as in "you can prove one from the other"), with equivalence being bidirectional implication; and there would indeed be a relation "is generalization of" for results, and also a relation "proof proves result" as you are proposing. If you wish, you can propose the creation of these properties. That said, it won't solve the usage problem. One idea I had mentioned in the property creation proposal was to migrate things from the Template:Infobox mathematical statement on Wikipedia [2], which sometimes has a field "Consequences". --A3nm (talk) 12:22, 15 September 2020 (UTC)
- I don't have any strong feelings on this, especially given the low usage right now. I guess my preference would be to, if renaming is required, do so in a way that will allow maximum use of the property. "is generalization of" sounds ok to me, with "implies" as an alias. I think it would be fine to leave it for axiomatic cases where the relation is symmetric. ArthurPSmith (talk) 12:54, 15 September 2020 (UTC)
- @A3nm, ArthurPSmith: Since there were no objections, I made the edits. What is the best way to get the changes translated? The-erinaceous-one (talk) 08:28, 17 September 2020 (UTC)
- Thanks The-erinaceous-one for editing. I'm afraid I'm not familiar enough with Wikidata to know about translations, sorry. :-/ Best --A3nm (talk) 09:15, 17 September 2020 (UTC)
- The-erinaceous-one : isn’t there an ambiguity in the label here too since generalising a theory, for example, can mean « the same theory with less axioms/property » so that theorems in the specialised version may not hold in the more general one ? author TomT0m / talk page 11:23, 27 February 2022 (UTC)