# Is Curry's paradox caused by allowing definitions to implicitly assert existence?

Context: I'm studying the lambda-calculus and formal systems of logic, and it seems that the naive approach to extending the lambda-calculus into a higher-order logic leads to Curry's paradox (https://en.wikipedia.org/wiki/Curry's_paradox).

Everything I've read about Curry's paradox suggests that it is caused by allowing self-referential statements to be made in the logical system being used. Simply prohibiting such statements would solve the problem; however, not all self-referential statements lead to paradoxes and this solution would prohibit those as well.

I'm wondering if there is a more general issue here involving the act of introducing a definition. When I say "let X be the statement that X implies Y", I am implicitly asserting that X represents a valid mathematical object (in this case, a statement that can be proven true or false).

To illustrate, here is a proof that TRUE = FALSE.

Let B be a boolean value such that B = TRUE and B = FALSE.
B = B        (tautology)
TRUE = B     (substitute definition of B)
TRUE = FALSE (substitute definition of B)


The (obvious) flaw here is that B cannot represent a valid mathematical object. Using B as if it did exist leads to contradiction.

I'm wondering if there are any systems of logic out there that require definitions to be accompanied with proof that they don't contradict the axioms of the system or any previous definitions.

Could such a system avoid Curry's paradox without ever explicitly prohibiting self-referential statements?

• I'm wondering if there are any systems of logic out there that require definitions to be accompanied with proof that they don't contradict the axioms of the system - yes, most of them? Commented Apr 27 at 1:42
• @MishaLavrov Standard formal systems like ZFC do not allow definitions to be made within them, they are part of informal meta-language. When mathematicians make definitions they are expected to prove existence before the objects defined can be used, but that norm is not formalized or formalizable in ZFC. The lambda-calculus is different because definitions can be made within the calculus itself, not just as informal abbreviations. Commented Apr 27 at 6:07