3 ms·

I’m not sure what a trivial existential quantifier is, but an existential quantifier is the statement ‘there exists’, usually written ∃.

• marcosdumay 7y ago
  The 'for all' statement is also an existential quantifier, as is the 'this one value' statement implicit on the imperative statements. The entire meat of the article depends on this concept of "non-trivial" quantifier.
  • bawolff 7y ago
    Umm, isnt the universal quantifier by definition not the existential qualifier?
  • disconcision 7y ago
    From the comments, it seems likely that the author doesn't have a precise definition of non-trivial. But the framework still feels potentially useful as a way to precisely parameterize disagreements about whether or not a given semantics is declarative. That said, I'm also having some trouble with the concept. Take for example the rule: there exists x such that succ(x) = y ⊢ dec(y) = x. If we're used to operational semantics which include pattern matching, this feels trivial. But otherwise we have to be clever to avoid exhaustive search. I'm a bit out of my depth here, but it sort-of feels like 'non-trivial' here means 'I can't immediately/uniquely produce a corresponding well-moded operational semantics'. Whether this lends any clarity might be a matter of taste...
  • JadeNB 7y ago
    > The 'for all' statement is also an existential quantifier, as is the 'this one value' statement implicit on the imperative statements. If you're making a technical claim, rather than some informal claim whose meaning I'm missing, then "for all" is a universal, not an existential, quantifier. The truth of universal quantification over an empty set is an important part of predicate logic.