Despite a CS major, I still get confused about the meaning of |– vs. |=, and about the respective meta-syntactic levels of the variables used. Ironically, one issue for me is the lack of explicit typing in the notation itself.
This reminds me that the “model” terminology also confuses me. A “model of X” for me is an idealized and simplified/abstracted version of X, whereas in mathematical logic it seems to be the opposite, a concretization/instantiation.
