Premium
Intuitionistic ϵ‐ and τ‐calculi
Author(s) -
Devidi David
Publication year - 1995
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.19950410409
Subject(s) - extensionality , mathematics , extensional definition , calculus (dental) , operator (biology) , algebra over a field , intuitionistic logic , predicate (mathematical logic) , semantics (computer science) , discrete mathematics , pure mathematics , linear logic , computer science , programming language , tectonics , medicine , paleontology , biochemistry , chemistry , dentistry , repressor , gene , transcription factor , biology
There are several open problems in the study of the calculi which result from adding either of Hilbert's ϵ‐ or τ‐operators to the first order intuitionistic predicate calculus. This paper provides answers to several of them. In particular, the first complete and sound semantics for these calculi are presented, in both a “quasi‐extensional” version which uses choice functions in a straightforward way to interpret the ϵ‐ or τ‐terms, and in a form which does not require extensionality assumptions. Unlike the classical case, the addition of either operator to intuitionistic logic is non‐conservative. Several interesting consequences of the addition of each operator are proved. Finally, the independence of several other schemes in either calculus are also proved, making use of the semantics supplied earlier in the paper.