:: Transition of Consistency and Satisfiability under Language Extensions
:: by Julian J. Schl\"oder and Peter Koepke
::
:: Received May 7, 2012
:: Copyright (c) 2012-2021 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 ;

cluster non empty Relation-like Al -expanding for QC-alphabet ;

existence
ex b₁ being QC-alphabet st b₁ is Al -expanding by Def1;

end;

registration

let Al1, Al2 be countable QC-alphabet ;

cluster non empty Relation-like countable Al1 -expanding Al2 -expanding for QC-alphabet ;

existence
ex b₁ being QC-alphabet st
( b₁ is countable & b₁ is Al1 -expanding & b₁ 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 b₁ being Subset of (CQC-WFF Al) st
( not b₁ is empty & b₁ is Consistent )

proof end;

end;

registration

let Al be QC-alphabet ;

cluster Consistent -> Al -Consistent for Element of bool (CQC-WFF Al);

coherence
for b₁ being Subset of (CQC-WFF Al) st b₁ is Consistent holds
b₁ is Al -Consistent ;

cluster Al -Consistent -> Consistent for Element of bool (CQC-WFF Al);

coherence
for b₁ being Subset of (CQC-WFF Al) st b₁ is Al -Consistent holds
b₁ 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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 Th4, TARSKI:def 3;

end;

:: deftheorem defines -Cast QC_TRANS:def 4 :
for Al being QC-alphabet
for Al2 being b₁ -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 b₁ -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 b₁ -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 b₁ -expanding QC-alphabet holds
( Al2 -Cast (VERUM Al) = VERUM Al2 & Al2 -Cast (P ! l) = (Al2 -Cast P) ! (Al2 -Cast l) & Al2 -Cast ('not' p) = '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 b₁ -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 | (QC-pred_symbols Al) & vp = v2 | (bound_QC-variables Al) 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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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);

cluster still_not-bound_in PHI -> finite ;

coherence
still_not-bound_in PHI is finite

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 b₁ -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 b₁ -expanding QC-alphabet holds PHI is Al2 -Consistent

proof end;