Order of quantifiers

In the original team submission it is stated:

"If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials."

As a consequence, the formulae @forAll <#h>. @forSome <#g>. <#g> <#loves> <#h> . @forSome <#g>. @forAll <#h>. <#g> <#loves> <#h> . have the exact same meaning, namely:

means

for all h

for some g

 g loves h

("Every has someone who loves them" rather than "Somebody loves everybody")

or

∀h(∃g(loves(g,h))

Problems

• this behaviour might be confusing for users especially if they are used to other logics including explicit quantification where this reordering of quantifiers does not take place
• to make statements where the scope of universal quantification is outside the scope of existential quantification, auxiliary constructs need to be used. For example, "Somebody loves everybody" could be expressed as @forSome <#g>. {}=>{@forAll <#h>. <#g> <#loves> <#h> }. this is very cumbersome

Advantages

• quantifiers behave like triples in the sense that their exact position on one nesting level does not matter.

Options

1. Keep the current semantics and the automatic reordering of quantifiers

2. Keep the current semantics but only allow quantifiers at the beginning of each formula and only in a fixed order such that it is not even possible to state universal quantification after existential quantification.

3. Interpret the quantifiers in the order they occur like it is for example done in FOL

Pros

• the interpretations of quantifiers gets less confusing for the user
• even without "syntactic tricks" (see above) the language gets quite expressive

Cons

• the expressiveness could make the logic difficult to implement