| 1. Domain | 1.1 Scope of the Domain | Boundaries | The range of phenomena the science includes and excludes. | Studies proof systems for logics that deviate from classical principles (e.g., intuitionistic, modal, linear, relevant, paraconsistent, many-valued). Includes sequent calculi, natural deduction, tableaux, deep inference, and structural variants tailored to each logic. Excludes model-theoretic semantics except where required to validate or motivate proof rules. |
| | Scale | The spatial, temporal, or organizational level at which the science operates (e.g., quantum, cellular, social, cosmic). | Operates at the level of proof rules, derivation structures, structural constraints (resource sensitivity, relevance conditions), modal rule schemes, and logic-specific sequent formats. |
| 1.2 Ontological Commitments | Entities | The kinds of things assumed to exist within the domain (particles, organisms, agents, fields, etc.). | Non-classical sequents, labeled sequents, worlds/accessible indices (in modal systems), resources (linear/affine), relevance constraints, polarity annotations, structural-rule variants, logic-specific inference rules. |
| | Properties | The fundamental attributes these entities possess (mass, charge, genotype, preference, etc.). | Resource usage, polarity, accessibility, valuation multiplicity (many-valued), relevance constraints, structural-rule admissibility, normalization behavior, cut properties, context sensitivity. |
| | Categories | The basic ontological types used to classify domain elements (substances, processes, relations, structures). | Modal, intuitionistic, linear, affine, relevant, paraconsistent, paracomplete, many-valued calculi; labeled vs. unlabeled systems; deep vs. shallow inference; analytic vs. non-analytic rules. |
| 1.3 State-Variables | Variables | The measurable or definable properties that describe system conditions. | World labels, resource counts, polarity markers, context configurations, accessibility relations, structural-rule availability, sequent form (single-succedent, multi-succedent), cut occurrences, valuation indices. |
| | Parameterization | How variables encode and represent the system’s state. | Encoded using labeled sequents (w:Γ ⊢ Δ), resource-sensitive contexts (multisets, ordered structures), modal accessibility graphs, polarity annotations, relevance constraints, graded valuations. |
| 1.4 Admissible Idealizations | Simplifications | Conceptual reductions used to make the domain tractable (point masses, rational agents, perfect gases). | Idealizing accessibility relations, treating resources as discrete tokens, simplifying relevance conditions, using analytic variants with subformula property, ignoring global modalities in local derivations, omitting non-local constraints when tractable. |
| | Validity Conditions | The limits and contexts in which idealizations hold or break down. | Idealizations break down in logics with non-well-behaved modalities, nonlocal structural behavior, nonterminating normalization, unrestricted resource usage, or logics where analytic calculi cannot be recovered. |
| 1.5 Domain Assumptions | Structural Assumptions | Background ontological stances such as determinism, continuity, randomness, discreteness. | Proofs follow the logic’s structural discipline: no weakening/contraction (linear), restricted explosion (paraconsistent), single-succedent (intuitionistic), relevance preservation (relevant logic), modality-respecting structural rules. |
| | Implicit Commitments | Unstated but necessary assumptions that shape the field’s conceptual structure. | Assumes rule schemas are aligned with each logic’s philosophical constraints; assumes correct propagation of labels, resources, and accessibility; presumes structural coherence between sequent format and underlying logic. |
| 1.6 Internal Coherence Requirements | Consistency | The demand that domain concepts do not contradict one another. | Rule systems must not collapse into classical logic unless intended; structural discipline must preserve each logic’s non-classical character; cut-elimination must not introduce forbidden structural behavior. |
| | Compatibility | The requirement that entities, variables, and assumptions fit together into a unified descriptive framework. | Alignment required between structural constraints (resource sensitivity, relevance, modality), inference rules, sequent formats, normalization behaviors, and semantic motivations (e.g., accessibility, many-valued truth, paraconsistency). |
| 2. Evidence Layer | 2.1 Observable Phenomena | Observables | The aspects of the domain that can produce detectable signals accessible to measurement. | Labeled-sequent transformations, modal rule applications, resource-sensitive rule usage, relevance-preserving steps, multi-valued rule firings, accessibility propagation, cut behavior in non-classical systems, normalization traces. |
| | Detection Limits | The boundaries of what can be resolved or sensed by current instruments or methods. | Limited by complexity of non-classical proof search, undecidability of certain systems, difficulty tracking modalities or resources, branching explosion in relevant or paraconsistent tableaux, and limits of automated prover support for exotic rules. |
| 2.2 Measurement Systems | Units | Standardized quantifications (meters, seconds, volts, decibels, dollars, etc.) necessary for consistent comparison. | Proof height, resource counts, modality depth, label-propagation steps, relevance-preservation checks, cut-rank, number of accessibility transitions, valuation degrees in many-valued systems. |
| | Instruments | Devices and tools (microscopes, spectrometers, sensors, surveys, detectors) used to produce measurements. | Labeled-sequent proof assistants, modal proof search engines, linear-logic provers (e.g., LO types), relevant-logic tableaux generators, paraconsistent proof checkers, deep-inference tools, many-valued proof analyzers, structural-rule verifiers. |
| 2.3 Operational Definitions | Definitions | Terms defined by specific measurement procedures, ensuring empirical clarity. | Derivability defined relative to logic-specific rule sets; modal accessibility defined by labeled transitions; resource usage defined via structural constraints; relevance defined by syntactic connection; valuation levels defined in many-valued calculi. |
| | Procedures | The explicit steps required to perform a measurement in a reproducible way. | Running logic-specific proof search, verifying accessibility paths, checking resource compliance, enforcing relevance constraints, executing cut-elimination in non-classical settings, performing normalization sensitive to modality or resource structures. |
| 2.4 Data Acquisition | Protocols | Formal processes for gathering data under controlled or standardized conditions. | Standardized modal proof construction, resource-sensitive derivation protocols, relevance-preservation verification, multi-valued rule application sequences, canonical labeled-sequent workflows, systematic cut-elimination tests. |
| | Sampling | Rules determining which subset of the domain is measured and how representative it is. | Selecting representative modal depths, resource-sensitive derivations, relevance-constrained proof patterns, canonical many-valued derivation cases, typical normalization paths across non-classical variants. |
| 2.5 Data Character & Format | Data Types | The form raw evidence takes (time series, spectra, images, counts, qualitative records). | Labeled sequents, modal derivations, resource-annotated contexts, relevance-constrained proof trees, many-valued tableaux, normalization graphs, accessibility transition logs, structural-rule usage traces. |
| | Resolution | The granularity or precision with which data is captured. | Determined by granularity of label tracking, resource annotation precision, fidelity of accessibility graphs, number of valuation levels (finite or infinite), and detail level in modal or relevance-based normalization sequences. |
| 2.6 Reliability & Calibration | Calibration | Adjustment procedures ensuring instruments produce accurate results. | Validating modal accessibility rules, verifying resource-discipline implementation, checking relevance constraints, ensuring correctness of many-valued rule schemas, calibrating deep-inference systems, validating normalization procedures across logics. |
| | Error Characterization | Identification and quantification of noise, uncertainty, bias, and measurement error. | Misapplied modal or resource-sensitive rules, incorrect label propagation, faulty relevance tracking, rule-schema misalignment with logic’s semantics, normalization failures, implementation errors in non-classical proof assistants. |
| 3. Structural Layer | 3.1 Patterns & Regularities | Laws / Relations | Stable, repeatable patterns governing how observables behave across conditions. | Modal accessibility propagation rules, resource-sensitive rule interactions (linear/affine), relevance-preservation constraints, paraconsistent non-explosion patterns, many-valued rule behaviors, intuitionistic single-succedent structure, cut-reduction laws adapted to each logic. |
| | Invariants | Quantities or properties that remain constant under transformations (symmetries, conservation laws). | Accessibility invariants in modal systems, resource invariants in linear/affine logics, relevance invariants, polarity preservation, valuation invariants in many-valued systems, preservation of constructive content in intuitionistic logics, cut-rank monotonicity across non-classical calculi. |
| 3.2 Causal Architecture | Mechanisms | Underlying processes or structures that produce the observed regularities. | World-label propagation (modal logics), resource consumption/production (linear), relevance-filtering mechanisms, non-explosive inference mechanisms (paraconsistent), valuation propagation in many-valued systems, constructive introduction/elimination rules. |
| | Pathways | Organized sequences of interactions forming a causal chain or network. | Modal rule chains (□/◇ introduction–elimination sequences), resource-tracking derivation paths, relevance-preserving proof flows, paraconsistent derivation branches avoiding triviality, many-valued proof propagation chains, intuitionistic constructive proof pathways. |
| 3.3 Theoretical Vocabulary | Concepts | Core terms that encode the domain’s structure (force, gene, equilibrium, field). | Accessibility, resource sensitivity, relevance, paraconsistency, paracompleteness, polarity, valuation degrees, linearity, constructivity, modality depth, single-succedent structure, analytic/non-analytic rules. |
| | Classifications | Taxonomies, categories, or typologies that organize entities and relations. | Modal (K, T, S4, S5), intuitionistic (LJ variants), linear/affine (LL, MILL), relevant logics (R, RW), paraconsistent calculi (LP, da Costa systems), paracomplete logics, many-valued logics, labeled vs. unlabeled systems, deep inference vs. sequent calculus. |
| 3.4 Formal Representations | Equations | Mathematical constructs expressing laws, relations, or mechanisms. | Modal accessibility equations (wRu), resource-balance equations, polarity equations, many-valued truth-transform equations, permutation conversions adapted to non-classical constraints, specialized cut-reduction equalities. |
| | Models | Structured representations—mathematical, computational, or conceptual—used to predict and explain phenomena. | Labeled-sequent derivation trees, Kripke-style proof structures, resource-annotated proof graphs, relevance-filtered tableaux, many-valued tableaux, deep-inference derivation networks, intuitionistic proof trees. |
| 3.5 Idealized Structures | Simplified Models | Purposeful abstractions that capture essential dynamics while omitting irrelevant detail. | Analytic calculi with logic-specific subformula properties, restricted structural rules, simplified accessibility relations, compressed resource annotations, idealized relevance constraints, finite-valued truncations of many-valued systems. |
| | Limit Conditions | Regimes where specific models or approximations hold (classical vs. quantum, linear vs. nonlinear). | Breakdown under non-well-founded accessibility, infinite-valued logics, nonterminating normalization, systems lacking analytic reformulations, resource-sensitive logics without contraction/weakening, modal logics requiring non-local structural rules. |
| 3.6 Integrative Frameworks | Unifying Theories | Higher-order structures that connect disparate laws or mechanisms under a coherent whole. | Generalized cut-elimination across non-classical families, proof-theoretic semantics, labeled-sequent meta-frameworks, deep inference as unifier of structural variation, category-theoretic unification for resource/logical structure. |
| | Interdisciplinary Links | Points where the theory connects to adjacent sciences or larger explanatory systems. | Links to Kripke semantics, category theory (monoidal categories for linear logic), type theory (polarity and constructivity), computational complexity of non-classical proof search, modal/temporal semantics, substructural logics in computer science. |
| 4. Method Layer | 4.1 Inquiry Design | Experimental Design | Structured plans for manipulating variables to test causal claims. | Manipulating modal rules, altering accessibility constraints, adding/removing resource-sensitive structural rules, restricting or permitting relevance conditions, adjusting truth-degree rules in many-valued systems, toggling contraction/weakening, and modifying succedent structure to observe effects on derivability and normalization. |
| | Observational Design | Systematic approaches for gathering non-manipulated data (surveys, field studies, natural experiments). | Observing how derivations evolve under fixed logic-specific constraints: tracking modal accessibility propagation, resource accounting, relevance preservation, non-explosion behavior, multi-valued propagation patterns, and constructive proof evolution without modifying the calculus. |
| 4.2 Testing & Validation | Hypothesis Testing | Procedures for evaluating whether evidence supports or contradicts specific claims. | Testing admissibility of non-classical structural rules, verifying preservation of modality or resource conditions, determining whether cut-elimination holds in each system, checking relevance or paraconsistency constraints, testing equivalence between labeled and unlabeled proofs. |
| | Replication | The requirement that results be independently reproducible under similar conditions. | Reproducing modal or linear derivations across independent calculi, verifying accessibility paths, replicating resource-sensitive proofs, cross-running cut-elimination procedures, validating consistency across different proof assistants for the same non-classical logic. |
| 4.3 Inference & Evaluation | Statistical Inference | Rules for drawing conclusions from noisy or incomplete data. | Analyzing frequency distribution of rule applications (modal, resource-sensitive, relevance-based), complexity of proof search under constraints, data on normalization lengths, cut-rank changes, and multi-valued propagation patterns across representative proof families. |
| | Model Comparison | Criteria (fit, simplicity, predictive accuracy, robustness) used to evaluate competing models. | Comparing logics by normalization strength, cut-elimination feasibility, analytic vs. non-analytic rule behavior, rule schema simplicity, proof-length bounds, modal-depth growth, resource sensitivity, relevance enforcement, and computational complexity of proof search across systems. |
| 4.4 Error Management | Error Analysis | Identification and quantification of random and systematic errors. | Identifying mispropagated labels or modalities, resource miscounts, broken relevance constraints, incorrect many-valued rule applications, invalid structural transformations, failed normalization sequences, and flawed rule schemas in non-classical proof implementations. |
| | Bias Control | Methods for minimizing subjective, instrumental, or procedural biases. | Avoiding structural bias in rule ordering, preventing over-reliance on classical heuristics in non-classical proof search, ensuring neutral treatment of modal depth, controlling implementation bias in relevance checking or resource tracking, and standardizing multi-valued evaluation strategies. |
| 4.5 Adjudication & Revision | Peer Scrutiny | Collective evaluation of claims through critique, review, and debate. | Reviewing derivations across modal/linear/relevant/paraconsistent calculi, evaluating normalization and cut-elimination arguments, critiquing rule schemas, verifying equivalence between different formulations (e.g., labeled vs. unlabeled), and meta-theoretic scrutiny of logic-specific proof properties. |
| | Theory Revision | Procedures for modifying, replacing, or discarding models based on new evidence. | Updating accessibility rules, adjusting resource constraints, modifying relevance conditions, refining many-valued rule schemas, altering sequent formats, strengthening or restricting structural rules, repairing failures in normalization or cut-elimination, and reformulating systems to better match semantic motivations. |
| 4.6 Integrity Conditions | Transparency | Requirements to disclose methods, data, assumptions, and limitations. | Full disclosure of modal rules, accessibility frameworks, resource annotations, relevance constraints, valuation schemes for many-valued systems, normalization steps, cut-elimination details, and implementation documentation for proof assistants. |
| | Ethical Standards | Norms ensuring responsible conduct in experimentation, data handling, and publication. | Honest reporting of logic-specific inference behavior, avoiding hidden semantic assumptions in rule definitions, ensuring reproducible non-classical proof experiments, documenting structural constraints clearly, and maintaining principled handling of non-classical derivability claims. |