Category:Proof theory

• Proof theory (computing)

A

• Analytic proof (philosophy)

B

• Bachmann–Howard ordinal (computing)
• Bounded quantifier (computing)
• Büchi arithmetic (computing)

C

• Church–Kleene ordinal (computing)
• Cirquent calculus (computing)
• Completeness (logic) (philosophy)
• Completeness of atomic initial sequents (physics)
• Conservative extension (computing)
• Conservativity theorem (computing)
• Consistency (computing)
• Curry–Howard correspondence (computing)
• Cut-elimination theorem (computing)

D

• Decidability (logic) (philosophy)
• Decidable sublanguages of set theory (computing)
• Deduction theorem (computing)
• Deep inference (philosophy)
• Dialectica interpretation (philosophy)
• Disjunction and existence properties (computing)

E

• Elementary function arithmetic (computing)
• Epsilon calculus (philosophy)
• Extension by definitions (computing)
• Extension by new constant and function names (computing)

F

• Fast-growing hierarchy (computing)
• Feferman–Schütte ordinal (computing)
• Formal proof (computing)
• Friedman translation (computing)

G

• Gentzen's consistency proof (computing)
• Geometry of interaction (computing)
• Original proof of Gödel's completeness theorem (computing)
• Gödel's speed-up theorem (computing)
• Double-negation translation (philosophy)
• Gödel's completeness theorem (computing)
• Gödel's incompleteness theorems (computing)

H

• Hardy hierarchy (computing)
• Herbrand's theorem (computing)
• Hilbert system (computing)
• Hilbert's program (computing)
• Hypersequent (philosophy)

I

• Independence (mathematical logic) (philosophy)
• Interpretability (philosophy)

J

• Japaridze's polymodal logic (philosophy)
• Judgment (mathematical logic) (computing)

L

• Lambda-mu calculus (computing)
• Large countable ordinal (computing)
• LowerUnits (computing)

M

• Mathematical fallacy (philosophy)
• Metalanguage (philosophy)

N

• Natural deduction (philosophy)
• Nested sequent calculus (philosophy)
• Non-surveyable proof (computing)

O

• Ω-consistent theory (philosophy)
• Ordinal analysis (computing)
• Ordinal notation (computing)

P

• Paraconsistent mathematics (philosophy)
• Peano–Russell notation (philosophy)
• Presburger arithmetic (computing)
• Primitive recursive functional (computing)
• Proof (truth) (computing)
• Proof calculus (philosophy)
• Proof compression (philosophy)
• Proof mining (philosophy)
• Proof net (philosophy)
• Proof procedure (philosophy)
• Proof-theoretic semantics (philosophy)
• Provability logic (philosophy)
• Ψ₀(Ωω) (computing)
• Pure type system (computing)

R

• Realizability (computing)
• Redundant proof (philosophy)
• Resolution inference (computing)
• Resolution proof compression by splitting (philosophy)
• Resolution proof reduction via local context rewriting (philosophy)
• Reverse mathematics (computing)
• Reverse Mathematics: Proofs from the Inside Out

S

• Self-verifying theories (philosophy)
• Sequent (computing)
• Sequent calculus (computing)
• Setoid (computing)
• Slicing the Truth (computing)
• Slow-growing hierarchy (computing)
• Soundness (computing)
• Soundness (interactive proof) (philosophy)
• Structural proof theory (philosophy)
• Structural rule (computing)
• System U (computing)

T

• Takeuti's conjecture (computing)
• Tolerant sequence (philosophy)
• Turnstile (symbol) (computing)

V

• Veblen function (computing)
• VIPER microprocessor (engineering)

W

• Weak interpretability (philosophy)