godelian wrote: ↑Wed Jun 22, 2022 2:18 pm
The problem with the untyped lambda calculus revolves around Haskell Curry's paradox.
I am familiar with Curry's paradox. What I don't understand is why you think this paradox, or any paradox is a "problem".
It's just a theorem. It's true that allowing conditionals such as "if A, then B" is sufficient to prove any B.
Or if you want me to say this in a Reverse Mathematical setting. What are the sufficient conditions for proving any B?
Answer: Conditionals in the form of "if A, then B"
godelian wrote: ↑Wed Jun 22, 2022 2:18 pm
The paradox is closely connected to the problem of unrestricted set comprehension in set theory
Nor do I understand why you think unrestricted comprehension is a "problem".
godelian wrote: ↑Wed Jun 22, 2022 2:18 pm
Standard Set Theory (ZFC) hedges against that problem by introducing axioms that outlaw unrestricted set comprehension
I didn't realise there were legal and moral authorities in Mathematics. So much so that you could "outlaw" stuff?
godelian wrote: ↑Wed Jun 22, 2022 2:18 pm
Allowing this in the untyped lambda calculus has the same effect as allowing unrestricted set comprehension in ZFC. It makes the theory inconsistent
Sure. And? Are you willing to give up unrestricted comprehension for the sake of consistency? It's just an engineering trade-off - a design choice.
Consistency, inconsistency, para-consistency, completeness, incompleteness, decidability, semi-decidability etc. are just semantic properties of the theory itself. Surely people can design their theories to exhibit whatever semantic properties their hearts desire?
You can design a consistent-but-incomplete theory about the numbers.
You can design a complete-but-inconsistent theory about the numbers.
You just can't design a consistent AND complete theory about the numbers.
What I see is a choice, but I don't see a problem?
godelian wrote: ↑Wed Jun 22, 2022 2:18 pm
In principle, set theory has the same problem as the lambda calculus, but in set theory the problem can be reined in by adding axioms that deal with it. However, even a set theory improved with axiomatic restrictions cannot add axioms that will successfully defeat Gödel's incompleteness theorems.
Perhaps it's best you define what you mean by "problem", because it sure seems to me that you think a whole bunch of semantic properties/features of formal systems are "problematic". You seem to think those features are bugs - so much so that you are willing to limit the expressive power of your system just to avoid them.
Could it be that you carry some sort of an axiomatic bias?
Could it be that you hold an axiom so dear that you wouldn't consider giving it up?
Could it be that you have a sacred cow that you would never consider slaughtering?
Could you be religious?