How do NOT EXISTS and correlated subqueries work internally

Question

I would like to understand how NOT EXISTS works in a correlated subquery.

In this query, it's returned the patient that takes all the medications, but I don't understand why.

Could someone please explain what's happening in each step of execution of this query and which records are being considered and dismissed in each step.

create table medication
(
    idmedic INT PRIMARY KEY,
    name VARCHAR(20),
    dosage NUMERIC(8,2)
);

create table patient 
(
    idpac INT PRIMARY KEY,
    name VARCHAR(20)
);

create table prescription  
(
    idpac INT,
    idmedic INT,
    date DATE,
    time TIME,
    FOREIGN KEY (idpac) REFERENCES patient(idpac),
    FOREIGN KEY (idmedic) REFERENCES medication(idmedic)
);

insert into patient (idpac, name) 
values (1, 'joe'), (2, 'tod'), (3, 'ric');

insert into medication (idmedic, name, dosage) 
values (1, 'tilenol', 0.01), (2, 'omega3', 0.02);

insert into prescription (idpac, idmedic, date, time) 
values (1, 1, '2018-01-01', '20:00'), (1, 2, '2018-01-01', '20:00'),
       (2, 2, '2018-01-01', '20:00');

select 
    pa.name 
from 
    patient pa
where 
    not exists (select 1 from medication me
                where not exists (select 1
                                  from prescription pr
                                  where pr.idpac = pa.idpac 
                                    and pr.idmedic = me.idmedic))

Answer 1

If you see a doubly nested "not exists" in a query that's usually an indication that relational division is being performed (google that, you'll find plenty of stuff).

Translating the query clause by clause into informal language yields something like :

get patients
for which there does not exist
a medication
for which there does not exist
a prescription for that patient to take that medication

which translates to

patients for which there is no medication they don't take.

which translates to

patients that take all medications.

Relational division is the relational algebra operator that corresponds to universal quantification in predicate logic.