An intutionistic Sheffer's stroke (Pistone-Tranchini)

This topic refers to the course Proof-theoretic harmony (Pistone-Tranchini). Here is a description and a bibliography for addressing it.

In classical propositional logic, Sheffer's stroke is a connective denoting a truth-function in terms of which every other truth-function can be defined. Analogous connectives can be found in the intuitionistic case, i.e. connectives in terms of which all (standard) intuitionistic connectives can be defined. Your task is to provide harmonious natural deduction rules for such a connective, and using them show the definability of the usual connectives.

Bibliography

• K. Došen, "An intuitionistic Sheffer function", Notre Dame journal of formal logic 26:479-482, 1985

• P. Schroeder-Heister, "The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony", Studia Logica 102:1185-1216, 2014