Comment by tmerr

I might be corrupted by programming because it doesn't bother me when I hear a vacuously true claim like "All flying horses are three-legged". My mental model corresponds to Python's definition of "all":

    def all(xs, predicate):
        for x in xs:
            if not predicate(x):
                return False
        return True

Similarly,

    def any(xs, predicate):
        for x in xs:
            if predicate(x):
                return True
        return False

You say "Ex falso quodlibet" which makes it sound like you believe such a system leads to contradictions, but this would come down to the choice of rewrite rules.

Example: a rewrite rule from "NOT all(xs, predicate)" to "any(xs, NOT predicate)" would lead to contradictions. Reasoning:

    A. all({}, predicate) is true by def of all
    B. any({}, NOT predicate) is false by def of any
    C. NOT all({}, predicate} is false follows from A
    D. applying the rewrite rule to C, any({}, NOT predicate) is true, which contradicts B.

However, in first-order-logic, that same rewrite rule is fine since sets always contain elements. It doesn't seem like to much work to go from Python-esque any and all to ∀ and ∃. For example "all(xs, predicate)" could be rewritten to: "¬P ∨ (∀ xs. predicate)" where P is a new proposition variable for whether xs contains elements. This relies on the semantics including short-circuiting evaluation (which may be cheating, I don't know).

Or maybe the above is what you already meant when you said "following the embeding..."?