| 1. Domain | 1.1 Scope of the Domain | Boundaries | The range of phenomena the science includes and excludes. | Studies the resources required to produce proofs in various formal systems. Includes proof length, size, width, space, depth, and time; comparisons of propositional proof systems; complexity lower bounds; automatizability; and relationships between proof systems and classical complexity classes (e.g., NP, coNP, PSPACE). Excludes semantic validity except when used to relate proof systems to complexity-theoretic classes. |
| | Scale | The spatial, temporal, or organizational level at which the science operates (e.g., quantum, cellular, social, cosmic). | Operates at computational-resource scales: polynomial vs. exponential proof lengths, space utilization, width constraints, time-bounded proof search, depth of proof trees, and structural complexity across propositional and first-order fragments. |
| 1.2 Ontological Commitments | Entities | The kinds of things assumed to exist within the domain (particles, organisms, agents, fields, etc.). | Propositional formulas, CNF/DNF representations, circuits, derivation DAGs, refutation proofs, inference rules, proof systems (Resolution, Frege, Extended Frege, Cutting Planes, Polynomial Calculus, Nullstellensatz), complexity classes. |
| | Properties | The fundamental attributes these entities possess (mass, charge, genotype, preference, etc.). | Proof length, proof size, width, space, depth, degree (in algebraic systems), rank, automatizability, p-simulation relationships, lower-bound hardness, derivation structure, branching complexity. |
| | Categories | The basic ontological types used to classify domain elements (substances, processes, relations, structures). | Propositional proof systems, algebraic proof systems, geometric proof systems, semi-algebraic systems, bounded-depth Frege variants, Resolution variants (tree-like, regular), proof-system hierarchies, complexity-class correspondences. |
| 1.3 State-Variables | Variables | The measurable or definable properties that describe system conditions. | Current proof size, width, depth, degree, resource usage, branching factor, clause count, derived polynomial degree, rank of derivation, height of proof DAG, complexity of rule application. |
| | Parameterization | How variables encode and represent the system’s state. | Encoded by size bounds, width constraints, degree parameters, rank systems, space measures, depth bounds, complexity-theoretic input size n, and system-specific resource metrics (e.g., pivot choices, variable elimination order). |
| 1.4 Admissible Idealizations | Simplifications | Conceptual reductions used to make the domain tractable (point masses, rational agents, perfect gases). | Idealizing formulas into CNF/DNF, restricting attention to complete proof systems, reducing general derivations to canonical normal forms, abstracting resource measures to asymptotic classes, ignoring lower-order terms, focusing on representative hard instances. |
| | Validity Conditions | The limits and contexts in which idealizations hold or break down. | Break down when proofs require non-standard representations, when non-CNF forms are essential, when asymptotic abstractions mask critical behavior, or in systems where resource measures interact in non-linear ways (space vs. width). |
| 1.5 Domain Assumptions | Structural Assumptions | Background ontological stances such as determinism, continuity, randomness, discreteness. | Proofs are finitary derivations; resource usage is well-defined; complexity measures behave monotonically; reductions between proof systems preserve resource relationships; simulation relations are transitive and meaningful. |
| | Implicit Commitments | Unstated but necessary assumptions that shape the field’s conceptual structure. | Assumes CNF reductions are benign; complexity classes used as anchors (NP, coNP, etc.) are stable; p-simulation captures meaningful proof power; hard instances reflect true lower-bound structure; algebraic encodings preserve proof complexity faithfully. |
| 1.6 Internal Coherence Requirements | Consistency | The demand that domain concepts do not contradict one another. | Resource measures must align across systems; simulation relations must not contradict known complexity separations; lower-bound arguments cannot collapse standard complexity assumptions. |
| | Compatibility | The requirement that entities, variables, and assumptions fit together into a unified descriptive framework. | Requires harmony among resource metrics (size, width, space), simulation hierarchies, algebraic and combinatorial encodings, and relationships to complexity classes; proof-system definitions must integrate with computational models underlying them. |
| 2. Evidence Layer | 2.1 Observable Phenomena | Observables | The aspects of the domain that can produce detectable signals accessible to measurement. | Proof lengths, proof sizes, widths of clauses, space usage, degree of algebraic derivations, depth of proof trees, performance of proof search, lower-bound hardness instances, simulation relations between proof systems. |
| | Detection Limits | The boundaries of what can be resolved or sensed by current instruments or methods. | Limited by computational intractability of proof search (coNP-hard, PSPACE-hard), inability to certify minimal proofs, exponential-size lower bounds, difficulty observing degree growth in algebraic systems, and complexity-theoretic barriers (e.g., NP vs coNP). |
| 2.2 Measurement Systems | Units | Standardized quantifications (meters, seconds, volts, decibels, dollars, etc.) necessary for consistent comparison. | Length (number of steps), size (total symbol count), width (maximum clause width), space (memory footprint of active clauses), depth (height of proof tree/DAG), degree (Polynomial Calculus), rank (Nullstellensatz), and asymptotic growth with respect to input size n. |
| | Instruments | Devices and tools (microscopes, spectrometers, sensors, surveys, detectors) used to produce measurements. | Resolution engines, SAT solvers, proof-log checkers, algebraic proof analyzers, Cutting Planes verifiers, Frege and Extended Frege provers, Nullstellensatz checkers, polynomial calculus evaluators, automated lower-bound search tools. |
| 2.3 Operational Definitions | Definitions | Terms defined by specific measurement procedures, ensuring empirical clarity. | Proof size defined as symbol count; width defined as max clause width; space defined by number of simultaneously maintained derived objects; degree defined by highest polynomial degree in derivations; rank defined via algebraic hierarchy; refutation defined via contradiction in propositional encodings. |
| | Procedures | The explicit steps required to perform a measurement in a reproducible way. | Running SAT-based or Resolution-based refutations, constructing Frege proofs, executing Cutting Planes derivations, computing polynomial degrees, verifying Nullstellensatz certificates, measuring space usage during proof search, applying reduction to normal forms. |
| 2.4 Data Acquisition | Protocols | Formal processes for gathering data under controlled or standardized conditions. | Standardized benchmarking on hard instances (e.g., pigeonhole principle, Tseitin tautologies), canonical CNF encodings, systematic width and space measurement protocols, controlled clause-ordering strategies, algebraic-derivation sampling for polynomial calculus. |
| | Sampling | Rules determining which subset of the domain is measured and how representative it is. | Choosing formula families with known hardness profiles, sampling across clause densities, selecting representative CNF encodings, using extremal lower-bound examples, and selecting random or worst-case instances across proof-system hierarchies. |
| 2.5 Data Character & Format | Data Types | The form raw evidence takes (time series, spectra, images, counts, qualitative records). | Refutation logs, clause traces, DAG-form proofs, Resolution trees, Frege derivation scripts, Cutting Planes inequalities, algebraic derivations, Nullstellensatz certificates, size/width/space measurements. |
| | Resolution | The granularity or precision with which data is captured. | Determined by granularity of proof logs, precision of clause width measurement, accuracy in space tracking, precision of polynomial degree/monomial count, and the fidelity of recording combinatorial structure in proof traces. |
| 2.6 Reliability & Calibration | Calibration | Adjustment procedures ensuring instruments produce accurate results. | Verifying correctness of proof logs, checking Resolution refutation validity, confirming polynomial calculus computations, validating degree/rank assignments, ensuring space/width metrics are applied consistently across systems. |
| | Error Characterization | Identification and quantification of noise, uncertainty, bias, and measurement error. | Mis-measured widths or sizes, incorrect clause elimination, faulty algebraic derivations, errors in inequality application in Cutting Planes, corrupted proof logs, incorrect simulation reductions, and implementation mistakes in automated provers. |
| 3. Structural Layer | 3.1 Patterns & Regularities | Laws / Relations | Stable, repeatable patterns governing how observables behave across conditions. | Size–width tradeoffs, space–width relations, degree–size relations in algebraic systems, depth–size relations in Frege systems, p-simulation hierarchies, exponential lower-bound patterns (e.g., pigeonhole, Tseitin), known separations between proof systems. |
| | Invariants | Quantities or properties that remain constant under transformations (symmetries, conservation laws). | Invariance of lower bounds across equivalent encodings, monotonicity of resource measures, structural invariants of DAG-like vs. tree-like proofs, invariance of hardness under p-simulations, degree-based invariants in algebraic systems, clause-width invariants in Resolution. |
| 3.2 Causal Architecture | Mechanisms | Underlying processes or structures that produce the observed regularities. | Resolution rule mechanisms, clause propagation, Cutting Planes inequality derivation, polynomial reduction mechanisms, Nullstellensatz rank increases, simulation maps between proof systems, combinatorial bottlenecks driving lower bounds. |
| | Pathways | Organized sequences of interactions forming a causal chain or network. | Derivation pathways from axioms to contradiction, clause elimination chains, inequality escalation in Cutting Planes, polynomial-growth pathways in algebraic proofs, proof-tree expansion sequences, DAG-compaction pathways, simulation paths across systems. |
| 3.3 Theoretical Vocabulary | Concepts | Core terms that encode the domain’s structure (force, gene, equilibrium, field). | Proof size, width, space, depth, degree, rank, p-simulation, automatizability, refutation complexity, derivation DAG, lower-bound hardness, Resolution, Frege, Extended Frege, Cutting Planes, Nullstellensatz, Polynomial Calculus. |
| | Classifications | Taxonomies, categories, or typologies that organize entities and relations. | Resolution family (tree-like, DAG-like, regular, ordered), Frege vs. Extended Frege, algebraic systems (PC, PC⁺, Nullstellensatz), geometric/semi-algebraic systems, depth-limited proof systems, bounded-space systems, p-simulation hierarchies, complexity-class-linked systems (NP, coNP, PSPACE). |
| 3.4 Formal Representations | Equations | Mathematical constructs expressing laws, relations, or mechanisms. | Width–size tradeoff equations, degree–rank relations, polynomial identities in Nullstellensatz proofs, Cutting Planes inequality derivation equations, depth–size recurrence relations, asymptotic lower-bound identities. |
| | Models | Structured representations—mathematical, computational, or conceptual—used to predict and explain phenomena. | Resolution DAGs, Frege derivation trees, Cutting Planes inequality trees, polynomial-derivation graphs, Nullstellensatz proof matrices, combinatorial structures capturing clause growth, resource-measure models for proof complexity. |
| 3.5 Idealized Structures | Simplified Models | Purposeful abstractions that capture essential dynamics while omitting irrelevant detail. | Canonical CNF encodings, normalized derivation forms, restricted Resolution (regular, ordered), linearized Cutting Planes systems, bounded-degree Polynomial Calculus, simplified rank-limited algebraic frameworks, depth-bounded Frege systems. |
| | Limit Conditions | Regimes where specific models or approximations hold (classical vs. quantum, linear vs. nonlinear). | Breakdown under non-CNF encodings, failure of simplified width measures in deep algebraic systems, inadequacy of bounded-depth approximations, degenerate behavior under Extended Frege expansions, collapse of lower bounds if complexity assumptions (e.g., NP ≠ coNP) fail. |
| 3.6 Integrative Frameworks | Unifying Theories | Higher-order structures that connect disparate laws or mechanisms under a coherent whole. | Connections between proof systems and complexity classes (proof complexity ↔ NP vs coNP), simulation hierarchies, algebraic–combinatorial unification of proof strength, lower-bound frameworks, rank/degree hierarchies as unifying structural tools. |
| | Interdisciplinary Links | Points where the theory connects to adjacent sciences or larger explanatory systems. | Links to computational complexity theory (P vs NP, PSPACE), Boolean function analysis, algebraic complexity, SAT solving, combinatorics of CNF structures, circuit complexity (proofs-as-circuits analogy), communication complexity. |
| 4. Method Layer | 4.1 Inquiry Design | Experimental Design | Structured plans for manipulating variables to test causal claims. | Manipulating CNF encodings, altering clause ordering, varying pivot choices in Resolution, adjusting inequality configurations in Cutting Planes, modifying polynomial degree bounds in algebraic systems, controlling DAG vs tree-like derivation formats, and testing proof-size sensitivity to structural constraints. |
| | Observational Design | Systematic approaches for gathering non-manipulated data (surveys, field studies, natural experiments). | Observing proof-search trajectories, monitoring clause growth, tracking space usage, recording polynomial degree escalation, measuring width evolution, examining simulation behavior across systems, and analyzing refutation bottlenecks without modifying rule sets. |
| 4.2 Testing & Validation | Hypothesis Testing | Procedures for evaluating whether evidence supports or contradicts specific claims. | Testing whether certain tautologies require exponential proofs in specific systems, checking whether one system p-simulates another, verifying proposed lower bounds, evaluating automatizability claims, and determining whether proof-size reductions hold under system transformations. |
| | Replication | The requirement that results be independently reproducible under similar conditions. | Reproducing refutation traces across multiple solvers, verifying consistency of lower-bound results, re-running polynomial degree computations, confirming space and width measurements, and validating simulation results across independent implementations and proof systems. |
| 4.3 Inference & Evaluation | Statistical Inference | Rules for drawing conclusions from noisy or incomplete data. | Analyzing distribution of proof lengths across random instances, assessing average vs. worst-case complexities, evaluating clause-density effects on proof size, comparing growth rates across systems, and quantifying variance in proof resources across benchmark families. |
| | Model Comparison | Criteria (fit, simplicity, predictive accuracy, robustness) used to evaluate competing models. | Comparing Resolution, Frege, Extended Frege, Cutting Planes, Polynomial Calculus, and Nullstellensatz in terms of proof size, width, degree, rank, space, depth, and ability to simulate one another; evaluating tradeoffs between combinatorial and algebraic systems. |
| 4.4 Error Management | Error Analysis | Identification and quantification of random and systematic errors. | Identifying miscomputed widths or sizes, incorrect pivots in Resolution, faulty inequality derivations in Cutting Planes, miscalculated degrees in polynomial systems, corrupted proof logs, and erroneous simulation reductions; detecting solver implementation errors. |
| | Bias Control | Methods for minimizing subjective, instrumental, or procedural biases. | Controlling clause-ordering biases, avoiding solver-specific optimizations that distort proof-size measurements, using standardized CNF encodings, ensuring neutral benchmark selection, and reducing researcher-driven bias in lower-bound argument construction. |
| 4.5 Adjudication & Revision | Peer Scrutiny | Collective evaluation of claims through critique, review, and debate. | Cross-verifying lower-bound proofs, reviewing combinatorial arguments, checking algebraic derivations, evaluating simulation claims between proof systems, auditing solver logs, analyzing canonical hard instances, and conducting meta-theoretic critique of complexity claims. |
| | Theory Revision | Procedures for modifying, replacing, or discarding models based on new evidence. | Updating proof-system definitions, refining resource measures (width, rank, degree), modifying simulation frameworks, strengthening or weakening lower-bound arguments, adding new combinatorial principles, and revising asymptotic analyses based on new results. |
| 4.6 Integrity Conditions | Transparency | Requirements to disclose methods, data, assumptions, and limitations. | Full disclosure of CNF encodings, solver parameters, derivation logs, polynomial computations, inequality derivations, data used for lower bounds, assumptions behind simulation claims, and limitations of resource measurements. |
| | Ethical Standards | Norms ensuring responsible conduct in experimentation, data handling, and publication. | Honest reporting of empirical and theoretical proof sizes, avoiding selective example bias, clearly stating unproven complexity assumptions, ensuring reproducibility of experiments, and maintaining accuracy in claims about proof-system separations and lower bounds. |