An intuitionistic Sheffer function.
Kosta Došen · Notre Dame Journal of Formal Logic · 1985
The purpose of this note is to present a ternary propositional function which is a Sheffer function in the Heyting propositional calculus.We shall also consider some related Sheffer functions in positive logic.Although it is easy to guess what should be the general notion of a Sheffer function in a propositional calculus, we shall first fix our terminology.Following [2] and [1], we shall say that a set of functions F is a Sheffer set for a set of functions G iff every member of G can be defined by a finite number of compositions from the members of F. A set F is an indigenous Sheffer set for G iff F is a Sheffer set for G and G is a Sheffer set for F, A function / is an (indigenous) Sheffer function for G iff {/} is a (indigenous) Sheffer set for G.Of course these notions will interest us here only when the functions in question are propositional functions.Unless stated otherwise, ->, Λ, V, ->, , Λ, v}, since in the Heyting propositional calculus we can prove (A-+B)~((AvB)~B) (A ΛB)++((A vB)++(A ~B)) .(A useful survey of such equivalences can be found in [3] and [4], p. 21.)Some further economy was achieved by Schroeder-Heister in [7].He shows that {s, ±} is an indigenous Sheffer set for {->, Λ, V, -«}, where 5* is a ternary propositional function defined by s(Aι,A 2 ,A 3 )~((A l "A 2 )vA 3 ) .Then in the Heyting propositional calculus we can prove