Remarks on variable binding term operators
Abstract
A variable binding term operator is an operator which binds variables of formulas to give origin to terms. Examples of vbtos are the description operator ι, Hilbert’s ε-symbol, the classifier { : }, and Russell’s abstraction operator ˆx1xˆ2 . . . xˆnF. It is usual to introduce vbtos by contextual definition, though their treatment in first- and higherorder languages as new primitive symbols, added to them, is more convenient, especially from the semantic point of view. A semantic approach to vbtos in classical logic is contained in da Costa 1980 . In this note we outline how vbtos can be handled in some paraconsistent and paracomplete logics, precisely those logics of da Costa 1974 and da Costa and Marconi 1986. But our methods apply equally will to several other non-classical systems. Although in some particular cases, for instance in the case of the description operator in certain first-order languages, the contextual treatment of vbtos seems to be reasonable, we limit ourselves here to the semantic approach to these operators. In order to develop our semantic analysis, we combine the methods of da Costa 1980 with those of Alves 1984; in this last paper, a paraconsistent model theory is studied relative to da Costa’s predicate calculi with equality C = n , 1 ≤ n ≤ ω