Proof Theory

← Back to Domain-Specific Abstractions by Domain

7 domain-specific abstractions whose origin domain is Proof Theory.

• Elementary function arithmetic — A weak first-order arithmetic theory whose provably total functions are the elementary recursive functions, typically extending bounded arithmetic with exponentiation.
• Hilbert system — An axiomatic proof calculus in which theorems are generated from axiom schemata by a small set of inference rules, often only modus ponens plus a rule for quantification.
• Independence of premise — A constructive-logical principle allowing an existential witness to be moved outside an implication when the premise does not contain that witness variable.
• Ludics — Reconstruct logical propositions and proofs from address-based designs, polarized actions, and successful interaction, defining meaning extensionally through orthogonality rather than presupposed formulas.
• Negation introduction — A rule of inference that derives not-P after assuming P and deriving a contradiction within a properly discharged subproof.
• Ordinal collapsing function — A notation-building function that introduces symbols for very large ordinals and systematically collapses them into canonical notations for large countable ordinals.
• Slow-Growing Hierarchy — Builds an ordinal-indexed family of natural-number functions by successor increments and fundamental-sequence descent at limits.