Category:Proof theory

• Proof theory

*

• Epsilon calculus

A

• Analytic proof

B

• Bachmann–Howard ordinal
• Bounded quantifier
• Büchi arithmetic

C

• Church–Kleene ordinal
• Completeness
• Completeness of atomic initial sequents
• Conservative extension
• Conservativity theorem
• Consistency
• Curry–Howard correspondence
• Cut-elimination theorem

D

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

E

• Elementary function arithmetic
• Extension by definitions

F

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

G

• Gentzen's consistency proof
• Geometry of interaction

G cont.

• Original proof of Gödel's completeness theorem
• Gödel's speed-up theorem
• Gödel's completeness theorem
• Double-negation translation
• Gödel's incompleteness theorems

H

• Hardy hierarchy
• Herbrand's theorem
• Hilbert system
• Hilbert's program

I

• Independence (mathematical logic)
• Interpretability

J

• Judgment (mathematical logic)

L

• Lambda-mu calculus
• Large countable ordinal
• User:Larissanpa/sandbox

M

• Mathematical fallacy
• Mathematical induction
• Metalanguage

N

• Natural deduction
• NuPRL

O

• Ω-consistent theory
• Ordinal analysis
• Ordinal notation

P

• Paraconsistent mathematics
• Peano-Russell notation
• Presburger arithmetic
• Primitive recursive functional
• Proof (truth)
• Proof calculus

P cont.

• Proof compression
• Proof mining
• Proof net
• Proof procedure
• Proof-theoretic semantics
• Provability logic
• Ψ₀(Ωω)
• Pure type system

R

• Realizability
• Resolution proof compression by splitting
• Resolution proof reduction via local context rewriting
• Reverse mathematics

S

• Self-verifying theories
• Sequent
• Sequent calculus
• Setoid
• Slow-growing hierarchy
• Soundness
• Soundness (interactive proof)
• Structural proof theory
• Structural rule

T

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

U

• Undecidable problem

V

• Veblen function
• VIPER microprocessor

W

• Weak interpretability

Z

• Zariski's lemma