Category:Proof theory
![]() | Computing portal |
Here is a list of articles in the Proof theory category of the Computing portal that unifies foundations of mathematics and computations using computers.
In mathematics, Proof theory is the study of formalized arguments.
Subcategories
This category has the following 6 subcategories, out of 6 total.
M
P
R
S
Pages in category "Proof theory"
The following 93 pages are in this category, out of 93 total.
- 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)