On the definition of negation by a fixed proposition in inferential calculus
Haskell Brooks Curry · Journal of Symbolic Logic · 1952
It is well known that negation can be defined by postulating a fixed proposition F and specifying that where “≡” indicates identity by definition. I propose to discuss this way of introducing negation in relation to the inferential systems of my Notre Dame lectures of 1948. Acquaintance with these lectures is presupposed; they will be referred to as TFD. The definition (1) was used there, essentially, in connection with the T-systems; but it was not used in connection with the L-systems because of a certain difficulty which I was not able to overcome at that time. This paper contains proofs of results concerning L-systems which have been announced elsewhere.