Premium
Extended Curry‐Howard terms for second‐order logic
Author(s) -
Vejjajiva Pimpen
Publication year - 2013
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201100102
Subject(s) - curry , axiom , mathematics , mathematical proof , order (exchange) , calculus (dental) , mathematical economics , discrete mathematics , algebra over a field , pure mathematics , computer science , programming language , medicine , geometry , dentistry , finance , economics
In order to allow the use of axioms in a second‐order system of extracting programs from proofs, we define constant terms , a form of Curry‐Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry‐Howard terms are strongly normalizable.