Proof Calculi

				Formal Sciences
				Logic
				Proof Theory
Element	Scope Category	Sub-Item	Definition	Proof Calculi
1. Domain	1.1 Scope of the Domain	Boundaries	The range of phenomena the science includes and excludes.	Studies formal systems for derivations and inference; includes syntactic proof structures, rule applications, derivability; excludes semantic truth conditions except as constraints on proof correctness.
		Scale	The spatial, temporal, or organizational level at which the science operates (e.g., quantum, cellular, social, cosmic).	Operates at the symbolic/logical level: proof steps, inference rules, sequents, derivation trees, tableaux branches, and rule schemas.
	1.2 Ontological Commitments	Entities	The kinds of things assumed to exist within the domain (particles, organisms, agents, fields, etc.).	Formulas, sequents, contexts, inference rules, proof trees, derivations, metavariables, structural rules.
		Properties	The fundamental attributes these entities possess (mass, charge, genotype, preference, etc.).	Well-formedness, admissibility, derivability, proof height, proof length, structural position, rule applicability, substitution behavior.
		Categories	The basic ontological types used to classify domain elements (substances, processes, relations, structures).	Logical rules, structural rules, axioms, derivations, Hilbert systems, sequent systems, natural deduction rules, analytic tableaux expansions.
	1.3 State-Variables	Variables	The measurable or definable properties that describe system conditions.	Current sequent/formula, active rule, proof depth, branching factor, open/closed tableaux branches, structural configuration.
		Parameterization	How variables encode and represent the system’s state.	Representation via sequents (Γ ⊢ Δ), natural-deduction contexts, rule schemas, substitution assignments, structural constraints.
	1.4 Admissible Idealizations	Simplifications	Conceptual reductions used to make the domain tractable (point masses, rational agents, perfect gases).	Treating rules as schematic rather than instantiated; idealized structural rules; ignoring resource sensitivity unless the calculus requires it.
		Validity Conditions	The limits and contexts in which idealizations hold or break down.	Break down in substructural logics (no contraction/weakening), relevance logics, resource-sensitive calculi, or systems with restricted rule forms.
	1.5 Domain Assumptions	Structural Assumptions	Background ontological stances such as determinism, continuity, randomness, discreteness.	Assumes discrete symbolic steps, rule-based derivability, finitary inference, effective rule application.
		Implicit Commitments	Unstated but necessary assumptions that shape the field’s conceptual structure.	Assumes syntactic correctness, substitution principles, structural rule behavior, and meta-level reasoning about rule admissibility and derivability.
	1.6 Internal Coherence Requirements	Consistency	The demand that domain concepts do not contradict one another.	Requires rule systems to avoid triviality; derivations must not generate contradictions unless modeling paraconsistent systems.
		Compatibility	The requirement that entities, variables, and assumptions fit together into a unified descriptive framework.	Requires alignment between rule schemas, structural conventions (e.g., exchange, contraction), derivation formats, and meta-theoretical notions such as admissibility and cut-elimination.
2. Evidence Layer	2.1 Observable Phenomena	Observables	The aspects of the domain that can produce detectable signals accessible to measurement.	Derivation steps, rule applications, sequent transformations, proof-tree expansions, closure of tableaux branches, admissibility of rules, derivability judgments (⊢).
		Detection Limits	The boundaries of what can be resolved or sensed by current instruments or methods.	Limited by formal syntax, decidability of derivability, proof-search complexity, rule-schema generality, and computability of admissibility or cut-elimination.
	2.2 Measurement Systems	Units	Standardized quantifications (meters, seconds, volts, decibels, dollars, etc.) necessary for consistent comparison.	Proof length, proof depth, number of rule applications, branching factor, derivation height, complexity class (e.g., P, NP, PSPACE).
		Instruments	Devices and tools (microscopes, spectrometers, sensors, surveys, detectors) used to produce measurements.	Automated theorem provers, proof checkers, SMT/SAT solvers, sequent-calculus engines, tableaux provers, proof assistants (Coq, Lean, Isabelle).
	2.3 Operational Definitions	Definitions	Terms defined by specific measurement procedures, ensuring empirical clarity.	Derivability defined by explicit rule applications; admissibility defined by elimination of rule instances; cut-free derivation defined by structural criteria.
		Procedures	The explicit steps required to perform a measurement in a reproducible way.	Running proof search, normalizing derivations, applying rule schemas, checking branch closure, verifying cut-elimination, computing proof height/length.
	2.4 Data Acquisition	Protocols	Formal processes for gathering data under controlled or standardized conditions.	Standardized proof-search strategies, sequent-calculus search trees, normalization workflows, canonical proof transformations.
		Sampling	Rules determining which subset of the domain is measured and how representative it is.	Selecting representative derivations, rule applications, structural configurations, subsets of formulas, extremal proof paths.
	2.5 Data Character & Format	Data Types	The form raw evidence takes (time series, spectra, images, counts, qualitative records).	Proof trees, sequent derivations, tableaux branches, rule-application sequences, normal forms, cut-free proofs, derivation graphs.
		Resolution	The granularity or precision with which data is captured.	Determined by granularity of derivation encoding, rule-schema specificity, proof-step detail, substitution tracking, and context changes.
	2.6 Reliability & Calibration	Calibration	Adjustment procedures ensuring instruments produce accurate results.	Verifying proof-checker correctness, validating rule implementations, confirming structural-rule behavior, checking normalization algorithm reliability.
		Error Characterization	Identification and quantification of noise, uncertainty, bias, and measurement error.	Misapplied rules, incorrect substitutions, flawed heuristics, non-admissible steps, incorrect closure conditions, implementation errors in automated provers.
3. Structural Layer	3.1 Patterns & Regularities	Laws / Relations	Stable, repeatable patterns governing how observables behave across conditions.	Rule-application patterns, sequent-structural behavior, normalization relations, introduction/elimination correspondences, cut–reduction patterns, rule admissibility relations.
		Invariants	Quantities or properties that remain constant under transformations (symmetries, conservation laws).	Structural invariants (e.g., context preservation), proof height monotonicity under normalization, admissibility invariants, substitution invariants, symmetry of rule schemas, invariance under renaming of variables.
	3.2 Causal Architecture	Mechanisms	Underlying processes or structures that produce the observed regularities.	Rule-triggering mechanisms (e.g., decomposition of formulas), structural rule effects (exchange, weakening, contraction), cut-elimination processes, tableau branch expansion/closure.
		Pathways	Organized sequences of interactions forming a causal chain or network.	Ordered sequences of rule applications forming derivation paths: natural-deduction introduction→elimination cycles, sequent-calculus left/right rule chains, tableaux branching→closure sequences, normalization pathways in proof reduction.
	3.3 Theoretical Vocabulary	Concepts	Core terms that encode the domain’s structure (force, gene, equilibrium, field).	Derivability, sequents, contexts, inference rules, admissibility, analyticity, cut, normalization, subformula property, proof height, proof identity, rule invertibility.
		Classifications	Taxonomies, categories, or typologies that organize entities and relations.	Hilbert calculi, natural deduction systems, sequent calculi (LK, LJ), analytic tableaux, structural-rule taxonomies (with/without contraction/weakening), classical vs. intuitionistic vs. modal proof calculi.
	3.4 Formal Representations	Equations	Mathematical constructs expressing laws, relations, or mechanisms.	Structural reflection principles (e.g., Γ, A ⊢ B ⇔ Γ ⊢ A → B), normalization equations, proof-equality conditions, cut-reduction equalities, rule-permutation equalities.
		Models	Structured representations—mathematical, computational, or conceptual—used to predict and explain phenomena.	Derivation trees, proof graphs, sequent-forest representations, tableaux branching models, canonical proof-search models, normalization models, cut-free proof frameworks.
	3.5 Idealized Structures	Simplified Models	Purposeful abstractions that capture essential dynamics while omitting irrelevant detail.	Cut-free calculi, analytic calculi with subformula property, idealized rule sets (minimal structural rules), simplified derivation trees, restricted proof forms (normal forms).
		Limit Conditions	Regimes where specific models or approximations hold (classical vs. quantum, linear vs. nonlinear).	Breakdown in non-classical logics (substructural, relevance, modal), calculi without structural rules, systems requiring resource sensitivity, proofs exceeding decidability limits, contexts where normalization fails or is non-terminating.
	3.6 Integrative Frameworks	Unifying Theories	Higher-order structures that connect disparate laws or mechanisms under a coherent whole.	Curry–Howard correspondences (proofs-as-programs), cut-elimination as unifying structural principle, general proof-theoretic semantics, meta-theoretic frameworks connecting calculi across logics.
		Interdisciplinary Links	Points where the theory connects to adjacent sciences or larger explanatory systems.	Links to type theory, lambda calculus, automated reasoning, computational complexity, semantics of programming languages, category theory (e.g., cartesian closed categories), and modal/temporal logics.
4. Method Layer	4.1 Inquiry Design	Experimental Design	Structured plans for manipulating variables to test causal claims.	Manipulating rule sets, adding/removing structural rules, modifying sequent contexts, constraining introduction/elimination rules, enforcing or restricting cut to test derivability behavior.
		Observational Design	Systematic approaches for gathering non-manipulated data (surveys, field studies, natural experiments).	Observing derivation trees, proof-search behavior, rule application frequency, normalization dynamics, closure of tableaux branches, and admissibility patterns without altering the calculus.
	4.2 Testing & Validation	Hypothesis Testing	Procedures for evaluating whether evidence supports or contradicts specific claims.	Testing whether a rule is admissible, whether a formula is derivable, whether cut-elimination holds, whether normalization terminates, or whether two proofs are equivalent.
		Replication	The requirement that results be independently reproducible under similar conditions.	Reproducing derivations across different proof systems, re-running normalization, verifying sequent derivations via independent proof assistants, checking tableau closures across solvers.
	4.3 Inference & Evaluation	Statistical Inference	Rules for drawing conclusions from noisy or incomplete data.	Analyzing proof-search complexity, frequency of rule applications, distribution of proof lengths, and performance of automated provers under systematic variation.
		Model Comparison	Criteria (fit, simplicity, predictive accuracy, robustness) used to evaluate competing models.	Comparing calculi by proof length, cut-elimination strength, analytic vs. non-analytic proofs, decidability, normalization behavior, and computational complexity (e.g., PSPACE vs. EXPTIME).
	4.4 Error Management	Error Analysis	Identification and quantification of random and systematic errors.	Detecting incorrect rule applications, faulty substitutions, illegal structural transformations, non-terminating proof searches, misclassified branches, or false rule-admissibility claims.
		Bias Control	Methods for minimizing subjective, instrumental, or procedural biases.	Preventing heuristic-driven distortions in proof search, avoiding rule-priority biases, using canonical derivation forms, controlling for implementation biases in theorem provers.
	4.5 Adjudication & Revision	Peer Scrutiny	Collective evaluation of claims through critique, review, and debate.	Cross-verifying derivations, reviewing admissibility proofs, evaluating normalization arguments, comparing encodings of systems across proof assistants, meta-theoretic critique of calculi.
		Theory Revision	Procedures for modifying, replacing, or discarding models based on new evidence.	Updating rule sets, repairing non-admissible rules, strengthening structural principles, refining sequent formats, replacing non-normalizing rules, modifying systems to regain cut-elimination.
	4.6 Integrity Conditions	Transparency	Requirements to disclose methods, data, assumptions, and limitations.	Releasing full derivations, rule schemas, cut-elimination proofs, normalization steps, and prover configurations; documenting admissibility tests and search heuristics.
		Ethical Standards	Norms ensuring responsible conduct in experimentation, data handling, and publication.	Ensuring honest reporting of derivations, avoiding hidden assumptions in rule definitions, maintaining reproducible proof-search environments, and accurately documenting system limitations.