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)[1] before they cause harm in the field. 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.
References¶
[1] Gödel, K. "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I". Monatshefte für Mathematik und Physik 38, 173–198 (1931). Establishes incompleteness and formally undecidable propositions for sufficiently strong formal systems. registry ↩ Show verification details
Supported in partVerified against the publisher's abstract
Gödel's retrieved text gives the unentscheidbare Satz and Satz IX unprovability, backing incompleteness/undecidability as intrinsic limits only.
“Man beachte, daß “[ R (q); q ]” (oder was dasselbe bedeutet “[ S; q ]”) bloß eine metamathematische Beschreibung des unentscheidbaren Satzes ist.”