scientific article; zbMATH DE number 432699

MaRDI QIDQ3138826zbMATH OpenFDO

Authors Stanley S. Wainer, Lincoln Wallen

Publication date 11 November 1993

zbMATH Keywords

\(\Sigma_ 1\)-inductive fragment of arithmeticcompletenessCurry-Howard correspondencecut-eliminationintroductory lecturelinear logicnatural deductionnormalizationpure prediate logicsequent calculussynthesis of primitive recursive bounding functions

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30)

Recommendations

• scientific article; zbMATH DE number 949290
• scientific article; zbMATH DE number 42059
• scientific article; zbMATH DE number 1215493
• scientific article; zbMATH DE number 1469885
• Lectures on the Curry-Howard isomorphism

Cited in

(10)

• Normal functors, power series and -calculus
• Programming in metric temporal logic
• Some results on cut-elimination, provable well-orderings, induction and reflection
• Verified Prover
• scientific article; zbMATH DE number 1552073 (Why is no real title available?)
• scientific article; zbMATH DE number 941039 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• Proofs, reasoning and the metamorphosis of logic
• Introduction to proof theory
• Predicates as types

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3138826)