On Skolemization in constructive theories

DOI10.2178/JSL/1230396760zbMath1171.03035OpenAlexW3023954237MaRDI QIDQ3617374

Rosalie Iemhoff, Matthias Baaz

Publication date: 23 March 2009

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1005.5856

zbMATH Keywords

cut eliminationderivabilityintuitionistic theoryconstructive theoryHerbrand expansionorderizationconstructive Skolemization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Related Items (5)

The eskolemization of universal quantifiers ⋮ Proof analysis in intermediate logics ⋮ Skolemization and Herbrand theorems for lattice-valued logics ⋮ The Skolemization of prenex formulas in intermediate logics ⋮ Automating Theories in Intuitionistic Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Constructivism in mathematics. An introduction. Volume I
• Handbook of proof theory
• The Skolemization of existential quantifiers in intuitionistic logic

This page was built for publication: On Skolemization in constructive theories