I am reading http://okmij.org/ftp/gengo/applicative-symantics/AACG1.pdf and there is defined language TL (see last row in the table on page 4). It seems to me from this definition of TL, that lambda calculus is the language of universal logic - each connective (unary, binary, ternary, etc.; quantifiers can be expressed in this language as well - as unary functions) is just another function (of type t->t->t - for binary connective) and the only difference between this simple function and connective function is the following: connective functions have constraints in the form of logical rules (e.g. connective or quantifier introduction or elimination rules), simple functions have no such rules.
So - my questions are:
- Do I understand correctly, that lambda calculus is (can be) the language of Universal Logic (in the tradition of https://link.springer.com/journal/11787)? If no, then why not? If yes, then why there is no wide adoption of lambda calculus in the Univeral Logic community?
- Do I understand correctly that connectives are just another functions with the constraints. Is it possible to defined constraints on other functions (simple functions) in the lambda calculus without changing the base logic? I.s. how logical rules for connective functions differ from the user-defined additional rules/constraints for simple functions?
So - the fully hierarchy of the logics can be defined purely by the introduction of connective functions in lambda calculus and by the additional rules on them. So simple?
Of course, I am aware of Curry-Howard isomorphism but its talk about "propositions as types, proofs as lambda terms" is somehow disconnected with the straight appearance of lambda calculus as the language of universal logic. Maybe there exists answer that connects my feelings about lambda calculus as the language of universal logic with the CHI.
