-
Notifications
You must be signed in to change notification settings - Fork 52
Description
There are 2 problems regarding First Order Logic Formulas
1. Quantifiers Scope
Currently, the quantifier's scope defaults to the end of the string if there are no parentheses. Meaning, for instance, the following formula:
\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 ONLY the WFF following immediately after the "such as" (dot, vertical line etc'); 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"]]]]
We would get that MathJSON if we would write (\forall x.P(x))\rightarrow Q(x)
2. Representing Atomic Formulas in FOL
The second problem is that in the language of First Order Logic, Capital Latin Letters designate a relational symbol and with them we create the atomic proposition in FOL, for instance P(x). But, as we saw in MathJSON above produced for \forall x.P(x)\rightarrow Q(x) there is an InvisibleOperator involved. But this in way a multiplication. We would want to represent atomic propositions in FOL with MathJSON.