[TYPES] Recovering functions from classical disjunction and negation

Klaus Ostermann klaus.ostermann at uni-tuebingen.de
Sat Aug 28 17:28:33 EDT 2021


In classical logic, implication A -> B can be encoded as (not A \/ B).

Is there any work on how that encoding works on the term side of things, 
that is, how
to encode lambda abstraction and application in terms of these logical 
connectives.
For instance, there are variants of Parigot's lambda mu calculus with 
primitive disjunction
and negation (such as by Pym, Ritter and Wallen or de Groote (2001) ). 
Shouldn't it
be possible to remove implication / lambda from such calculi and encode 
them as macros?
Has this been done?

Regards,

Klaus




More information about the Types-list mailing list