Today I just had an insight:
Haskell Curry proposed combinatory logic as a logica universalis, but it ran into inconsistency problems. (I'm trying to use fuzzy-probabilistic truth values to get around that problem, but that's a different topic.)
So, in 1963 JA Robinson discovered resolution, which is really unification + propositional resolution. Unification decides if 2 terms can be made equationally identical. Propositional resolution deals with the "calculus of thinking" at the proposition level.
Combinatory logic provides a free way to compose terms via "application". I regard terms as concepts. For example:
"tall handsome guy"
is the combination of the concepts
tall ∙ (handsome ∙ guy).
Now, a few examples:
"tall handsome guy" is equivalent to "handsome tall guy";
"very tall guy" implies "tall guy"; but
"very tall guy" does not equal "tall very guy";
Thus the unification theory is modulo some special rules akin to commutativity, associativity, etc, and certain reduction rules. In other words, unification modulo a theory = "the calculus of concepts".
So we have a neat decomposition:
calculus of thoughts = calculus of concepts
+ calculus of propositions
+ calculus of propositions
