:: Transition of Consistency and Satisfiability under Language Extensions
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Copyright (c) 2012-2019 Association of Mizar Users

definition
let Al, Al2 be QC-alphabet ;
attr Al2 is Al -expanding means :Def1: :: QC_TRANS:def 1
Al c= Al2;
end;

:: deftheorem Def1 defines -expanding QC_TRANS:def 1 :
for Al, Al2 being QC-alphabet holds
( Al2 is Al -expanding iff Al c= Al2 );

registration
let Al be QC-alphabet ;
existence
ex b1 being QC-alphabet st b1 is Al -expanding
by Def1;
end;

registration
let Al1, Al2 be countable QC-alphabet ;
existence
ex b1 being QC-alphabet st
( b1 is countable & b1 is Al1 -expanding & b1 is Al2 -expanding )
proof end;
end;

definition
let Al, Al2 be QC-alphabet ;
let P be Subset of (CQC-WFF Al);
attr P is Al2 -Consistent means :: QC_TRANS:def 2
for S being Subset of (CQC-WFF Al2) st P = S holds
S is Consistent ;
end;

:: deftheorem defines -Consistent QC_TRANS:def 2 :
for Al, Al2 being QC-alphabet
for P being Subset of (CQC-WFF Al) holds
( P is Al2 -Consistent iff for S being Subset of (CQC-WFF Al2) st P = S holds
S is Consistent );

registration
let Al be QC-alphabet ;
cluster non empty Consistent for Element of bool (CQC-WFF Al);
existence
ex b1 being Subset of (CQC-WFF Al) st
( not b1 is empty & b1 is Consistent )
proof end;
end;

registration
let Al be QC-alphabet ;
cluster Consistent -> Al -Consistent for Element of bool (CQC-WFF Al);
coherence
for b1 being Subset of (CQC-WFF Al) st b1 is Consistent holds
b1 is Al -Consistent
;
cluster Al -Consistent -> Consistent for Element of bool (CQC-WFF Al);
coherence
for b1 being Subset of (CQC-WFF Al) st b1 is Al -Consistent holds
b1 is Consistent
;
end;

theorem Th1: :: QC_TRANS:1
for Al being QC-alphabet
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds the_arity_of P = len l
proof end;

theorem Th2: :: QC_TRANS:2
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet holds QC-symbols Al c= QC-symbols Al2
proof end;

theorem Th3: :: QC_TRANS:3
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet holds QC-pred_symbols Al c= QC-pred_symbols Al2
proof end;

theorem Th4: :: QC_TRANS:4
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet holds bound_QC-variables Al c= bound_QC-variables Al2
proof end;

theorem Th5: :: QC_TRANS:5
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for k being Nat
for l being CQC-variable_list of k,Al holds l is CQC-variable_list of k,Al2
proof end;

theorem Th6: :: QC_TRANS:6
for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for Al2 being b1 -expanding QC-alphabet holds P is QC-pred_symbol of k,Al2
proof end;

theorem Th7: :: QC_TRANS:7
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2
proof end;

definition
let Al be QC-alphabet ;
let Al2 be Al -expanding QC-alphabet ;
let p be Element of CQC-WFF Al;
func Al2 -Cast p -> Element of CQC-WFF Al2 equals :: QC_TRANS:def 3
p;
coherence
p is Element of CQC-WFF Al2
by Th7;
end;

:: deftheorem defines -Cast QC_TRANS:def 3 :
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p being Element of CQC-WFF Al holds Al2 -Cast p = p;

definition
let Al be QC-alphabet ;
let Al2 be Al -expanding QC-alphabet ;
let x be bound_QC-variable of Al;
func Al2 -Cast x -> bound_QC-variable of Al2 equals :: QC_TRANS:def 4
x;
coherence
x is bound_QC-variable of Al2
by ;
end;

:: deftheorem defines -Cast QC_TRANS:def 4 :
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for x being bound_QC-variable of Al holds Al2 -Cast x = x;

definition
let Al be QC-alphabet ;
let Al2 be Al -expanding QC-alphabet ;
let k be Nat;
let P be QC-pred_symbol of k,Al;
func Al2 -Cast P -> QC-pred_symbol of k,Al2 equals :: QC_TRANS:def 5
P;
coherence
P is QC-pred_symbol of k,Al2
by Th6;
end;

:: deftheorem defines -Cast QC_TRANS:def 5 :
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al holds Al2 -Cast P = P;

definition
let Al be QC-alphabet ;
let Al2 be Al -expanding QC-alphabet ;
let k be Nat;
let l be CQC-variable_list of k,Al;
func Al2 -Cast l -> CQC-variable_list of k,Al2 equals :: QC_TRANS:def 6
l;
coherence
l is CQC-variable_list of k,Al2
by Th5;
end;

:: deftheorem defines -Cast QC_TRANS:def 6 :
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for k being Nat
for l being CQC-variable_list of k,Al holds Al2 -Cast l = l;

theorem Th8: :: QC_TRANS:8
for Al being QC-alphabet
for k being Nat
for p, r being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Al2 being b1 -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast () = 'not' (Al2 -Cast p) & Al2 -Cast (p '&' r) = (Al2 -Cast p) '&' (Al2 -Cast r) & Al2 -Cast (All (x,p)) = All ((Al2 -Cast x),(Al2 -Cast p)) )
proof end;

theorem Th9: :: QC_TRANS:9
for Al being QC-alphabet
for r being Element of CQC-WFF Al
for A being non empty set
for Al2 being b1 -expanding QC-alphabet
for J2 being interpretation of Al2,A
for Jp being interpretation of Al,A
for v2 being Element of Valuations_in (Al2,A)
for vp being Element of Valuations_in (Al,A) st Jp = J2 | () & vp = v2 | () holds
( J2,v2 |= Al2 -Cast r iff Jp,vp |= r )
proof end;

theorem :: QC_TRANS:10
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for Al2 being b1 -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI c= THETA holds
for A2 being non empty set
for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
proof end;

theorem Th11: :: QC_TRANS:11
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for f being FinSequence of CQC-WFF Al2
for g being FinSequence of CQC-WFF Al st f = g holds
( Ant f = Ant g & Suc f = Suc g )
proof end;

theorem Th12: :: QC_TRANS:12
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in p = still_not-bound_in (Al2 -Cast p)
proof end;

theorem Th13: :: QC_TRANS:13
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
RestrictSub (x,p,S) = RestrictSub (x2,p2,S2)
proof end;

theorem Th14: :: QC_TRANS:14
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being finite CQC_Substitution of Al
for S2 being finite CQC_Substitution of Al2
for p being Element of CQC-WFF Al st S = S2 & p = p2 holds
upVar (S,p) = upVar (S2,p2)
proof end;

theorem Th15: :: QC_TRANS:15
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for S being CQC_Substitution of Al
for S2 being CQC_Substitution of Al2
for x2 being bound_QC-variable of Al2
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al st p = p2 & S = S2 & x = x2 holds
ExpandSub (x,p,(RestrictSub (x,(All (x,p)),S))) = ExpandSub (x2,p2,(RestrictSub (x2,(All (x2,p2)),S2)))
proof end;

theorem Th16: :: QC_TRANS:16
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for Z being Element of CQC-Sub-WFF Al
for Z2 being Element of CQC-Sub-WFF Al2 st Z 1 is universal & Z2 1 is universal & bound_in (Z 1) = bound_in (Z2 1) & the_scope_of (Z 1) = the_scope_of (Z2 1) & Z = Z2 holds
S_Bound (@ Z) = S_Bound (@ Z2)
proof end;

theorem Th17: :: QC_TRANS:17
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for p2 being Element of CQC-WFF Al2
for x2, y2 being bound_QC-variable of Al2
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al st p = p2 & x = x2 & y = y2 holds
p . (x,y) = p2 . (x2,y2)
proof end;

theorem Th18: :: QC_TRANS:18
for Al being QC-alphabet
for Al2 being b1 -expanding QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al2) st PHI is Subset of (CQC-WFF Al) holds
PHI is Al -Consistent
proof end;

theorem Th19: :: QC_TRANS:19
for Al being QC-alphabet
for p being Element of CQC-WFF Al ex Al1 being countable QC-alphabet st
( p is Element of CQC-WFF Al1 & Al is Al1 -expanding )
proof end;

theorem Th20: :: QC_TRANS:20
for Al being QC-alphabet
for PHI being finite Subset of (CQC-WFF Al) ex Al1 being countable QC-alphabet st
( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )
proof end;

registration
let Al be QC-alphabet ;
let PHI be finite Subset of (CQC-WFF Al);
coherence
proof end;
end;

theorem Th21: :: QC_TRANS:21
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for Al2 being b1 -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= PHI holds
ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA
proof end;

theorem Th22: :: QC_TRANS:22
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds
CHI is Consistent
proof end;

theorem :: QC_TRANS:23
for Al being QC-alphabet
for PHI being Consistent Subset of (CQC-WFF Al)
for Al2 being b1 -expanding QC-alphabet holds PHI is Al2 -Consistent
proof end;