scientific article; zbMATH DE number 150217

Authors

Publication date 1 April 1993

axiomatization implicational fragment of classical propositional logic implicational fragment of intuitionistic propositional logic implicational logic

Mathematics Subject Classification ID

Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20) Logical aspects of lattices and related structures (03G10)

Review text

The lattice of subsets of the following family of axioms is considered: \[ \begin{aligned} \text{I}. & \qquad p\to p\\ \text{B}. & \qquad (q\to r)\to ((p\to q)\to (p\to r))\\ \text{C}. & \qquad (p\to (q\to r))\to (q\to (p\to r))\\ \text{W}. & \qquad (p\to (p\to q))\to (p\to q)\\ \text{K}_ 1. & \qquad (p\to q)\to (r\to (p\to q)).\end{aligned} \] The rules of inference: substitution and modus ponens. Let \(H_ \to\) be an implicational fragment of intuitionistic propositional logic, and \(TV_ \to\) be an implicational fragment of classical propositional logic. Then I, B, C, W, \(\text{K}_ 1\) form an independent axiomatization of \(H_ \to\). The problem of extending \(H_ \to\) to \(TV_ \to\) by some formula \(X\) (with such properties that I, B, C, W, \(\text{K}_ 1\), \(X\) is an independent axiomatization of \(TV_ \to\)) was raised. This problem was solved by the author in 1992, where \(X\) is \[ (p\to ((q\to q)\to p))\to (((p\to q)\to q)\to ((q\to p)\to p)) \] with the condition that \(\text{K}_ 1\) is replaced equivalently by \(\text{K}_ 1'\): \[ r\to ((p\to q)\to (p\to q)). \] A complete proof will be published in the same journal in the paper ``Construction of classical propositional logic.

Recommendations

Cited in

(22)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4032849)