:: Predicate Calculus for Boolean Valued Functions, { I } :: by Shunichi Kobayashi and Yatsuka Nakamura :: :: Received December 21, 1998 :: Copyright (c) 1998-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, PARTIT1, MARGREL1, EQREL_1, BVFUNC_1, BVFUNC_2, XBOOLEAN, FUNCT_1; notations XBOOLE_0, SUBSET_1, XBOOLEAN, MARGREL1, FUNCT_2, EQREL_1, BVFUNC_1, BVFUNC_2; constructors BVFUNC_1, BVFUNC_2, RELSET_1, NUMBERS; registrations MARGREL1, ORDINAL1; requirements NUMERALS; begin :: Chap. 1 Predicate Calculus reserve Y for non empty set, G for Subset of PARTITIONS(Y), a,b,c,u for Function of Y,BOOLEAN, PA for a_partition of Y; theorem :: BVFUNC_3:1 (a 'imp' b) '<' (All(a,PA,G) 'imp' Ex(b,PA,G)); theorem :: BVFUNC_3:2 (All(a,PA,G) '&' All(b,PA,G)) '<' (a '&' b); theorem :: BVFUNC_3:3 (a '&' b) '<' (Ex(a,PA,G) '&' Ex(b,PA,G)); theorem :: BVFUNC_3:4 'not' (All(a,PA,G) '&' All(b,PA,G)) = Ex('not' a,PA,G) 'or' Ex('not' b , PA, G ); theorem :: BVFUNC_3:5 'not' (Ex(a,PA,G) '&' Ex(b,PA,G)) = All('not' a,PA,G) 'or' All('not' b ,PA,G) ; theorem :: BVFUNC_3:6 (All(a,PA,G) 'or' All(b,PA,G)) '<' (a 'or' b); theorem :: BVFUNC_3:7 (a 'or' b) '<' (Ex(a,PA,G) 'or' Ex(b,PA,G)); theorem :: BVFUNC_3:8 (a 'xor' b) '<' ('not' (Ex('not' a,PA,G) 'xor' Ex(b,PA,G)) 'or' 'not' (Ex(a,PA,G) 'xor' Ex( 'not' b,PA,G))); theorem :: BVFUNC_3:9 All(a 'or' b,PA,G) '<' All(a,PA,G) 'or' Ex(b,PA,G); theorem :: BVFUNC_3:10 All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' All(b,PA,G); theorem :: BVFUNC_3:11 All(a 'or' b,PA,G) '<' Ex(a,PA,G) 'or' Ex(b,PA,G); theorem :: BVFUNC_3:12 Ex(a,PA,G) '&' All(b,PA,G) '<' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:13 All(a,PA,G) '&' Ex(b,PA,G) '<' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:14 All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G); theorem :: BVFUNC_3:15 All(a 'imp' b,PA,G) '<' Ex(a,PA,G) 'imp' Ex(b,PA,G); theorem :: BVFUNC_3:16 Ex(a,PA,G) 'imp' All(b,PA,G) '<' All(a 'imp' b,PA,G); theorem :: BVFUNC_3:17 (a 'imp' b) '<' (a 'imp' Ex(b,PA,G)); theorem :: BVFUNC_3:18 (a 'imp' b) '<' (All(a,PA,G) 'imp' b); theorem :: BVFUNC_3:19 Ex(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G); theorem :: BVFUNC_3:20 All(a,PA,G) '<' Ex(b,PA,G) 'imp' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:21 u is_independent_of PA,G implies Ex(u 'imp' a,PA,G) '<' (u 'imp' Ex(a, PA,G)) ; theorem :: BVFUNC_3:22 u is_independent_of PA,G implies Ex(a 'imp' u,PA,G) '<' (All(a,PA,G) 'imp' u) ; theorem :: BVFUNC_3:23 All(a,PA,G) 'imp' Ex(b,PA,G) = Ex(a 'imp' b,PA,G); theorem :: BVFUNC_3:24 All(a,PA,G) 'imp' All(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G); theorem :: BVFUNC_3:25 Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' All(a,PA,G) 'imp' Ex(b,PA,G); theorem :: BVFUNC_3:26 All(a 'imp' b,PA,G) = All('not' a 'or' b,PA,G); theorem :: BVFUNC_3:27 All(a 'imp' b,PA,G) = 'not' (Ex(a '&' 'not' b,PA,G)); theorem :: BVFUNC_3:28 Ex(a,PA,G) '<' 'not' (All(a 'imp' b,PA,G) '&' All(a 'imp' 'not' b,PA,G )); theorem :: BVFUNC_3:29 Ex(a,PA,G) '<' 'not' ('not' Ex(a '&' b,PA,G) '&' 'not' Ex(a '&' 'not' b,PA,G)); theorem :: BVFUNC_3:30 Ex(a,PA,G) '&' All(a 'imp' b,PA,G) '<' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:31 Ex(a,PA,G) '&' 'not' Ex(a '&' b,PA,G) '<' 'not' All(a 'imp' b,PA,G); theorem :: BVFUNC_3:32 All(a 'imp' c,PA,G) '&' All(c 'imp' b,PA,G) '<' All(a 'imp' b,PA,G); theorem :: BVFUNC_3:33 All(c 'imp' b,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:34 All(b 'imp' 'not' c,PA,G) '&' All(a 'imp' c,PA,G) '<' All(a 'imp' 'not' b,PA,G); theorem :: BVFUNC_3:35 All(b 'imp' c,PA,G) '&' All(a 'imp' 'not' c,PA,G) '<' All(a 'imp' 'not' b,PA,G); theorem :: BVFUNC_3:36 All(b 'imp' 'not' c,PA,G) '&' Ex(a '&' c,PA,G) '<' Ex(a '&' 'not' b,PA ,G ); theorem :: BVFUNC_3:37 All(b 'imp' c,PA,G) '&' Ex(a '&' 'not' c,PA,G) '<' Ex(a '&' 'not' b,PA ,G ); theorem :: BVFUNC_3:38 Ex(c,PA,G) '&' All(c 'imp' b,PA,G) '&' All(c 'imp' a,PA,G) '<' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:39 All(b 'imp' c,PA,G) '&' All(c 'imp' 'not' a,PA,G) '<' All(a 'imp' 'not' b,PA,G); theorem :: BVFUNC_3:40 Ex(b,PA,G) '&' All(b 'imp' c,PA,G) '&' All(c 'imp' a,PA,G) '<' Ex(a '&' b,PA,G); theorem :: BVFUNC_3:41 Ex(c,PA,G) '&' All(b 'imp' 'not' c,PA,G) '&' All(c 'imp' a,PA,G) '<' Ex(a '&' 'not' b,PA,G);