Skip to content

[FEATURE] Quantifier Scope and Relational Calculus Identifier #263

@mathematicswizard

Description

@mathematicswizard

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.

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