Re: Logical Implication

From: Vik Fearing <vik(at)postgresfriends(dot)org>
To: Nathan Bossart <nathandbossart(at)gmail(dot)com>
Cc: PostgreSQL Hackers <pgsql-hackers(at)lists(dot)postgresql(dot)org>
Subject: Re: Logical Implication
Date: 2026-09-29 15:20:11
Message-ID: 9ab35dbb-d9a4-4c1e-bae2-7763ddeb720c@postgresfriends.org
Views: Whole Thread | Raw Message | Download mbox | Resend email
Thread:
Lists: pgsql-hackers


On 24/09/2026 16:33, Nathan Bossart wrote:
> I spent some time looking at this one from a few different angles.

Thanks!

> * NULL behavior: while not a conscious decision of your patch, a straight
> translation of "a IMPLIES b" to "NOT a OR b" would settle the standard on
> Kleene logic for material implication [0]. I think that's okay; IIUC that
> would be the case for any popular SQL database that implements it in a
> similar fashion. According to Wikipedia, SQL uses "a comment fragment of
> the Kleene and Łukasiewicz three-valued logic (which differ in their
> definition of implication; however, SQL defines no such operation)" [1].
> This proposal changes that, so it seems worth calling out.

I've added some documentation for this.

> * Short circuiting: IIUC the new IMPLIES operation wouldn't be guaranteed
> to short-circuit, which matches the behavior of AND and OR and thus is
> probably fine.

Yeah, SQL is not a short-circuiting language, and since this gets
transformed during parse analysis, it inherits whatever short-circuiting
postgres does do.

> * Precedence: Placing it below OR seems to be pretty common, so no concerns
> there. I don't know where it belongs in relation to INTERSECT, UNION, or
> EXCEPT, though. Any thoughts about that?

It doesn't belong anywhere in relation to those.  Those are set
operators and this is a boolean operator.

> * Associativity: The proposal chooses right associativity. I thought about
> this part the most, and I'm not sure any associativity is desirable. I
> think we should forbid chained implications for two reasons: 1) if we do it
> one way and the SQL committee chooses the other, we're in a tight spot, and

I will make sure this is settled with the committee long before v20 hits
feature freeze.  I don't expect them to contradict me on this because
all languages that have this operator (e.g. Haskell, Rocq, Agda, TLA+,
SMT-LIB, Alloy, Isabelle, etc) all use right associativity.

The precedent for right associativity is enormous.

> 2) I cannot come up with any natural examples to illustrate the desired
> behavior. Take the following example:
>
> shipped IMPLIES zip code set IMPLIES ship date in the past
>
> Under right associativity, this would translate to
>
> NOT shipped OR NOT zip code set OR ship date in the past
>
> The former reads as "if shipped, then the zip code is set and the ship date
> is in the past", but the latter is pretty obviously not that. If "shipped"
> is true and "zip code" is not set, it would return true, for example.
> Granted, the user probably should have written
>
> shipped IMPLIES (zip code set AND ship date in the past)
>
> but that feels like an easy mistake to make, at least to me. I'm not sure
> left associativity is any better in this regard.

I disagree with you here.

    a IMPLIES b IMPLIES c
    NOT a OR (NOT b OR c)
    (NOT a OR NOT b) OR c
    NOT (a AND b) OR c
    (a AND b) IMPLIES c

which reads as "if shipped and the zip code is set then the ship date is
in the past".

In your example, if not shipped or the zip code is not set, the
antecedent is not true so the implication asserts nothing and is
satisfied, so your conclusion that it would return true is correct.

Attached is a v2 with doc and test improvements. No code changes.

--

Vik Fearing

Attachment Content-Type Size
v2-0001-doc-Rearrange-the-logical-operator-truth-tables.patch text/plain 4.5 KB
v2-0002-Add-the-IMPLIES-boolean-operator.patch text/plain 19.2 KB

In response to

Responses

Browse pgsql-hackers by date

  From Date Subject
Next Message Anthonin Bonnefoy 2026-09-29 15:37:46 Re: Protocol Compression (fourth attempt)
Previous Message Tom Lane 2026-09-29 15:11:50 Re: remove_useless_joins vs. bug #19560