:: The Axiomatization of Propositional Logic
:: by Mariusz Giero
::
:: Received October 18, 2016
:: Copyright (c) 2016-2021 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
proof end;

theorem th1: :: PL_AXIOM:2
for p, q being boolean object holds (p '&' q) => p = TRUE
proof end;

theorem th2: :: PL_AXIOM:3
for p being boolean object holds ('not' ()) <=> p = TRUE
proof end;

theorem th3: :: PL_AXIOM:4
for p, q being boolean object holds ('not' (p '&' q)) <=> (() 'or' ()) = TRUE
proof end;

theorem th3a: :: PL_AXIOM:5
for p, q being boolean object holds ('not' (p 'or' q)) <=> (() '&' ()) = TRUE
proof end;

theorem th4: :: PL_AXIOM:6
for p, q being boolean object holds (p => q) => (() => ()) = TRUE
proof end;

theorem th5: :: PL_AXIOM:7
for p, q, r being boolean object holds (p => q) => ((p => r) => (p => (q '&' r))) = TRUE
proof end;

theorem th5a: :: PL_AXIOM:8
for p, q, r being boolean object holds (p => r) => ((q => r) => ((p 'or' q) => r)) = TRUE
proof end;

theorem th6: :: PL_AXIOM:9
for p, q being boolean object holds (p '&' q) <=> (q '&' p) = TRUE
proof end;

theorem th6a: :: PL_AXIOM:10
for p, q being boolean object holds (p 'or' q) <=> (q 'or' p) = TRUE
proof end;

theorem th7: :: PL_AXIOM:11
for p, q, r being boolean object holds ((p '&' q) '&' r) <=> (p '&' (q '&' r)) = TRUE
proof end;

theorem th7a: :: PL_AXIOM:12
for p, q, r being boolean object holds ((p 'or' q) 'or' r) <=> (p 'or' (q 'or' r)) = TRUE
proof end;

theorem Th17a: :: PL_AXIOM:13
for p, q being boolean object holds (() => ()) => ((() => p) => q) = TRUE
proof end;

theorem th8: :: PL_AXIOM:14
for p, q, r being boolean object holds (p '&' (q 'or' r)) <=> ((p '&' q) 'or' (p '&' r)) = TRUE
proof end;

theorem th8a: :: PL_AXIOM:15
for p, q, r being boolean object holds (p 'or' (q '&' r)) <=> ((p 'or' q) '&' (p 'or' r)) = TRUE
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 )
proof end;

definition
let D be set ;
attr D is with_propositional_variables means :Def4: :: PL_AXIOM:def 1
for n being Element of NAT holds <*(3 + n)*> in D;
end;

:: 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 );

definition
let D be set ;
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 );
end;

:: 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 ) );

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

proof end;

registration
coherence
for b1 being set st b1 is PL-closed holds
( b1 is with_FALSUM & b1 is with_implication & b1 is with_propositional_variables & not b1 is empty )
by Lm1;
coherence
for b1 being Subset of () st b1 is with_FALSUM & b1 is with_implication & b1 is with_propositional_variables holds
b1 is PL-closed
;
end;

definition
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
ex b1 being set st
( b1 is PL-closed & ( for D being set st D is PL-closed holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being set st b1 is PL-closed & ( for D being set st D is PL-closed holds
b1 c= D ) & b2 is PL-closed & ( for D being set st D is PL-closed holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines PL-WFF PL_AXIOM:def 3 :
for b1 being set holds
( b1 = PL-WFF iff ( b1 is PL-closed & ( for D being set st D is PL-closed holds
b1 c= D ) ) );

registration
coherence by Def6;
end;

registration
cluster non empty PL-closed for set ;
existence
ex b1 being set st
( b1 is PL-closed & not b1 is empty )
proof end;
end;

registration
coherence
proof end;
end;

registration
coherence
for b1 being Element of PL-WFF holds b1 is FinSequence-like
proof end;
end;

definition
correctness
coherence ;
by INTPRO_1:def 1;
let p, q be Element of PL-WFF ;
func p => q -> Element of PL-WFF equals :: PL_AXIOM:def 5
(<*1*> ^ p) ^ q;
coherence
(<*1*> ^ p) ^ q is Element of PL-WFF
by HILBERT1:def 2;
end;

:: deftheorem defines FaLSUM PL_AXIOM:def 4 :

:: deftheorem defines => PL_AXIOM:def 5 :
for p, q being Element of PL-WFF holds p => q = (<*1*> ^ p) ^ q;

definition
let n be Element of NAT ;
func Prop n -> Element of PL-WFF equals :: PL_AXIOM:def 6
<*(3 + n)*>;
coherence
<*(3 + n)*> is Element of PL-WFF
by Def4;
end;

:: deftheorem defines Prop PL_AXIOM:def 6 :
for n being Element of NAT holds Prop n = <*(3 + n)*>;

definition
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
ex b1 being Subset of PL-WFF st
for x being set holds
( x in b1 iff ex n being Element of NAT st x = Prop n )
proof end;
uniqueness
for b1, b2 being Subset of PL-WFF st ( for x being set holds
( x in b1 iff ex n being Element of NAT st x = Prop n ) ) & ( for x being set holds
( x in b2 iff ex n being Element of NAT st x = Prop n ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defprops defines props PL_AXIOM:def 7 :
for b1 being Subset of PL-WFF holds
( b1 = props iff for x being set holds
( x in b1 iff ex n being Element of NAT st x = Prop n ) );

definition
let D be Subset of PL-WFF;
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
( 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;
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 );

scheme :: PL_AXIOM:sch 1
PLInd{ P1[ set ] } :
for r being Element of PL-WFF holds P1[r]
provided
A1: P1[ FaLSUM ] and
A2: for n being Element of NAT holds P1[ Prop n] and
A3: for r, s being Element of PL-WFF st P1[r] & P1[s] holds
P1[r => s]
proof end;

theorem plhp: :: PL_AXIOM:17
proof end;

definition
let p be Element of PL-WFF ;
func 'not' p -> Element of PL-WFF equals :: PL_AXIOM:def 9
p => FaLSUM;
correctness
coherence ;
;
end;

:: deftheorem defines 'not' PL_AXIOM:def 9 :
for p being Element of PL-WFF holds 'not' p = p => FaLSUM;

definition
correctness
coherence ;
;
end;

:: deftheorem defines VeRUM PL_AXIOM:def 10 :

definition
let p, q be Element of PL-WFF ;
func p '&' q -> Element of PL-WFF equals :: PL_AXIOM:def 11
'not' (p => ());
coherence
'not' (p => ()) is Element of PL-WFF
;
func p 'or' q -> Element of PL-WFF equals :: PL_AXIOM:def 12
() => q;
coherence
() => q is Element of PL-WFF
;
end;

:: deftheorem defines '&' PL_AXIOM:def 11 :
for p, q being Element of PL-WFF holds p '&' q = 'not' (p => ());

:: deftheorem defines 'or' PL_AXIOM:def 12 :
for p, q being Element of PL-WFF holds p 'or' q = () => q;

definition
let p, q be Element of PL-WFF ;
func p <=> q -> Element of PL-WFF equals :: PL_AXIOM:def 13
(p => q) '&' (q => p);
correctness
coherence
(p => q) '&' (q => p) is Element of PL-WFF
;
;
end;

:: deftheorem defines <=> PL_AXIOM:def 13 :
for p, q being Element of PL-WFF holds p <=> q = (p => q) '&' (q => p);

definition end;

definition
let M be PLModel;
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
ex b1 being Function of PL-WFF,BOOLEAN st
( b1 . FaLSUM = 0 & ( for k being Element of NAT holds
( b1 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b1 . (p => q) = (b1 . p) => (b1 . q) ) )
proof end;
uniqueness
for b1, b2 being Function of PL-WFF,BOOLEAN st b1 . FaLSUM = 0 & ( for k being Element of NAT holds
( b1 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b1 . (p => q) = (b1 . p) => (b1 . q) ) & b2 . FaLSUM = 0 & ( for k being Element of NAT holds
( b2 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b2 . (p => q) = (b2 . p) => (b2 . q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SAT PL_AXIOM:def 14 :
for M being PLModel
for b2 being Function of PL-WFF,BOOLEAN holds
( b2 = SAT M iff ( b2 . FaLSUM = 0 & ( for k being Element of NAT holds
( b2 . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b2 . (p => q) = (b2 . p) => (b2 . q) ) ) );

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 ) )
proof end;

theorem semnot2: :: PL_AXIOM:19
for p being Element of PL-WFF
for M being PLModel holds (SAT M) . () = 'not' ((SAT M) . p)
proof end;

theorem semnot: :: PL_AXIOM:20
for A being Element of PL-WFF
for M being PLModel holds
( (SAT M) . () = 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)
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 ) )
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)
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 ) )
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)
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 )
proof end;

definition
let M be PLModel;
let p be Element of PL-WFF ;
pred M |= p means :: PL_AXIOM:def 15
(SAT M) . p = 1;
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 );

definition
let M be PLModel;
let F be Subset of PL-WFF;
pred M |= F means :: PL_AXIOM:def 16
for p being Element of PL-WFF st p in F holds
M |= p;
end;

:: 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 );

definition
let F be Subset of PL-WFF;
let p be Element of PL-WFF ;
pred F |= p means :: PL_AXIOM:def 17
for M being PLModel st M |= F holds
M |= p;
end;

:: 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 );

definition
let A be Element of PL-WFF ;
attr A is tautology means :: PL_AXIOM:def 18
for M being PLModel holds (SAT M) . A = 1;
end;

:: 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 );

theorem tautsat: :: PL_AXIOM:27
for A being Element of PL-WFF holds
( A is tautology iff {} PL-WFF |= A )
proof end;

theorem Th15: :: PL_AXIOM:28
for p, q being Element of PL-WFF holds p => (q => p) is tautology
proof end;

theorem Th16: :: PL_AXIOM:29
for p, q, r being Element of PL-WFF holds (p => (q => r)) => ((p => q) => (p => r)) is tautology
proof end;

theorem Th17: :: PL_AXIOM:30
for p, q being Element of PL-WFF holds (() => ()) => ((() => p) => q) is tautology
proof end;

theorem :: PL_AXIOM:31
for p, q being Element of PL-WFF holds (p => q) => (() => ()) is tautology
proof end;

theorem :: PL_AXIOM:32
for p, q being Element of PL-WFF holds (p '&' q) => p is tautology
proof end;

theorem :: PL_AXIOM:33
for p, q being Element of PL-WFF holds (p '&' q) => q is tautology
proof end;

theorem :: PL_AXIOM:34
for p, q being Element of PL-WFF holds p => (p 'or' q) is tautology
proof end;

theorem :: PL_AXIOM:35
for p, q being Element of PL-WFF holds q => (p 'or' q) is tautology
proof end;

theorem :: PL_AXIOM:36
for p, q being Element of PL-WFF holds (p '&' q) <=> (q '&' p) is tautology
proof end;

theorem :: PL_AXIOM:37
for p, q being Element of PL-WFF holds (p 'or' q) <=> (q 'or' p) is tautology
proof end;

theorem :: PL_AXIOM:38
for p, q, r being Element of PL-WFF holds ((p '&' q) '&' r) <=> (p '&' (q '&' r)) is tautology
proof end;

theorem :: PL_AXIOM:39
for p, q, r being Element of PL-WFF holds ((p 'or' q) 'or' r) <=> (p 'or' (q 'or' r)) 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:42
for p being Element of PL-WFF holds ('not' ()) <=> p is tautology
proof end;

theorem :: PL_AXIOM:43
for p, q being Element of PL-WFF holds ('not' (p '&' q)) <=> (() 'or' ()) is tautology
proof end;

theorem :: PL_AXIOM:44
for p, q being Element of PL-WFF holds ('not' (p 'or' q)) <=> (() '&' ()) is tautology
proof end;

theorem :: PL_AXIOM:45
for p, q, r being Element of PL-WFF holds (p => q) => ((p => r) => (p => (q '&' r))) is tautology
proof end;

theorem :: PL_AXIOM:46
for p, q, r being Element of PL-WFF holds (p => r) => ((q => r) => ((p 'or' q) => r)) is tautology
proof end;

theorem th24: :: PL_AXIOM:47
for A, B being Element of PL-WFF
for F being Subset of PL-WFF st F |= A & F |= A => B holds
F |= B
proof end;

definition
let D be set ;
attr D is with_PL_axioms means :withplax: :: PL_AXIOM:def 19
for p, q, r being Element of PL-WFF holds
( p => (q => p) in D & (p => (q => r)) => ((p => q) => (p => r)) in D & (() => ()) => ((() => p) => q) in D );
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 & (() => ()) => ((() => p) => q) in D ) );

definition
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
ex b1 being Subset of PL-WFF st
( b1 is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being Subset of PL-WFF st b1 is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b1 c= D ) & b2 is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem defplax defines PL_axioms PL_AXIOM:def 20 :
for b1 being Subset of PL-WFF holds
( b1 = PL_axioms iff ( b1 is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b1 c= D ) ) );

registration
coherence by defplax;
end;

definition
let p, q, r be Element of PL-WFF ;
pred p,q MP_rule r means :: PL_AXIOM:def 21
q = p => r;
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 );

registration
cluster PL_axioms -> non empty ;
coherence
not PL_axioms is empty
by withplax;
end;

definition
let A be Element of PL-WFF ;
attr A is axpl1 means :defaxpl1: :: PL_AXIOM:def 22
ex p, q being Element of PL-WFF st A = p => (q => p);
attr A is axpl2 means :defaxpl2: :: PL_AXIOM:def 23
ex p, q, r being Element of PL-WFF st A = (p => (q => r)) => ((p => q) => (p => r));
attr A is axpl3 means :defaxpl3: :: PL_AXIOM:def 24
ex p, q being Element of PL-WFF st A = (() => ()) => ((() => p) => q);
end;

:: 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) );

:: 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)) );

:: 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 = (() => ()) => ((() => p) => q) );

theorem Th36: :: PL_AXIOM:48
for A being Element of PL_axioms holds
( A is axpl1 or A is axpl2 or A is axpl3 )
proof end;

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
proof end;

definition
let i be Nat;
let f be FinSequence of PL-WFF ;
let F be Subset of PL-WFF;
pred prc f,F,i means :defprc: :: PL_AXIOM:def 25
( 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 ) );
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 ) ) );

definition
let F be Subset of PL-WFF;
let p be Element of PL-WFF ;
pred F |- p means :: PL_AXIOM:def 26
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 ) );
end;

:: 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 ) ) );

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
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
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 )
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
proof end;

theorem th43: :: PL_AXIOM:54
for p, q being Element of PL-WFF
for F being Subset of PL-WFF st F |- p & F |- p => q holds
F |- q
proof end;

theorem monmp: :: PL_AXIOM:55
for p being Element of PL-WFF
for F, G being Subset of PL-WFF st F c= G & F |- p holds
G |- p
proof end;

::#INSERT: Soundness theorem
theorem sth: :: PL_AXIOM:56
for A being Element of PL-WFF
for F being Subset of PL-WFF st F |- A holds
F |= A
proof end;

theorem thaa: :: PL_AXIOM:57
for A being Element of PL-WFF
for F being Subset of PL-WFF holds F |- A => A
proof end;

:: Deduction theorem
theorem ded: :: PL_AXIOM:58
for A, B being Element of PL-WFF
for F being Subset of PL-WFF st F \/ {A} |- B holds
F |- A => B
proof end;

theorem :: PL_AXIOM:59
for A, B being Element of PL-WFF
for F being Subset of PL-WFF st F |- A => B holds
F \/ {A} |- B
proof end;

theorem naab: :: PL_AXIOM:60
for A, B being Element of PL-WFF
for F being Subset of PL-WFF holds F |- () => (A => B)
proof end;

theorem naa: :: PL_AXIOM:61
for A being Element of PL-WFF
for F being Subset of PL-WFF holds F |- (() => A) => A
proof end;

definition
let F be Subset of PL-WFF;
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 );
end;

:: 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 ) );

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 )
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 \/ {()} 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 ) )
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 )
proof end;

definition
let F be Subset of PL-WFF;
attr F is maximal means :: PL_AXIOM:def 28
for p being Element of PL-WFF holds
( p in F or 'not' p in F );
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 ) );

theorem incsub: :: PL_AXIOM:66
for F, G being Subset of PL-WFF st F c= G & not F is consistent holds
not G is consistent
proof end;

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 \/ {()} is consistent
proof end;

:: Lindenbaum's lemma
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 )
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 )
proof end;

::#INSERT: Completeness theorem
theorem ct: :: PL_AXIOM:70
for A being Element of PL-WFF
for F being Subset of PL-WFF st F |= A holds
F |- A
proof end;

theorem :: PL_AXIOM:71
for A being Element of PL-WFF holds
( A is tautology iff {} PL-WFF |- A ) by ;