I am in the exact same position with respect to type theory, it's maddening and depressing in equal measure. Not claiming to be any kind of expert here but may

I am in the exact same position with respect to type theory, it's maddening and depressing in equal measure. Not claiming to be any kind of expert here but maybe what is making the glass frosted for you is not quite grasping the following (not saying that I fully grasp it): > This new and revolutionary idea has had a far reaching and manifold impact on the development of modern logic. It provides the means to uniformly complete the formal apparatus of a functional analysis of language by generalizing the concept of a function and introducing a special kind of functions, namely propositional functions, or truth value functions, whose range of values consists of the set of truth values. Among the most typical representatives of propositional functions one finds predicate expressions and logical connectives. Predicate expressions[0] are: is tall? is green? is a woman? (adjectives and nominal and so on.) Logical connectives[1] are: and, or, not, … Imagine thinking about these concepts before the notion of using functions[2] arrived on the scene in mathematical logic and thinking about these concepts after. A part of me would love to believe that the problem (such as it is) resides with the communicative powers of the entire community of mathematical logicians and not with the learning power of my cerebral cortex but alas I fear the failure is mine. --- Anyway, what would one do without the Wikiverse? [0] https://en.wikipedia.org/wiki/Predicative_expression https://en.wikipedia.org/wiki/Predicative_expression [1] https://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/The_Sentential_Language#Sentential_connectives https://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/... [2] https://en.wikipedia.org/wiki/History_of_the_function_concept https://en.wikipedia.org/wiki/History_of_the_function_concep...