Copyright (c) 2003 Association of Mizar Users
environ
vocabulary FINSEQ_1, RELAT_1, FUNCT_1, ZF_LANG, BOOLE, INTPRO_1, QC_LANG2;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1, NAT_1,
FINSEQ_1;
constructors NAT_1, CQC_LANG, MEMBERED;
clusters RELSET_1, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI;
theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
begin :: Intuitionistic propositional calculus IPC in the extended
:: language with modal operator
definition let E be set;
attr E is with_FALSUM means :Def1:
<*0*>in E;
end;
definition let E be set;
attr E is with_int_implication means :Def2:
for p, q being FinSequence st
p in E & q in E holds <*1*>^p^q in E;
end;
definition let E be set;
attr E is with_int_conjunction means :Def3:
for p, q being FinSequence st
p in E & q in E holds <*2*>^p^q in E;
end;
definition let E be set;
attr E is with_int_disjunction means :Def4:
for p, q being FinSequence st
p in E & q in E holds <*3*>^p^q in E;
end;
definition let E be set;
attr E is with_int_propositional_variables means :Def5:
for n being Nat holds <* 5+2*n *> in E;
end;
definition let E be set;
attr E is with_modal_operator means :Def6:
for p being FinSequence st
p in E holds <*6*>^p in E;
end;
:: We reserve <*4*> for verum for a possible formulation.
:: So do we <* 5+2*n+1 *> for every n >= 1 for introduction of a number of
:: other logical connectives (e.g. for polymodal logics,
:: hybrid logics, recent computer-oriented logics and so on).
definition let E be set;
attr E is MC-closed means :Def7:
E c= NAT* &
E is with_FALSUM with_int_implication
with_int_conjunction with_int_disjunction
with_int_propositional_variables
with_modal_operator;
end;
Lm1: for E be set st E is MC-closed holds E is non empty
proof
let E be set;
assume E is MC-closed;
then E is with_FALSUM by Def7;
hence thesis by Def1;
end;
definition
cluster MC-closed ->
with_FALSUM with_int_implication
with_int_conjunction with_int_disjunction
with_int_propositional_variables
with_modal_operator non empty set;
coherence by Def7,Lm1;
cluster
with_FALSUM with_int_implication
with_int_conjunction with_int_disjunction
with_int_propositional_variables
with_modal_operator -> MC-closed Subset of NAT*;
coherence by Def7;
end;
definition
func MC-wff -> set means :Def8:
it is MC-closed &
for E being set st E is MC-closed holds it c= E;
existence
proof
defpred P[set] means
for E being set st E is MC-closed holds $1 in E;
consider E0 being set such that
A1: for x being set holds x in E0 iff x in NAT* & P[x]
from Separation;
A2: <*0*> in NAT* by FINSEQ_1:def 11;
A3: for E being set st E is MC-closed holds <*0*> in E
proof
let E be set; assume E is MC-closed;
then E is with_FALSUM by Def7;
hence thesis by Def1;
end;
then reconsider E0 as non empty set by A1,A2;
take E0;
A4: E0 c= NAT*
proof let x be set;
thus thesis by A1;
end;
<*0*> in E0 by A1,A2,A3;
then A5:E0 is with_FALSUM by Def1;
for n being Nat holds <* 5+2*n *> in E0
proof let n be Nat;
set p = 5+2*n;
reconsider h = <*p*> as FinSequence of NAT;
A6: h in NAT* by FINSEQ_1:def 11;
for E being set st E is MC-closed holds <*p*> in E
proof
let E be set;
assume E is MC-closed;
then E is with_int_propositional_variables by Def7;
hence thesis by Def5;
end;
hence thesis by A1,A6;
end;
then A7: E0 is with_int_propositional_variables by Def5;
for p, q being FinSequence
st p in E0 & q in E0 holds <*1*>^p^q in E0
proof
let p, q be FinSequence such that
A8: p in E0 & q in E0;
p in NAT* & q in NAT* by A1,A8;
then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
A9: <*1*>^p'^q' in NAT* by FINSEQ_1:def 11;
for E being set
st E is MC-closed holds <*1*>^p^q in E
proof let E be set; assume
A10: E is MC-closed;
then A11: E is with_int_implication by Def7;
p in E & q in E by A1,A8,A10;
hence thesis by A11,Def2;
end;
hence <*1*>^p^q in E0 by A1,A9;
end;
then A12: E0 is with_int_implication by Def2;
for p, q being FinSequence
st p in E0 & q in E0 holds <*2*>^p^q in E0
proof
let p, q be FinSequence such that
A13: p in E0 & q in E0;
p in NAT* & q in NAT* by A1,A13;
then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
A14: <*2*>^p'^q' in NAT* by FINSEQ_1:def 11;
for E being set
st E is MC-closed holds <*2*>^p^q in E
proof let E be set; assume
A15: E is MC-closed;
then A16: E is with_int_conjunction by Def7;
p in E & q in E by A1,A13,A15;
hence thesis by A16,Def3;
end;
hence <*2*>^p^q in E0 by A1,A14;
end;
then A17: E0 is with_int_conjunction by Def3;
for p, q being FinSequence
st p in E0 & q in E0 holds <*3*>^p^q in E0
proof
let p, q be FinSequence such that
A18: p in E0 & q in E0;
p in NAT* & q in NAT* by A1,A18;
then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
A19: <*3*>^p'^q' in NAT* by FINSEQ_1:def 11;
for E being set
st E is MC-closed holds <*3*>^p^q in E
proof let E be set; assume
A20: E is MC-closed;
then A21: E is with_int_disjunction by Def7;
p in E & q in E by A1,A18,A20;
hence thesis by A21,Def4;
end;
hence <*3*>^p^q in E0 by A1,A19;
end;
then A22: E0 is with_int_disjunction by Def4;
for p being FinSequence
st p in E0 holds <*6*>^p in E0
proof
let p be FinSequence such that
A23: p in E0;
p in NAT* by A1,A23;
then reconsider p'=p as FinSequence of NAT by FINSEQ_1:def 11;
A24: <*6*>^p' in NAT* by FINSEQ_1:def 11;
for E being set
st E is MC-closed holds <*6*>^p in E
proof let E be set; assume
A25: E is MC-closed;
then A26: E is with_modal_operator by Def7;
p in E by A1,A23,A25;
hence thesis by A26,Def6;
end;
hence <*6*>^p in E0 by A1,A24;
end;
then E0 is with_modal_operator by Def6;
hence E0 is MC-closed by A4,A5,A7,A12,A17,A22,Def7;
let E be set such that
A27: E is MC-closed;
let x be set; assume
x in E0;
hence thesis by A1,A27;
end;
uniqueness
proof
let E1, E2 be set such that
A28: E1 is MC-closed & for E being set
st E is MC-closed holds E1 c= E and
A29: E2 is MC-closed & for E being set
st E is MC-closed holds E2 c= E;
E1 c= E2 & E2 c= E1 by A28,A29;
hence E1 = E2 by XBOOLE_0:def 10;
end;
end;
definition
cluster MC-wff -> MC-closed;
coherence by Def8;
end;
definition
cluster MC-closed non empty set;
existence
proof
take MC-wff;
thus thesis;
end;
end;
definition
cluster -> Relation-like Function-like Element of MC-wff;
coherence
proof let p be Element of MC-wff;
MC-wff c= NAT* & p in MC-wff by Def7;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
cluster -> FinSequence-like Element of MC-wff;
coherence
proof let p be Element of MC-wff;
MC-wff c= NAT* & p in MC-wff by Def7;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
mode MC-formula is Element of MC-wff;
end;
definition
func FALSUM -> MC-formula equals
<*0*>;
correctness by Def1;
let p, q be Element of MC-wff;
func p => q -> MC-formula equals
<*1*>^p^q;
correctness by Def2;
func p '&' q -> MC-formula equals
<*2*>^p^q;
correctness by Def3;
func p 'or' q -> MC-formula equals
<*3*>^p^q;
correctness by Def4;
end;
definition
let p be Element of MC-wff;
func Nes p -> MC-formula equals
<*6*>^p;
correctness by Def6;
end;
reserve T, X, Y for Subset of MC-wff;
reserve p, q, r, s for Element of MC-wff;
definition let T be Subset of MC-wff;
attr T is IPC_theory means :Def14:
for p, q, r being Element of MC-wff holds
p => (q => p) in T &
(p => (q => r)) => ((p => q) => (p => r)) in T &
(p '&' q) => p in T &
(p '&' q) => q in T &
p => (q => (p '&' q)) in T &
p => (p 'or' q) in T &
q => (p 'or' q) in T &
(p => r) => ((q => r) => ((p 'or' q) => r)) in T &
FALSUM => p in T &
(p in T & p => q in T implies q in T);
correctness;
end;
definition let X;
func CnIPC X -> Subset of MC-wff means :Def15:
r in it iff for T st T is IPC_theory & X c= T holds r in T;
existence
proof
defpred P[set] means
for T st T is IPC_theory & X c= T holds $1 in T;
consider Y being set such that
A1: for a being set holds a in Y iff
a in MC-wff & P[a] from Separation;
Y c= MC-wff
proof
let a be set; assume a in Y;
hence a in MC-wff by A1;
end;
then reconsider Z = Y as Subset of MC-wff;
take Z;
thus r in Z iff for T st T is IPC_theory & X c= T holds r in T by A1;
end;
uniqueness
proof
let Y,Z be Subset of MC-wff such that
A2: r in Y iff for T st T is IPC_theory & X c= T holds r in T and
A3: r in Z iff for T st T is IPC_theory & X c= T holds r in T;
for a being set holds a in Y iff a in Z
proof
let a be set;
hereby assume A4: a in Y;
then reconsider t=a as Element of MC-wff;
for T st T is IPC_theory & X c= T holds t in T by A2,A4;
hence a in Z by A3;
end;
assume A5: a in Z;
then reconsider t=a as Element of MC-wff;
for T st T is IPC_theory & X c= T holds t in T by A3,A5;
hence a in Y by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func IPC-Taut -> Subset of MC-wff equals :Def16:
CnIPC({}(MC-wff));
correctness;
end;
definition
let p be Element of MC-wff;
func neg p -> MC-formula equals
(p => FALSUM);
correctness;
end;
definition
func IVERUM -> MC-formula equals :Def18:
(FALSUM => FALSUM);
correctness;
end;
theorem Th1:
p => (q => p) in CnIPC (X)
proof
T is IPC_theory & X c= T implies p => (q => p) in T by Def14;
hence thesis by Def15;
end;
theorem Th2:
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X)
proof
T is IPC_theory & X c= T implies
(p => (q => r)) => ((p => q) => (p => r)) in T by Def14;
hence thesis by Def15;
end;
theorem Th3:
p '&' q => p in CnIPC(X)
proof
T is IPC_theory & X c= T implies p '&' q => p in T by Def14;
hence thesis by Def15;
end;
theorem Th4:
p '&' q => q in CnIPC(X)
proof
T is IPC_theory & X c= T implies p '&' q => q in T by Def14;
hence thesis by Def15;
end;
theorem Th5:
p => (q => (p '&' q)) in CnIPC (X)
proof
T is IPC_theory & X c= T implies p => (q => (p '&' q)) in T by Def14;
hence thesis by Def15;
end;
theorem Th6:
p => (p 'or' q) in CnIPC (X)
proof
T is IPC_theory & X c= T implies p => (p 'or' q) in T by Def14;
hence thesis by Def15;
end;
theorem Th7:
q => (p 'or' q) in CnIPC (X)
proof
T is IPC_theory & X c= T implies q => (p 'or' q) in T by Def14;
hence thesis by Def15;
end;
theorem Th8:
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X)
proof
T is IPC_theory & X c= T
implies (p => r) => ((q => r) => ((p 'or' q) => r)) in T by Def14;
hence thesis by Def15;
end;
theorem Th9:
FALSUM => p in CnIPC (X)
proof
T is IPC_theory & X c= T implies FALSUM => p in T by Def14;
hence thesis by Def15;
end;
theorem Th10:
p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X)
proof
assume A1: p in CnIPC(X) & p => q in CnIPC(X);
T is IPC_theory & X c= T implies q in T
proof
assume A2: T is IPC_theory & X c= T;
then p in T & p => q in T by A1,Def15;
hence thesis by A2,Def14;
end;
hence thesis by Def15;
end;
theorem Th11: T is IPC_theory & X c= T implies CnIPC(X) c= T
proof
assume that A1:T is IPC_theory and A2: X c= T;
let a be set;
thus thesis by A1,A2,Def15;
end;
theorem Th12:
X c= CnIPC(X)
proof
let a be set;
assume A1: a in X;
then reconsider t = a as Element of MC-wff;
for T st T is IPC_theory & X c= T holds t in T by A1;
hence a in CnIPC(X) by Def15;
end;
theorem Th13:
X c= Y implies CnIPC(X) c= CnIPC(Y)
proof
assume A1: X c= Y;
thus CnIPC(X) c= CnIPC(Y)
proof
let a be set; assume A2: a in CnIPC(X);
then reconsider t = a as Element of MC-wff;
for T st T is IPC_theory & Y c= T holds t in T
proof
let T such that A3: T is IPC_theory and A4: Y c= T;
X c= T by A1,A4,XBOOLE_1:1;
hence t in T by A2,A3,Def15;
end;
hence thesis by Def15;
end;
end;
Lm2: CnIPC(CnIPC(X)) c= CnIPC(X)
proof
let a be set; assume A1: a in CnIPC(CnIPC(X));
then reconsider t = a as Element of MC-wff;
for T st T is IPC_theory & X c= T holds t in T
proof
let T; assume that A2: T is IPC_theory and A3: X c= T;
CnIPC(X) c= T by A2,A3,Th11;
hence t in T by A1,A2,Def15;
end;
hence thesis by Def15;
end;
theorem :: Th14:
CnIPC(CnIPC(X)) = CnIPC(X)
proof
CnIPC(CnIPC(X)) c= CnIPC(X) & CnIPC(X) c= CnIPC(CnIPC(X)) by Lm2,Th12;
hence thesis by XBOOLE_0:def 10;
end;
Lm3:
CnIPC(X) is IPC_theory
proof
let p, q, r;
thus p => (q => p) in CnIPC(X) by Th1;
thus (p => (q => r)) => ((p => q) => (p => r)) in CnIPC(X) by Th2;
thus (p '&' q) => p in CnIPC(X) by Th3;
thus (p '&' q) => q in CnIPC(X) by Th4;
thus p => (q => (p '&' q)) in CnIPC(X) by Th5;
thus p => (p 'or' q) in CnIPC(X) by Th6;
thus q => (p 'or' q) in CnIPC(X) by Th7;
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC(X) by Th8;
thus FALSUM => p in CnIPC(X) by Th9;
thus (p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X)) by Th10;
end;
definition let X be Subset of MC-wff;
cluster CnIPC(X) -> IPC_theory;
coherence by Lm3;
end;
theorem Th15:
T is IPC_theory iff CnIPC(T) = T
proof
hereby assume A1: T is IPC_theory;
A2: T c= CnIPC(T) by Th12;
CnIPC(T) c= T
proof
let a be set; assume a in CnIPC(T);
hence a in T by A1,Def15;
end;
hence CnIPC(T) = T by A2,XBOOLE_0:def 10;
end;
thus CnIPC(T) = T implies T is IPC_theory;
end;
theorem :: Th16:
T is IPC_theory implies IPC-Taut c= T
proof
assume A1: T is IPC_theory;
{}(MC-wff) c= T by XBOOLE_1:2;
then IPC-Taut c= CnIPC(T) by Def16,Th13;
hence thesis by A1,Th15;
end;
definition
cluster IPC-Taut -> IPC_theory;
coherence by Def16;
end;
begin :: Formulas provable in IPC : implication
theorem Th17: :: Identity law
p => p in IPC-Taut
proof
A1:p => (p => p) in IPC-Taut by Def14;
A2:(p => ((p => p) => p))
=> ((p => (p => p)) => (p => p)) in IPC-Taut by Def14;
p => ((p => p) => p) in IPC-Taut by Def14;
then (p => (p => p)) => (p => p) in IPC-Taut by A2,Def14;
hence thesis by A1,Def14;
end;
theorem Th18:
q in IPC-Taut implies p => q in IPC-Taut
proof
q => (p => q) in IPC-Taut by Def14;
hence thesis by Def14;
end;
theorem :: Th19:
IVERUM in IPC-Taut by Def14,Def18;
theorem :: Th20:
(p => q) => (p => p) in IPC-Taut
proof
(p => p) in IPC-Taut by Th17;
hence thesis by Th18;
end;
theorem :: Th21:
(q => p) => (p => p) in IPC-Taut
proof
(p => p) in IPC-Taut by Th17;
hence thesis by Th18;
end;
theorem Th22:
(q => r) => ((p => q) => (p => r)) in IPC-Taut
proof
A1:((p => (q => r)) => ((p => q) => (p => r))) =>
( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut
by Def14;
((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;
then A2: ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut
by A1,Def14;
( (q => r) => ((p => (q => r)) => ((p => q) => (p => r))))
=> (((q => r) => (p => (q => r))) =>
((q => r) => ((p => q) => (p => r)))) in IPC-Taut
by Def14;
then A3: ((q => r) => (p => (q => r))) =>
((q => r) => ((p => q) => (p => r))) in IPC-Taut
by A2,Def14;
(q => r) => (p => (q => r)) in IPC-Taut by Def14;
hence thesis by A3,Def14;
end;
theorem Th23:
p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut
proof
assume A1: p => (q => r) in IPC-Taut;
(p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then A2: ((p => q) => (p => r)) in IPC-Taut by A1,Def14;
((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in IPC-Taut
by Th22;
then A3:((q => (p => q)) => (q => (p => r))) in IPC-Taut by A2,Def14;
q => (p => q) in IPC-Taut by Def14;
hence thesis by A3,Def14;
end;
theorem Th24: :: Hypothetical syllogism
(p => q) => ((q => r) => (p => r)) in IPC-Taut
proof
(q => r) => ((p => q) => (p => r)) in IPC-Taut by Th22;
hence thesis by Th23;
end;
theorem Th25:
p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut
proof assume
A1: p => q in IPC-Taut;
(p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
hence (q => r) => (p => r) in IPC-Taut by A1,Def14;
end;
theorem Th26:
p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut
proof assume that
A1: p => q in IPC-Taut and
A2: q => r in IPC-Taut;
(p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
then (q => r) => (p => r) in IPC-Taut by A1,Def14;
hence p => r in IPC-Taut by A2,Def14;
end;
Lm4: (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
proof
(p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
hence thesis by Th25;
end;
theorem Th27:
(p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut
proof
A1: ((((q => r) => (s => r)) => (p => (s => r))) =>
((s => q) => (p => (s => r)))) =>
((p => (q => r)) => ((s => q) => (p => (s => r)))) in IPC-Taut by Lm4;
(((q => r) => (s => r)) => (p => (s => r))) =>
((s => q) => (p => (s => r))) in IPC-Taut by Lm4;
hence thesis by A1,Def14;
end;
theorem :: Th28:
((p => q) => r) => (q => r) in IPC-Taut
proof
q => (p => q) in IPC-Taut &
(q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut
by Def14,Th24;
hence thesis by Def14;
end;
theorem Th29: :: Contraposition
(p => (q => r)) => (q => (p => r)) in IPC-Taut
proof
(p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then A1:(p => q) => ((p => (q => r)) => (p => r)) in IPC-Taut by Th23;
((p => q) => ((p => (q => r)) => (p => r))) =>
((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in IPC-Taut
by Th22;
then A2:(q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut
by A1,Def14;
q => (p => q) in IPC-Taut by Def14;
then (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A2,Def14;
hence thesis by Th23;
end;
theorem Th30: :: A Hilbert axiom
(p => (p => q)) => (p => q) in IPC-Taut
proof
A1:p => p in IPC-Taut by Th17;
(p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14;
then (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23;
hence thesis by A1,Def14;
end;
theorem :: Th31: :: Modus ponendo ponens
q => ((q => p) => p) in IPC-Taut
proof
A1:(q => p) => (q => p) in IPC-Taut by Th17;
((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29;
hence thesis by A1,Def14;
end;
theorem Th32:
s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut
proof
assume A1: s => (q => p) in IPC-Taut & q in IPC-Taut;
(s => (q => p)) => (q => (s => p)) in IPC-Taut by Th29;
then q => (s => p) in IPC-Taut by A1,Def14;
hence thesis by A1,Def14;
end;
begin :: Formulas provable in IPC : conjunction
theorem Th33:
p => (p '&' p) in IPC-Taut
proof
A1:p => (p => (p '&' p)) in IPC-Taut by Def14;
(p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30;
hence thesis by A1,Def14;
end;
theorem Th34:
(p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut
proof
hereby assume A1: p '&' q in IPC-Taut;
(p '&' q) => p in IPC-Taut & (p '&' q) => q in IPC-Taut by Def14;
hence p in IPC-Taut & q in IPC-Taut by A1,Def14;
end;
assume A2: p in IPC-Taut & q in IPC-Taut;
p => (q => (p '&' q)) in IPC-Taut by Def14;
then q => (p '&' q) in IPC-Taut by A2,Def14;
hence thesis by A2,Def14;
end;
theorem :: Th35:
(p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut
proof
hereby assume p '&' q in IPC-Taut;
then p in IPC-Taut & q in IPC-Taut by Th34;
hence q '&' p in IPC-Taut by Th34;
end;
assume q '&' p in IPC-Taut;
then q in IPC-Taut & p in IPC-Taut by Th34;
hence p '&' q in IPC-Taut by Th34;
end;
theorem Th36:
(( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut
proof
( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r )) in IPC-Taut
by Th24;
then A1: p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r )))
in IPC-Taut by Th18;
set qp = ( q => ( p '&' q ));
set pr = (( p '&' q ) => r) => ( q => r );
( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) in IPC-Taut by
Def14
;
then A2: ( ( p => qp ) => ( p => pr )) in IPC-Taut by A1,Def14;
p => ( q => ( p '&' q )) in IPC-Taut by Def14;
then A3: p => ((( p '&' q ) => r ) => ( q => r )) in IPC-Taut by A2,Def14;
(p => ((( p '&' q ) => r ) => ( q => r ))) =>
((( p '&' q ) => r ) => ( p => ( q => r ))) in IPC-Taut by Th29;
hence thesis by A3,Def14;
end;
theorem Th37:
( p => ( q => r )) => (( p '&' q ) => r ) in IPC-Taut
proof
A1: ( p '&' q ) => q in IPC-Taut by Def14;
(( p '&' q ) => q) => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut
by Th24;
then ( q => r ) => (( p '&' q ) => r ) in IPC-Taut by A1,Def14;
then A2: p => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut by Th18;
p => (( q => r ) => (( p '&' q ) => r )) =>
((p => ( q => r )) => ( p => (( p '&' q ) => r ))) in IPC-Taut
by Def14;
then A3: (p => ( q => r )) => ( p => (( p '&' q ) => r )) in IPC-Taut
by A2,Def14;
( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut
by Th29;
then A4: (p => ( q => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by A3,
Th26;
A5: ((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q )
=> r )) in IPC-Taut by Def14;
( p '&' q ) => p in IPC-Taut by Def14;
then ((p '&' q ) => ( p => r )) => (( p '&' q ) => r ) in IPC-Taut by A5,
Th32;
hence thesis by A4,Th26;
end;
theorem Th38:
( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in IPC-Taut
proof
p => ( q => ( p '&' q )) in IPC-Taut by Def14;
then A1: r => ( p => ( q => ( p '&' q ))) in IPC-Taut by Th18;
(r => ( p => ( q => ( p '&' q )))) =>
(( r => p ) => ( r => ( q => ( p '&' q )))) in IPC-Taut by Def14;
then A2: ( r => p ) => ( r => ( q => ( p '&' q ))) in IPC-Taut by A1,Def14;
( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q )))
in IPC-Taut by Def14;
hence thesis by A2,Th26;
end;
theorem Th39:
( (p => q) '&' p ) => q in IPC-Taut
proof
set P = p => q;
A1:( P => P ) => (( P '&' p ) => q ) in IPC-Taut by Th37;
P => P in IPC-Taut by Th17;
hence thesis by A1,Def14;
end;
theorem :: Th40:
(( (p => q) '&' p ) '&' s ) => q in IPC-Taut
proof
set P = (p => q) '&' p;
A1:(P '&' s) => P in IPC-Taut by Def14;
P => q in IPC-Taut by Th39;
hence thesis by A1,Th26;
end;
theorem :: Th41:
(q => s) => (( p '&' q ) => s) in IPC-Taut
proof
set P = p '&' q;
A1:(P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
P => q in IPC-Taut by Def14;
hence thesis by A1,Def14;
end;
theorem Th42:
(q => s) => (( q '&' p ) => s) in IPC-Taut
proof
set P = q '&' p;
A1:(P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
P => q in IPC-Taut by Def14;
hence thesis by A1,Def14;
end;
theorem Th43:
( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
set P = p '&' s;
A1:P => s in IPC-Taut by Def14;
( P => q ) => (( P => s ) => ( P => ( q '&' s ))) in IPC-Taut by Th38;
hence thesis by A1,Th32;
end;
theorem Th44:
( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
A1:(p => q) => (( p '&' s ) => q) in IPC-Taut by Th42;
( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43;
hence thesis by A1,Th26;
end;
theorem Th45:
(( p => q ) '&' ( p '&' s )) => ( q '&' s ) in IPC-Taut
proof
set P = p => q, Q = p '&' s, S = q '&' s;
A1:( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
P => (Q => S) in IPC-Taut by Th44;
hence thesis by A1,Def14;
end;
theorem Th46:
( p '&' q ) => ( q '&' p ) in IPC-Taut
proof
set P = p '&' q;
A1:( P => q ) => (( P => p ) => ( P => ( q '&' p ))) in IPC-Taut by Th38;
P => q in IPC-Taut by Def14;
then A2:( P => p ) => ( P => ( q '&' p )) in IPC-Taut by A1,Def14;
P => p in IPC-Taut by Def14;
hence thesis by A2,Def14;
end;
theorem Th47:
( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut
proof
A1:( p => q ) '&' ( p '&' s ) => ( q '&' s ) in IPC-Taut by Th45;
( q '&' s ) => ( s '&' q ) in IPC-Taut by Th46;
hence thesis by A1,Th26;
end;
theorem Th48:
( p => q ) => (( p '&' s ) => ( s '&' q )) in IPC-Taut
proof
set P = p => q, Q = p '&' s, S = s '&' q;
A1:(( P '&' Q ) => S ) => ( P => ( Q => S )) in IPC-Taut by Th36;
P '&' Q => S in IPC-Taut by Th47;
hence thesis by A1,Def14;
end;
theorem Th49:
( p => q ) => (( s '&' p ) => ( s '&' q )) in IPC-Taut
proof
set P = p => q, Q = p '&' s, S = s '&' q, T = s '&' p;
A1:(P => (Q => S)) => ((T => Q) => (P => (T => S))) in IPC-Taut by Th27;
P => (Q => S) in IPC-Taut by Th48;
then A2:(T => Q) => (P => (T => S)) in IPC-Taut by A1,Def14;
T => Q in IPC-Taut by Th46;
hence thesis by A2,Def14;
end;
theorem :: Th50:
( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut
proof
set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
P => Q in IPC-Taut by Th46;
hence thesis by A1,Def14;
end;
theorem :: Th51:
( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in IPC-Taut
proof
set P = p => q, Q = p => s, S = p => (q '&' s);
A1:( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
P => (Q => S) in IPC-Taut by Th38;
hence thesis by A1,Def14;
end;
Lm5:
( (p '&' q) '&' s ) => q in IPC-Taut
proof
A1:((p '&' q) '&' s) => (p '&' q) in IPC-Taut by Def14;
(p '&' q) => q in IPC-Taut by Def14;
hence thesis by A1,Th26;
end;
Lm6:
( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q
in IPC-Taut
proof
set P = (p '&' q) '&' s;
A1:( P => q ) => (( P '&' P ) => ( P '&' q )) in IPC-Taut by Th49;
P => q in IPC-Taut by Lm5;
hence thesis by A1,Def14;
end;
Lm7:
(p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut
proof
A1:( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s )
in IPC-Taut by Th33;
( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q
in IPC-Taut by Lm6;
hence thesis by A1,Th26;
end;
Lm8:
(p '&' q) '&' s => (p '&' s) in IPC-Taut
proof
set P = p '&' q;
A1:( P => p ) => ((P '&' s) => (p '&' s)) in IPC-Taut by Th44;
P => p in IPC-Taut by Def14;
hence thesis by A1,Def14;
end;
Lm9:
(p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut
proof
set P = p '&' q '&' s, Q = p '&' s;
A1:( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
P => Q in IPC-Taut by Lm8;
hence thesis by A1,Def14;
end;
Lm10:
(p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut
proof
A1:(p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut by Lm7;
(p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut by Lm9;
hence thesis by A1,Th26;
end;
Lm11:
(p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut
proof
set P = p '&' s, Q = s '&' p;
A1:( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
P => Q in IPC-Taut by Th46;
hence thesis by A1,Def14;
end;
Lm12:
(p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut
proof
A1:(p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut by Lm10;
(p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut by Lm11;
hence thesis by A1,Th26;
end;
Lm13:
(p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut
proof
A1:(p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut by Lm12;
(s '&' p) '&' q => (s '&' q) '&' p in IPC-Taut by Lm10;
hence thesis by A1,Th26;
end;
Lm14:
(p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut
proof
A1:(p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut by Lm13;
(s '&' q) '&' p => p '&' (s '&' q) in IPC-Taut by Th46;
hence thesis by A1,Th26;
end;
Lm15:
p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut
proof
set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
s '&' q => q '&' s in IPC-Taut by Th46;
hence thesis by A1,Def14;
end;
theorem :: Th52:
(p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut
proof
A1:(p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut by Lm14;
p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut by Lm15;
hence thesis by A1,Th26;
end;
Lm16:
p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut
proof
A1:p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm15;
p '&' (s '&' q) => (s '&' q) '&' p in IPC-Taut by Th46;
hence thesis by A1,Th26;
end;
Lm17:
(s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut
proof
set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => ((P '&' p) => (Q '&' p)) in IPC-Taut by Th44;
s '&' q => q '&' s in IPC-Taut by Th46;
hence thesis by A1,Def14;
end;
Lm18:
p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut
proof
A1:p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut by Lm16;
(s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut by Lm17;
hence thesis by A1,Th26;
end;
Lm19:
p '&' (q '&' s) => (p '&' s) '&' q in IPC-Taut
proof
A1:p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut by Lm18;
(q '&' s) '&' p => (p '&' s) '&' q in IPC-Taut by Lm13;
hence thesis by A1,Th26;
end;
Lm20:
p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut
proof
set P = q '&' s, Q = s '&' q;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
q '&' s => s '&' q in IPC-Taut by Th46;
hence thesis by A1,Def14;
end;
theorem :: Th53:
p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut
proof
A1:p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm20;
p '&' (s '&' q) => (p '&' q) '&' s in IPC-Taut by Lm19;
hence thesis by A1,Th26;
end;
begin :: Formulas provable in IPC: disjunction
theorem Th54:
(p 'or' p) => p in IPC-Taut
proof
A1:p => p in IPC-Taut by Th17;
(p => p) => ((p => p) => ((p 'or' p) => p)) in IPC-Taut by Def14;
then (p => p) => ((p 'or' p) => p) in IPC-Taut by A1,Def14;
hence thesis by A1,Def14;
end;
theorem :: Th55:
p in IPC-Taut or q in IPC-Taut implies (p 'or' q) in IPC-Taut
proof
assume A1: p in IPC-Taut or q in IPC-Taut;
now per cases by A1;
case A2: p in IPC-Taut;
p => (p 'or' q) in IPC-Taut by Def14;
hence thesis by A2,Def14;
case A3: q in IPC-Taut;
q => (p 'or' q) in IPC-Taut by Def14;
hence thesis by A3,Def14;
end;
hence thesis;
end;
theorem Th56:
(p 'or' q) => (q 'or' p) in IPC-Taut
proof
A1: (p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)))
in IPC-Taut by Def14;
A2: p => (q 'or' p) in IPC-Taut by Def14;
A3: q => (q 'or' p) in IPC-Taut by Def14;
((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)))
in IPC-Taut by A1,A2,Def14;
hence thesis by A3,Def14;
end;
theorem :: Th57:
(p 'or' q) in IPC-Taut iff (q 'or' p) in IPC-Taut
proof
hereby assume A1: p 'or' q in IPC-Taut;
(p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
hence q 'or' p in IPC-Taut by A1,Def14;
end;
assume A2: q 'or' p in IPC-Taut;
(q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
hence p 'or' q in IPC-Taut by A2,Def14;
end;
theorem Th58:
(p => q) => (p => (q 'or' s)) in IPC-Taut
proof
A1: q => (q 'or' s) in IPC-Taut by Def14;
(q => (q 'or' s)) => ((p => q) => (p => (q 'or' s))) in IPC-Taut by Th22;
hence thesis by A1,Def14;
end;
theorem Th59:
(p => q) => (p => (s 'or' q)) in IPC-Taut
proof
A1: q => (s 'or' q) in IPC-Taut by Def14;
(q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22;
hence thesis by A1,Def14;
end;
theorem Th60:
( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut
proof
set P = p 'or' s, Q = q 'or' s;
(p => Q) => ((s => Q) => (P => Q)) in IPC-Taut by Def14;
then A1: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Th23;
s => Q in IPC-Taut by Def14;
then A2: (p => Q) => (P => Q) in IPC-Taut by A1,Def14;
(p => q) => (p => Q) in IPC-Taut by Th58;
hence thesis by A2,Th26;
end;
theorem Th61:
p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut
proof
assume A1: p => q in IPC-Taut;
( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by Th60;
hence thesis by A1,Def14;
end;
theorem Th62:
( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut
proof
set P = s 'or' p, Q = s 'or' q;
A1: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Def14;
s => Q in IPC-Taut by Def14;
then A2: (p => Q) => (P => Q) in IPC-Taut by A1,Def14;
(p => q) => (p => Q) in IPC-Taut by Th59;
hence thesis by A2,Th26;
end;
theorem Th63:
p => q in IPC-Taut implies ( s 'or' p ) => ( s 'or' q ) in IPC-Taut
proof
assume A1: p => q in IPC-Taut;
( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut by Th62;
hence thesis by A1,Def14;
end;
theorem Th64:
( p 'or' (q 'or' s) ) => ( q 'or' (p 'or' s) ) in IPC-Taut
proof
set P = p 'or' s, Q = q 'or' s;
s => P in IPC-Taut by Def14;
then (q 'or' s) => (q 'or' P) in IPC-Taut by Th63;
:: Q => (q 'or' P) in IPC-Taut; then
then A1: (p 'or' Q) => (p 'or' (q 'or' P)) in IPC-Taut by Th63;
(p 'or' (q 'or' P)) => ((q 'or' P) 'or' p) in IPC-Taut by Th56;
then A2: (p 'or' Q) => ((q 'or' P) 'or' p) in IPC-Taut by A1,Th26;
A3: p => P in IPC-Taut by Def14;
P => (q 'or' P) in IPC-Taut by Def14;
then p => (q 'or' P) in IPC-Taut by A3,Th26;
then A4: ((q 'or' P) 'or' p) => ((q 'or' P) 'or' (q 'or' P))
in IPC-Taut by Th63;
((q 'or' P) 'or' (q 'or' P)) => (q 'or' P) in IPC-Taut by Th54;
then ((q 'or' P) 'or' p) => (q 'or' P) in IPC-Taut by A4,Th26;
hence thesis by A2,Th26;
end;
theorem :: Th65:
( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut
proof
(q 'or' s) => (s 'or' q) in IPC-Taut by Th56;
then A1: (p 'or' (q 'or' s)) => (p 'or' (s 'or' q)) in IPC-Taut by Th63;
(p 'or' (s 'or' q)) => (s 'or' (p 'or' q)) in IPC-Taut by Th64;
then A2: (p 'or' (q 'or' s)) => (s 'or' (p 'or' q))
in IPC-Taut by A1,Th26;
(s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56;
hence thesis by A2,Th26;
end;
theorem :: Th66:
( (p 'or' q) 'or' s ) => ( p 'or' (q 'or' s) ) in IPC-Taut
proof
(p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
then A1: ((p 'or' q) 'or' s) => ((q 'or' p) 'or' s) in IPC-Taut by Th61;
((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56;
then A2: ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1,Th26;
(q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
then (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63;
then A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26;
(s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64;
then A4: ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3,Th26;
(s 'or' q) => (q 'or' s) in IPC-Taut by Th56;
then (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63;
hence thesis by A4,Th26;
end;
begin :: Classical propositional calculus CPC
reserve T, X, Y for Subset of MC-wff;
reserve p, q, r for Element of MC-wff;
definition let T be Subset of MC-wff;
attr T is CPC_theory means :Def19:
for p, q, r being Element of MC-wff holds
p => (q => p) in T &
(p => (q => r)) => ((p => q) => (p => r)) in T &
(p '&' q) => p in T &
(p '&' q) => q in T &
p => (q => (p '&' q)) in T &
p => (p 'or' q) in T &
q => (p 'or' q) in T &
(p => r) => ((q => r) => ((p 'or' q) => r)) in T &
FALSUM => p in T &
p 'or' (p => FALSUM) in T &
(p in T & p => q in T implies q in T);
correctness;
end;
theorem Th67:
T is CPC_theory implies T is IPC_theory
proof
assume A1: T is CPC_theory;
let p, q, r be Element of MC-wff;
thus thesis by A1,Def19;
end;
definition let X;
func CnCPC X -> Subset of MC-wff means :Def20:
r in it iff for T st T is CPC_theory & X c= T holds r in T;
existence
proof
defpred P[set] means
for T st T is CPC_theory & X c= T holds $1 in T;
consider Y being set such that
A1: for a being set holds a in Y iff
a in MC-wff & P[a] from Separation;
Y c= MC-wff
proof
let a be set; assume a in Y;
hence a in MC-wff by A1;
end;
then reconsider Z = Y as Subset of MC-wff;
take Z;
thus r in Z iff for T st T is CPC_theory & X c= T holds r in T by A1;
end;
uniqueness
proof
let Y,Z be Subset of MC-wff such that
A2: r in Y iff for T st T is CPC_theory & X c= T holds r in T and
A3: r in Z iff for T st T is CPC_theory & X c= T holds r in T;
for a being set holds a in Y iff a in Z
proof
let a be set;
hereby assume A4: a in Y;
then reconsider t=a as Element of MC-wff;
for T st T is CPC_theory & X c= T holds t in T by A2,A4;
hence a in Z by A3;
end;
assume A5: a in Z;
then reconsider t=a as Element of MC-wff;
for T st T is CPC_theory & X c= T holds t in T by A3,A5;
hence a in Y by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func CPC-Taut -> Subset of MC-wff equals :Def21:
CnCPC({}(MC-wff));
correctness;
end;
theorem Th68:
CnIPC (X) c= CnCPC (X)
proof
let a be set;
assume A1: a in CnIPC (X);
then reconsider r = a as Element of MC-wff;
for T st T is CPC_theory & X c= T holds r in T
proof
let T such that A2: T is CPC_theory and A3: X c= T;
T is IPC_theory by A2,Th67;
hence r in T by A1,A3,Def15;
end;
hence thesis by Def20;
end;
theorem Th69:
p => (q => p) in CnCPC (X) &
(p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X) &
p '&' q => p in CnCPC (X) &
p '&' q => q in CnCPC (X) &
p => (q => (p '&' q)) in CnCPC (X) &
p => (p 'or' q) in CnCPC (X) &
q => (p 'or' q) in CnCPC (X) &
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X) &
FALSUM => p in CnCPC (X) &
p 'or' (p => FALSUM) in CnCPC (X)
proof
thus p => (q => p) in CnCPC (X)
proof
A1: p => (q => p) in CnIPC (X) by Th1;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A1;
end;
thus (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X)
proof
A2: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A2;
end;
thus p '&' q => p in CnCPC (X)
proof
A3: p '&' q => p in CnIPC (X) by Th3;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A3;
end;
thus p '&' q => q in CnCPC (X)
proof
A4: p '&' q => q in CnIPC (X) by Th4;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A4;
end;
thus p => (q => (p '&' q)) in CnCPC (X)
proof
A5: p => (q => (p '&' q)) in CnIPC (X) by Th5;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A5;
end;
thus p => (p 'or' q) in CnCPC (X)
proof
A6: p => (p 'or' q) in CnIPC (X) by Th6;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A6;
end;
thus q => (p 'or' q) in CnCPC (X)
proof
A7: q => (p 'or' q) in CnIPC (X) by Th7;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A7;
end;
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X)
proof
A8: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A8;
end;
thus FALSUM => p in CnCPC (X)
proof
A9: FALSUM => p in CnIPC (X) by Th9;
CnIPC(X) c= CnCPC(X) by Th68;
hence thesis by A9;
end;
thus p 'or' (p => FALSUM) in CnCPC (X)
proof
T is CPC_theory & X c= T implies
p 'or' (p => FALSUM) in T by Def19;
hence thesis by Def20;
end;
end;
theorem Th70:
p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X)
proof
assume A1: p in CnCPC(X) & p => q in CnCPC(X);
T is CPC_theory & X c= T implies q in T
proof
assume A2: T is CPC_theory & X c= T;
then p in T & p => q in T by A1,Def20;
hence thesis by A2,Def19;
end;
hence thesis by Def20;
end;
theorem Th71: T is CPC_theory & X c= T implies CnCPC(X) c= T
proof
assume that A1:T is CPC_theory and A2: X c= T;
let a be set;
thus thesis by A1,A2,Def20;
end;
theorem Th72:
X c= CnCPC(X)
proof
let a be set;
assume A1: a in X;
then reconsider t = a as Element of MC-wff;
for T st T is CPC_theory & X c= T holds t in T by A1;
hence a in CnCPC(X) by Def20;
end;
theorem Th73:
X c= Y implies CnCPC(X) c= CnCPC(Y)
proof
assume A1: X c= Y;
thus CnCPC(X) c= CnCPC(Y)
proof
let a be set; assume A2: a in CnCPC(X);
then reconsider t = a as Element of MC-wff;
for T st T is CPC_theory & Y c= T holds t in T
proof
let T such that A3: T is CPC_theory and A4: Y c= T;
X c= T by A1,A4,XBOOLE_1:1;
hence t in T by A2,A3,Def20;
end;
hence thesis by Def20;
end;
end;
Lm21: CnCPC(CnCPC(X)) c= CnCPC(X)
proof
let a be set; assume A1: a in CnCPC(CnCPC(X));
then reconsider t = a as Element of MC-wff;
for T st T is CPC_theory & X c= T holds t in T
proof
let T; assume that A2: T is CPC_theory and A3: X c= T;
CnCPC(X) c= T by A2,A3,Th71;
hence t in T by A1,A2,Def20;
end;
hence thesis by Def20;
end;
theorem :: Th6C:
CnCPC(CnCPC(X)) = CnCPC(X)
proof
CnCPC(CnCPC(X)) c= CnCPC(X) & CnCPC(X) c= CnCPC(CnCPC(X)) by Lm21,Th72;
hence thesis by XBOOLE_0:def 10;
end;
Lm22:
CnCPC(X) is CPC_theory
proof
let p, q, r;
thus p => (q => p) in CnCPC(X) by Th69;
thus (p => (q => r)) => ((p => q) => (p => r)) in CnCPC(X) by Th69;
thus (p '&' q) => p in CnCPC(X) by Th69;
thus (p '&' q) => q in CnCPC(X) by Th69;
thus p => (q => (p '&' q)) in CnCPC(X) by Th69;
thus p => (p 'or' q) in CnCPC(X) by Th69;
thus q => (p 'or' q) in CnCPC(X) by Th69;
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC(X) by Th69;
thus FALSUM => p in CnCPC(X) by Th69;
thus p 'or' (p => FALSUM) in CnCPC (X) by Th69;
thus (p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X)) by Th70;
end;
definition let X be Subset of MC-wff;
cluster CnCPC(X) -> CPC_theory;
coherence by Lm22;
end;
theorem Th75:
T is CPC_theory iff CnCPC(T) = T
proof
hereby assume A1: T is CPC_theory;
A2: T c= CnCPC(T) by Th72;
CnCPC(T) c= T
proof
let a be set; assume a in CnCPC(T);
hence a in T by A1,Def20;
end;
hence CnCPC(T) = T by A2,XBOOLE_0:def 10;
end;
thus CnCPC(T) = T implies T is CPC_theory;
end;
theorem :: Th8C:
T is CPC_theory implies CPC-Taut c= T
proof
assume A1: T is CPC_theory;
{}(MC-wff) c= T by XBOOLE_1:2;
then CPC-Taut c= CnCPC(T) by Def21,Th73;
hence thesis by A1,Th75;
end;
definition
cluster CPC-Taut -> CPC_theory;
coherence by Def21;
end;
theorem :: CPCincIPC:
IPC-Taut c= CPC-Taut by Def16,Def21,Th68;
begin :: Modal calculus S4
reserve T, X, Y for Subset of MC-wff;
reserve p, q, r for Element of MC-wff;
definition let T be Subset of MC-wff;
attr T is S4_theory means :Def22:
for p, q, r being Element of MC-wff holds
p => (q => p) in T &
(p => (q => r)) => ((p => q) => (p => r)) in T &
(p '&' q) => p in T &
(p '&' q) => q in T &
p => (q => (p '&' q)) in T &
p => (p 'or' q) in T &
q => (p 'or' q) in T &
(p => r) => ((q => r) => ((p 'or' q) => r)) in T &
FALSUM => p in T &
p 'or' (p => FALSUM) in T &
(Nes (p => q)) => ((Nes p) => (Nes q)) in T &
(Nes p) => p in T &
(Nes p) => Nes (Nes p) in T &
(p in T & p => q in T implies q in T) &
(p in T implies Nes p in T);
correctness;
end;
theorem Th78:
T is S4_theory implies T is CPC_theory
proof
assume A1: T is S4_theory;
let p, q, r be Element of MC-wff;
thus thesis by A1,Def22;
end;
theorem :: S4TincIPCT:
T is S4_theory implies T is IPC_theory
proof
assume A1: T is S4_theory;
let p, q, r be Element of MC-wff;
thus thesis by A1,Def22;
end;
definition let X;
func CnS4 X -> Subset of MC-wff means :Def23:
r in it iff for T st T is S4_theory & X c= T holds r in T;
existence
proof
defpred P[set] means
for T st T is S4_theory & X c= T holds $1 in T;
consider Y being set such that
A1: for a being set holds a in Y iff
a in MC-wff & P[a] from Separation;
Y c= MC-wff
proof
let a be set; assume a in Y;
hence a in MC-wff by A1;
end;
then reconsider Z = Y as Subset of MC-wff;
take Z;
thus r in Z iff for T st T is S4_theory & X c= T holds r in T by A1;
end;
uniqueness
proof
let Y,Z be Subset of MC-wff such that
A2: r in Y iff for T st T is S4_theory & X c= T holds r in T and
A3: r in Z iff for T st T is S4_theory & X c= T holds r in T;
for a being set holds a in Y iff a in Z
proof
let a be set;
hereby assume A4: a in Y;
then reconsider t=a as Element of MC-wff;
for T st T is S4_theory & X c= T holds t in T by A2,A4;
hence a in Z by A3;
end;
assume A5: a in Z;
then reconsider t=a as Element of MC-wff;
for T st T is S4_theory & X c= T holds t in T by A3,A5;
hence a in Y by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func S4-Taut -> Subset of MC-wff equals :Def24:
CnS4({}(MC-wff));
correctness;
end;
theorem Th80:
CnCPC (X) c= CnS4 (X)
proof
let a be set;
assume A1: a in CnCPC (X);
then reconsider r = a as Element of MC-wff;
for T st T is S4_theory & X c= T holds r in T
proof
let T such that A2: T is S4_theory and A3: X c= T;
T is CPC_theory by A2,Th78;
hence thesis by A1,A3,Def20;
end;
hence thesis by Def23;
end;
theorem Th81:
CnIPC (X) c= CnS4 (X)
proof
A1: CnIPC (X) c= CnCPC (X) by Th68;
CnCPC (X) c= CnS4 (X) by Th80;
hence thesis by A1,XBOOLE_1:1;
end;
theorem Th82:
p => (q => p) in CnS4 (X) &
(p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X) &
p '&' q => p in CnS4 (X) &
p '&' q => q in CnS4 (X) &
p => (q => (p '&' q)) in CnS4 (X) &
p => (p 'or' q) in CnS4 (X) &
q => (p 'or' q) in CnS4 (X) &
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X) &
FALSUM => p in CnS4 (X) &
p 'or' (p => FALSUM) in CnS4 (X)
proof
thus p => (q => p) in CnS4 (X)
proof
A1: p => (q => p) in CnIPC (X) by Th1;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A1;
end;
thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X)
proof
A2: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A2;
end;
thus p '&' q => p in CnS4 (X)
proof
A3: p '&' q => p in CnIPC (X) by Th3;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A3;
end;
thus p '&' q => q in CnS4 (X)
proof
A4: p '&' q => q in CnIPC (X) by Th4;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A4;
end;
thus p => (q => (p '&' q)) in CnS4 (X)
proof
A5: p => (q => (p '&' q)) in CnIPC (X) by Th5;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A5;
end;
thus p => (p 'or' q) in CnS4 (X)
proof
A6: p => (p 'or' q) in CnIPC (X) by Th6;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A6;
end;
thus q => (p 'or' q) in CnS4 (X)
proof
A7: q => (p 'or' q) in CnIPC (X) by Th7;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A7;
end;
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X)
proof
A8: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A8;
end;
thus FALSUM => p in CnS4 (X)
proof
A9: FALSUM => p in CnIPC (X) by Th9;
CnIPC (X) c= CnS4 (X) by Th81;
hence thesis by A9;
end;
thus p 'or' (p => FALSUM) in CnS4 (X)
proof
T is S4_theory & X c= T implies
p 'or' (p => FALSUM) in T by Def22;
hence thesis by Def23;
end;
end;
theorem Th83:
p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X)
proof
assume A1: p in CnS4 (X) & p => q in CnS4 (X);
T is S4_theory & X c= T implies q in T
proof
assume A2: T is S4_theory & X c= T;
then p in T & p => q in T by A1,Def23;
hence thesis by A2,Def22;
end;
hence thesis by Def23;
end;
theorem Th84:
(Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 (X)
proof
T is S4_theory & X c= T
implies (Nes (p => q)) => ((Nes p) => (Nes q)) in T by Def22;
hence thesis by Def23;
end;
theorem Th85:
(Nes p) => p in CnS4 (X)
proof
T is S4_theory & X c= T implies (Nes p) => p in T by Def22;
hence thesis by Def23;
end;
theorem Th86:
(Nes p) => Nes (Nes p) in CnS4 (X)
proof
T is S4_theory & X c= T implies (Nes p) => Nes (Nes p) in T by Def22;
hence thesis by Def23;
end;
theorem Th87:
p in CnS4 (X) implies Nes p in CnS4 (X)
proof
assume A1: p in CnS4 (X);
T is S4_theory & X c= T implies Nes p in T
proof
assume A2: T is S4_theory & X c= T;
then p in T by A1,Def23;
hence thesis by A2,Def22;
end;
hence thesis by Def23;
end;
theorem Th88: T is S4_theory & X c= T implies CnS4(X) c= T
proof
assume that A1:T is S4_theory and A2: X c= T;
let a be set;
thus thesis by A1,A2,Def23;
end;
theorem Th89:
X c= CnS4(X)
proof
let a be set;
assume A1: a in X;
then reconsider t = a as Element of MC-wff;
for T st T is S4_theory & X c= T holds t in T by A1;
hence a in CnS4(X) by Def23;
end;
theorem Th90:
X c= Y implies CnS4(X) c= CnS4(Y)
proof
assume A1: X c= Y;
thus CnS4(X) c= CnS4(Y)
proof
let a be set; assume A2: a in CnS4(X);
then reconsider t = a as Element of MC-wff;
for T st T is S4_theory & Y c= T holds t in T
proof
let T such that A3: T is S4_theory and A4: Y c= T;
X c= T by A1,A4,XBOOLE_1:1;
hence t in T by A2,A3,Def23;
end;
hence thesis by Def23;
end;
end;
Lm23: CnS4(CnS4(X)) c= CnS4(X)
proof
let a be set; assume A1: a in CnS4(CnS4(X));
then reconsider t = a as Element of MC-wff;
for T st T is S4_theory & X c= T holds t in T
proof
let T; assume that A2: T is S4_theory and A3: X c= T;
CnS4(X) c= T by A2,A3,Th88;
hence t in T by A1,A2,Def23;
end;
hence thesis by Def23;
end;
theorem :: Th10M:
CnS4(CnS4(X)) = CnS4(X)
proof
CnS4(CnS4(X)) c= CnS4(X) & CnS4(X) c= CnS4(CnS4(X)) by Lm23,Th89;
hence thesis by XBOOLE_0:def 10;
end;
Lm24:
CnS4(X) is S4_theory
proof
let p, q, r;
thus p => (q => p) in CnS4(X) by Th82;
thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4(X) by Th82;
thus (p '&' q) => p in CnS4(X) by Th82;
thus (p '&' q) => q in CnS4(X) by Th82;
thus p => (q => (p '&' q)) in CnS4(X) by Th82;
thus p => (p 'or' q) in CnS4(X) by Th82;
thus q => (p 'or' q) in CnS4(X) by Th82;
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4(X) by Th82;
thus FALSUM => p in CnS4(X) by Th82;
thus p 'or' (p => FALSUM) in CnS4 (X) by Th82;
thus (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4(X) by Th84;
thus (Nes p) => p in CnS4(X) by Th85;
thus (Nes p) => Nes (Nes p) in CnS4(X) by Th86;
thus p in CnS4(X) & p => q in CnS4(X) implies q in CnS4(X) by Th83;
thus (p in CnS4(X) implies Nes p in CnS4(X)) by Th87;
end;
definition let X be Subset of MC-wff;
cluster CnS4(X) -> S4_theory;
coherence by Lm24;
end;
theorem Th92:
T is S4_theory iff CnS4(T) = T
proof
hereby assume A1: T is S4_theory;
A2: T c= CnS4(T) by Th89;
CnS4(T) c= T
proof
let a be set; assume a in CnS4(T);
hence a in T by A1,Def23;
end;
hence CnS4(T) = T by A2,XBOOLE_0:def 10;
end;
thus CnS4(T) = T implies T is S4_theory;
end;
theorem :: Th12M:
T is S4_theory implies S4-Taut c= T
proof
assume A1: T is S4_theory;
{}(MC-wff) c= T by XBOOLE_1:2;
then S4-Taut c= CnS4(T) by Def24,Th90;
hence thesis by A1,Th92;
end;
definition
cluster S4-Taut -> S4_theory;
coherence by Def24;
end;
theorem :: S4incCPC:
CPC-Taut c= S4-Taut by Def21,Def24,Th80;
theorem :: S4incIPC:
IPC-Taut c= S4-Taut by Def16,Def24,Th81;