メタ記号を色々

• M |= A
• A1, ..., An |⇒ B
• |≡ (A1, ..., An → B)
• τ |≡ (A1, ..., An → B)

読み方は、

• model M satisfies formula A
• A1, ..., An entailes B
• (A1, ..., An → B) is valid
• τ ensures that (A1, ..., An → B) is valid