A formal system for the non-theorems of the propositional calculus.
Xavier Caicedo · Notre Dame Journal of Formal Logic · 1978
Axioms and rulesWe assume that the only connectives are ~ and ^>.P> q> Pu p2, denote atomic formulae, a, β, y, . . .denote arbitrary formulae.We define P(a) = {p\p occurs in a}. AxiomsAl />=> ~/> {p atomic) A2 ~p ^ p (p atomic) Rules Rl (a) ---(p atomic, p does not occur in a)