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