Wikidata

Wikidata:Property proposal/Implies (necessary condition)

< Wikidata:Property proposal

Logically implies (necessary condition) edit

Originally proposed at Wikidata:Property proposal/Generic

   Not done
DescriptionNecessary condition, i.e. logical consequence of a mathematical statement
RepresentsLogical consequence (Q374182), requirement (Q774228)
Data typeMathematical expression
DomainMaxwell's equations (Q51501)
Allowed valuesMathematical theorems (or other mathematical laws e.g. from theoretical physics)
ExampleMaxwell's equations (Q51501) =>(P?) Coulomb's law (Q83152)
Sourcehttps://en.wikipedia.org/wiki/Logical_consequence
Planned useconnect physics theorems / axioms by logical relation to annotate constraints / necessary conditions
Robot and gadget jobsshould be allowed

Motivation

My vision is to enable creating a logically structured semantic network of mathematical theorems (starting with theoretical physics). This would allow researchers to quickly grasp the constraints of the formulae (Wikidata items) they are working on, the framework they are working in. A theorem / formula (Wikidata item) is falsified already if one of its necessary conditions turns out to be falsified. Thus it is vital to know them, in order to prevent mathematical researchers from wasting their time working on something that may be invalid.  – The preceding unsigned comment was added by PhilMINT (talk • contribs) at February 19, 2018‎ (UTC).

Discussion

  •   Support @PhilMINT: This is an interesting proposal - unfortunate that it seems to have gotten lost. I believe the datatype should be item, not "formula" (your example follows that pattern). I don't particularly like the parenthetical label - you can add that as an alias. Perhaps to be clearer the main English label should be "logically implies"? ArthurPSmith (talk) 20:30, 13 September 2018 (UTC)[reply]
  • Conditional   Support. I agree that the datatype should be item. I think this property could be useful, although I don't know how many interesting theorems imply other interesting theorems outright, rather than imply in the context of plausible background assumptions. The "source" will be different secondary and textbook sources depending on the relation claimed. "Domain" is another field that seems to be filled in incorrectly: the domain of this property should be something like mathematical object (Q246672) or proposition (Q108163): we need a clear decision on what the domain will be. MartinPoulter (talk) 10:10, 19 September 2018 (UTC)[reply]
  •   Comment(s) I also included this in Invalid topic given
       Under discussion
    DescriptionMISSING
    Data typeMISSING
    Example 1MISSING
    Example 2MISSING
    Example 3MISSING
    in the maths section.     Interesting proposal. I’d propose to add qualifiers to add the necessary axiom and logic in which the implication is valid (eg. some implications are true under ZFC but fot in ZF, or true in first order logic but not in a substructural one). But this needs more development : Banach–Tarski paradox (Q737851) is a logical consequence of ZFC, ie. it is a theorem of ZFC. Specifically, commenting your example, if we consider Maxwell equation an axiomatic system, does not this simply state that Coulomb’s law are a theorem of the Maxwell theory in first order logic ? This is what a logician would tell. In that spirit, I’d complete the proposal with the following properties and/or qualifier that might be needed in a context of mathematical logic like the refinement around the different logics and axiom-set. Please feel free to discuss the best models for the different combinations. For example it might be better to create a « theorem of » property with a theory range « Coulomb's law theorem of Maxwell equation (in first order logic) » considering maxwell equation as a logical theory. author  TomT0m / talk page 14:40, 3 October 2018 (UTC)[reply]
  •   Weak oppose - I agree with the comments above that from a logical perspective this is pretty ill defined. It is likely to be misused because of that, I would say. It is not the proposal's fault at all - I just don't think there is a way to represent this sort of knowledge in a natural way in Wikidata's data model. Perhaps this could be narrowed down to a smaller scope which would make it well defined. − Pintoch (talk) 23:02, 13 January 2019 (UTC)[reply]
  •   Oppose The notion "Implies" is not well-defined for mathematical theorems. If "implies" means Material conditional then, formally all theorems implies each other. If "implies" means "can be derived from", then it is not well-defined: one textbook may fist prove theorem A and then prove theorem B as a corollary of A, other textbook may go the opposite way. It is not well-defined for physical theories either. Are Kepler's laws a corollary of Newton's law of gravity or other way around? Historically, Newton's law was deduced from Kepler's laws, which are based on observation, but one can argue that Newton's law is more "fundamental", and Kepler's laws are just an implication. But mathematically they just two equivalent ways to describe planetary motion. Finally, if "Implies" means "necessary condition", then it is well defined, but we don't have wikidata elements that represent conditions. We have wikidata elements that represent sets, but for sets we have: subclass of: e.g. rhombus is subclass of parallelogram. Alexei Kopylov (talk) 18:18, 12 May 2019 (UTC)[reply]

logic and axiom system edit

Originally proposed at Wikidata:Property proposal/Generic

   Not done
DescriptionNecessary condition, i.e. logical consequence of a mathematical statement
Representslogical system (Q17488292)      -- or specifically the set of rule of inference (Q1068763) (resp. rule of inference (Q1068763) - the set of axiom or logical theory)
Data typeItem
Domainqualifier of « implies » statement (the previous proposal), maybe useful elsewhere
Allowed valueslogical system (Q17488292)      (resp rule of inference (Q1068763) - the set of axiom or logical theory)
Example 1
⟨ Banach–Tarski paradox (Q737851) ⟩ theorem of Search ⟨ ZFC set theory ⟩
logic Search ⟨ Q4055684 ⟩
Example 2Something with a higher order logic theorem : Courcelle's theorem (Q5178114). What is the best way to model ?
Example 3Something with a weaker logic : Markov's principle (Q3922074) that is true in a weaker logic than classical logic but is not obvious. What is the best way to model ? This article discusses the different axioms we can choose in an intuitionistic logic : http://math.fau.edu/lubarsky/Separating%20LLPO.pdf
Robot and gadget jobsshould be allowed
discussion edit

These properties or qualifiers are useful to model en:Deductive_system used to derive the theorems, but there may be terminology issues and different way to model this, so this is only a proposition starting point that needs to be discussed and amended. Taking into account the axiom and inference rules leads to the difficulty that complete logical systems includes the two and that items topic often implies the inference rules used. We already have some properties for logic like admissible in Search to link inference rules to logic, for example, but it’s not enough obviously) author  TomT0m / talk page 14:40, 3 October 2018 (UTC)[reply]

@MartinPoulter, ArthurPSmith, PhilMINT:

  Notified participants of WikiProject Mathematics author  TomT0m / talk page 14:44, 3 October 2018 (UTC)[reply]

  •   Comment I don't have any strong opinion on this. How many different logic/axiom systems are there? And aren't those two different things anyway? Maybe we already have a qualifier that can capture this appropriately? ArthurPSmith (talk) 18:51, 5 October 2018 (UTC)[reply]
  •   Comment This proposal is more sound than previous one. One axiom system may be a weaker or stronger than the other, and a theorem may be proved in one axiom system and not proved in other. We may want to represent this in wikidata. But the proposal is not finished. It misses a clear description what exactly is proposed. Also note that there are different relations between logical theories, e.g., Conservative extension (Q864213). Alexei Kopylov (talk) 18:34, 12 May 2019 (UTC)[reply]
Retrieved from "https://www.wikidata.org/w/index.php?title=Wikidata:Property_proposal/Implies_(necessary_condition)&oldid=941000370"