MATH.6:4 - Solution
State the implication → construct its failure condition → realize the objects and rules → establish assumptions and failure together → use the result or change the search.
MATH.6:4.1 - Recover the mathematical claim
Name the carrier sets, constants, operations and relations that may vary. Retain the restrictions already given: total or partial operations, finite or infinite carriers, allowed values, and any equations or other assumptions. Expand a definition when its content determines the case you need to build.
Write the proposed implication in the form “under these assumptions, this conclusion holds.” Keep a definition or assumption separate from the conclusion being tested. For example, adding transitivity to the assumptions would remove all nontransitive relations from a test of whether reflexivity and symmetry imply transitivity.
If the claim comes from another practice, first recover its mathematical formulation and the intended interpretation through FPF C.29. The mathematical countermodel will test that formulation. Its consequence for the practice depends on that correspondence.
MATH.6:4.2 - Work out what failure requires
Keep the assumptions true and negate the conclusion. Preserve the order and permitted dependence of choices. The following ordinary forms cover common starting points; P and R denote the stated properties, and each variable keeps its declared domain.
| Conclusion to defeat | Construction or argument needed for failure |
|---|---|
Every x has property P(x). | One allowed x for which P(x) fails. |
Some y has property P(y). | A reason why P(y) fails for every allowed y. |
For every x, some y satisfies R(x,y). | One allowed x for which every allowed y fails. |
Some y satisfies R(x,y) for every x. | For each allowed y, an x that defeats it; this x may depend on y. |
An equation between operations can often be defeated by one input tuple. Failure of transitivity requires three elements with the first two links present and the third absent. Start with those witnesses and use them to constrain the construction.
Where failure contains a universal requirement, give its argument or a complete finite case distinction. Finding one unsuccessful candidate for an existential conclusion leaves the other candidates open.
MATH.6:4.3 - Build objects that can realize the failure
Choose a familiar structure or a small carrier that has room for the required witnesses. Assign the constants and the critical relation entries or operation values first. Fill the remaining entries so that the assumptions continue to hold. Total operations need an output for every allowed input; partial operations retain their domains of definition.
For a finite relation, a table can make the critical choices visible. For a function, give its value at each element or give a defining rule. If the objects are classes of expressions, ensure the operation has the same value for equivalent representatives; MATH.2 supplies that construction.
Use the assumptions to reduce the choices. Symmetry determines the reversed relation entry; an identity law determines part of an operation table. After a forced assignment, return to any assumption that uses the changed entry. A conflict means this attempted construction needs revision.
Try a larger carrier or another kind of structure when the failure condition needs it. Smallness is useful for discovery and explanation; a smallest countermodel is required only when its minimality answers the question. A symbolic construction can cover an infinite carrier without listing its elements.
A model finder can supply assignments when the interacting constraints make manual construction expensive. Give it the assumptions together with the negated conclusion and the chosen search scope. Retain the meaning of its types, arithmetic and undefined values when interpreting the returned assignment.
MATH.6:4.4 - Establish that the construction defeats the claim
Evaluate every assumption used by the implication in the constructed case. Then exhibit the false conclusion with the witnesses or quantified argument from :4.2. These two parts establish the countermodel.
For a finite carrier, universal premises can be checked over all relevant tuples. For an infinite carrier, use a rule and an argument covering the required inputs. A program’s finite output can help discover that rule; the argument determines the wider conclusion.
If a search tool used a restricted interpretation, substitute its proposed counterexample back into the intended mathematical definitions. For example, a truncated representation of the natural numbers needs its missing values accounted for. Repair an assignment that relies on an unavailable value or an altered operation before using it to refute the original statement.
Suppose the source claim is n+1≠0 for natural numbers. An encoding instead uses addition modulo 2 and returns n=1. Its 1+1=0 becomes 1+1=2 in the source arithmetic, so this assignment fails to refute the source claim. Restore the source arithmetic before continuing that search, or prove the claim directly from n+1≥1.
Remove dispensable elements or assignments when that makes the reason easier to see. After such a simplification, repeat the affected assumption and failure checks. Keep a larger readable case if further minimization adds work without helping its use.
MATH.6:4.5 - Interpret an unsuccessful search
State what the search covered. Exhaustive failure to find a countermodel establishes absence only in the fully searched class and under the encoded semantics. A timeout or a partial enumeration leaves even that class unresolved.
When this absence is unexpected, compare the encoded assumptions with the intended ones. A contradictory or overrestrictive premise set can exclude the very cases under examination. Constructing one model of the assumptions alone can help distinguish that problem from an unsuccessful search for failure.
Choose the next move from what could answer the question: a different carrier, a symbolic infinite construction, a proof of the proposed claim, a weaker conclusion, or stopping with the searched-scope result. FPF C.11.DUA helps decide whether further inquiry is worth its cost. Enlarging the search is one option.
MATH.6:4.6 - Use the failure to revise the mathematical work
Return the assumptions that survived, the failed consequence, and the construction that separates them. This can reject an identification, stop an invalid proof attempt, expose a needed input, or identify an operation for which a proposed representation is unsuitable.
A repair is a new mathematical question. Restrict the domain, strengthen a justified premise, weaken the requested conclusion, or change the construction according to what the receiving work needs. Establish the revised claim on that scope; merely excluding the exhibited case can leave other failures.
Use B.5.RR to follow the effect through an existing argument. Use MATH.2 or MATH.5 when the affected step forms classes or interprets generating operations. Stop once the countermodel and its intended consequence are usable. No separate report form is needed for an ordinary calculation.