Metatheory Review Checklist¶
Review protocol — instantiates Formal Derivation System Design
A structured human review that interrogates the whole formal system for its meta-properties — soundness, completeness, decidability — and polices the line between formal derivability and real-world truth.
A Metatheory Review Checklist steps outside the derivation kernel to ask the questions a formal system cannot ask about itself. Working through a fixed list of meta-properties — is the system sound (does everything derivable actually hold under the intended reading?), complete (can everything that should hold be derived?), decidable (will checks terminate?), and known-consistent? — reviewers produce a documented judgment about the system as a whole. Its defining commitment is that it is human reasoning about the system, not a mechanical run inside it; and its most important job is to draw and defend the interpretation boundary — the explicit line between "derivable in the formalism" and "true, legal, safe, or right in the world."
Example¶
A team is designing a new domain-specific logic to verify safety properties of smart contracts. Before shipping it, they run a metatheory review. Soundness: does every property the logic pronounces "verified" actually hold of the contract's execution semantics, or could the proof system bless something the machine would violate? Completeness: are there true safety properties the logic simply cannot express or prove? Decidability: can validity checks hang on some contracts, and what happens operationally when they do? And the sharpest question of all, the interpretation boundary: when the system stamps a contract "formally verified safe," does that mean safe in deployment — against reentrancy, against economic exploits outside the model — or only safe relative to the modeled semantics? The review records each answer with its caveats, and explicitly writes down what a green verification result does and does not license anyone to claim.
How it works¶
- Walk the meta-property checklist. Reviewers move through soundness, completeness, decidability/termination, and known-consistency, answering each with argument and evidence rather than assertion.
- Interrogate, don't derive. The review reasons about the calculus and its intended semantics; it constructs or cites metatheorems but is itself a human judgment, not a proof run inside the system.
- Draw the interpretation boundary. It states in plain terms what a derivation licenses about the world and — crucially — what it does not, so "formally verified" is never silently upgraded to "true" or "safe."
- Record the verdict with caveats. The output is a metatheory review record: answers, supporting arguments, known limits, and open questions, kept as a living document.
Tuning parameters¶
- Rigor — an informal expert walkthrough vs. fully proved metatheorems. Higher rigor gives stronger guarantees at much greater cost; a walkthrough is fast but weaker.
- Scope — which meta-properties are in scope this round. Broad scope is thorough; narrow scope concentrates effort where risk is highest.
- Reviewer independence — whether reviewers are the system's authors or outsiders. Independent reviewers catch blind spots; author-reviewers know the system best.
- Interpretation-boundary conservatism — how narrowly the real-world claim is drawn. A conservative boundary under-promises and rarely misleads; a generous one claims more and risks overreach.
When it helps, and when it misleads¶
Its strength is catching category errors — mistaking formal validity for real-world truth, legality, or safety — and surfacing intrinsic limits (incompleteness, undecidability) before they cause harm in the field.[n1] It is the one mechanism whose whole purpose is to keep the system honest about what it does not establish.
Its failure mode is false comfort. A checklist answered superficially — a box ticked "sound" with no argument behind it — manufactures confidence without warrant, and a review is only as good as the rigor and independence of the reviewers. The classic misuse is declaring a system "sound and complete" on the strength of a review that never actually constructed the metatheoretic argument. The guarding discipline is to treat every unproven meta-claim as an open question, keep the interpretation boundary explicit and conservative, and never let "we reviewed it" stand in for "we established it."
How it implements the components¶
metatheory_review_record— it produces the documented judgment on the system's meta-properties: soundness, completeness, decidability, consistency, with arguments and caveats.interpretation_boundary— it draws and defends the explicit line between what is derivable in the formalism and what may be claimed about the world.
It is human review, not a mechanical run inside the system: it does not automatically search the axiom-and-rule set for a derivable contradiction (consistency_guardrail — that computational hunt is its nearest twin, the Consistency and Contradiction Test, whose result this review then interprets).
Related¶
- Instantiates: Formal Derivation System Design — governs the metatheoretic limits and interpretation of the whole system.
- Consumes: Consistency and Contradiction Test — its contradiction-search results feed the review's soundness and consistency questions.
- Sibling mechanisms: Formal Grammar Specification · Well-Formedness Linter · Axiom Schema Catalog · Inference Rule Calculus · Rewrite or Transition Rule Engine · Proof Tree or Derivation Log · Mechanical Proof Checker · Consistency and Contradiction Test · Formal-System Change-Control Workflow
Editorial Notes¶
Form Classification¶
Form family: Assessment, Review & Assurance
Rationale: Metatheory Review Checklist operates as a bounded evaluation of existing evidence or work that produces a finding or disposition because it a structured human review that interrogates the whole formal system for its meta-properties — soundness, completeness, decidability — and polices the line between formal derivability and real-world truth.
Independent corroboration: The frozen evidence defines Metatheory Review Checklist as 'A structured human review that interrogates the whole formal system for its meta-properties — soundness, completeness, decidability — and polices the line between formal derivability and real-world truth', so its operative form is Assessment, Review & Assurance.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Mathematics
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Specialized
Rationale: Soundness, completeness, and decidability are metatheoretic properties formalized in mathematical logic. Philosophy supplies the distinction between formal derivability and truth, and computer science supplies executable and decidability concerns.
Related originating lineages:
- Computer Science & Software Engineering — Computability and formal-methods practice operationalize decidability and verification review.
- Philosophy — Retained as a formative lineage independently identified as primary: Soundness, completeness, decidability, and the derivability-truth boundary are metatheoretic concerns in logic and philosophy.
Review resolution: The formal-logic literature defines soundness and completeness as relations between proof systems and semantics and treats decidability as a metatheoretic property. The human review checklist is a corpus synthesis over that mathematical foundation. The alternates are retained only as formative or independently established origins, not because the mechanism can be applied there. origin_mode=cross_disciplinary_synthesis states the provenance relationship; domain_reach=specialized separately records breadth because established use remains concentrated in a bounded professional context. confidence=high reflects the strength and specificity of the evidence; encyclopedia_synthesis=true because the entry deliberately composes those documented lineages into this exact artifact.
Encyclopedia synthesis: The exact catalogued form synthesizes established practice rather than reproducing a single standard historical label.
Review outcome: Researched adjudication after independent review; high confidence.
Sources consulted:
- https://plato.stanford.edu/archives/win2012/entries/logic-classical/ — Authoritative logic reference surveys formal semantics, proof systems, soundness, completeness, and decidability.
Notes¶
[n1] Gödel's incompleteness theorems show that any sufficiently expressive, consistent formal system contains true statements it cannot prove, and cannot prove its own consistency. They are the standing reason a metatheory review must treat completeness and self-certification as intrinsically limited rather than assumed. ↩