I think Mike is thinking of my question in a different way than I intended. If p, q, and r range over the set {0,1}, then (p-->q)-->r is one Boolean function on {0,1}^3 and p-->(q-->r) is another; they are different ternary Boolean functions because they have different truth-tables. Do all five of the Boolean functions obtained by parenthesizing p-->q-->r-->s have distinct truth-tables? What about the fourteen Boolean functions obtained by parenthesizing p-->q-->r-->s-->t? Etc. Jim Propp On Fri, Dec 1, 2017 at 11:09 AM, Mike Stay <metaweta@gmail.com> wrote:
On Fri, Dec 1, 2017 at 8:52 AM, James Propp <jamespropp@gmail.com> wrote:
A different kind of "exponentiation" is logical implication (-->), which has the same relation to conjunction that exponentiation has to multiplication, inasmuch as the equivalence between p --> (q --> r) and (p and q) --> r resembles the equality between (c^b)^a =and c^(ba).
This isomorphism is called "Currying" after Haskell Curry. It works in any monoidal closed category. In particular, as you suggest below, by the Curry-Howard isomorphism logical implication corresponds to the "arrow type" or internal hom in the category of sets and functions.
Do all the Catalan-many parenthesizations of p_1 --> p_2 --> ... --> p_n yield distinct Boolean functions?
That doesn't quite parse. The expression with arrows in it is a type, which describes a set of functions. You could ask whether any two parenthesizations of p_1 --> p_2 --> ... --> p_n are equal as sets, but that's a category-theoretic "evil", since it depends on the representation you choose; instead you can ask whether the sets are isomorphic. The answer is yes; for example,
(3^(3^3))^(((3^3)^3)^3) = (((3^3)^3)^3)^(3^(3^3))
thought of combinatorically exhibits an isomorphism between the sets.
Comparing two functions for equality, both of whose type is the same parenthesization of p_1 --> p_2 --> ... --> p_n, does make sense, but it has nothing to do with moving around the parens.
-- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun