Skip to content

[FEATURE] Quantifier Scope and Relational Calculus Identifier #263

@mathematicswizard

Description

@mathematicswizard

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"]]

Metadata

Metadata

Assignees

No one assigned

    Labels

    featureNew feature or enhancement

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions