Contradiction introduction

In symbolic logic, a valid inference in a system of truth-functional rules. The rule whereby a contradiction (P and ¬ P) is proved on separate lines in a proof or subproof.