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

::

:: Received May 7, 2012

:: Copyright (c) 2012-2016 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-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 } ):];

for Al being QC-alphabet holds FCEx Al = [: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 } ):];

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

[4,[ the free_symbol of Al,[x,p]]] is bound_QC-variable of (FCEx Al)

end;
let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

func Example_of (p,x) -> bound_QC-variable of (FCEx Al) equals :: GOEDCPUC:def 4

[4,[ the free_symbol of Al,[x,p]]];

coherence [4,[ the free_symbol of Al,[x,p]]];

[4,[ the free_symbol of Al,[x,p]]] is bound_QC-variable of (FCEx Al)

proof end;

:: deftheorem defines Example_of GOEDCPUC:def 4 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds Example_of (p,x) = [4,[ the free_symbol of Al,[x,p]]];

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds Example_of (p,x) = [4,[ the free_symbol of Al,[x,p]]];

definition

let Al be QC-alphabet ;

let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x)))) is Element of CQC-WFF (FCEx Al) ;

end;
let p be Element of CQC-WFF Al;

let x be bound_QC-variable of Al;

func Example_Formula_of (p,x) -> Element of CQC-WFF (FCEx Al) equals :: GOEDCPUC:def 5

('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));

coherence ('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));

('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x)))) is Element of CQC-WFF (FCEx Al) ;

:: deftheorem defines Example_Formula_of GOEDCPUC:def 5 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds Example_Formula_of (p,x) = ('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds Example_Formula_of (p,x) = ('not' (Ex (((FCEx Al) -Cast x),((FCEx Al) -Cast p)))) 'or' (((FCEx Al) -Cast p) . (((FCEx Al) -Cast x),(Example_of (p,x))));

definition

let Al be QC-alphabet ;

{ (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } is Subset of (CQC-WFF (FCEx Al))

end;
func Example_Formulae_of Al -> Subset of (CQC-WFF (FCEx Al)) equals :: GOEDCPUC:def 6

{ (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

coherence { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

{ (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } is Subset of (CQC-WFF (FCEx Al))

proof end;

:: deftheorem defines Example_Formulae_of GOEDCPUC:def 6 :

for Al being QC-alphabet holds Example_Formulae_of Al = { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

for Al being QC-alphabet holds Example_Formulae_of Al = { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

theorem Th2: :: GOEDCPUC:2

for Al being QC-alphabet

for k being Element of NAT st k > 0 holds

ex F being b_{2} -element FinSequence st

( ( for n being Nat st n <= k & 1 <= n holds

F . n is QC-alphabet ) & F . 1 = Al & ( for n being Nat st n < k & 1 <= n holds

ex Al2 being QC-alphabet st

( F . n = Al2 & F . (n + 1) = FCEx Al2 ) ) )

for k being Element of NAT st k > 0 holds

ex F being b

( ( for n being Nat st n <= k & 1 <= n holds

F . n is QC-alphabet ) & F . 1 = Al & ( for n being Nat st n < k & 1 <= n holds

ex Al2 being QC-alphabet st

( F . n = Al2 & F . (n + 1) = FCEx Al2 ) ) )

proof end;

definition

let Al be QC-alphabet ;

let k be Nat;

ex b_{1} being k + 1 -element FinSequence st

( ( for n being Nat st n <= k + 1 & 1 <= n holds

b_{1} . n is QC-alphabet ) & b_{1} . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds

ex Al2 being QC-alphabet st

( b_{1} . n = Al2 & b_{1} . (n + 1) = FCEx Al2 ) ) )
by Th2;

end;
let k be Nat;

mode FCEx-Sequence of Al,k -> k + 1 -element FinSequence means :Def7: :: GOEDCPUC:def 7

( ( for n being Nat st n <= k + 1 & 1 <= n holds

it . n is QC-alphabet ) & it . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds

ex Al2 being QC-alphabet st

( it . n = Al2 & it . (n + 1) = FCEx Al2 ) ) );

existence ( ( for n being Nat st n <= k + 1 & 1 <= n holds

it . n is QC-alphabet ) & it . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds

ex Al2 being QC-alphabet st

( it . n = Al2 & it . (n + 1) = FCEx Al2 ) ) );

ex b

( ( for n being Nat st n <= k + 1 & 1 <= n holds

b

ex Al2 being QC-alphabet st

( b

:: deftheorem Def7 defines FCEx-Sequence GOEDCPUC:def 7 :

for Al being QC-alphabet

for k being Nat

for b_{3} being b_{2} + 1 -element FinSequence holds

( b_{3} is FCEx-Sequence of Al,k iff ( ( for n being Nat st n <= k + 1 & 1 <= n holds

b_{3} . n is QC-alphabet ) & b_{3} . 1 = Al & ( for n being Nat st n < k + 1 & 1 <= n holds

ex Al2 being QC-alphabet st

( b_{3} . n = Al2 & b_{3} . (n + 1) = FCEx Al2 ) ) ) );

for Al being QC-alphabet

for k being Nat

for b

( b

b

ex Al2 being QC-alphabet st

( b

theorem Th3: :: GOEDCPUC:3

for Al being QC-alphabet

for k being Nat

for S being FCEx-Sequence of Al,k holds S . (k + 1) is QC-alphabet

for k being Nat

for S being FCEx-Sequence of Al,k holds S . (k + 1) is QC-alphabet

proof end;

theorem Th4: :: GOEDCPUC:4

for Al being QC-alphabet

for k being Nat

for S being FCEx-Sequence of Al,k holds S . (k + 1) is b_{1} -expanding QC-alphabet

for k being Nat

for S being FCEx-Sequence of Al,k holds S . (k + 1) is b

proof end;

definition

let Al be QC-alphabet ;

let k be Nat;

the FCEx-Sequence of Al,k . (k + 1) is Al -expanding QC-alphabet by Th4;

end;
let k be Nat;

func k -th_FCEx Al -> Al -expanding QC-alphabet equals :: GOEDCPUC:def 8

the FCEx-Sequence of Al,k . (k + 1);

coherence the FCEx-Sequence of Al,k . (k + 1);

the FCEx-Sequence of Al,k . (k + 1) is Al -expanding QC-alphabet by Th4;

:: deftheorem defines -th_FCEx GOEDCPUC:def 8 :

for Al being QC-alphabet

for k being Nat holds k -th_FCEx Al = the FCEx-Sequence of Al,k . (k + 1);

for Al being QC-alphabet

for k being Nat holds k -th_FCEx Al = the FCEx-Sequence of Al,k . (k + 1);

definition

let Al be QC-alphabet ;

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

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = PHI & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) )

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

mode EF-Sequence of Al,PHI -> Function means :Def9: :: GOEDCPUC:def 9

( dom it = NAT & it . 0 = PHI & ( for n being Nat holds it . (n + 1) = (it . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) );

existence ( dom it = NAT & it . 0 = PHI & ( for n being Nat holds it . (n + 1) = (it . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) );

ex b

( dom b

proof end;

:: deftheorem Def9 defines EF-Sequence GOEDCPUC:def 9 :

for Al being QC-alphabet

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

for b_{3} being Function holds

( b_{3} is EF-Sequence of Al,PHI iff ( dom b_{3} = NAT & b_{3} . 0 = PHI & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) ) );

for Al being QC-alphabet

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

for b

( b

theorem Th6: :: GOEDCPUC:6

for Al being QC-alphabet

for k, n being Element of NAT st n <= k holds

n -th_FCEx Al c= k -th_FCEx Al

for k, n being Element of NAT st n <= k holds

n -th_FCEx Al c= k -th_FCEx Al

proof end;

definition

let Al be QC-alphabet ;

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

let k be Nat;

the EF-Sequence of Al,PHI . k is Subset of (CQC-WFF (k -th_FCEx Al))

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

let k be Nat;

func k -th_EF (Al,PHI) -> Subset of (CQC-WFF (k -th_FCEx Al)) equals :: GOEDCPUC:def 10

the EF-Sequence of Al,PHI . k;

coherence the EF-Sequence of Al,PHI . k;

the EF-Sequence of Al,PHI . k is Subset of (CQC-WFF (k -th_FCEx Al))

proof end;

:: deftheorem defines -th_EF GOEDCPUC:def 10 :

for Al being QC-alphabet

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

for k being Nat holds k -th_EF (Al,PHI) = the EF-Sequence of Al,PHI . k;

for Al being QC-alphabet

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

for k being Nat holds k -th_EF (Al,PHI) = the EF-Sequence of Al,PHI . k;

theorem Th7: :: GOEDCPUC:7

for Al being QC-alphabet

for Al2 being b_{1} -expanding QC-alphabet

for r, s being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds

( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )

for Al2 being b

for r, s being Element of CQC-WFF Al

for x being bound_QC-variable of Al holds

( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )

proof end;

theorem Th8: :: GOEDCPUC:8

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )

for p, q being Element of CQC-WFF Al

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) holds

( ( J,v |= p or J,v |= q ) iff J,v |= p 'or' q )

proof end;

:: Ebbinghaus Lemma 5.3.4

theorem Th9: :: GOEDCPUC:9

for Al being QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al) holds PHI \/ (Example_Formulae_of Al) is Consistent Subset of (CQC-WFF (FCEx Al))

for PHI being Consistent Subset of (CQC-WFF Al) holds PHI \/ (Example_Formulae_of Al) is Consistent Subset of (CQC-WFF (FCEx Al))

proof end;

:: Ebbinghaus Lemma 5.3.1

theorem Th10: :: GOEDCPUC:10

for Al being QC-alphabet

for PHI being Consistent Subset of (CQC-WFF Al) ex Al2 being b_{1} -expanding QC-alphabet ex PSI being Consistent Subset of (CQC-WFF Al2) st

( PHI c= PSI & PSI is with_examples )

for PHI being Consistent Subset of (CQC-WFF Al) ex Al2 being b

( PHI c= PSI & PSI is with_examples )

proof end;

theorem Th11: :: GOEDCPUC:11

for Al being QC-alphabet

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

for p being Element of CQC-WFF Al holds

( PHI \/ {p} is Consistent or PHI \/ {('not' p)} is Consistent )

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

for p being Element of CQC-WFF Al holds

( PHI \/ {p} is Consistent or PHI \/ {('not' p)} is Consistent )

proof end;

:: Ebbinghaus Lemma 5.3.2

theorem Th12: :: GOEDCPUC:12

for Al being QC-alphabet

for PSI being Consistent Subset of (CQC-WFF Al) ex THETA being Consistent Subset of (CQC-WFF Al) st

( THETA is negation_faithful & PSI c= THETA )

for PSI being Consistent Subset of (CQC-WFF Al) ex THETA being Consistent Subset of (CQC-WFF Al) st

( THETA is negation_faithful & PSI c= THETA )

proof end;

theorem Th13: :: GOEDCPUC:13

for Al being QC-alphabet

for PHI, THETA being Consistent Subset of (CQC-WFF Al) st PHI c= THETA & PHI is with_examples holds

THETA is with_examples

for PHI, THETA being Consistent Subset of (CQC-WFF Al) st PHI c= THETA & PHI is with_examples holds

THETA is with_examples

proof end;

:: Ebbinghaus Corollary 5.3.3

:: Model Existence Theorem

:: Model Existence Theorem

registration

let Al be QC-alphabet ;

coherence

for b_{1} being Subset of (CQC-WFF Al) st b_{1} is Consistent holds

b_{1} is satisfiable

end;
coherence

for b

b

proof end;

:: Completeness Theorem

theorem :: GOEDCPUC:14

for Al being QC-alphabet

for PSI being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st PSI |= p holds

PSI |- p

for PSI being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al st PSI |= p holds

PSI |- p

proof end;