:: by Julian J. Schl\"oder and Peter Koepke

::

:: Received May 7, 2012

:: Copyright (c) 2012-2018 Association of Mizar Users

definition

let Al be QC-alphabet ;

let PHI be Subset of (CQC-WFF Al);

end;
let PHI be Subset of (CQC-WFF Al);

attr PHI is satisfiable means :Def1: :: GOEDCPUC:def 1

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;

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;

:: deftheorem Def1 defines satisfiable GOEDCPUC:def 1 :

for Al being QC-alphabet

for PHI being Subset of (CQC-WFF Al) holds

( PHI is satisfiable iff 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 );

for Al being QC-alphabet

for PHI being Subset of (CQC-WFF Al) holds

( PHI is satisfiable iff 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 );

theorem Th1: :: GOEDCPUC:1

for Al being QC-alphabet ex s being set st

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [s,[x,p]] in QC-symbols Al

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [s,[x,p]] in QC-symbols Al

proof end;

definition

let Al be QC-alphabet ;

ex b_{1} being set st

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [b_{1},[x,p]] in QC-symbols Al
by Th1;

end;
mode free_symbol of Al -> set means :Def2: :: GOEDCPUC:def 2

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [it,[x,p]] in QC-symbols Al;

existence for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [it,[x,p]] in QC-symbols Al;

ex b

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [b

:: deftheorem Def2 defines free_symbol GOEDCPUC:def 2 :

for Al being QC-alphabet

for b_{2} being set holds

( b_{2} is free_symbol of Al iff for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds not [b_{2},[x,p]] in QC-symbols Al );

for Al being QC-alphabet

for b

( b

for x being bound_QC-variable of Al holds not [b

definition

let Al be QC-alphabet ;

[:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is Al -expanding QC-alphabet

end;
func FCEx Al -> Al -expanding QC-alphabet equals :: GOEDCPUC:def 3

[:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):];

coherence [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):];

[:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is Al -expanding QC-alphabet

proof end;

:: deftheorem defines FCEx GOEDCPUC:def 3 :

for Al being QC-alphabet holds FCEx Al = [:NAT,((QC-symbo

for Al being QC-alphabet holds FCEx Al = [:NAT,((QC-symbo