- Notifications
You must be signed in to change notification settings - Fork 51
Description
Currently, the quantifier's scope is by default till the end of the string - if there are no parentheses. Meaning, for instance, that:
\forall x.P(x)\rightarrow Q(x)
Is parsed as:
["ForAll", "x", ["To",["InvisibleOperator", "P", ["Delimiter", "x"]], ["InvisibleOperator", "Q", ["Delimiter", "x"]]]
But in fact, in many First Order Logic conventions, the quantified expression is the following immediately after the "such as" (dot, vertical line etc') or if a delimiter follows then all the expression under that delimiter.
Hence for \forall x.P(x)\rightarrow Q(x) - we would expect:
["To", ["ForAll", "x", ["InvisibleOperator", "P", ["Delimiter", "x"]]], ["InvisibleOperator", "Q", ["Delimiter", "x"]]]]
The second problem is that in language of First Order Logic, Capital Latin Letters designate a relational symbol. So, instead of the MathJSON above produced of \forall x.P(x)\rightarrow Q(x) we would want:
["To", ["ForAll", "x", ["P","x"]], ["Q","x"]]