Revision #896 → #1502 · back to history
addedProof theory93fe048b8fef
addedStructural proof theory1f04728c500f
addedCut-elimination property99faed4ff4f3
addedCorollaries of cut-elimination (midsequent, Craig interpolation, Herbrand)08e0b26e63fe
addedSubformula property496614d38ea8
addedSubformula property implies consistency513daf9c0931
addedAnalytic proofs as normal forms (natural deduction)b7cdb6c65f04
addedFocused proofsb172b7de026b
addedHarmony of introduction/elimination rules9ca762a58967
addedMaximal formulaf84e4ce95498
addedNon-local !-rule in linear logic427e3d662072
addedCurry–Howard correspondence790e9a38a12f
addedOrdinal analysis0d30f6691075
addedWell-foundedness implies consistency of T99e07776ede5
addedGentzen's consistency of Peano Arithmetic60f4d9078ffb
addedTakeuti's consistency of Π¹₁-CA₀9b8be68af601
addedProvability logic445263364dc8
addedLöb's theorem25ea66fd8722
addedSolovay's completeness theorem for GL3be51c627195
addedReverse mathematicsf4feaf2b1023
addedAxiom of choice and Zorn's lemma equivalence263e36082f7c
addedBounded sequence has supremum2286c4b49141
addedReversal in reverse mathematics532a1a1a99ec
addedRobustness of the Big Five4aa8035d6e78
addedFunctional interpretations634d486e2cd3
addedDialectica interpretationdca46ea65c42