Identity and Permutation

Aleksandar Kron

Publications de l'Institut Mathématique, _N_S_57 (1995) no. 71, p. 165

Résumé

It is known that in the purely implicational fragment of the system TW$_{\to}$ if both $(A\to B)$ and $ (B\to A)$ are theorems, then $A$ and $B$ are the same formula (the Anderson--Belnap conjecture). This property is equivalent to NOID (no identity!): if the axiom-shema $(A\to A)$ is omitted from TW$_{\to}$ and the system TW$_{\to}$-ID is obtained, then there is no theorem of the form $(A\to A)$. A Gentzen-style purely implicational system J is here constructed such that NOID holds for J. NOID is proved to be equivalent to NOE: there no theorem of J of the form $((A\to A)\to B)\to B$, i.e., of the form of the characteristic axiom of the implicational system E$_{\to}$ of entailment. If $ (p\to p)$ is adjoined to J as an axiom-schema (ID), then there are theorems $(A\to B)$ and $(B\to A)$ such that $A$ and $B$ are distinct formulas, which shows that for J the Anderson--Belnap conjecture is not equivalent to NOID. The system J+ID is equivalent to bf RW$_{\to}$ of relevance logic.

Détail

Classification : 11A05