:: Connectives and Subformulae of the First Order Language :: by Grzegorz Bancerek :: :: Received November 23, 1989 :: Copyright (c) 1990-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 NUMBERS, FINSEQ_1, QC_LANG1, SUBSET_1, ZF_LANG, XBOOLEAN, XXREAL_0, CARD_1, ORDINAL4, BVFUNC_2, FUNCT_1, CLASSES2, MCART_1, REALSET1, ARYTM_3, NAT_1, RELAT_1, ARYTM_1, TARSKI, XBOOLE_0, QC_LANG2; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, NAT_1, FINSEQ_1, XTUPLE_0, MCART_1, QC_LANG1, XXREAL_0; constructors ENUMSET1, XXREAL_0, XREAL_0, NAT_1, QC_LANG1, XTUPLE_0, NUMBERS; registrations RELSET_1, XREAL_0, FINSEQ_1, ORDINAL1, NAT_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve A for QC-alphabet; reserve sq for FinSequence, x,y,z for bound_QC-variable of A, p,q,p1,p2,q1 for Element of QC-WFF(A); theorem :: QC_LANG2:1 the_argument_of 'not' p = p; theorem :: QC_LANG2:2 p '&' q = p1 '&' q1 implies p = p1 & q = q1; theorem :: QC_LANG2:3 p is conjunctive implies p = (the_left_argument_of p) '&' the_right_argument_of p; theorem :: QC_LANG2:4 the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q; theorem :: QC_LANG2:5 All(x,p) = All(y,q) implies x = y & p = q; theorem :: QC_LANG2:6 p is universal implies p = All(bound_in p, the_scope_of p); theorem :: QC_LANG2:7 bound_in All(x,p) = x & the_scope_of All(x,p) = p; definition let A be QC-alphabet; func FALSUM(A) -> QC-formula of A equals :: QC_LANG2:def 1 'not' VERUM(A); let p,q be Element of QC-WFF(A); func p => q -> QC-formula of A equals :: QC_LANG2:def 2 'not' (p '&' 'not' q); func p 'or' q -> QC-formula of A equals :: QC_LANG2:def 3 'not' ('not' p '&' 'not' q); end; definition let A be QC-alphabet; let p,q be Element of QC-WFF(A); func p <=> q -> QC-formula of A equals :: QC_LANG2:def 4 (p => q) '&' (q => p); end; definition let A be QC-alphabet; let x be bound_QC-variable of A, p be Element of QC-WFF(A); func Ex(x,p) -> QC-formula of A equals :: QC_LANG2:def 5 'not' All(x,'not' p); end; theorem :: QC_LANG2:8 FALSUM(A) is negative & the_argument_of FALSUM(A) = VERUM(A); theorem :: QC_LANG2:9 p 'or' q = 'not' p => q; theorem :: QC_LANG2:10 p 'or' q = p1 'or' q1 implies p = p1 & q = q1; theorem :: QC_LANG2:11 p => q = p1 => q1 implies p = p1 & q = q1; theorem :: QC_LANG2:12 p <=> q = p1 <=> q1 implies p = p1 & q = q1; theorem :: QC_LANG2:13 Ex(x,p) = Ex(y,q) implies x = y & p = q; definition let A be QC-alphabet; let x,y be bound_QC-variable of A, p be Element of QC-WFF(A); func All(x,y,p) -> QC-formula of A equals :: QC_LANG2:def 6 All(x,All(y,p)); func Ex(x,y,p) -> QC-formula of A equals :: QC_LANG2:def 7 Ex(x,Ex(y,p)); end; theorem :: QC_LANG2:14 All(x,y,p) = All(x,All(y,p)) & Ex(x,y,p) = Ex(x,Ex(y,p)); theorem :: QC_LANG2:15 for x1,x2,y1,y2 being bound_QC-variable of A st All(x1,y1,p1) = All( x2,y2,p2) holds x1 = x2 & y1 = y2 & p1 = p2; theorem :: QC_LANG2:16 All(x,y,p) = All(z,q) implies x = z & All(y,p) = q; theorem :: QC_LANG2:17 for x1,x2,y1,y2 being bound_QC-variable of A st Ex(x1,y1,p1) = Ex(x2, y2,p2) holds x1 = x2 & y1 = y2 & p1 = p2; theorem :: QC_LANG2:18 Ex(x,y,p) = Ex(z,q) implies x = z & Ex(y,p) = q; theorem :: QC_LANG2:19 All(x,y,p) is universal & bound_in All(x,y,p) = x & the_scope_of All(x ,y,p) = All(y,p); definition let A be QC-alphabet; let x,y,z be bound_QC-variable of A, p be Element of QC-WFF(A); func All(x,y,z,p) -> QC-formula of A equals :: QC_LANG2:def 8 All(x,All(y,z,p)); func Ex(x,y,z,p) -> QC-formula of A equals :: QC_LANG2:def 9 Ex(x,Ex(y,z,p)); end; theorem :: QC_LANG2:20 All(x,y,z,p) = All(x,All(y,z,p)) & Ex(x,y,z,p) = Ex(x,Ex(y,z,p)); theorem :: QC_LANG2:21 for x1,x2,y1,y2,z1,z2 being bound_QC-variable of A st All(x1,y1,z1,p1) = All(x2,y2,z2,p2) holds x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2; reserve s,t for bound_QC-variable of A; theorem :: QC_LANG2:22 All(x,y,z,p) = All(t,q) implies x = t & All(y,z,p) = q; theorem :: QC_LANG2:23 All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q; theorem :: QC_LANG2:24 for x1,x2,y1,y2,z1,z2 being bound_QC-variable of A st Ex(x1,y1,z1,p1) = Ex( x2,y2,z2,p2) holds x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2; theorem :: QC_LANG2:25 Ex(x,y,z,p) = Ex(t,q) implies x = t & Ex(y,z,p) = q; theorem :: QC_LANG2:26 Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q; theorem :: QC_LANG2:27 All(x,y,z,p) is universal & bound_in All(x,y,z,p) = x & the_scope_of All(x,y,z,p) = All(y,z,p); definition let A be QC-alphabet; let H be Element of QC-WFF(A); attr H is disjunctive means :: QC_LANG2:def 10 ex p,q being Element of QC-WFF(A) st H = p 'or' q; attr H is conditional means :: QC_LANG2:def 11 ex p,q being Element of QC-WFF(A) st H = p => q; attr H is biconditional means :: QC_LANG2:def 12 ex p,q being Element of QC-WFF(A) st H = p <=> q; attr H is existential means :: QC_LANG2:def 13 ex x being bound_QC-variable of A, p being Element of QC-WFF(A) st H = Ex(x,p); end; theorem :: QC_LANG2:28 Ex(x,y,p) is existential & Ex(x,y,z,p) is existential; definition let A be QC-alphabet; let H be Element of QC-WFF(A); func the_left_disjunct_of H -> QC-formula of A equals :: QC_LANG2:def 14 the_argument_of the_left_argument_of the_argument_of H; func the_right_disjunct_of H -> QC-formula of A equals :: QC_LANG2:def 15 the_argument_of the_right_argument_of the_argument_of H; func the_antecedent_of H -> QC-formula of A equals :: QC_LANG2:def 16 the_left_argument_of the_argument_of H; end; notation let A be QC-alphabet; let H be Element of QC-WFF(A); synonym the_consequent_of H for the_right_disjunct_of H; end; definition let A be QC-alphabet; let H be Element of QC-WFF(A); func the_left_side_of H -> QC-formula of A equals :: QC_LANG2:def 17 the_antecedent_of the_left_argument_of H; func the_right_side_of H -> QC-formula of A equals :: QC_LANG2:def 18 the_consequent_of the_left_argument_of H; end; reserve F,G,H,H1 for Element of QC-WFF(A); theorem :: QC_LANG2:29 the_left_disjunct_of(F 'or' G) = F & the_right_disjunct_of(F 'or' G) = G & the_argument_of F 'or' G = 'not' F '&' 'not' G; theorem :: QC_LANG2:30 the_antecedent_of(F => G) = F & the_consequent_of(F => G) = G & the_argument_of F => G = F '&' 'not' G; theorem :: QC_LANG2:31 the_left_side_of(F <=> G) = F & the_right_side_of(F <=> G) = G & the_left_argument_of(F <=> G) = F => G & the_right_argument_of(F <=> G) = G => F; theorem :: QC_LANG2:32 the_argument_of Ex(x,H) = All(x,'not' H); theorem :: QC_LANG2:33 H is disjunctive implies H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of the_argument_of H is negative & the_right_argument_of the_argument_of H is negative; theorem :: QC_LANG2:34 H is conditional implies H is negative & the_argument_of H is conjunctive & the_right_argument_of the_argument_of H is negative; theorem :: QC_LANG2:35 H is biconditional implies H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional; theorem :: QC_LANG2:36 H is existential implies H is negative & the_argument_of H is universal & the_scope_of the_argument_of H is negative; theorem :: QC_LANG2:37 H is disjunctive implies H = (the_left_disjunct_of H) 'or' ( the_right_disjunct_of H); theorem :: QC_LANG2:38 H is conditional implies H = (the_antecedent_of H) => ( the_consequent_of H); theorem :: QC_LANG2:39 H is biconditional implies H = (the_left_side_of H) <=> ( the_right_side_of H); theorem :: QC_LANG2:40 H is existential implies H = Ex(bound_in the_argument_of H, the_argument_of the_scope_of the_argument_of H); :: :: Immediate constituents of QC-formulae :: definition let A be QC-alphabet; let G,H be Element of QC-WFF(A); pred G is_immediate_constituent_of H means :: QC_LANG2:def 19 H = 'not' G or (ex F being Element of QC-WFF(A) st H = G '&' F or H = F '&' G) or ex x being bound_QC-variable of A st H = All(x,G); end; reserve x,y,z for bound_QC-variable of A, k,n,m for Nat, P for ( QC-pred_symbol of k, A), V for QC-variable_list of k, A; theorem :: QC_LANG2:41 not H is_immediate_constituent_of VERUM(A); theorem :: QC_LANG2:42 not H is_immediate_constituent_of P!V; theorem :: QC_LANG2:43 F is_immediate_constituent_of 'not' H iff F = H; theorem :: QC_LANG2:44 H is_immediate_constituent_of FALSUM(A) iff H = VERUM(A); theorem :: QC_LANG2:45 F is_immediate_constituent_of G '&' H iff F = G or F = H; theorem :: QC_LANG2:46 F is_immediate_constituent_of All(x,H) iff F = H; theorem :: QC_LANG2:47 H is atomic implies not F is_immediate_constituent_of H; theorem :: QC_LANG2:48 H is negative implies (F is_immediate_constituent_of H iff F = the_argument_of H); theorem :: QC_LANG2:49 H is conjunctive implies (F is_immediate_constituent_of H iff F = the_left_argument_of H or F = the_right_argument_of H); theorem :: QC_LANG2:50 H is universal implies (F is_immediate_constituent_of H iff F = the_scope_of H); :: :: Subformulae of QC-formulae :: reserve L,L9 for FinSequence; definition let A be QC-alphabet; let G,H be Element of QC-WFF(A); pred G is_subformula_of H means :: QC_LANG2:def 20 ex n,L st 1 <= n & len L = n & L.1 = G & L.n = H & for k st 1 <= k & k < n ex G1,H1 being Element of QC-WFF(A) st L.k = G1 & L.(k+1) = H1 & G1 is_immediate_constituent_of H1; reflexivity; end; definition let A be QC-alphabet; let H,F be Element of QC-WFF(A); pred H is_proper_subformula_of F means :: QC_LANG2:def 21 H is_subformula_of F & H <> F; irreflexivity; end; theorem :: QC_LANG2:51 H is_immediate_constituent_of F implies len @H < len @F; theorem :: QC_LANG2:52 H is_immediate_constituent_of F implies H is_subformula_of F; theorem :: QC_LANG2:53 H is_immediate_constituent_of F implies H is_proper_subformula_of F; theorem :: QC_LANG2:54 H is_proper_subformula_of F implies len @H < len @F; theorem :: QC_LANG2:55 H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F; theorem :: QC_LANG2:56 F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H; theorem :: QC_LANG2:57 F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H; theorem :: QC_LANG2:58 G is_subformula_of H & H is_subformula_of G implies G = H; theorem :: QC_LANG2:59 not (G is_proper_subformula_of H & H is_subformula_of G); theorem :: QC_LANG2:60 not (G is_proper_subformula_of H & H is_proper_subformula_of G); theorem :: QC_LANG2:61 not (G is_subformula_of H & H is_immediate_constituent_of G); theorem :: QC_LANG2:62 not (G is_proper_subformula_of H & H is_immediate_constituent_of G); theorem :: QC_LANG2:63 F is_proper_subformula_of G & G is_subformula_of H or F is_subformula_of G & G is_proper_subformula_of H or F is_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_subformula_of H or F is_proper_subformula_of G & G is_immediate_constituent_of H or F is_immediate_constituent_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H; theorem :: QC_LANG2:64 not F is_proper_subformula_of VERUM(A); theorem :: QC_LANG2:65 not F is_proper_subformula_of P!V; theorem :: QC_LANG2:66 F is_subformula_of H iff F is_proper_subformula_of 'not' H; theorem :: QC_LANG2:67 'not' F is_subformula_of H implies F is_proper_subformula_of H; theorem :: QC_LANG2:68 F is_proper_subformula_of FALSUM(A) iff F is_subformula_of VERUM(A); theorem :: QC_LANG2:69 F is_subformula_of G or F is_subformula_of H iff F is_proper_subformula_of G '&' H; theorem :: QC_LANG2:70 F '&' G is_subformula_of H implies F is_proper_subformula_of H & G is_proper_subformula_of H; theorem :: QC_LANG2:71 F is_subformula_of H iff F is_proper_subformula_of All(x,H); theorem :: QC_LANG2:72 All(x,H) is_subformula_of F implies H is_proper_subformula_of F; theorem :: QC_LANG2:73 F '&' 'not' G is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G; theorem :: QC_LANG2:74 'not' F '&' 'not' G is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G; theorem :: QC_LANG2:75 H is atomic implies not F is_proper_subformula_of H; theorem :: QC_LANG2:76 H is negative implies the_argument_of H is_proper_subformula_of H; theorem :: QC_LANG2:77 H is conjunctive implies the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ; theorem :: QC_LANG2:78 H is universal implies the_scope_of H is_proper_subformula_of H; theorem :: QC_LANG2:79 H is_subformula_of VERUM(A) iff H = VERUM(A); theorem :: QC_LANG2:80 H is_subformula_of P!V iff H = P!V; theorem :: QC_LANG2:81 H is_subformula_of FALSUM(A) iff H = FALSUM(A) or H = VERUM(A); :: :: Set of subformulae of QC-formulae :: definition let A be QC-alphabet; let H be Element of QC-WFF(A); func Subformulae H -> set means :: QC_LANG2:def 22 for a being object holds a in it iff ex F being Element of QC-WFF(A) st F = a & F is_subformula_of H; end; theorem :: QC_LANG2:82 G in Subformulae H implies G is_subformula_of H; theorem :: QC_LANG2:83 F is_subformula_of H implies Subformulae F c= Subformulae H; theorem :: QC_LANG2:84 G in Subformulae H implies Subformulae G c= Subformulae H; theorem :: QC_LANG2:85 Subformulae(VERUM(A)) = { VERUM(A) }; theorem :: QC_LANG2:86 Subformulae(P!V) = { P!V }; theorem :: QC_LANG2:87 Subformulae(FALSUM(A)) = { VERUM(A), FALSUM(A) }; theorem :: QC_LANG2:88 Subformulae 'not' H = Subformulae H \/ { 'not' H }; theorem :: QC_LANG2:89 Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F }; theorem :: QC_LANG2:90 Subformulae All(x,H) = Subformulae H \/ { All(x,H) }; theorem :: QC_LANG2:91 Subformulae (F => G) = Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }; theorem :: QC_LANG2:92 Subformulae (F 'or' G) = Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&' 'not' G, F 'or' G}; theorem :: QC_LANG2:93 Subformulae (F <=> G) = Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G, 'not' F, G '&' 'not' F, G => F, F <=> G }; theorem :: QC_LANG2:94 H = VERUM(A) or H is atomic iff Subformulae H = { H }; theorem :: QC_LANG2:95 H is negative implies Subformulae H = Subformulae the_argument_of H \/ { H }; theorem :: QC_LANG2:96 H is conjunctive implies Subformulae H = Subformulae the_left_argument_of H \/ Subformulae the_right_argument_of H \/ { H }; theorem :: QC_LANG2:97 H is universal implies Subformulae H = Subformulae the_scope_of H \/ { H }; theorem :: QC_LANG2:98 (H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G) & G in Subformulae F implies H in Subformulae F;