An intuitionistic Sheffer function (Q1073779)

A function f is a Sheffer function for a set of functions F iff every function in F can be defined with the help of f by a finite number of compositions, and f can be defined by a finite number of compositions with the help of functions in F. Let \(\to,\wedge,\vee,\neg\) and \(\leftrightarrow\) be the usual propositional functions of the Heyting propositional calculus HPC. \textit{A. V. Kuznetsov} [Dokl. Akad. Nauk SSSR 160, 274-277 (1965; Zbl 0147.250)] and \textit{H. E. Hendry} [Notre Dame J. Formal Logic 22, 183-186 (1981; Zbl 0423.03021)] have shown that there is no binary Sheffer function for \(\{\) \(\to,\wedge,\vee,\neg \}\). Here it is shown that for this set we have the ternary Sheffer function t defined by \(t(p_ 1,p_ 2,p_ 3)\leftrightarrow ((p_ 1\vee p_ 2)\leftrightarrow (p_ 3\leftrightarrow \neg p_ 2))\). If \(f_ 1\) and \(f_ 2\) are n-ary propositional functions in HPC, then \(f_ 1\) and \(f_ 2\) are equivalent iff for some permutations \(P_ 1\) and \(P_ 2\) of the sequence \(p_ 1,...,p_ n\), in HPC we can prove \(f_ 1(P_ 1)\leftrightarrow f_ 2(P_ 2)\). The ternary propositional functions \(s_ 1\) and \(s_ 2\), defined by \(s_ 1(p_ 1,p_ 2,p_ 3)\leftrightarrow ((p_ 1\leftrightarrow p_ 2)\vee (p_ 1\leftrightarrow p_ 3))\) and \(s_ 2(p_ 1,p_ 2,p_ 3)\leftrightarrow ((p_ 1\vee p_ 2)\leftrightarrow p_ 3)\) are nonequivalent Sheffer functions for \(\{\) \(\to,\vee,\wedge \}\). There is also more than one nonequivalent Sheffer function for the whole set \(\{\) \(\to,\wedge,\vee,\neg \}\), but it is left open how many exactly.