Propositional Calculus for Boolean Valued Functions. Part VII Shunichi Kobayashi Matsumoto University

Summary. In this paper, we proved some elementary propositional calculus formulae for Boolean valued functions. MML Identifier:BVFUNC25. WWW:http://mizar.org/JFM/Vol15/bvfunc25.html The articles [4], [3], [2], and [1] provide the notation and terminology for this paper. We use the following convention: Y is a non empty set and a, b, c, d are elements of Boolean Y. We now state a number of propositions: (1) ¬(a ⇒ b) = a ∧ ¬b. (2) ¬b ⇒ ¬a ⇒ a ⇒ b = true(Y). (3) a ⇒ b = ¬b ⇒ ¬a. (4) a ⇔ b = ¬a ⇔ ¬b. (5) a ⇒ b = a ⇒ a ∧ b. (6) a ⇔ b = a ∨ b ⇒ a ∧ b. (7) a ⇔ ¬a = false(Y). (8) a ⇒ b ⇒ c = b ⇒ a ⇒ c