MATH.22:8 - Common Anti-Patterns and How to Avoid Them

Removing a premise while retaining its rewrite permission. Dropping commutativity in :5.1 permits noncommuting operations. Reordering their factors requires a local commutation argument.

Defining an object that need not exist. The four-object order in :5.2 has common upper bounds but no least one. Supply a construction or change the assumptions before using join as a total operation.

Extending notation and silently strengthening a law. Total reciprocal notation in :5.3 is available with a conditional inverse law. The unconditional law contradicts the retained arithmetic.

Treating a failed proof as independence. The proof may need a different lemma. Establish non-consequence through a separating model or a suitable metatheoretic argument. For the model route in :4.5, establish both directions of separation before claiming independence.