Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

app

app2

app3

arrow

atr0_ordinal_gamma0_ty

atr0_ordinal_gamma0 : OrdinalAnalysis ATR0 Gamma0

barwise_compactness_ty

BarwiseCompactness : Prop Barwise compactness for admissible sets.

bezem_majorizability_ty

BezemMajorizability : (Nat → Nat) → (Nat → Nat) → Prop Bezem’s strong majorizability.

bezem_realizability_ty

BezemRealizability : Formula → Type Bezem’s strong computability realizability.

bool_ty

bounded_arithmetic_ty

BoundedArithmetic: PA^ω conservativity results

bounded_primitive_recursor_ty

BoundedPrimitiveRecursor : (Nat → Nat → Nat) → Nat → Nat Bounded primitive recursion (Kohlenbach’s T^ω_b).

build_env

Register all proof mining and realizability axioms into the kernel environment.

build_env_extended

Extend the proof mining environment with the new §7–§15 axioms.

bvar

cauchy_rate_ty

CauchyRate : (Nat → Nat) → Prop A modulus of convergence (Cauchy rate) for a sequence.

choice_function_realization_ty

ChoiceFunctionRealization : (Nat → Prop) → (Nat → Nat) Realizing a choice function from a provability assumption.

clause_ty

Clause: disjunction of literals

complexity_bound_ty

ComplexityBound: polynomial/exponential bound extracted

compute_bound_ty

compute_bound: extract a uniform bound from a proof compute_bound : WitnessExtractor → Nat

cook_reckhow_thm_ty

CookReckhowThm: NP-completeness ↔ no efficient proof system CookReckhow : (∃ sys : ProofSystem, Efficient sys) ↔ NP_equals_CoNP

cst

curry_howard_ty

CurryHoward: proof-as-program correspondence

dialectica_formula_ty

DialecticaFormula: Gödel’s Dialectica translation A^D as (∃u.∀x. A_D(u,x))

dialectica_nci_equiv_ty

dialectica_no_counterexample_equiv : ∀ A, Dialectica A ↔ NCI A

dialectica_soundness_ty

dialectica_soundness: if PA proves A then A^D is realized dialectica_soundness : ∀ (A : Formula), Provable A → Realized (Dialectica A)

empty_clause_ty

EmptyClause: ⊥ (contradiction)

epsilon0_ty

Epsilon0 : Ordinal — ε_0, the proof-theoretic ordinal of PA.

ergodic_theorem_mining_ty

ergodic_theorem_mining : Prop Quantitative bounds extracted from the ergodic theorem (Avigad-Rute).

extract_witness_ty

extract_witness: given a proof of ∃x.P(x), produce a term extract_witness : ∀ (P : Nat → Prop), (∃ x, P x) → HerbrandTerm

extracted_program_ty

ExtractedProgram: ML-like program extracted from constructive proof

fluctuation_rate_ty

FluctuationRate : Nat → Nat Upper bound on the number of ε-fluctuations of a sequence.

functional_interpretation_ty

FunctionalInterpretation: computable functional realizing ∀∃ statements

functional_interpretations

Functional interpretation of arithmetic.

gamma0_ty

Gamma0 : Ordinal — Γ_0, the Feferman-Schütte ordinal (ATR_0).

godel_functional_interp_ty

GodelFunctionalInterp : Formula → Type Full Gödel functional interpretation (combining Dialectica with T).

herbrand_bound_extraction_ty

herbrand_bound_extraction : ∀ (f : Nat → Nat), MetastabilityBound f → ∃ n, Φ n ≤ HerbrandBound n

herbrand_bound_ty

HerbrandBound : Nat → Nat A Herbrand-style bound on the number of instances needed.

herbrand_complexity_ty

herbrand_complexity : HerbrandSequence F → Nat The size (number of ground instances) in a Herbrand sequence.

herbrand_sequence_ty

HerbrandSequence : Formula → Type A Herbrand sequence (finite disjunction of ground instances).

herbrand_term_ty

HerbrandTerm: explicit witness extracted from ∃x.P(x)

herbrand_theorem_ty

herbrand_theorem : ∀ (A : Formula), Valid A → ∃ H, HerbrandSequence A H ∧ TautologyGround H

heuristic_fn_ty

HeuristicFn: estimate distance to proof

howard_majorizability_ty

HowardMajorizability : (Nat → Nat) → (Nat → Nat) → Prop Howard’s majorizability: f majorizes g if ∀n, g n ≤ f n.

impl_pi

is_realizable_ty

is_realizable: check realizability of a formula is_realizable : Formula → Prop

kreisel_modified_realizability_ty

KreiselModifiedRealizability : Formula → Type Kreisel’s modified realizability interpretation.

majorizability_closure_ty

majorizability_closure : ∀ f g h, HowardMaj f g → HowardMaj g h → HowardMaj f h

metastability_bound_ty_axiom

MetastabilityBoundTy : (Nat → Nat) → Prop Terence Tao’s metastability: ∀ ε k, ∃ n ≤ Φ(ε,k), …

model_checking_bound_ty

ModelCheckingBound: bounded model checking with BMC encoding

model_theoretic_mining_ty

ModelTheoreticMining : Prop — model-theoretic metatheorem for proof mining.

modified_realizability_soundness_ty

modified_realizability_soundness : ∀ A, Provable A → KreiselMR A

monotone_functional_interp_ty

MonotoneFunctionalInterp : DialecticaFormula → Type Kohlenbach’s bounded / monotone functional interpretation.

nat_ty

no_counterexample_interp_ty

NoCounterexampleInterpretation : Formula → Type Kreisel’s no-counterexample interpretation (nci) of PA.

ordinal_analysis_ty

OrdinalAnalysis : ProofSystem → Ordinal → Prop The proof-theoretic ordinal of a system S is α.

ordinal_ty

Ordinal : Type — the type of proof-theoretic ordinals.

pa_ordinal_epsilon0_ty

pa_ordinal_epsilon0 : OrdinalAnalysis PA Epsilon0

pi

program_extraction_soundness_ty

program_extraction_soundness: extracted program computes the right function program_extraction_soundness : ∀ (P : Prop), Proof P → Realizes (Extract P) P

proof_complexity_measure_ty

ProofComplexityMeasure: size, depth, width, degree

proof_mining_results_survey

Survey of proof mining results in analysis.

proof_searcher_ty

ProofSearcher: systematic proof search with backtracking

proof_state_ty

ProofState: current goals, applied tactics, remaining budget

proof_system_ty

ProofSystem enum type

prop

propositional_proof_ty

PropositionalProof: sequence of lines with justifications

realizability_interpretation_ty

RealizabilityInterpretation: Kleene’s or Kreisel’s modified realizability

realized_formula_ty

RealizedFormula: realizability type for a formula

resolution_completeness_ty

resolution_completeness: unsatisfiable CNF has a resolution refutation resolution_completeness : ∀ (F : CNFFormula), ¬Satisfiable F → ResolutionRefutation F

resolution_proof_ty

ResolutionProof: DAG of resolution steps

resolution_refutation_ty

ResolutionRefutation: proof of unsatisfiability

resolution_step_ty

ResolutionStep: C_1 ∨ x, C_2 ∨ ¬x ⊢ C_1 ∨ C_2

saturation_strategy_name

search_strategy_ty

SearchStrategy type

shoenfield_completeness_ty

ShoenfieldCompleteness : Prop Shoenfield’s completeness theorem for realizability.

termination_proof_ty

TerminationProof: well-founded induction certificate

troelstra_modified_realizability_ty

TroelstraModifiedRealizability : Formula → Type Troelstra’s variant of modified realizability.

type0

uniform_continuity_extraction_ty

uniform_continuity_extraction : ∀ (f : Nat → Nat), WeakCompact f → ∃ ω, UniformContinuityModulus f ω

uniform_continuity_modulus_ty

UniformContinuityModulus : (Nat → Nat) → Nat → Nat ω(f, ε) = modulus of uniform continuity of f at precision ε.

veblen_function_ty

VeblenFunction : Ordinal → Ordinal → Ordinal φ(α, β) — the Veblen φ-function for ordinal analysis.

we_hpca_ty

WE_HPCA : Prop — WE-HPCA metatheorem (Kohlenbach): uniform bound extraction in metric spaces.

we_hrca_ty

WE_HRCA : Prop — WE-HRCA metatheorem: system for real-closed arithmetic.

weak_compactness_mining_ty

weak_compactness_mining : Prop Mining uniform bounds from weak compactness arguments.

weak_koenighs_lemma_ty

WeakKoenigsLemma: WKL and its Dialectica interpretation

witness_extractor_ty

WitnessExtractor: extracts computational content from a proof