:: by Mariusz Giero

::

:: Received October 18, 2016

:: Copyright (c) 2016-2019 Association of Mizar Users

theorem rnginc: :: PL_AXIOM:1

for f, g being Function st dom f c= dom g & ( for x being set st x in dom f holds

f . x = g . x ) holds

rng f c= rng g

f . x = g . x ) holds

rng f c= rng g

proof end;

theorem uniolinf: :: PL_AXIOM:16

for X being finite set

for Y being set st Y is c=-linear & X c= union Y & Y <> {} holds

ex Z being set st

( X c= Z & Z in Y )

for Y being set st Y is c=-linear & X c= union Y & Y <> {} holds

ex Z being set st

( X c= Z & Z in Y )

proof end;

definition

let D be set ;

end;
attr D is with_propositional_variables means :Def4: :: PL_AXIOM:def 1

for n being Element of NAT holds <*(3 + n)*> in D;

for n being Element of NAT holds <*(3 + n)*> in D;

:: deftheorem Def4 defines with_propositional_variables PL_AXIOM:def 1 :

for D being set holds

( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );

for D being set holds

( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );

definition

let D be set ;

end;
attr D is PL-closed means :Def5: :: PL_AXIOM:def 2

( D c= NAT * & D is with_FALSUM & D is with_implication & D is with_propositional_variables );

( D c= NAT * & D is with_FALSUM & D is with_implication & D is with_propositional_variables );

:: deftheorem Def5 defines PL-closed PL_AXIOM:def 2 :

for D being set holds

( D is PL-closed iff ( D c= NAT * & D is with_FALSUM & D is with_implication & D is with_propositional_variables ) );

for D being set holds

( D is PL-closed iff ( D c= NAT * & D is with_FALSUM & D is with_implication & D is with_propositional_variables ) );

Lm1: for D being set st D is PL-closed holds

not D is empty

proof end;

registration

coherence

for b_{1} being set st b_{1} is PL-closed holds

( b_{1} is with_FALSUM & b_{1} is with_implication & b_{1} is with_propositional_variables & not b_{1} is empty )
by Lm1;

for b_{1} being Subset of (NAT *) st b_{1} is with_FALSUM & b_{1} is with_implication & b_{1} is with_propositional_variables holds

b_{1} is PL-closed
;

end;
for b

( b

cluster with_implication with_FALSUM with_propositional_variables -> PL-closed for Element of bool (NAT *);

coherence for b

b

definition

ex b_{1} being set st

( b_{1} is PL-closed & ( for D being set st D is PL-closed holds

b_{1} c= D ) )

for b_{1}, b_{2} being set st b_{1} is PL-closed & ( for D being set st D is PL-closed holds

b_{1} c= D ) & b_{2} is PL-closed & ( for D being set st D is PL-closed holds

b_{2} c= D ) holds

b_{1} = b_{2}
end;

func PL-WFF -> set means :Def6: :: PL_AXIOM:def 3

( it is PL-closed & ( for D being set st D is PL-closed holds

it c= D ) );

existence ( it is PL-closed & ( for D being set st D is PL-closed holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines PL-WFF PL_AXIOM:def 3 :

for b_{1} being set holds

( b_{1} = PL-WFF iff ( b_{1} is PL-closed & ( for D being set st D is PL-closed holds

b_{1} c= D ) ) );

for b

( b

b

registration
end;

registration
end;

definition

correctness

coherence

<*0*> is Element of PL-WFF ;

by INTPRO_1:def 1;

let p, q be Element of PL-WFF ;

coherence

(<*1*> ^ p) ^ q is Element of PL-WFF by HILBERT1:def 2;

end;
coherence

<*0*> is Element of PL-WFF ;

by INTPRO_1:def 1;

let p, q be Element of PL-WFF ;

coherence

(<*1*> ^ p) ^ q is Element of PL-WFF by HILBERT1:def 2;

:: deftheorem defines => PL_AXIOM:def 5 :

for p, q being Element of PL-WFF holds p => q = (<*1*> ^ p) ^ q;

for p, q being Element of PL-WFF holds p => q = (<*1*> ^ p) ^ q;

definition

ex b_{1} being Subset of PL-WFF st

for x being set holds

( x in b_{1} iff ex n being Element of NAT st x = Prop n )

for b_{1}, b_{2} being Subset of PL-WFF st ( for x being set holds

( x in b_{1} iff ex n being Element of NAT st x = Prop n ) ) & ( for x being set holds

( x in b_{2} iff ex n being Element of NAT st x = Prop n ) ) holds

b_{1} = b_{2}
end;

func props -> Subset of PL-WFF means :defprops: :: PL_AXIOM:def 7

for x being set holds

( x in it iff ex n being Element of NAT st x = Prop n );

existence for x being set holds

( x in it iff ex n being Element of NAT st x = Prop n );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem defprops defines props PL_AXIOM:def 7 :

for b_{1} being Subset of PL-WFF holds

( b_{1} = props iff for x being set holds

( x in b_{1} iff ex n being Element of NAT st x = Prop n ) );

for b

( b

( x in b

definition

let D be Subset of PL-WFF;

( D is with_implication iff for p, q being Element of PL-WFF st p in D & q in D holds

p => q in D )

end;
redefine attr D is with_implication means :: PL_AXIOM:def 8

for p, q being Element of PL-WFF st p in D & q in D holds

p => q in D;

compatibility for p, q being Element of PL-WFF st p in D & q in D holds

p => q in D;

( D is with_implication iff for p, q being Element of PL-WFF st p in D & q in D holds

p => q in D )

proof end;

:: deftheorem defines with_implication PL_AXIOM:def 8 :

for D being Subset of PL-WFF holds

( D is with_implication iff for p, q being Element of PL-WFF st p in D & q in D holds

p => q in D );

for D being Subset of PL-WFF holds

( D is with_implication iff for p, q being Element of PL-WFF st p in D & q in D holds

p => q in D );

definition
end;

:: deftheorem defines 'not' PL_AXIOM:def 9 :

for p being Element of PL-WFF holds 'not' p = p => FaLSUM;

for p being Element of PL-WFF holds 'not' p = p => FaLSUM;

definition

let p, q be Element of PL-WFF ;

coherence

'not' (p => ('not' q)) is Element of PL-WFF ;

coherence

('not' p) => q is Element of PL-WFF ;

end;
coherence

'not' (p => ('not' q)) is Element of PL-WFF ;

coherence

('not' p) => q is Element of PL-WFF ;

:: deftheorem defines '&' PL_AXIOM:def 11 :

for p, q being Element of PL-WFF holds p '&' q = 'not' (p => ('not' q));

for p, q being Element of PL-WFF holds p '&' q = 'not' (p => ('not' q));

:: deftheorem defines 'or' PL_AXIOM:def 12 :

for p, q being Element of PL-WFF holds p 'or' q = ('not' p) => q;

for p, q being Element of PL-WFF holds p 'or' q = ('not' p) => q;

definition
end;

:: deftheorem defines <=> PL_AXIOM:def 13 :

for p, q being Element of PL-WFF holds p <=> q = (p => q) '&' (q => p);

for p, q being Element of PL-WFF holds p <=> q = (p => q) '&' (q => p);

definition

let M be PLModel;

ex b_{1} being Function of PL-WFF,BOOLEAN st

( b_{1} . FaLSUM = 0 & ( for k being Element of NAT holds

( b_{1} . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b_{1} . (p => q) = (b_{1} . p) => (b_{1} . q) ) )

for b_{1}, b_{2} being Function of PL-WFF,BOOLEAN st b_{1} . FaLSUM = 0 & ( for k being Element of NAT holds

( b_{1} . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b_{1} . (p => q) = (b_{1} . p) => (b_{1} . q) ) & b_{2} . FaLSUM = 0 & ( for k being Element of NAT holds

( b_{2} . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b_{2} . (p => q) = (b_{2} . p) => (b_{2} . q) ) holds

b_{1} = b_{2}

end;
func SAT M -> Function of PL-WFF,BOOLEAN means :Def11: :: PL_AXIOM:def 14

( it . FaLSUM = 0 & ( for k being Element of NAT holds

( it . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds it . (p => q) = (it . p) => (it . q) ) );

existence ( it . FaLSUM = 0 & ( for k being Element of NAT holds

( it . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds it . (p => q) = (it . p) => (it . q) ) );

ex b

( b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def11 defines SAT PL_AXIOM:def 14 :

for M being PLModel

for b_{2} being Function of PL-WFF,BOOLEAN holds

( b_{2} = SAT M iff ( b_{2} . FaLSUM = 0 & ( for k being Element of NAT holds

( b_{2} . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b_{2} . (p => q) = (b_{2} . p) => (b_{2} . q) ) ) );

for M being PLModel

for b

( b

( b

theorem :: PL_AXIOM:18

for A, B being Element of PL-WFF

for M being PLModel holds

( (SAT M) . (A => B) = 1 iff ( (SAT M) . A = 0 or (SAT M) . B = 1 ) )

for M being PLModel holds

( (SAT M) . (A => B) = 1 iff ( (SAT M) . A = 0 or (SAT M) . B = 1 ) )

proof end;

theorem semnot: :: PL_AXIOM:20

for A being Element of PL-WFF

for M being PLModel holds

( (SAT M) . ('not' A) = 1 iff (SAT M) . A = 0 )

for M being PLModel holds

( (SAT M) . ('not' A) = 1 iff (SAT M) . A = 0 )

proof end;

theorem semcon2: :: PL_AXIOM:21

for A, B being Element of PL-WFF

for M being PLModel holds (SAT M) . (A '&' B) = ((SAT M) . A) '&' ((SAT M) . B)

for M being PLModel holds (SAT M) . (A '&' B) = ((SAT M) . A) '&' ((SAT M) . B)

proof end;

theorem :: PL_AXIOM:22

for A, B being Element of PL-WFF

for M being PLModel holds

( (SAT M) . (A '&' B) = 1 iff ( (SAT M) . A = 1 & (SAT M) . B = 1 ) )

for M being PLModel holds

( (SAT M) . (A '&' B) = 1 iff ( (SAT M) . A = 1 & (SAT M) . B = 1 ) )

proof end;

theorem semdis2: :: PL_AXIOM:23

for A, B being Element of PL-WFF

for M being PLModel holds (SAT M) . (A 'or' B) = ((SAT M) . A) 'or' ((SAT M) . B)

for M being PLModel holds (SAT M) . (A 'or' B) = ((SAT M) . A) 'or' ((SAT M) . B)

proof end;

theorem :: PL_AXIOM:24

for A, B being Element of PL-WFF

for M being PLModel holds

( (SAT M) . (A 'or' B) = 1 iff ( (SAT M) . A = 1 or (SAT M) . B = 1 ) )

for M being PLModel holds

( (SAT M) . (A 'or' B) = 1 iff ( (SAT M) . A = 1 or (SAT M) . B = 1 ) )

proof end;

theorem semequ2: :: PL_AXIOM:25

for A, B being Element of PL-WFF

for M being PLModel holds (SAT M) . (A <=> B) = ((SAT M) . A) <=> ((SAT M) . B)

for M being PLModel holds (SAT M) . (A <=> B) = ((SAT M) . A) <=> ((SAT M) . B)

proof end;

theorem :: PL_AXIOM:26

for A, B being Element of PL-WFF

for M being PLModel holds

( (SAT M) . (A <=> B) = 1 iff (SAT M) . A = (SAT M) . B )

for M being PLModel holds

( (SAT M) . (A <=> B) = 1 iff (SAT M) . A = (SAT M) . B )

proof end;

definition
end;

:: deftheorem defines |= PL_AXIOM:def 15 :

for M being PLModel

for p being Element of PL-WFF holds

( M |= p iff (SAT M) . p = 1 );

for M being PLModel

for p being Element of PL-WFF holds

( M |= p iff (SAT M) . p = 1 );

:: deftheorem defines |= PL_AXIOM:def 16 :

for M being PLModel

for F being Subset of PL-WFF holds

( M |= F iff for p being Element of PL-WFF st p in F holds

M |= p );

for M being PLModel

for F being Subset of PL-WFF holds

( M |= F iff for p being Element of PL-WFF st p in F holds

M |= p );

:: deftheorem defines |= PL_AXIOM:def 17 :

for F being Subset of PL-WFF

for p being Element of PL-WFF holds

( F |= p iff for M being PLModel st M |= F holds

M |= p );

for F being Subset of PL-WFF

for p being Element of PL-WFF holds

( F |= p iff for M being PLModel st M |= F holds

M |= p );

:: deftheorem defines tautology PL_AXIOM:def 18 :

for A being Element of PL-WFF holds

( A is tautology iff for M being PLModel holds (SAT M) . A = 1 );

for A being Element of PL-WFF holds

( A is tautology iff for M being PLModel holds (SAT M) . A = 1 );

theorem Th17: :: PL_AXIOM:30

for p, q being Element of PL-WFF holds (('not' q) => ('not' p)) => ((('not' q) => p) => q) is tautology

proof end;

theorem :: PL_AXIOM:40

for p, q, r being Element of PL-WFF holds (p '&' (q 'or' r)) <=> ((p '&' q) 'or' (p '&' r)) is tautology

proof end;

theorem :: PL_AXIOM:41

for p, q, r being Element of PL-WFF holds (p 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' r)) is tautology

proof end;

theorem :: PL_AXIOM:43

for p, q being Element of PL-WFF holds ('not' (p '&' q)) <=> (('not' p) 'or' ('not' q)) is tautology

proof end;

theorem :: PL_AXIOM:44

for p, q being Element of PL-WFF holds ('not' (p 'or' q)) <=> (('not' p) '&' ('not' q)) is tautology

proof end;

:: deftheorem withplax defines with_PL_axioms PL_AXIOM:def 19 :

for D being set holds

( D is with_PL_axioms iff for p, q, r being Element of PL-WFF holds

( p => (q => p) in D & (p => (q => r)) => ((p => q) => (p => r)) in D & (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D ) );

for D being set holds

( D is with_PL_axioms iff for p, q, r being Element of PL-WFF holds

( p => (q => p) in D & (p => (q => r)) => ((p => q) => (p => r)) in D & (('not' q) => ('not' p)) => ((('not' q) => p) => q) in D ) );

definition

ex b_{1} being Subset of PL-WFF st

( b_{1} is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds

b_{1} c= D ) )

for b_{1}, b_{2} being Subset of PL-WFF st b_{1} is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds

b_{1} c= D ) & b_{2} is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds

b_{2} c= D ) holds

b_{1} = b_{2}
end;

func PL_axioms -> Subset of PL-WFF means :defplax: :: PL_AXIOM:def 20

( it is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds

it c= D ) );

existence ( it is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defplax defines PL_axioms PL_AXIOM:def 20 :

for b_{1} being Subset of PL-WFF holds

( b_{1} = PL_axioms iff ( b_{1} is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds

b_{1} c= D ) ) );

for b

( b

b

registration
end;

definition
end;

:: deftheorem defines MP_rule PL_AXIOM:def 21 :

for p, q, r being Element of PL-WFF holds

( p,q MP_rule r iff q = p => r );

for p, q, r being Element of PL-WFF holds

( p,q MP_rule r iff q = p => r );

definition

let A be Element of PL-WFF ;

end;
attr A is axpl1 means :defaxpl1: :: PL_AXIOM:def 22

ex p, q being Element of PL-WFF st A = p => (q => p);

ex p, q being Element of PL-WFF st A = p => (q => p);

:: deftheorem defaxpl1 defines axpl1 PL_AXIOM:def 22 :

for A being Element of PL-WFF holds

( A is axpl1 iff ex p, q being Element of PL-WFF st A = p => (q => p) );

for A being Element of PL-WFF holds

( A is axpl1 iff ex p, q being Element of PL-WFF st A = p => (q => p) );

:: deftheorem defaxpl2 defines axpl2 PL_AXIOM:def 23 :

for A being Element of PL-WFF holds

( A is axpl2 iff ex p, q, r being Element of PL-WFF st A = (p => (q => r)) => ((p => q) => (p => r)) );

for A being Element of PL-WFF holds

( A is axpl2 iff ex p, q, r being Element of PL-WFF st A = (p => (q => r)) => ((p => q) => (p => r)) );

:: deftheorem defaxpl3 defines axpl3 PL_AXIOM:def 24 :

for A being Element of PL-WFF holds

( A is axpl3 iff ex p, q being Element of PL-WFF st A = (('not' q) => ('not' p)) => ((('not' q) => p) => q) );

for A being Element of PL-WFF holds

( A is axpl3 iff ex p, q being Element of PL-WFF st A = (('not' q) => ('not' p)) => ((('not' q) => p) => q) );

theorem Th37: :: PL_AXIOM:49

for A being Element of PL-WFF

for F being Subset of PL-WFF st ( A is axpl1 or A is axpl2 or A is axpl3 ) holds

F |= A

for F being Subset of PL-WFF st ( A is axpl1 or A is axpl2 or A is axpl3 ) holds

F |= A

proof end;

:: deftheorem defprc defines prc PL_AXIOM:def 25 :

for i being Nat

for f being FinSequence of PL-WFF

for F being Subset of PL-WFF holds

( prc f,F,i iff ( f . i in PL_axioms or f . i in F or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) );

for i being Nat

for f being FinSequence of PL-WFF

for F being Subset of PL-WFF holds

( prc f,F,i iff ( f . i in PL_axioms or f . i in F or ex j, k being Nat st

( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) );

:: deftheorem defines |- PL_AXIOM:def 26 :

for F being Subset of PL-WFF

for p being Element of PL-WFF holds

( F |- p iff ex f being FinSequence of PL-WFF st

( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds

prc f,F,i ) ) );

for F being Subset of PL-WFF

for p being Element of PL-WFF holds

( F |- p iff ex f being FinSequence of PL-WFF st

( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds

prc f,F,i ) ) );

theorem Th38: :: PL_AXIOM:50

for F being Subset of PL-WFF

for f, f2 being FinSequence of PL-WFF

for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i holds

prc f2,F,i + n

for f, f2 being FinSequence of PL-WFF

for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds

f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i holds

prc f2,F,i + n

proof end;

theorem Th39: :: PL_AXIOM:51

for F being Subset of PL-WFF

for f, f1, f2 being FinSequence of PL-WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc f,F,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,F,i ) holds

for i being Nat st 1 <= i & i <= len f2 holds

prc f2,F,i

for f, f1, f2 being FinSequence of PL-WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds

prc f,F,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,F,i ) holds

for i being Nat st 1 <= i & i <= len f2 holds

prc f2,F,i

proof end;

theorem Th40: :: PL_AXIOM:52

for p being Element of PL-WFF

for F being Subset of PL-WFF

for f, f1 being FinSequence of PL-WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,F,i ) & prc f,F, len f holds

( ( for i being Nat st 1 <= i & i <= len f holds

prc f,F,i ) & F |- p )

for F being Subset of PL-WFF

for f, f1 being FinSequence of PL-WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds

prc f1,F,i ) & prc f,F, len f holds

( ( for i being Nat st 1 <= i & i <= len f holds

prc f,F,i ) & F |- p )

proof end;

theorem th42: :: PL_AXIOM:53

for p being Element of PL-WFF

for F being Subset of PL-WFF st ( p in PL_axioms or p in F ) holds

F |- p

for F being Subset of PL-WFF st ( p in PL_axioms or p in F ) holds

F |- p

proof end;

::#INSERT: Soundness theorem

definition

let F be Subset of PL-WFF;

end;
attr F is consistent means :: PL_AXIOM:def 27

for p being Element of PL-WFF holds

( not F |- p or not F |- 'not' p );

for p being Element of PL-WFF holds

( not F |- p or not F |- 'not' p );

:: deftheorem defines consistent PL_AXIOM:def 27 :

for F being Subset of PL-WFF holds

( F is consistent iff for p being Element of PL-WFF holds

( not F |- p or not F |- 'not' p ) );

for F being Subset of PL-WFF holds

( F is consistent iff for p being Element of PL-WFF holds

( not F |- p or not F |- 'not' p ) );

theorem conco: :: PL_AXIOM:62

for F being Subset of PL-WFF holds

( F is consistent iff not for A being Element of PL-WFF holds F |- A )

( F is consistent iff not for A being Element of PL-WFF holds F |- A )

proof end;

theorem th34: :: PL_AXIOM:63

for A being Element of PL-WFF

for F being Subset of PL-WFF st not F |- A holds

F \/ {('not' A)} is consistent

for F being Subset of PL-WFF st not F |- A holds

F \/ {('not' A)} is consistent

proof end;

theorem exfin: :: PL_AXIOM:64

for F being Subset of PL-WFF

for A being Element of PL-WFF holds

( F |- A iff ex G being Subset of PL-WFF st

( G c= F & G is finite & G |- A ) )

for A being Element of PL-WFF holds

( F |- A iff ex G being Subset of PL-WFF st

( G c= F & G is finite & G |- A ) )

proof end;

theorem finin: :: PL_AXIOM:65

for F being Subset of PL-WFF st not F is consistent holds

ex G being Subset of PL-WFF st

( G is finite & not G is consistent & G c= F )

ex G being Subset of PL-WFF st

( G is finite & not G is consistent & G c= F )

proof end;

:: deftheorem defines maximal PL_AXIOM:def 28 :

for F being Subset of PL-WFF holds

( F is maximal iff for p being Element of PL-WFF holds

( p in F or 'not' p in F ) );

for F being Subset of PL-WFF holds

( F is maximal iff for p being Element of PL-WFF holds

( p in F or 'not' p in F ) );

theorem onecon: :: PL_AXIOM:67

for A being Element of PL-WFF

for F being Subset of PL-WFF st F is consistent & not F \/ {A} is consistent holds

F \/ {('not' A)} is consistent

for F being Subset of PL-WFF st F is consistent & not F \/ {A} is consistent holds

F \/ {('not' A)} is consistent

proof end;

theorem th37: :: PL_AXIOM:68

for F being Subset of PL-WFF st F is consistent holds

ex G being Subset of PL-WFF st

( F c= G & G is consistent & G is maximal )

ex G being Subset of PL-WFF st

( F c= G & G is consistent & G is maximal )

proof end;

theorem inder: :: PL_AXIOM:69

for F being Subset of PL-WFF st F is maximal & F is consistent holds

for p being Element of PL-WFF holds

( F |- p iff p in F )

for p being Element of PL-WFF holds

( F |- p iff p in F )

proof end;

::#INSERT: Completeness theorem

theorem :: PL_AXIOM:71