Issue with 5 First-order_logic

[philsMINT]

what about the scope of \forall quantors? position vertically instead of horizontally? Link to First-order_logic, qID 5

[physikerwelt]

There is http://www.w3.org/TR/MathML3/chapter4.html#contm.forall we should ensure that the generated MathML is according to this spec.

[physikerwelt]

See also http://dlmf.nist.gov/LaTeXML/manual/customization/customization.latexml.html#SS1.SSS0.Px1 for details on the macro creation.

[philsMINT]

tree looks good! macro \forallscope not used, delete?

[physikerwelt]

@philsMINT the tree does not look good. There is no \times in the formulae.

[philsMINT]

where do we need \times? the tree seems now to be branched logically correctly (even without using my macro \forallscope - should I delete it?)

[physikerwelt]

@philsMINT I don't understand your question. The MathML, we currently visualize has times in it which is incorrect.

<math xmlns="http://www.w3.org/1998/Math/MathML"
      xmlns:xlink="http://www.w3.org/1999/xlink"
      alttext="\forall x\,\forall y\,P(x,y)\Leftrightarrow\forall y\,\forall x\,P(x,y)"
      class="ltx_Math"
      display="inline"
      id="p1.1.m1.1">
  <semantics id="p1.1.m1.1a">
      <mrow id="p1.1.m1.1.26" xref="p1.1.m1.1.26.cmml">
         <mrow id="p1.1.m1.1.26.1" xref="p1.1.m1.1.26.1.cmml">
            <mo id="p1.1.m1.1.1" xref="p1.1.m1.1.1.cmml">∀</mo>
            <mrow id="p1.1.m1.1.26.1.1" xref="p1.1.m1.1.26.1.1.cmml">
               <mpadded id="p1.1.m1.1.2" width="+1.7pt" xref="p1.1.m1.1.2.cmml">
                  <mi id="p1.1.m1.1.2a" xref="p1.1.m1.1.2.cmml">x</mi>
               </mpadded>
               <mo id="p1.1.m1.1.26.1.1.1" xref="p1.1.m1.1.26.1.1.1.cmml">⁢</mo>
               <mrow id="p1.1.m1.1.26.1.1.2" xref="p1.1.m1.1.26.1.1.2.cmml">
                  <mo id="p1.1.m1.1.4" xref="p1.1.m1.1.4.cmml">∀</mo>
                  <mrow id="p1.1.m1.1.26.1.1.2.1" xref="p1.1.m1.1.26.1.1.2.1.cmml">
                     <mpadded id="p1.1.m1.1.5" width="+1.7pt" xref="p1.1.m1.1.5.cmml">
                        <mi id="p1.1.m1.1.5a" xref="p1.1.m1.1.5.cmml">y</mi>
                     </mpadded>
                     <mo id="p1.1.m1.1.26.1.1.2.1.1" xref="p1.1.m1.1.26.1.1.2.1.1.cmml">⁢</mo>
                     <mrow id="p1.1.m1.1.26.1.1.2.1.2.2" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">
                        <mi id="p1.1.m1.1.7" xref="p1.1.m1.1.7.cmml">P</mi>
                        <mo id="p1.1.m1.1.26.1.1.2.1.2.2a" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">⁡</mo>
                        <mrow id="p1.1.m1.1.26.1.1.2.1.2.2.1" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">
                           <mo id="p1.1.m1.1.8"
                               stretchy="false"
                               xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">(</mo>
                           <mi id="p1.1.m1.1.9" xref="p1.1.m1.1.9.cmml">x</mi>
                           <mo id="p1.1.m1.1.10" xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">,</mo>
                           <mi id="p1.1.m1.1.11" xref="p1.1.m1.1.11.cmml">y</mi>
                           <mo id="p1.1.m1.1.12"
                               stretchy="false"
                               xref="p1.1.m1.1.26.1.1.2.1.2.1.cmml">)</mo>
                        </mrow>
                     </mrow>
                  </mrow>
               </mrow>
            </mrow>
         </mrow>
         <mo id="p1.1.m1.1.13" xref="p1.1.m1.1.13.cmml">⇔</mo>
         <mrow id="p1.1.m1.1.26.2" xref="p1.1.m1.1.26.2.cmml">
            <mo id="p1.1.m1.1.14" xref="p1.1.m1.1.14.cmml">∀</mo>
            <mrow id="p1.1.m1.1.26.2.1" xref="p1.1.m1.1.26.2.1.cmml">
               <mpadded id="p1.1.m1.1.15" width="+1.7pt" xref="p1.1.m1.1.15.cmml">
                  <mi id="p1.1.m1.1.15a" xref="p1.1.m1.1.15.cmml">y</mi>
               </mpadded>
               <mo id="p1.1.m1.1.26.2.1.1" xref="p1.1.m1.1.26.2.1.1.cmml">⁢</mo>
               <mrow id="p1.1.m1.1.26.2.1.2" xref="p1.1.m1.1.26.2.1.2.cmml">
                  <mo id="p1.1.m1.1.17" xref="p1.1.m1.1.17.cmml">∀</mo>
                  <mrow id="p1.1.m1.1.26.2.1.2.1" xref="p1.1.m1.1.26.2.1.2.1.cmml">
                     <mpadded id="p1.1.m1.1.18" width="+1.7pt" xref="p1.1.m1.1.18.cmml">
                        <mi id="p1.1.m1.1.18a" xref="p1.1.m1.1.18.cmml">x</mi>
                     </mpadded>
                     <mo id="p1.1.m1.1.26.2.1.2.1.1" xref="p1.1.m1.1.26.2.1.2.1.1.cmml">⁢</mo>
                     <mrow id="p1.1.m1.1.26.2.1.2.1.2.2" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">
                        <mi id="p1.1.m1.1.20" xref="p1.1.m1.1.20.cmml">P</mi>
                        <mo id="p1.1.m1.1.26.2.1.2.1.2.2a" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">⁡</mo>
                        <mrow id="p1.1.m1.1.26.2.1.2.1.2.2.1" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">
                           <mo id="p1.1.m1.1.21"
                               stretchy="false"
                               xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">(</mo>
                           <mi id="p1.1.m1.1.22" xref="p1.1.m1.1.22.cmml">x</mi>
                           <mo id="p1.1.m1.1.23" xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">,</mo>
                           <mi id="p1.1.m1.1.24" xref="p1.1.m1.1.24.cmml">y</mi>
                           <mo id="p1.1.m1.1.25"
                               stretchy="false"
                               xref="p1.1.m1.1.26.2.1.2.1.2.1.cmml">)</mo>
                        </mrow>
                     </mrow>
                  </mrow>
               </mrow>
            </mrow>
         </mrow>
      </mrow>
      <annotation-xml encoding="MathML-Content" id="p1.1.m1.1b">
         <apply id="p1.1.m1.1.26.cmml" xref="p1.1.m1.1.26">
            <ci id="p1.1.m1.1.13.cmml" xref="p1.1.m1.1.13">⇔</ci>
            <apply id="p1.1.m1.1.26.1.cmml" xref="p1.1.m1.1.26.1">
               <csymbol cd="latexml" id="p1.1.m1.1.1.cmml" xref="p1.1.m1.1.1">for-all</csymbol>
               <apply id="p1.1.m1.1.26.1.1.cmml" xref="p1.1.m1.1.26.1.1">
                  <times id="p1.1.m1.1.26.1.1.1.cmml" xref="p1.1.m1.1.26.1.1.1"/>
                  <ci id="p1.1.m1.1.2.cmml" xref="p1.1.m1.1.2">𝑥</ci>
                  <apply id="p1.1.m1.1.26.1.1.2.cmml" xref="p1.1.m1.1.26.1.1.2">
                     <csymbol cd="latexml" id="p1.1.m1.1.4.cmml" xref="p1.1.m1.1.4">for-all</csymbol>
                     <apply id="p1.1.m1.1.26.1.1.2.1.cmml" xref="p1.1.m1.1.26.1.1.2.1">
                        <times id="p1.1.m1.1.26.1.1.2.1.1.cmml" xref="p1.1.m1.1.26.1.1.2.1.1"/>
                        <ci id="p1.1.m1.1.5.cmml" xref="p1.1.m1.1.5">𝑦</ci>
                        <apply id="p1.1.m1.1.26.1.1.2.1.2.1.cmml" xref="p1.1.m1.1.26.1.1.2.1.2.2">
                           <csymbol cd="wikidata" id="p1.1.m1.1.7.cmml" xref="p1.1.m1.1.7">Q1144319</csymbol>
                           <ci id="p1.1.m1.1.9.cmml" xref="p1.1.m1.1.9">𝑥</ci>
                           <ci id="p1.1.m1.1.11.cmml" xref="p1.1.m1.1.11">𝑦</ci>
                        </apply>
                     </apply>
                  </apply>
               </apply>
            </apply>
            <apply id="p1.1.m1.1.26.2.cmml" xref="p1.1.m1.1.26.2">
               <csymbol cd="latexml" id="p1.1.m1.1.14.cmml" xref="p1.1.m1.1.14">for-all</csymbol>
               <apply id="p1.1.m1.1.26.2.1.cmml" xref="p1.1.m1.1.26.2.1">
                  <times id="p1.1.m1.1.26.2.1.1.cmml" xref="p1.1.m1.1.26.2.1.1"/>
                  <ci id="p1.1.m1.1.15.cmml" xref="p1.1.m1.1.15">𝑦</ci>
                  <apply id="p1.1.m1.1.26.2.1.2.cmml" xref="p1.1.m1.1.26.2.1.2">
                     <csymbol cd="latexml" id="p1.1.m1.1.17.cmml" xref="p1.1.m1.1.17">for-all</csymbol>
                     <apply id="p1.1.m1.1.26.2.1.2.1.cmml" xref="p1.1.m1.1.26.2.1.2.1">
                        <times id="p1.1.m1.1.26.2.1.2.1.1.cmml" xref="p1.1.m1.1.26.2.1.2.1.1"/>
                        <ci id="p1.1.m1.1.18.cmml" xref="p1.1.m1.1.18">𝑥</ci>
                        <apply id="p1.1.m1.1.26.2.1.2.1.2.1.cmml" xref="p1.1.m1.1.26.2.1.2.1.2.2">
                           <csymbol cd="wikidata" id="p1.1.m1.1.20.cmml" xref="p1.1.m1.1.20">Q1144319</csymbol>
                           <ci id="p1.1.m1.1.22.cmml" xref="p1.1.m1.1.22">𝑥</ci>
                           <ci id="p1.1.m1.1.24.cmml" xref="p1.1.m1.1.24">𝑦</ci>
                        </apply>
                     </apply>
                  </apply>
               </apply>
            </apply>
         </apply>
      </annotation-xml>
      <annotation encoding="application/x-tex" id="p1.1.m1.1c">\forall x\,\forall y\,P(x,y)\Leftrightarrow\forall y\,\forall x\,P(x,y)</annotation>
  </semantics>
</math>