:: Connectives and Subformulae of the First Order Language
:: by Grzegorz Bancerek
::
:: Received November 23, 1989
:: Copyright (c) 1990-2026 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;
definitions TARSKI, QC_LANG1, XBOOLE_0;
equalities QC_LANG1;
expansions QC_LANG1;
theorems TARSKI, ENUMSET1, NAT_1, FUNCT_1, FINSEQ_1, QC_LANG1, XBOOLE_0,
XBOOLE_1, XREAL_1, XXREAL_0;
schemes NAT_1, XBOOLE_0;
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 Th1:
the_argument_of 'not' p = p
proof
'not' p is negative;
hence thesis by QC_LANG1:def 24;
end;
theorem Th2:
p '&' q = p1 '&' q1 implies p = p1 & q = q1
proof
assume
A1: p '&' q = p1 '&' q1;
<*[2,0]*>^@p^@q = <*[2,0]*>^(@p^@q) & <*[2,0]*>^@p1^@q1 = <*[2,0]*>^(@p1
^@q1 ) by FINSEQ_1:32;
then
A2: @p^@q = @p1^@q1 by A1,FINSEQ_1:33;
then
A3: len @p1 <= len @p implies ex sq st @p = @p1^sq by FINSEQ_1:47;
A4: len @p <= len @p1 implies ex sq st @p1 = @p^sq by A2,FINSEQ_1:47;
hence p = p1 by A3,QC_LANG1:13;
(ex sq st @p1 = @p^sq) implies p1 = p by QC_LANG1:13;
hence thesis by A1,A3,A4,FINSEQ_1:33,QC_LANG1:13;
end;
theorem Th3:
p is conjunctive implies p = (the_left_argument_of p) '&'
the_right_argument_of p
proof
given p1,q1 such that
A1: p = p1 '&' q1;
A2: p is conjunctive by A1;
then p1 = the_left_argument_of p by A1,QC_LANG1:def 25;
hence thesis by A1,A2,QC_LANG1:def 26;
end;
theorem Th4:
the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q
proof
p '&' q is conjunctive;
hence thesis by QC_LANG1:def 25,def 26;
end;
theorem Th5:
All(x,p) = All(y,q) implies x = y & p = q
proof
A1: <*[3,0]*>^<*x*>^@p = <*[3,0]*>^(<*x*>^@p) & <*[3,0]*>^<*y*>^@q = <*[3,0]
*>^( <*y*>^@q) by FINSEQ_1:32;
A2: (<*x*>^@p).1 = x & (<*y*>^@q).1 = y by FINSEQ_1:41;
assume
A3: All(x,p) = All(y,q);
hence x = y by A1,A2,FINSEQ_1:33;
<*x*>^@p = <*y*>^@q by A3,A1,FINSEQ_1:33;
hence thesis by A2,FINSEQ_1:33;
end;
theorem Th6:
p is universal implies p = All(bound_in p, the_scope_of p)
proof
given x,q such that
A1: p = All(x,q);
A2: p is universal by A1;
then x = bound_in p by A1,QC_LANG1:def 27;
hence thesis by A1,A2,QC_LANG1:def 28;
end;
theorem Th7:
bound_in All(x,p) = x & the_scope_of All(x,p) = p
proof
All(x,p) is universal;
then All(x,p) = All(bound_in All(x,p), the_scope_of All(x,p)) by Th6;
hence thesis by Th5;
end;
definition
let A be QC-alphabet;
func FALSUM(A) -> QC-formula of A equals
'not' VERUM(A);
correctness;
let p,q be Element of QC-WFF(A);
func p => q -> QC-formula of A equals
'not' (p '&' 'not' q);
correctness;
func p 'or' q -> QC-formula of A equals
'not' ('not' p '&' 'not' q);
correctness;
end;
definition
let A be QC-alphabet;
let p,q be Element of QC-WFF(A);
func p <=> q -> QC-formula of A equals
(p => q) '&' (q => p);
correctness;
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
'not' All(x,'not' p);
correctness;
end;
theorem
FALSUM(A) is negative & the_argument_of FALSUM(A) = VERUM(A)
by Th1;
theorem
p 'or' q = 'not' p => q;
theorem
p 'or' q = p1 'or' q1 implies p = p1 & q = q1
proof
assume p 'or' q = p1 'or' q1;
then 'not' p '&' 'not' q = 'not' p1 '&' 'not' q1 by FINSEQ_1:33;
then 'not' p = 'not' p1 & 'not' q = 'not' q1 by Th2;
hence thesis by FINSEQ_1:33;
end;
theorem Th11:
p => q = p1 => q1 implies p = p1 & q = q1
proof
assume p => q = p1 => q1;
then
A1: p '&' 'not' q = p1 '&' 'not' q1 by FINSEQ_1:33;
hence p = p1 by Th2;
'not' q = 'not' q1 by A1,Th2;
hence thesis by FINSEQ_1:33;
end;
theorem
p <=> q = p1 <=> q1 implies p = p1 & q = q1
proof
assume p <=> q = p1 <=> q1;
then p => q = p1 => q1 by Th2;
hence thesis by Th11;
end;
theorem Th13:
Ex(x,p) = Ex(y,q) implies x = y & p = q
proof
assume Ex(x,p) = Ex(y,q);
then
A1: All(x,'not' p) = All(y,'not' q) by FINSEQ_1:33;
then 'not' p = 'not' q by Th5;
hence thesis by A1,Th5,FINSEQ_1:33;
end;
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
All(x,All(y,p));
correctness;
func Ex(x,y,p) -> QC-formula of A equals
Ex(x,Ex(y,p));
correctness;
end;
theorem
All(x,y,p) = All(x,All(y,p)) & Ex(x,y,p) = Ex(x,Ex(y,p));
theorem Th15:
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
proof
let x1,x2,y1,y2 be bound_QC-variable of A such that
A1: All(x1,y1,p1) = All(x2,y2,p2);
thus x1 = x2 by A1,Th5;
All(y1,p1) = All(y2,p2) by A1,Th5;
hence thesis by Th5;
end;
theorem
All(x,y,p) = All(z,q) implies x = z & All(y,p) = q by Th5;
theorem Th17:
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
proof
let x1,x2,y1,y2 be bound_QC-variable of A such that
A1: Ex(x1,y1,p1) = Ex(x2,y2,p2);
thus x1 = x2 by A1,Th13;
Ex(y1,p1) = Ex(y2,p2) by A1,Th13;
hence thesis by Th13;
end;
theorem
Ex(x,y,p) = Ex(z,q) implies x = z & Ex(y,p) = q by Th13;
theorem
All(x,y,p) is universal & bound_in All(x,y,p) = x & the_scope_of All(x
,y,p) = All(y,p) by Th7;
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
All(x,All(y,z,p));
correctness;
func Ex(x,y,z,p) -> QC-formula of A equals
Ex(x,Ex(y,z,p));
correctness;
end;
theorem
All(x,y,z,p) = All(x,All(y,z,p)) & Ex(x,y,z,p) = Ex(x,Ex(y,z,p));
theorem
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
proof
let x1,x2,y1,y2,z1,z2 be bound_QC-variable of A such that
A1: All(x1,y1,z1,p1) = All(x2,y2,z2,p2);
thus x1 = x2 by A1,Th5;
All(y1,z1,p1) = All(y2,z2,p2) by A1,Th5;
hence thesis by Th15;
end;
reserve s,t for bound_QC-variable of A;
theorem
All(x,y,z,p) = All(t,q) implies x = t & All(y,z,p) = q by Th5;
theorem
All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q
proof
assume
A1: All(x,y,z,p) = All(t,s,q);
hence x = t by Th5;
All(y,z,p) = All(s,q) by A1,Th5;
hence thesis by Th5;
end;
theorem
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
proof
let x1,x2,y1,y2,z1,z2 be bound_QC-variable of A such that
A1: Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2);
thus x1 = x2 by A1,Th13;
Ex(y1,z1,p1) = Ex(y2,z2,p2) by A1,Th13;
hence thesis by Th17;
end;
theorem
Ex(x,y,z,p) = Ex(t,q) implies x = t & Ex(y,z,p) = q by Th13;
theorem
Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q
proof
assume
A1: Ex(x,y,z,p) = Ex(t,s,q);
hence x = t by Th13;
Ex(y,z,p) = Ex(s,q) by A1,Th13;
hence thesis by Th13;
end;
theorem
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) by Th7;
definition
let A be QC-alphabet;
let H be Element of QC-WFF(A);
attr H is disjunctive means
ex p,q being Element of QC-WFF(A) st H = p 'or' q;
attr H is conditional means
ex p,q being Element of QC-WFF(A) st H = p => q;
attr H is biconditional means
ex p,q being Element of QC-WFF(A) st H = p <=> q;
attr H is existential means
ex x being bound_QC-variable of A, p being Element of QC-WFF(A)
st H = Ex(x,p);
end;
theorem
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
the_argument_of
the_left_argument_of the_argument_of H;
correctness;
func the_right_disjunct_of H -> QC-formula of A equals
the_argument_of
the_right_argument_of the_argument_of H;
correctness;
func the_antecedent_of H -> QC-formula of A equals
the_left_argument_of
the_argument_of H;
correctness;
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
the_antecedent_of
the_left_argument_of H;
correctness;
func the_right_side_of H -> QC-formula of A equals
the_consequent_of
the_left_argument_of H;
correctness;
end;
reserve F,G,H,H1 for Element of QC-WFF(A);
theorem Th29:
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
proof
thus the_left_disjunct_of(F 'or' G) = the_argument_of the_left_argument_of (
'not' F '&' 'not' G) by Th1
.= the_argument_of 'not' F by Th4
.= F by Th1;
thus the_right_disjunct_of(F 'or' G) = the_argument_of the_right_argument_of
('not' F '&' 'not' G) by Th1
.= the_argument_of 'not' G by Th4
.= G by Th1;
thus thesis by Th1;
end;
theorem Th30:
the_antecedent_of(F => G) = F & the_consequent_of(F => G) = G &
the_argument_of F => G = F '&' 'not' G
proof
thus the_antecedent_of(F => G) = the_left_argument_of (F '&' 'not' G) by Th1
.= F by Th4;
thus the_consequent_of(F => G) = the_argument_of the_right_argument_of (F
'&' 'not' G) by Th1
.= the_argument_of 'not' G by Th4
.= G by Th1;
thus thesis by Th1;
end;
theorem Th31:
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
proof
the_antecedent_of(F => G) = F & the_consequent_of(F => G) = G by Th30;
hence thesis by Th4;
end;
theorem
the_argument_of Ex(x,H) = All(x,'not' H) by Th1;
theorem
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
proof
given F,G such that
A1: H = F 'or' G;
F 'or' G = 'not' F => G;
hence H is conditional by A1;
thus H is negative by A1;
A2: the_argument_of H = 'not' F '&' 'not' G by A1,Th1;
hence the_argument_of H is conjunctive;
the_left_argument_of the_argument_of H = 'not' F & the_right_argument_of
the_argument_of H = 'not' G by A2,Th4;
hence thesis;
end;
theorem
H is conditional implies H is negative & the_argument_of H is
conjunctive & the_right_argument_of the_argument_of H is negative
proof
given F,G such that
A1: H = F => G;
the_argument_of 'not'(F '&' 'not' G) = F '&' 'not' G &
the_right_argument_of (F '&' 'not' G) = 'not' G by Th1,Th4;
hence thesis by A1;
end;
theorem
H is biconditional implies H is conjunctive & the_left_argument_of H
is conditional & the_right_argument_of H is conditional
by Th4;
theorem
H is existential implies H is negative & the_argument_of H is
universal & the_scope_of the_argument_of H is negative
proof
given x,H1 such that
A1: H = Ex(x,H1);
the_argument_of 'not' All(x,'not' H1) = All(x,'not' H1) & the_scope_of
All(x,'not' H1) = 'not' H1 by Th1,Th7;
hence thesis by A1;
end;
theorem
H is disjunctive implies H = (the_left_disjunct_of H) 'or' (
the_right_disjunct_of H)
proof
given F,G such that
A1: H = F 'or' G;
the_left_disjunct_of H = F by A1,Th29;
hence thesis by A1,Th29;
end;
theorem
H is conditional implies H = (the_antecedent_of H) => ( the_consequent_of H)
proof
given F,G such that
A1: H = F => G;
the_antecedent_of H = F by A1,Th30;
hence thesis by A1,Th30;
end;
theorem
H is biconditional implies H = (the_left_side_of H) <=> (
the_right_side_of H)
proof
given F,G such that
A1: H = F <=> G;
the_left_side_of H = F by A1,Th31;
hence thesis by A1,Th31;
end;
theorem
H is existential implies H = Ex(bound_in the_argument_of H,
the_argument_of the_scope_of the_argument_of H)
proof
given x,H1 such that
A1: H = Ex(x,H1);
A2: the_argument_of 'not' H1 = H1 by Th1;
the_argument_of 'not' All(x,'not' H1) = All(x,'not' H1) & the_scope_of
All(x,'not' H1) = 'not' H1 by Th1,Th7;
hence thesis by A1,A2,Th7;
end;
::
:: 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
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 Th41:
not H is_immediate_constituent_of VERUM(A)
proof
not ( VERUM(A) is negative or VERUM(A) is conjunctive
or VERUM(A) is universal) by QC_LANG1:20;
then not ((VERUM(A) = 'not' H)
or (ex H1 st VERUM(A) = H '&' H1 or VERUM(A) = H1 '&' H)
or (ex x being bound_QC-variable of A st VERUM(A) = All(x,H)));
hence thesis;
end;
theorem Th42:
not H is_immediate_constituent_of P!V
proof
assume
A1: not thesis;
A2: P!V is atomic;
then
A3: (@(P!V).1)`1 <> 3 by QC_LANG1:19;
A4: (@(P!V).1)`1 <> 2 by A2,QC_LANG1:19;
A5: not ex H1 being Element of QC-WFF(A) st P!V = H '&' H1 or P!V = H1 '&' H
by A4,QC_LANG1:18,def 20;
'not' H is negative;
then
A6: (@('not' H).1)`1 = 1 by QC_LANG1:18;
(@(P!V).1)`1 <> 1 by A2,QC_LANG1:19;
then consider z such that
A7: P!V = All(z,H) by A1,A6,A5;
All(z,H) is universal;
hence contradiction by A3,A7,QC_LANG1:18;
end;
theorem Th43:
F is_immediate_constituent_of 'not' H iff F = H
proof
thus F is_immediate_constituent_of 'not' H implies F = H
proof
'not' H is negative;
then
A1: (@('not' H).1)`1 = 1 by QC_LANG1:18;
A2: not ex H1 st 'not' H = F '&' H1 or 'not' H = H1 '&' F
by A1,QC_LANG1:18,def 20;
A3: not ex x st 'not' H = All(x,F) by A1,QC_LANG1:18,def 21;
assume 'not' H = 'not' F or ( ex H1 st 'not' H = F '&' H1 or 'not' H = H1
'&' F ) or ex x st 'not' H = All(x,F);
hence thesis by A2,A3,FINSEQ_1:33;
end;
thus thesis;
end;
theorem
H is_immediate_constituent_of FALSUM(A) iff H = VERUM(A) by Th43;
theorem Th45:
F is_immediate_constituent_of G '&' H iff F = G or F = H
proof
thus F is_immediate_constituent_of G '&' H implies F = G or F = H
proof
G '&' H is conjunctive;
then
A1: (@(G '&' H).1)`1 = 2 by QC_LANG1:18;
A2: G '&' H <> 'not' F by A1,QC_LANG1:18,def 19;
A3: not ex x st G '&' H = All(x,F) by A1,QC_LANG1:18,def 21;
assume G '&' H = 'not' F or (ex H1 st G '&' H = F '&' H1 or G '&' H = H1
'&' F) or ex x st G '&' H = All(x,F);
hence thesis by A2,A3,Th2;
end;
assume F = G or F = H;
hence thesis;
end;
theorem Th46:
F is_immediate_constituent_of All(x,H) iff F = H
proof
thus F is_immediate_constituent_of All(x,H) implies F = H
proof
All(x,H) is universal;
then
A1: (@All(x,H).1)`1 = 3 by QC_LANG1:18;
A2: All(x,H) <> 'not' F by A1,QC_LANG1:18,def 19;
A3: not ex G st All(x,H) = F '&' G or All(x,H) = G '&' F
by A1,QC_LANG1:18,def 20;
assume All(x,H) = 'not' F or (ex H1 st All(x,H) = F '&' H1 or All(x,H) =
H1 '&' F) or ex y st All(x,H) = All(y,F);
hence thesis by A2,A3,Th5;
end;
thus thesis;
end;
theorem Th47:
H is atomic implies not F is_immediate_constituent_of H
by Th42;
theorem Th48:
H is negative implies (F is_immediate_constituent_of H iff F =
the_argument_of H)
proof
assume H is negative;
then H = 'not' the_argument_of H by QC_LANG1:def 24;
hence thesis by Th43;
end;
theorem Th49:
H is conjunctive implies (F is_immediate_constituent_of H iff F
= the_left_argument_of H or F = the_right_argument_of H)
proof
assume H is conjunctive;
then H = (the_left_argument_of H)'&' the_right_argument_of H by Th3;
hence thesis by Th45;
end;
theorem Th50:
H is universal implies (F is_immediate_constituent_of H iff F =
the_scope_of H)
proof
assume H is universal;
then H = All(bound_in H, the_scope_of H) by Th6;
hence thesis by Th46;
end;
::
:: 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
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
proof
let H be Element of QC-WFF(A);
reconsider L = <*H*> as FinSequence;
take 1 , L;
thus 1 <= 1 & len L = 1 & L.1 = H & L.1 = H by FINSEQ_1:40;
let k;
assume 1 <= k & k < 1;
hence thesis;
end;
end;
definition
let A be QC-alphabet;
let H,F be Element of QC-WFF(A);
pred H is_proper_subformula_of F means
: Def21:
H is_subformula_of F & H <> F;
irreflexivity;
end;
theorem Th51:
H is_immediate_constituent_of F implies len @H < len @F
proof
A1: F = VERUM(A) or F is atomic or F is negative or F is conjunctive or F is
universal by QC_LANG1:9;
assume H is_immediate_constituent_of F;
then F is negative & H = the_argument_of F or F is conjunctive & H =
the_left_argument_of F or F is conjunctive & H = the_right_argument_of F or F
is universal & H = the_scope_of F by A1,Th41,Th47,Th48,Th49,Th50;
hence thesis by QC_LANG1:14,15,16;
end;
theorem Th52:
H is_immediate_constituent_of F implies H is_subformula_of F
proof
assume
A1: H is_immediate_constituent_of F;
take n = 2 , L = <* H,F *>;
thus 1 <= n;
thus len L = n by FINSEQ_1:44;
thus L.1 = H & L.n = F;
let k;
assume that
A2: 1 <= k and
A3: k < n;
take H,F;
k < 1 + 1 by A3;
then k <= 1 by NAT_1:13;
then k = 1 by A2,XXREAL_0:1;
hence L.k = H & L.(k + 1) = F;
thus thesis by A1;
end;
theorem Th53:
H is_immediate_constituent_of F implies H is_proper_subformula_of F
proof
assume
A1: H is_immediate_constituent_of F;
hence H is_subformula_of F by Th52;
assume H = F;
then len @H = len @F;
hence contradiction by A1,Th51;
end;
theorem Th54:
H is_proper_subformula_of F implies len @H < len @F
proof
given n,L such that
A1: 1 <= n and
len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 being Element of QC-WFF(A) st L.k = H1
& L.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
defpred P[Nat] means 1 <= $1 & $1 < n implies for H1 st L.($1 + 1
) = H1 holds len @H < len @H1;
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: 1 <= k & k < n implies for H1 st L.(k + 1) = H1 holds len @H < len @H1 and
A7: 1 <= k + 1 and
A8: k + 1 < n;
consider F1,G be Element of QC-WFF(A) such that
A9: L.(k + 1) = F1 and
A10: L.(k + 1 + 1) = G & F1 is_immediate_constituent_of G by A4,A7,A8;
let H1 such that
A11: L.(k + 1 + 1) = H1;
A12: now
given m be Nat such that
A13: k = m + 1;
len @H < len @F1 by A6,A8,A9,A13,NAT_1:11,13;
hence thesis by A11,A10,Th51,XXREAL_0:2;
end;
k = 0 implies len @H < len @H1 by A2,A11,A9,A10,Th51;
hence thesis by A12,NAT_1:6;
end;
assume H <> F;
then 1 < n by A1,A2,A3,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A14: n = 2 + k by NAT_1:10;
A15: P[0];
A16: for k holds P[k] from NAT_1:sch 2(A15,A5);
reconsider k as Nat;
A17: 1 + 1 + k = (1 + k) + 1;
then 1 + k < n by A14,NAT_1:13;
hence thesis by A3,A16,A14,A17,NAT_1:11;
end;
theorem Th55:
H is_proper_subformula_of F implies ex G st G is_immediate_constituent_of F
proof
given n,L such that
A1: 1 <= n and
len L = n and
A2: L.1 = H and
A3: L.n = F and
A4: for k st 1 <= k & k < n ex H1,F1 being Element of QC-WFF(A) st L.k = H1
& L.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
assume H <> F;
then 1 < n by A1,A2,A3,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A5: n = 2 + k by NAT_1:10;
reconsider k as Nat;
1 + 1 + k = (1 + k) + 1;
then 1 + k < n by A5,NAT_1:13;
then consider H1,F1 be Element of QC-WFF(A) such that
L.(1 + k) = H1 and
A6: L.(1 + k + 1) = F1 & H1 is_immediate_constituent_of F1 by A4,NAT_1:11;
take H1;
thus thesis by A3,A5,A6;
end;
theorem Th56:
F is_proper_subformula_of G & G is_proper_subformula_of H
implies F is_proper_subformula_of H
proof
assume that
A1: F is_proper_subformula_of G and
A2: G is_proper_subformula_of H;
F is_subformula_of G by A1;
then consider n,L such that
A3: 1 <= n and
A4: len L = n and
A5: L.1 = F and
A6: L.n = G and
A7: for k st 1 <= k & k < n ex H1,F1 being Element of QC-WFF(A) st L.k = H1
& L.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
1 < n by A1,A3,A5,A6,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A8: n = 2 + k by NAT_1:10;
G is_subformula_of H by A2;
then consider m,L9 such that
A9: 1 <= m and
A10: len L9 = m and
A11: L9.1 = G and
A12: L9.m = H and
A13: for k st 1 <= k & k < m ex H1,F1 being Element of QC-WFF(A) st L9.k =
H1 & L9.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
reconsider k as Nat;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
thus F is_subformula_of H
proof
take l = 1 + k + m, K = L1^L9;
A14: 1 + k + m - (1 + k) = m;
m <= m + (1 + k) by NAT_1:11;
hence 1 <= l by A9,XXREAL_0:2;
1 + 1 + k = 1 + k + 1;
then
A15: 1 + k <= n by A8,NAT_1:11;
then
A16: len L1 = 1 + k by A4,FINSEQ_1:17;
hence
A17: len K = l by A10,FINSEQ_1:22;
A18: now
let j be Nat;
assume 1 <= j & j <= 1 + k;
then
A19: j in Seg(1 + k) by FINSEQ_1:1;
then j in dom L1 by A4,A15,FINSEQ_1:17;
then K.j = L1.j by FINSEQ_1:def 7;
hence K.j = L.j by A19,FUNCT_1:49;
end;
1 <= 1 + k by NAT_1:11;
hence K.1 = F by A5,A18;
len L1 + 1 <= len L1 + m by A9,XREAL_1:7;
then len L1 < l by A16,NAT_1:13;
then K.l = L9.(l - len L1) by A17,FINSEQ_1:24;
hence K.l = H by A4,A12,A15,A14,FINSEQ_1:17;
let j be Nat such that
A20: 1 <= j and
A21: j < l;
j + 0 <= j + 1 by XREAL_1:7;
then
A22: 1 <= j + 1 by A20,XXREAL_0:2;
A23: now
assume
A24: j < 1 + k;
then
A25: j + 1 <= 1 + k by NAT_1:13;
then j + 1 <= n by A15,XXREAL_0:2;
then j < n by NAT_1:13;
then consider F1,G1 be Element of QC-WFF(A) such that
A26: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A7,A20;
take F1, G1;
thus K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A18
,A20,A22,A24,A25,A26;
end;
A27: now
A28: j + 1 <= l by A21,NAT_1:13;
assume
A29: 1 + k < j;
then
A30: 1 + k < j + 1 by NAT_1:13;
1 + k + 1 <= j by A29,NAT_1:13;
then consider j1 be Nat such that
A31: j = 1 + k + 1 + j1 by NAT_1:10;
reconsider j1 as Nat;
j - (1 + k) < l - (1 + k) by A21,XREAL_1:9;
then consider F1,G1 be Element of QC-WFF(A) such that
A32: L9.(1 + j1) = F1 & L9.(1 + j1 + 1) = G1 & F1
is_immediate_constituent_of G1 by A13,A31,NAT_1:11;
take F1, G1;
A33: 1 + j1 + (1 + k) - (1 + k) = 1 + j1 + (1 + k) + -(1 + k);
j + 1 - len L1 = 1 + (j + -len L1)
.= 1 + j1 + 1 by A4,A15,A31,A33,FINSEQ_1:17;
hence K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by
A16,A17,A21,A29,A30,A28,A33,A32,FINSEQ_1:24;
end;
now
A34: j + 1 <= l & j + 1 - j = j + 1 + -j by A21,NAT_1:13;
assume
A35: j = 1 + k;
then j < 1 + k + 1 by NAT_1:13;
then consider F1,G1 be Element of QC-WFF(A) such that
A36: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1
by A7,A8,A20;
take F1, G1;
1 + k < j + 1 by A35,NAT_1:13;
hence
K.j = F1 & K.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A6,A11
,A8,A16,A17,A18,A20,A35,A34,A36,FINSEQ_1:24;
end;
hence thesis by A23,A27,XXREAL_0:1;
end;
len @F < len @G by A1,Th54;
hence thesis by A2,Th54;
end;
theorem Th57:
F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H
proof
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H;
now
assume F <> G;
then
A3: F is_proper_subformula_of G by A1;
now
assume G <> H;
then G is_proper_subformula_of H by A2;
then F is_proper_subformula_of H by A3,Th56;
hence thesis;
end;
hence thesis by A1;
end;
hence thesis by A2;
end;
theorem Th58:
G is_subformula_of H & H is_subformula_of G implies G = H
proof
assume that
A1: G is_subformula_of H and
A2: H is_subformula_of G;
assume
A3: G <> H;
then G is_proper_subformula_of H by A1;
then
A4: len @G < len @H by Th54;
H is_proper_subformula_of G by A2,A3;
hence contradiction by A4,Th54;
end;
theorem Th59:
not (G is_proper_subformula_of H & H is_subformula_of G)
by Th58;
theorem
not (G is_proper_subformula_of H & H is_proper_subformula_of G)
by Th59;
theorem Th61:
not (G is_subformula_of H & H is_immediate_constituent_of G) by Th53,Th59;
theorem
not (G is_proper_subformula_of H & H is_immediate_constituent_of G)
by Th53,Th59;
theorem Th63:
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
proof
assume
A1: 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;
then F is_subformula_of G & G is_subformula_of H by Th52;
hence F is_subformula_of H by Th57;
thus thesis by A1,Th59,Th61;
end;
theorem Th64:
not F is_proper_subformula_of VERUM(A)
proof
assume not thesis;
then consider G such that
A1: G is_immediate_constituent_of VERUM(A) by Th55;
thus thesis by A1,Th41;
end;
theorem Th65:
not F is_proper_subformula_of P!V
proof
assume F is_proper_subformula_of P!V;
then ex G st G is_immediate_constituent_of P!V by Th55;
hence contradiction by Th42;
end;
theorem Th66:
F is_subformula_of H iff F is_proper_subformula_of 'not' H
proof
H is_immediate_constituent_of 'not' H;
hence F is_subformula_of H implies F is_proper_subformula_of 'not' H by Th63;
given n,L such that
A1: 1 <= n and
A2: len L = n and
A3: L.1 = F and
A4: L.n = 'not' H and
A5: for k st 1 <= k & k < n ex H1,F1 being Element of QC-WFF(A) st L.k = H1
& L.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
assume F <> 'not' H;
then 1 < n by A1,A3,A4,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k as Nat;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k, L1;
thus
A7: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A2,A6,FINSEQ_1:17;
A8: for j being Nat st 1 <= j <= m holds L1.j = L.j
by FUNCT_1:49, FINSEQ_1:1;
hence L1.1 = F by A3,A7;
m < m + 1 by NAT_1:13;
then consider F1,G1 be Element of QC-WFF(A) such that
A9: L.m = F1 and
A10: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A5,A6,NAT_1:11;
F1 = H by A4,A6,A10,Th43;
hence L1.m = H by A7,A8,A9;
let j be Nat;
assume that
A11: 1 <= j and
A12: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A6,A12,XXREAL_0:2;
then consider F1,G1 be Element of QC-WFF(A) such that
A13: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A5,A11;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A11,A12,NAT_1:13;
hence thesis by A8,A11,A12,A13;
end;
theorem
'not' F is_subformula_of H implies F is_proper_subformula_of H
proof
F is_proper_subformula_of 'not' F by Th66;
hence thesis by Th63;
end;
theorem
F is_proper_subformula_of FALSUM(A) iff F is_subformula_of VERUM(A) by Th66;
theorem Th69:
F is_subformula_of G or F is_subformula_of H iff F
is_proper_subformula_of G '&' H
proof
G is_immediate_constituent_of G '&' H & H is_immediate_constituent_of G
'&' H;
hence F is_subformula_of G or F is_subformula_of H implies F
is_proper_subformula_of G '&' H by Th63;
given n,L such that
A1: 1 <= n and
A2: len L = n and
A3: L.1 = F and
A4: L.n = G '&' H and
A5: for k st 1 <= k & k < n ex H1,F1 be Element of QC-WFF(A) st L.k = H1 &
L.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
assume F <> G '&' H;
then 1 < n by A1,A3,A4,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k as Nat;
1 + 1 + k = 1 + k + 1;
then 1 + k < n by A6,NAT_1:13;
then consider H1,G1 be Element of QC-WFF(A) such that
A7: L.(1 + k) = H1 and
A8: L.(1 + k + 1) = G1 & H1 is_immediate_constituent_of G1 by A5,NAT_1:11;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
F is_subformula_of H1
proof
take m = 1 + k, L1;
thus
A9: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A2,A6,FINSEQ_1:17;
A10: for j being Nat st 1 <= j <= m holds L1.j = L.j
by FUNCT_1:49,FINSEQ_1:1;
hence L1.1 = F by A3,A9;
thus L1.m = H1 by A7,A9,A10;
let j be Nat;
assume that
A11: 1 <= j and
A12: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A6,A12,XXREAL_0:2;
then consider F1,G1 be Element of QC-WFF(A) such that
A13: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A5,A11;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A11,A12,NAT_1:13;
hence thesis by A10,A11,A12,A13;
end;
hence thesis by A4,A6,A8,Th45;
end;
theorem
F '&' G is_subformula_of H implies F is_proper_subformula_of H & G
is_proper_subformula_of H
proof
F is_proper_subformula_of F '&' G & G is_proper_subformula_of F '&' G by Th69
;
hence thesis by Th63;
end;
theorem Th71:
F is_subformula_of H iff F is_proper_subformula_of All(x,H)
proof
H is_immediate_constituent_of All(x,H);
hence F is_subformula_of H implies F is_proper_subformula_of All(x,H) by Th63
;
given n,L such that
A1: 1 <= n and
A2: len L = n and
A3: L.1 = F and
A4: L.n = All(x,H) and
A5: for k st 1 <= k & k < n ex H1,F1 being Element of QC-WFF(A) st L.k = H1
& L.(k + 1) = F1 & H1 is_immediate_constituent_of F1;
assume F <> All(x,H);
then 1 < n by A1,A3,A4,XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k as Nat;
reconsider L1 = L|(Seg(1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k, L1;
thus
A7: 1 <= m by NAT_1:11;
1 + k <= 1 + k + 1 by NAT_1:11;
hence len L1 = m by A2,A6,FINSEQ_1:17;
A8: for j being Nat st 1 <= j <= m holds L1.j = L.j
by FUNCT_1:49,FINSEQ_1:1;
hence L1.1 = F by A3,A7;
m < m + 1 by NAT_1:13;
then consider F1,G1 be Element of QC-WFF(A) such that
A9: L.m = F1 and
A10: L.(m + 1) = G1 & F1 is_immediate_constituent_of G1 by A5,A6,NAT_1:11;
F1 = H by A4,A6,A10,Th46;
hence L1.m = H by A7,A8,A9;
let j be Nat;
assume that
A11: 1 <= j and
A12: j < m;
m <= m + 1 by NAT_1:11;
then j < n by A6,A12,XXREAL_0:2;
then consider F1,G1 be Element of QC-WFF(A) such that
A13: L.j = F1 & L.(j + 1) = G1 & F1 is_immediate_constituent_of G1 by A5,A11;
take F1,G1;
1 <= 1 + j & j + 1 <= m by A11,A12,NAT_1:13;
hence thesis by A8,A11,A12,A13;
end;
theorem
All(x,H) is_subformula_of F implies H is_proper_subformula_of F
proof
H is_proper_subformula_of All(x,H) by Th71;
hence thesis by Th63;
end;
theorem
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
proof
thus
A1: F '&' 'not' G is_proper_subformula_of F => G by Th66;
F is_proper_subformula_of F '&' 'not' G & 'not' G
is_proper_subformula_of F '&' 'not' G by Th69;
hence
A2: F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of
F => G by A1,Th56;
G is_proper_subformula_of 'not' G by Th66;
hence thesis by A2,Th56;
end;
theorem
'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
proof
thus
A1: 'not' F '&' 'not' G is_proper_subformula_of F 'or' G by Th66;
'not' F is_proper_subformula_of 'not' F '&' 'not' G & 'not' G
is_proper_subformula_of 'not' F '&' 'not' G by Th69;
hence
A2: 'not' F is_proper_subformula_of F 'or' G & 'not' G
is_proper_subformula_of F 'or' G by A1,Th56;
G is_proper_subformula_of 'not' G & F is_proper_subformula_of 'not' F by Th66
;
hence thesis by A2,Th56;
end;
theorem
H is atomic implies not F is_proper_subformula_of H
by Th65;
theorem
H is negative implies the_argument_of H is_proper_subformula_of H
proof
assume H is negative;
then the_argument_of H is_immediate_constituent_of H by Th48;
hence thesis by Th53;
end;
theorem
H is conjunctive implies the_left_argument_of H
is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H
proof
assume H is conjunctive;
then the_left_argument_of H is_immediate_constituent_of H &
the_right_argument_of H is_immediate_constituent_of H by Th49;
hence thesis by Th53;
end;
theorem
H is universal implies the_scope_of H is_proper_subformula_of H
proof
assume H is universal;
then the_scope_of H is_immediate_constituent_of H by Th50;
hence thesis by Th53;
end;
theorem Th79:
H is_subformula_of VERUM(A) iff H = VERUM(A)
by Def21,Th64;
theorem Th80:
H is_subformula_of P!V iff H = P!V
proof
thus H is_subformula_of P!V implies H = P!V
proof
assume
A1: H is_subformula_of P!V;
assume H <> P!V;
then H is_proper_subformula_of P!V by A1;
then ex F st F is_immediate_constituent_of P!V by Th55;
hence contradiction by Th42;
end;
thus thesis;
end;
theorem Th81:
H is_subformula_of FALSUM(A) iff H = FALSUM(A) or H = VERUM(A)
proof
thus H is_subformula_of FALSUM(A) implies H = FALSUM(A) or H = VERUM(A)
proof
assume H is_subformula_of FALSUM(A) & H <> FALSUM(A);
then H is_proper_subformula_of FALSUM(A);
then H is_subformula_of VERUM(A) by Th66;
hence thesis by Th79;
end;
VERUM(A) is_immediate_constituent_of FALSUM(A);
then VERUM(A) is_proper_subformula_of FALSUM(A) by Th53;
hence thesis;
end;
::
:: 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
: Def22:
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;
existence
proof
defpred P[object] means ex F being Element of QC-WFF(A)
st F = $1 & F is_subformula_of H;
consider X be set such that
A1: for a being object holds a in X iff a in QC-WFF(A) & P[a] from XBOOLE_0:
sch 1;
take X;
let a be object;
thus a in X implies ex F being Element of QC-WFF(A)
st F = a & F is_subformula_of H by A1;
given F be Element of QC-WFF(A) such that
A2: F = a & F is_subformula_of H;
thus thesis by A1,A2;
end;
uniqueness
proof
defpred P[object] means ex F being Element of QC-WFF(A)
st F = $1 & F is_subformula_of H;
let X,Y be set such that
A3: for a being object holds a in X iff P[a] and
A4: for a being object holds a in Y iff P[a];
thus thesis from XBOOLE_0:sch 2(A3,A4);
end;
end;
theorem Th82:
G in Subformulae H implies G is_subformula_of H
proof
assume G in Subformulae H;
then ex F st F = G & F is_subformula_of H by Def22;
hence thesis;
end;
theorem Th83:
F is_subformula_of H implies Subformulae F c= Subformulae H
proof
assume
A1: F is_subformula_of H;
let a be object;
assume a in Subformulae F;
then consider F1 be Element of QC-WFF(A) such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def22;
F1 is_subformula_of H by A1,A3,Th57;
hence thesis by A2,Def22;
end;
theorem
G in Subformulae H implies Subformulae G c= Subformulae H by Th82,Th83;
theorem Th85:
Subformulae(VERUM(A)) = { VERUM(A) }
proof
thus Subformulae VERUM(A) c= { VERUM(A) }
proof
let a be object;
assume a in Subformulae VERUM(A);
then consider F be Element of QC-WFF(A) such that
A1: F = a and
A2: F is_subformula_of VERUM(A) by Def22;
F = VERUM(A) by A2,Th79;
hence thesis by A1,TARSKI:def 1;
end;
let a be object;
assume a in { VERUM(A) };
then a = VERUM(A) by TARSKI:def 1;
hence thesis by Def22;
end;
theorem Th86:
Subformulae(P!V) = { P!V }
proof
thus Subformulae(P!V) c= { P!V }
proof
let a be object;
assume a in Subformulae(P!V);
then consider F such that
A1: F = a and
A2: F is_subformula_of P!V by Def22;
F = P!V by A2,Th80;
hence thesis by A1,TARSKI:def 1;
end;
let a be object;
assume a in { P!V };
then a = P!V by TARSKI:def 1;
hence thesis by Def22;
end;
theorem
Subformulae(FALSUM(A)) = { VERUM(A), FALSUM(A) }
proof
thus Subformulae(FALSUM(A)) c= { VERUM(A), FALSUM(A) }
proof
let a be object;
assume a in Subformulae(FALSUM(A));
then ex F st F = a & F is_subformula_of FALSUM(A) by Def22;
then a = FALSUM(A) or a = VERUM(A) by Th81;
hence thesis by TARSKI:def 2;
end;
let a be object;
assume
A1: a in { VERUM(A), FALSUM(A) };
then
A2: a = VERUM(A) or a = FALSUM(A) by TARSKI:def 2;
reconsider a as Element of QC-WFF(A) by A1,TARSKI:def 2;
a is_subformula_of FALSUM(A) by A2,Th81;
hence thesis by Def22;
end;
theorem Th88:
Subformulae 'not' H = Subformulae H \/ { 'not' H }
proof
thus Subformulae 'not' H c= Subformulae H \/ { 'not' H }
proof
let a be object;
assume a in Subformulae 'not' H;
then consider F such that
A1: F = a and
A2: F is_subformula_of 'not' H by Def22;
now
assume F <> 'not' H;
then F is_proper_subformula_of 'not' H by A2;
then F is_subformula_of H by Th66;
hence a in Subformulae H by A1,Def22;
end;
then a in Subformulae H or a in { 'not' H } by A1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let a be object such that
A3: a in Subformulae H \/ { 'not' H };
A4: now
assume a in Subformulae H;
then consider F such that
A5: F = a and
A6: F is_subformula_of H by Def22;
H is_immediate_constituent_of 'not' H;
then H is_proper_subformula_of 'not' H by Th53;
then H is_subformula_of 'not' H;
then F is_subformula_of 'not' H by A6,Th57;
hence thesis by A5,Def22;
end;
now
assume a in { 'not' H };
then a = 'not' H by TARSKI:def 1;
hence thesis by Def22;
end;
hence thesis by A3,A4,XBOOLE_0:def 3;
end;
theorem Th89:
Subformulae (H '&' F) = Subformulae H \/ Subformulae F \/ { H '&' F }
proof
thus Subformulae H '&' F c= Subformulae H \/ Subformulae F \/ { H '&' F }
proof
let a be object;
assume a in Subformulae H '&' F;
then consider G such that
A1: G = a and
A2: G is_subformula_of H '&' F by Def22;
now
assume G <> H '&' F;
then G is_proper_subformula_of H '&' F by A2;
then G is_subformula_of H or G is_subformula_of F by Th69;
then a in Subformulae H or a in Subformulae F by A1,Def22;
hence a in Subformulae H \/ Subformulae F by XBOOLE_0:def 3;
end;
then a in Subformulae H \/ Subformulae F or a in { H '&' F } by A1,
TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let a be object such that
A3: a in Subformulae H \/ Subformulae F \/ { H '&' F };
A4: now
assume a in { H '&' F };
then a = H '&' F by TARSKI:def 1;
hence thesis by Def22;
end;
A5: now
assume a in Subformulae F;
then consider G such that
A6: G = a and
A7: G is_subformula_of F by Def22;
F is_immediate_constituent_of H '&' F;
then F is_proper_subformula_of H '&' F by Th53;
then F is_subformula_of H '&' F;
then G is_subformula_of H '&' F by A7,Th57;
hence thesis by A6,Def22;
end;
A8: now
assume a in Subformulae H;
then consider G such that
A9: G = a and
A10: G is_subformula_of H by Def22;
H is_immediate_constituent_of H '&' F;
then H is_proper_subformula_of H '&' F by Th53;
then H is_subformula_of H '&' F;
then G is_subformula_of H '&' F by A10,Th57;
hence thesis by A9,Def22;
end;
a in Subformulae H \/ Subformulae F implies a in Subformulae H or a in
Subformulae F by XBOOLE_0:def 3;
hence thesis by A3,A8,A5,A4,XBOOLE_0:def 3;
end;
theorem Th90:
Subformulae All(x,H) = Subformulae H \/ { All(x,H) }
proof
thus Subformulae All(x,H) c= Subformulae H \/ { All(x,H) }
proof
let a be object;
assume a in Subformulae All(x,H);
then consider F such that
A1: F = a and
A2: F is_subformula_of All(x,H) by Def22;
now
assume F <> All(x,H);
then F is_proper_subformula_of All(x,H) by A2;
then F is_subformula_of H by Th71;
hence a in Subformulae H by A1,Def22;
end;
then a in Subformulae H or a in { All(x,H) } by A1,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let a be object such that
A3: a in Subformulae H \/ { All(x,H) };
A4: now
assume a in Subformulae H;
then consider F such that
A5: F = a and
A6: F is_subformula_of H by Def22;
H is_immediate_constituent_of All(x,H);
then H is_proper_subformula_of All(x,H) by Th53;
then H is_subformula_of All(x,H);
then F is_subformula_of All(x,H) by A6,Th57;
hence thesis by A5,Def22;
end;
now
assume a in { All(x,H) };
then a = All(x,H) by TARSKI:def 1;
hence thesis by Def22;
end;
hence thesis by A3,A4,XBOOLE_0:def 3;
end;
theorem Th91:
Subformulae (F => G) = Subformulae F \/ Subformulae G \/ {
'not' G, F '&' 'not' G, F => G }
proof
thus Subformulae (F => G) = Subformulae (F '&' 'not' G) \/ { F => G } by Th88
.= Subformulae F \/ Subformulae 'not' G \/ {F '&' 'not' G} \/ {F => G}
by Th89
.= Subformulae F \/ (Subformulae G \/ {'not' G}) \/ {F '&' 'not' G} \/ {
F => G } by Th88
.= Subformulae F \/ Subformulae G \/ {'not' G} \/ {F '&' 'not' G} \/ { F
=> G } by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G} \/ ({F '&' 'not' G} \/ {
F => G }) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ ({'not' G} \/ ({F '&' 'not' G} \/ {
F => G })) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ ({'not' G} \/ { F '&' 'not' G,F =>
G }) by ENUMSET1:1
.= Subformulae F \/ Subformulae G \/ { 'not' G,F '&' 'not' G,F => G } by
ENUMSET1:2;
end;
theorem
Subformulae (F 'or' G) = Subformulae F \/ Subformulae G \/ {'not' G,
'not' F, 'not' F '&' 'not' G, F 'or' G}
proof
thus Subformulae (F 'or' G) = Subformulae ('not' F '&' 'not' G) \/ { F 'or'
G } by Th88
.= Subformulae 'not' F \/ Subformulae 'not' G \/ {'not' F '&' 'not' G}
\/ {F 'or' G} by Th89
.= Subformulae 'not' F \/ (Subformulae G \/ {'not' G}) \/ {'not' F '&'
'not' G} \/ {F 'or' G} by Th88
.= Subformulae F \/ {'not' F} \/ (Subformulae G \/ {'not' G}) \/ {'not'
F '&' 'not' G} \/ {F 'or' G} by Th88
.= Subformulae F \/ ((Subformulae G \/ {'not' G}) \/ {'not' F}) \/ {
'not' F '&' 'not' G} \/ {F 'or' G} by XBOOLE_1:4
.= Subformulae F \/ (Subformulae G \/ ({'not' G} \/ {'not' F})) \/ {
'not' F '&' 'not' G} \/ {F 'or' G} by XBOOLE_1:4
.= Subformulae F \/ (Subformulae G \/ {'not' G,'not' F}) \/ {'not' F '&'
'not' G} \/ {F 'or' G} by ENUMSET1:1
.= Subformulae F \/ Subformulae G \/ {'not' G,'not' F} \/ {'not' F '&'
'not' G} \/ {F 'or' G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G,'not' F} \/ ({'not' F '&'
'not' G} \/ {F 'or' G}) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G,'not' F} \/ {'not' F '&'
'not' G, F 'or' G} by ENUMSET1:1
.= Subformulae F \/ Subformulae G \/ ({'not' G,'not' F} \/ {'not' F '&'
'not' G, F 'or' G}) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&'
'not' G, F 'or' G} by ENUMSET1:5;
end;
theorem
Subformulae (F <=> G) = Subformulae F \/ Subformulae G \/ { 'not' G, F
'&' 'not' G, F => G, 'not' F, G '&' 'not' F, G => F, F <=> G }
proof
thus Subformulae (F <=> G) = Subformulae(F => G) \/ Subformulae(G => F) \/ {
F <=> G} by Th89
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }
\/ Subformulae(G => F) \/ {F <=> G} by Th91
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G }
\/ (Subformulae F \/ Subformulae G \/ { 'not' F, G '&' 'not' F, G => F }) \/ {F
<=> G} by Th91
.= Subformulae F \/ Subformulae G \/ ((Subformulae F \/ Subformulae G \/
{ 'not' G, F '&' 'not' G, F => G }) \/ { 'not' F, G '&' 'not' F, G => F }) \/ {
F <=> G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ (Subformulae F \/ Subformulae G \/
({ 'not' G, F '&' 'not' G, F => G } \/ { 'not' F, G '&' 'not' F, G => F })) \/
{F <=> G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ (Subformulae F \/ Subformulae G) \/
({ 'not' G, F '&' 'not' G, F => G } \/ { 'not' F, G '&' 'not' F, G => F }) \/ {
F <=> G} by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G,
'not' F, G '&' 'not' F, G => F } \/ {F <=> G} by ENUMSET1:13
.= Subformulae F \/ Subformulae G \/ ({ 'not' G, F '&' 'not' G, F => G,
'not' F, G '&' 'not' F, G => F } \/ {F <=> G}) by XBOOLE_1:4
.= Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G,
'not' F, G '&' 'not' F, G => F, F <=> G } by ENUMSET1:21;
end;
theorem
H = VERUM(A) or H is atomic iff Subformulae H = { H }
proof
H is atomic implies Subformulae H = { H }
by Th86;
hence H = VERUM(A) or H is atomic implies Subformulae H = { H } by Th85;
assume
A1: Subformulae H = { H };
A2: now
assume H = 'not' the_argument_of H;
then
A3: the_argument_of H is_immediate_constituent_of H;
then the_argument_of H is_proper_subformula_of H by Th53;
then the_argument_of H is_subformula_of H;
then
A4: the_argument_of H in Subformulae H by Def22;
len @(the_argument_of H) <> len @H by A3,Th51;
hence contradiction by A1,A4,TARSKI:def 1;
end;
A5: now
assume H = (the_left_argument_of H) '&' the_right_argument_of H;
then
A6: the_left_argument_of H is_immediate_constituent_of H;
then the_left_argument_of H is_proper_subformula_of H by Th53;
then the_left_argument_of H is_subformula_of H;
then
A7: the_left_argument_of H in Subformulae H by Def22;
len @(the_left_argument_of H) <> len @H by A6,Th51;
hence contradiction by A1,A7,TARSKI:def 1;
end;
assume H <> VERUM(A) & not H is atomic;
then
H is negative or H is conjunctive or H is universal by QC_LANG1:9;
then H = 'not' the_argument_of H or H = (the_left_argument_of H) '&'
the_right_argument_of H or H = All(bound_in H,the_scope_of H)
by Th3,Th6,QC_LANG1:def 24;
then
A8: the_scope_of H is_immediate_constituent_of H by A2,A5;
then the_scope_of H is_proper_subformula_of H by Th53;
then the_scope_of H is_subformula_of H;
then
A9: the_scope_of H in Subformulae H by Def22;
len @(the_scope_of H) <> len @H by A8,Th51;
hence contradiction by A1,A9,TARSKI:def 1;
end;
theorem
H is negative implies Subformulae H = Subformulae the_argument_of H \/ { H }
proof
assume H is negative;
then H = 'not' the_argument_of H by QC_LANG1:def 24;
hence thesis by Th88;
end;
theorem
H is conjunctive implies Subformulae H = Subformulae
the_left_argument_of H \/ Subformulae the_right_argument_of H \/ { H }
proof
assume H is conjunctive;
then H = (the_left_argument_of H) '&' the_right_argument_of H by Th3;
hence thesis by Th89;
end;
theorem
H is universal implies Subformulae H = Subformulae the_scope_of H \/ { H }
proof
assume H is universal;
then H = All(bound_in H,the_scope_of H) by Th6;
hence thesis by Th90;
end;
theorem
(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
proof
assume that
A1: H is_immediate_constituent_of G or H is_proper_subformula_of G or H
is_subformula_of G and
A2: G in Subformulae F;
H is_proper_subformula_of G or H is_subformula_of G by A1,Th53;
then
A3: H is_subformula_of G;
G is_subformula_of F by A2,Th82;
then H is_subformula_of F by A3,Th57;
hence thesis by Def22;
end;