Truth table logic, with a survey of embeddability results (Q912092)

The propositional natural deduction systems considered here have standard introduction rules [including (A\(\vdash \Lambda)\vdash \sim A]\) and less standard elimination rules always having conclusion \(\Lambda\), for example, A,\(\sim A/\Lambda\) or A\&B, (A\(\vdash \Lambda)\vdash \Lambda\) etc. Only normal derivations are considered satisfying the relevance condition (discharged assumption cannot be absent), and the normalization theorem is invalid. The main lemma in Kalmar's proof of the completeness theorem, but not the theorem itself, can be proved in the system. A version of Glivenko's theorem (\(\vdash A\) classically implies \(\vdash \sim \sim A\) in the system considered) is also established.