Algebraic Logic Perspective on Prucnal’s Substitution
Alex Citkin · Notre Dame Journal of Formal Logic · 2016
A term td(p,q,r) is called a ternary deductive (TD) term for a variety of algebras V if the identity td(p,p,r)≈r holds in V and (c,d)∈θ(a,b) yields td(a,b,c)≈td(a,b,d) for any A∈V and any principal congruence θ on A. A connective f(p1,…,pn) is called td-distributive if td(p,q,f(r1,…,rn))≈ f(td(p,q,r1),…,td(p,q,rn)). If L is a propositional logic and V is a corresponding variety (algebraic semantic) that has a TD term td, then any admissible in L rule, the premises of which contain only td-distributive operations, is derivable, and the substitution r↦td(p,q,r) is a projective L-unifier for any formula containing only td-distributive connectives. The above substitution is a generalization of the substitution introduced by T. Prucnal to prove structural completeness of the implication fragment of intuitionistic propositional logic.