curiositech/lakatos

SKILL.md: Proofs and Refutations — The Logic of Discovery

license: Apache-2.0

name: proofs-and-refutations
version: 1.0
source: "Proofs and Refutations: The Logic of Mathematical Discovery — Imre Lakatos"
description: >
  A framework for reasoning under uncertainty, handling counterexamples,
  refining concepts iteratively, and understanding how knowledge actually
  grows through conjecture-refutation dialectics rather than accumulation
  of certified truths.
activation_triggers:
  - debugging complex systems where errors are ambiguous or hard to localize
  - designing ontologies, schemas, or type systems
  - handling edge cases, boundary conditions, or unexpected inputs
  - evaluating whether a proof, argument, or reasoning chain is sound
  - deciding how to respond to falsification or refutation of a hypothesis
  - building systems that must learn or improve from failure
  - coordinating across disagreement about definitions or success criteria
  - any situation where "is this really a counterexample?" is a live question

---

When to Use This Skill

Load this skill when:

• A system or argument fails and you need to decide whether the failure invalidates the whole approach or just a sub-component
• Edge cases appear that don't fit existing categories — and you must decide whether to expand definitions, exclude the case, or revise the conjecture
• Definitions are contested — when what counts as X is genuinely unclear and the answer matters for the conclusion
• You're tempted to redefine terms to make a problem go away rather than solve it
• Someone presents a "proof" and you need to assess what it actually establishes vs. what it assumes
• Ontologies or schemas are being designed and there's pressure to finalize them before adequate testing
• A reasoning chain reaches a wrong answer and you need to extract value from the failure rather than just discarding it
• A system appears to be learning but may actually be progressively narrowing its success criteria

---

Core Mental Models

1. Proofs Decompose, They Don't Certify

A proof does not establish truth — it breaks a conjecture into sub-conjectures (lemmas), each independently criticizable. Even a proof of a false conjecture is productive: it maps the hidden assumptions and creates new targets for inquiry. The "failed" reasoning chain is a diagnostic, not just waste.

Operational implication: When a reasoning chain produces a wrong answer, don't discard it — trace which lemma failed. The map of failure is often more valuable than the original goal.

2. Monster-Barring vs. Genuine Learning

When a counterexample appears, there are fundamentally different responses:

• Monster-barring: Redefine terms to exclude the counterexample by fiat ("that's not a real polyhedron") — preserves the conjecture but hollows it out
• Lemma-incorporation: Absorb the counterexample's lesson into a refined conjecture with explicit conditions
• Surrender: Abandon the conjecture as genuinely false

Monster-barring feels like clarification but is concept-contraction driven by the desire to protect a result. Systems that keep redefining success criteria to exclude inconvenient cases appear to learn while becoming more brittle.

3. Local vs. Global Counterexamples

A counterexample can attack:

• A lemma (local): The argument is flawed, but the conjecture may still be true — repair the proof
• The conjecture itself (global): The claim is wrong — revise or abandon

Conflating these causes two failure modes: (a) abandoning good conjectures because a sub-argument failed, or (b) defending bad conjectures by patching sub-arguments indefinitely.

Triage rule: Before deciding what a counterexample means, first determine what it hits.

4. Definitions Are Products of Inquiry, Not Preconditions

The right definition of a concept cannot be determined at the outset — it emerges from pressure applied by counterexamples. Every boundary case is an opportunity to discover what the concept actually needs to be. Initial ontologies are provisional hypotheses, not fixed infrastructure.

Operational implication: Treat schema freeze dates with suspicion. The concepts that matter most will be the ones that haven't been stress-tested yet.

5. The Dialectic Cannot Be Shortcut

The "Perfect Definition" move — define the domain as exactly the set of things for which the conjecture holds — collapses inquiry into triviality. Progress requires maintaining tension between conjecture and domain. Any architecture too eager to resolve ambiguity, lock down schemas, or close open questions will systematically prevent learning that only happens at the boundary between what works and what doesn't.

---

Decision Frameworks

When a Failure Appears

Is the failure in the argument or the claim?
├── Attack on a lemma (local) → Repair the proof; conjecture survives
│   ├── Can the lemma be rescued? → Revise sub-argument
│   └── Lemma is genuinely false → Weaken the conjecture's conditions (lemma-incorporation)
└── Attack on the conjecture (global) → Revision required
    ├── Is the counterexample a "monster"? → Check: am I excluding it to protect the conjecture?
    │   ├── Yes (monster-barring) → Dangerous; examine what you're giving up
    │   └── No (genuinely outside scope) → Narrow domain explicitly and document why
    └── Counterexample is legitimate → Revise conjecture or surrender

When Encountering a Counterexample

| Response | What it does | When it's legitimate | When it's a trap | |---|---|---|---| | Surrender | Abandons conjecture | Global counterexample is valid | Counterexample was only local | | Monster-barring | Redefines to exclude | Genuinely outside intended scope | Protecting conjecture from real falsification | | Exception-barring | Restricts domain explicitly | Principled scope limitation | Scope kept shrinking to preserve result | | Lemma-incorporation | Adds condition to conjecture | Local failure, fixable | Used to hide unresolvable problems | | Concept-stretching | Expands definition to cover case | Genuine generalization | Forces alien cases into concept |

When Designing a Schema or Ontology

Is there pressure to finalize definitions before boundary cases are tested?
└── Yes → Treat current definitions as v0 hypotheses; document known gaps
    
Are there cases the current schema handles awkwardly?
└── Yes → These are not "edge cases to handle later" — they are diagnostic pressure
    └── What would the concept need to be for these to fit naturally?
        └── That question is more valuable than patching the current schema

When Evaluating a Proof or Argument

What does this proof actually establish?
1. List the lemmas (explicit and implicit)
2. Which lemmas are independently verified vs. assumed?
3. If a lemma fails, does the conjecture fall or just the argument?
4. What domain assumptions are embedded silently?

---

Reference Files

| File | When to Load | |---|---| | references/proofs-as-decomposition-not-certification.md | When evaluating what a proof or reasoning chain actually establishes; when extracting value from a "failed" argument; when assessing implicit assumptions in a chain of reasoning | | references/monster-barring-and-concept-stretching.md | When a counterexample appears and there's temptation to redefine terms; when a system seems to be "learning" by progressively narrowing its success criteria; when definitions keep shifting after failures | | references/local-vs-global-counterexamples-error-triage.md | When triaging a failure — deciding whether it invalidates the whole approach or just a sub-component; when doing root cause analysis; when deciding whether to abandon or repair an approach | | references/definitions-as-products-not-preconditions.md | When designing or freezing ontologies, schemas, or type systems; when initial categories are failing under boundary cases; when asked to specify definitions before testing | | references/the-dialectic-of-conjecture-and-refutation.md | When understanding the overall arc of how knowledge grows; when a system's learning process needs to be evaluated or designed; foundational framing for most other references | | references/the-problem-of-concept-extension-and-boundary-cases.md | When boundary or edge cases are accumulating and need a principled treatment; when deciding whether to expand, restrict, or revise a concept under pressure | | references/the-social-structure-of-rigorous-inquiry.md | When coordinating across agents or team members who disagree; when a single reasoner is making all calls without challenge; when epistemic role distribution matters | | references/the-gap-between-knowing-and-proving.md | When a conjecture is highly credible but unproven; when deciding whether to act on an unproven hypothesis; when distinguishing justified confidence from formal proof |

---

Anti-Patterns

These are the failure modes Lakatos most directly warns against:

1. Monster-Barring by Drift Redefining terms incrementally after each counterexample, so no single redefinition looks unreasonable, but the cumulative effect is that the "theorem" now applies to almost nothing. The warning sign: each revision feels like a clarification.

2. Treating Schema Freeze as Progress Locking down definitions and ontologies before they've been stress-tested by boundary cases. The result is a system that handles everything it was tested on and fails badly at everything it wasn't.

3. Conflating Proof Failure with Conjecture Failure Abandoning a correct conjecture because a particular argument for it failed. The argument failing is information about the argument, not necessarily the claim.

4. The Trivializing Perfect Definition Defining the domain as exactly the set of things for which the result holds, then claiming the theorem is proven. This is the death of inquiry dressed as rigor.

5. Missing the Value in Failed Reasoning Discarding a reasoning chain that reached a wrong conclusion instead of tracing which lemma failed. Failed proofs are maps; throwing away the map is waste.

6. Concept-Stretching Under Pressure Forcing genuinely alien cases into an existing concept rather than admitting the concept needs revision or a new concept is needed. Produces categories that are simultaneously too broad and too narrow.

7. Solo Epistemics A single agent making all decisions about what counts as a counterexample, what counts as monster-barring, and whether a proof is sound — without structures that enable genuine challenge. Lakatos's dialogue format is itself an argument about process.

---

Shibboleths

How to tell if someone has actually internalized this book vs. just read the summary:

They have internalized it if they:

• Spontaneously ask "is this a local or global counterexample?" before deciding how to respond to failure
• Treat a wrong-answer reasoning chain as diagnostic rather than just discarding it
• Become suspicious when their definitions keep getting refined in the wake of counterexamples — and can say why that's suspicious
• Recognize the "perfect definition" move as a trap and can name what's lost
• Talk about proofs as programs of decomposition rather than as certificates
• Ask "what hidden lemmas is this argument relying on?" when evaluating someone else's reasoning
• Treat the boundary cases as the interesting part of a problem, not the annoying part

They have only read the summary if they:

• Use "monster-barring" as a generic insult for any definitional refinement, rather than a specific failure mode with specific conditions
• Think the lesson is "be open to counterexamples" — too vague, misses the precise taxonomy
• Think "definitions emerge from inquiry" means "don't define things upfront" — it means definitions are hypotheses that should be tested, not avoided
• Cannot distinguish between when lemma-incorporation is legitimate versus when it's covering for a fundamentally broken conjecture
• Treat the social/dialogic structure as stylistic rather than as a substantive claim about what rigorous inquiry requires

---

Load reference files on demand as specific situations arise. The dialectic of conjecture and refutation cannot be shortcut — neither can reading these references selectively based on what the situation actually requires.