A relational symbol representing non-provability or semantic non-consequence in mathematical logic and proof theory.
