:: 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' ('not' p)) <=> p = TRUE

proof end;

theorem th3: :: PL_AXIOM:4

for p, q being boolean object holds ('not' (p '&' q)) <=> (('not' p) 'or' ('not' q)) = TRUE

proof end;

theorem th3a: :: PL_AXIOM:5

for p, q being boolean object holds ('not' (p 'or' q)) <=> (('not' p) '&' ('not' q)) = TRUE

proof end;

theorem th4: :: PL_AXIOM:6

for p, q being boolean object holds (p => q) => (('not' q) => ('not' p)) = 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 (('not' q) => ('not' p)) => ((('not' q) => 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

cluster PL-closed -> non empty with_implication with_FALSUM with_propositional_variables for set ;

coherence
for b₁ being set st b₁ is PL-closed holds
( b₁ is with_FALSUM & b₁ is with_implication & b₁ is with_propositional_variables & not b₁ is empty ) by Lm1;

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

coherence
for b₁ being Subset of (NAT *) st b₁ is with_FALSUM & b₁ is with_implication & b₁ is with_propositional_variables holds
b₁ 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 b₁ being set st
( b₁ is PL-closed & ( for D being set st D is PL-closed holds
b₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ being set st b₁ is PL-closed & ( for D being set st D is PL-closed holds
b₁ c= D ) & b₂ is PL-closed & ( for D being set st D is PL-closed holds
b₂ c= D ) holds
b₁ = b₂

proof end;

end;

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

registration

cluster PL-WFF -> PL-closed ;

coherence
PL-WFF is PL-closed by Def6;

end;

registration

cluster non empty PL-closed for set ;

existence
ex b₁ being set st
( b₁ is PL-closed & not b₁ is empty )

proof end;

end;

registration

cluster PL-WFF -> functional ;

coherence
PL-WFF is functional

proof end;

end;

registration

cluster -> FinSequence-like for Element of PL-WFF ;

coherence
for b₁ being Element of PL-WFF holds b₁ is FinSequence-like

proof end;

end;

definition

func FaLSUM -> Element of PL-WFF equals :: PL_AXIOM:def 4
<*0*>;

correctness
coherence
<*0*> is Element of PL-WFF ;
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 :
FaLSUM = <*0*>;

:: 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 b₁ being Subset of PL-WFF st
for x being set holds
( x in b₁ iff ex n being Element of NAT st x = Prop n )

proof end;

uniqueness
for b₁, b₂ being Subset of PL-WFF st ( for x being set holds
( x in b₁ iff ex n being Element of NAT st x = Prop n ) ) & ( for x being set holds
( x in b₂ iff ex n being Element of NAT st x = Prop n ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defprops defines props PL_AXIOM:def 7 :
for b₁ being Subset of PL-WFF holds
( b₁ = props iff for x being set holds
( x in b₁ 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{ P₁[ set ] } :

for r being Element of PL-WFF holds P₁[r]

provided

A1: P₁[ FaLSUM ] and
A2: for n being Element of NAT holds P₁[ Prop n] and
A3: for r, s being Element of PL-WFF st P₁[r] & P₁[s] holds
P₁[r => s]

proof end;

theorem plhp: :: PL_AXIOM:17

PL-WFF c= HP-WFF

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
p => FaLSUM is Element of PL-WFF ;
;

end;

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

definition

func VeRUM -> Element of PL-WFF equals :: PL_AXIOM:def 10
'not' FaLSUM;

correctness
coherence
'not' FaLSUM is Element of PL-WFF ;
;

end;

:: deftheorem defines VeRUM PL_AXIOM:def 10 :
VeRUM = 'not' FaLSUM;

definition

let p, q be Element of PL-WFF ;

func p '&' q -> Element of PL-WFF equals :: PL_AXIOM:def 11
'not' (p => ('not' q));

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

func p 'or' q -> Element of PL-WFF equals :: PL_AXIOM:def 12
('not' p) => q;

coherence
('not' p) => 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 => ('not' q));

:: deftheorem defines 'or' PL_AXIOM:def 12 :
for p, q being Element of PL-WFF holds p 'or' q = ('not' p) => 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

mode PLModel is Subset of props;

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 b₁ being Function of PL-WFF,BOOLEAN st
( b₁ . FaLSUM = 0 & ( for k being Element of NAT holds
( b₁ . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b₁ . (p => q) = (b₁ . p) => (b₁ . q) ) )

proof end;

uniqueness
for b₁, b₂ being Function of PL-WFF,BOOLEAN st b₁ . FaLSUM = 0 & ( for k being Element of NAT holds
( b₁ . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b₁ . (p => q) = (b₁ . p) => (b₁ . q) ) & b₂ . FaLSUM = 0 & ( for k being Element of NAT holds
( b₂ . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b₂ . (p => q) = (b₂ . p) => (b₂ . q) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines SAT PL_AXIOM:def 14 :
for M being PLModel
for b₂ being Function of PL-WFF,BOOLEAN holds
( b₂ = SAT M iff ( b₂ . FaLSUM = 0 & ( for k being Element of NAT holds
( b₂ . (Prop k) = 1 iff Prop k in M ) ) & ( for p, q being Element of PL-WFF holds b₂ . (p => q) = (b₂ . p) => (b₂ . 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' p) = '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) . ('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)

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 (('not' q) => ('not' p)) => ((('not' q) => p) => q) is tautology

proof end;

theorem :: PL_AXIOM:31

for p, q being Element of PL-WFF holds (p => q) => (('not' q) => ('not' p)) 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' ('not' p)) <=> p 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;

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 & (('not' q) => ('not' p)) => ((('not' q) => 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 & (('not' q) => ('not' p)) => ((('not' q) => 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 b₁ being Subset of PL-WFF st
( b₁ is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ being Subset of PL-WFF st b₁ is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b₁ c= D ) & b₂ is with_PL_axioms & ( for D being Subset of PL-WFF st D is with_PL_axioms holds
b₂ c= D ) holds
b₁ = b₂

proof end;

end;

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

registration

cluster PL_axioms -> with_PL_axioms ;

coherence
PL_axioms is with_PL_axioms 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 = (('not' q) => ('not' p)) => ((('not' q) => 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 = (('not' q) => ('not' p)) => ((('not' q) => 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 |- ('not' A) => (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 |- (('not' A) => 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 \/ {('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 ) )

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 \/ {('not' A)} 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 tautsat, sth, ct;