:: Intuitionistic Propositional Calculus in the Extended Framework with Modal
:: Operator, Part I
:: by Takao Inou\'e
::
:: Received April 3, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, RELAT_1,
TARSKI, XBOOLE_0, FUNCT_1, QC_LANG2, XBOOLEAN, INTPRO_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
FUNCT_1, FINSEQ_1;
constructors NAT_1, FINSEQ_1, NUMBERS;
registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI;
expansions 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 Element of 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;
hence thesis;
end;
registration
cluster MC-closed -> with_FALSUM with_int_implication with_int_conjunction
with_int_disjunction with_int_propositional_variables with_modal_operator non
empty for set;
coherence by Lm1;
cluster with_FALSUM with_int_implication with_int_conjunction
with_int_disjunction with_int_propositional_variables with_modal_operator ->
MC-closed for Subset of NAT*;
coherence;
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
A1: <*0*> in NAT* by FINSEQ_1:def 11;
defpred P[object] means for E being set st E is MC-closed holds $1 in E;
consider E0 being set such that
A2: for x being object holds x in E0 iff x in NAT* & P[x] from XBOOLE_0:
sch 1;
A3: for E being set st E is MC-closed holds <*0*> in E by Def1;
then reconsider E0 as non empty set by A2,A1;
take E0;
A4: E0 c= NAT*
by A2;
for p being FinSequence st p in E0 holds <*6*>^p in E0
proof
let p be FinSequence such that
A5: p in E0;
p in NAT* by A2,A5;
then reconsider p9=p as FinSequence of NAT by FINSEQ_1:def 11;
A6: for E being set st E is MC-closed holds <*6*>^p in E
proof
let E be set;
assume
A7: E is MC-closed;
then p in E by A2,A5;
hence thesis by A7,Def6;
end;
<*6*>^p9 in NAT* by FINSEQ_1:def 11;
hence thesis by A2,A6;
end;
then
A8: E0 is with_modal_operator;
for n being Element of NAT holds <* 5+2*n *> in E0
proof
let n be Element of NAT;
set p = 5+2*n;
reconsider h = <*p*> as FinSequence of NAT;
A9: h in NAT* by FINSEQ_1:def 11;
for E being set st E is MC-closed holds <*p*> in E by Def5;
hence thesis by A2,A9;
end;
then
A10: E0 is with_int_propositional_variables;
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
A11: p in E0 and
A12: q in E0;
A13: q in NAT* by A2,A12;
A14: for E being set st E is MC-closed holds <*3*>^p^q in E
proof
let E be set;
assume
A15: E is MC-closed;
then
A16: q in E by A2,A12;
p in E by A2,A11,A15;
hence thesis by A15,A16,Def4;
end;
p in NAT* by A2,A11;
then reconsider p9=p, q9=q as FinSequence of NAT by A13,FINSEQ_1:def 11;
<*3*>^p9^q9 in NAT* by FINSEQ_1:def 11;
hence thesis by A2,A14;
end;
then
A17: E0 is with_int_disjunction;
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
A18: p in E0 and
A19: q in E0;
A20: q in NAT* by A2,A19;
A21: for E being set st E is MC-closed holds <*2*>^p^q in E
proof
let E be set;
assume
A22: E is MC-closed;
then
A23: q in E by A2,A19;
p in E by A2,A18,A22;
hence thesis by A22,A23,Def3;
end;
p in NAT* by A2,A18;
then reconsider p9=p, q9=q as FinSequence of NAT by A20,FINSEQ_1:def 11;
<*2*>^p9^q9 in NAT* by FINSEQ_1:def 11;
hence thesis by A2,A21;
end;
then
A24: E0 is with_int_conjunction;
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
A25: p in E0 and
A26: q in E0;
A27: q in NAT* by A2,A26;
A28: for E being set st E is MC-closed holds <*1*>^p^q in E
proof
let E be set;
assume
A29: E is MC-closed;
then
A30: q in E by A2,A26;
p in E by A2,A25,A29;
hence thesis by A29,A30,Def2;
end;
p in NAT* by A2,A25;
then reconsider p9=p, q9=q as FinSequence of NAT by A27,FINSEQ_1:def 11;
<*1*>^p9^q9 in NAT* by FINSEQ_1:def 11;
hence thesis by A2,A28;
end;
then
A31: E0 is with_int_implication;
<*0*> in E0 by A2,A1,A3;
then E0 is with_FALSUM;
hence E0 is MC-closed by A4,A10,A31,A24,A17,A8;
let E be set such that
A32: E is MC-closed;
let x be object;
assume x in E0;
hence thesis by A2,A32;
end;
uniqueness
proof
let E1, E2 be set such that
A33: E1 is MC-closed and
A34: for E being set st E is MC-closed holds E1 c= E and
A35: E2 is MC-closed and
A36: for E being set st E is MC-closed holds E2 c= E;
A37: E2 c= E1 by A33,A36;
E1 c= E2 by A34,A35;
hence thesis by A37,XBOOLE_0:def 10;
end;
end;
registration
cluster MC-wff -> MC-closed;
coherence by Def8;
end;
registration
cluster MC-closed non empty for set;
existence
proof
take MC-wff;
thus thesis;
end;
end;
registration
cluster MC-wff -> functional;
coherence
proof
MC-wff c= NAT* by Def7;
hence thesis;
end;
end;
registration
cluster -> FinSequence-like for Element of MC-wff;
coherence
proof
let p be Element of MC-wff;
MC-wff c= NAT* by Def7;
hence thesis;
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[object] 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 object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0:
sch 1;
Y c= MC-wff
by A1;
then reconsider Z = Y as Subset of MC-wff;
take Z;
thus thesis 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 object holds a in Y iff a in Z
proof
let a be object;
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 thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func IPC-Taut -> Subset of MC-wff equals
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
(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;
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;
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;
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;
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;
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;
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;
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;
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;
hence thesis by Def15;
end;
theorem Th10:
p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X)
proof
assume that
A1: p in CnIPC(X) and
A2: p => q in CnIPC(X);
T is IPC_theory & X c= T implies q in T
proof
assume that
A3: T is IPC_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def15;
p in T by A1,A3,A4,Def15;
hence thesis by A3,A5;
end;
hence thesis by Def15;
end;
theorem Th11:
T is IPC_theory & X c= T implies CnIPC(X) c= T
by Def15;
theorem Th12:
X c= CnIPC(X)
proof
let a be object;
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 thesis 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 object;
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;
hence thesis by A2,A3,Def15;
end;
hence thesis by Def15;
end;
end;
Lm2: CnIPC(CnIPC(X)) c= CnIPC(X)
proof
let a be object;
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 thesis by A1,A2,Def15;
end;
hence thesis by Def15;
end;
theorem
CnIPC(CnIPC(X)) = CnIPC(X)
proof
A1: CnIPC(X) c= CnIPC(CnIPC(X)) by Th12;
CnIPC(CnIPC(X)) c= CnIPC(X) by Lm2;
hence thesis by A1,XBOOLE_0:def 10;
end;
Lm3: CnIPC(X) is IPC_theory
by Th1,Th2,Th3,Th4,Th5,Th6,Th7,Th8,Th9,Th10;
registration
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: CnIPC(T) c= T
by A1,Def15;
T c= CnIPC(T) by Th12;
hence CnIPC(T) = T by A2,XBOOLE_0:def 10;
end;
thus thesis;
end;
theorem
T is IPC_theory implies IPC-Taut c= T
proof
assume
A1: T is IPC_theory;
IPC-Taut c= CnIPC(T) by Th13,XBOOLE_1:2;
hence thesis by A1,Th15;
end;
registration
cluster IPC-Taut -> IPC_theory;
coherence;
end;
begin :: Formulas provable in IPC : implication
theorem Th17:
p => p in IPC-Taut
proof
A1: p => (p => p) in IPC-Taut by Def14;
A2: p => ((p => p) => p) in IPC-Taut by Def14;
(p => ((p => p) => p)) => ((p => (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
IVERUM in IPC-Taut by Def14;
theorem
(p => q) => (p => p) in IPC-Taut by Th17,Th18;
theorem
(q => p) => (p => p) in IPC-Taut by Th17,Th18;
theorem Th22:
(q => r) => ((p => q) => (p => r)) in IPC-Taut
proof
A1: ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;
A2: ( (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;
((p => (q => r)) => ((p => q) => (p => r))) => ( (q => r) => ((p => (q
=> r)) => ((p => q) => (p => r)))) in IPC-Taut by Def14;
then ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut
by A1,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;
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in
IPC-Taut by Th22;
(p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then ((p => q) => (p => r)) in IPC-Taut by A1,Def14;
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 thesis 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 thesis 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))) in IPC-Taut by Lm4;
((((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;
hence thesis by A1,Def14;
end;
theorem
((p => q) => r) => (q => r) in IPC-Taut
proof
A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut by Th24;
q => (p => q) in IPC-Taut by Def14;
hence thesis by A1,Def14;
end;
theorem Th29: :: Contraposition
(p => (q => r)) => (q => (p => r)) in IPC-Taut
proof
A1: q => (p => q) in IPC-Taut by Def14;
(p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then
A2: (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 (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut by
A2,Def14;
then (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A1,Def14;
hence thesis by Th23;
end;
theorem Th30: :: A Hilbert axiom
(p => (p => q)) => (p => q) in IPC-Taut
proof
(p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14;
then
A1: (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23;
p => p in IPC-Taut by Th17;
hence thesis by A1,Def14;
end;
theorem :: Modus ponendo ponens
q => ((q => p) => p) in IPC-Taut
proof
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29;
(q => p) => (q => p) in IPC-Taut by Th17;
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 that
A1: s => (q => p) in IPC-Taut and
A2: 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 A2,Def14;
end;
begin :: Formulas provable in IPC : conjunction
theorem Th33:
p => (p '&' p) in IPC-Taut
proof
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30;
p => (p => (p '&' p)) in IPC-Taut by Def14;
hence thesis by A1,Def14;
end;
theorem Th34:
(p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut
proof
hereby
A1: (p '&' q) => q in IPC-Taut by Def14;
assume
A2: p '&' q in IPC-Taut;
(p '&' q) => p in IPC-Taut by Def14;
hence p in IPC-Taut & q in IPC-Taut by A2,A1,Def14;
end;
assume that
A3: p in IPC-Taut and
A4: q in IPC-Taut;
p => (q => (p '&' q)) in IPC-Taut by Def14;
then q => (p '&' q) in IPC-Taut by A3,Def14;
hence thesis by A4,Def14;
end;
theorem
(p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut
proof
hereby
assume
A1: p '&' q in IPC-Taut;
then
A2: q in IPC-Taut by Th34;
p in IPC-Taut by A1,Th34;
hence q '&' p in IPC-Taut by A2,Th34;
end;
assume
A3: q '&' p in IPC-Taut;
then
A4: p in IPC-Taut by Th34;
q in IPC-Taut by A3,Th34;
hence thesis by A4,Th34;
end;
theorem Th36:
(( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut
proof
set qp = ( q => ( p '&' q ));
set pr = (( p '&' q ) => r) => ( q => r );
A1: ( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) in IPC-Taut by Def14;
A2: p => ( q => ( p '&' q )) in IPC-Taut by Def14;
p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r ))) in
IPC-Taut by Th18,Th24;
then ( ( p => qp ) => ( p => pr )) in IPC-Taut by A1,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) => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut by
Th24;
( p '&' q ) => q in IPC-Taut by Def14;
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;
A3: ( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by
Th29;
p => (( q => r ) => (( p '&' q ) => r )) => ((p => ( q => r )) => ( p =>
(( p '&' q ) => r ))) in IPC-Taut by Def14;
then (p => ( q => r )) => ( p => (( p '&' q ) => r )) in IPC-Taut by A2,Def14
;
then
A4: (p => ( q => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by A3,Th26;
A5: ( p '&' q ) => p in IPC-Taut by Def14;
((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q ) => r
)) 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
A1: ( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q ))) in
IPC-Taut by Def14;
p => ( q => ( p '&' q )) in IPC-Taut by Def14;
then
A2: 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 ( r => p ) => ( r => ( q => ( p '&' q ))) in IPC-Taut by A2,Def14;
hence thesis by A1,Th26;
end;
theorem Th39:
( (p => q) '&' p ) => q in IPC-Taut
proof
set P = p => q;
A1: P => P in IPC-Taut by Th17;
( P => P ) => (( P '&' p ) => q ) in IPC-Taut by Th37;
hence thesis by A1,Def14;
end;
theorem
(( (p => q) '&' p ) '&' s ) => q in IPC-Taut
proof
set P = (p => q) '&' p;
A1: P => q in IPC-Taut by Th39;
(P '&' s) => P in IPC-Taut by Def14;
hence thesis by A1,Th26;
end;
theorem
(q => s) => (( p '&' q ) => s) in IPC-Taut
proof
set P = p '&' q;
A1: P => q in IPC-Taut by Def14;
(P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
hence thesis by A1,Def14;
end;
theorem Th42:
(q => s) => (( q '&' p ) => s) in IPC-Taut
proof
set P = q '&' p;
A1: P => q in IPC-Taut by Def14;
(P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
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 => q ) => (( P => s ) => ( P => ( q '&' s ))) in IPC-Taut by Th38;
P => s in IPC-Taut by Def14;
hence thesis by A1,Th32;
end;
theorem Th44:
( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
A1: ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43;
(p => q) => (( p '&' s ) => q) in IPC-Taut by Th42;
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) in IPC-Taut by Th44;
( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
hence thesis by A1,Def14;
end;
theorem Th46:
( p '&' q ) => ( q '&' p ) in IPC-Taut
proof
set P = p '&' q;
A1: P => q in IPC-Taut by Def14;
A2: P => p in IPC-Taut by Def14;
( P => q ) => (( P => p ) => ( P => ( q '&' p ))) in IPC-Taut by Th38;
then ( P => p ) => ( P => ( q '&' p )) in IPC-Taut by A1,Def14;
hence thesis by A2,Def14;
end;
theorem Th47:
( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut
proof
A1: ( q '&' s ) => ( s '&' q ) in IPC-Taut by Th46;
( p => q ) '&' ( p '&' s ) => ( q '&' s ) in IPC-Taut by Th45;
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 in IPC-Taut by Th47;
(( P '&' Q ) => S ) => ( P => ( Q => S )) in IPC-Taut by Th36;
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) in IPC-Taut by Th48;
A2: T => Q in IPC-Taut by Th46;
(P => (Q => S)) => ((T => Q) => (P => (T => S))) in IPC-Taut by Th27;
then (T => Q) => (P => (T => S)) in IPC-Taut by A1,Def14;
hence thesis by A2,Def14;
end;
theorem
( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut
proof
set P = s '&' q, Q = q '&' s;
A1: P => Q in IPC-Taut by Th46;
( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
hence thesis by A1,Def14;
end;
theorem
( ( 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) in IPC-Taut by Th38;
( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
hence thesis by A1,Def14;
end;
Lm5: ( (p '&' q) '&' s ) => q in IPC-Taut
proof
A1: (p '&' q) => q in IPC-Taut by Def14;
((p '&' q) '&' s) => (p '&' 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 in IPC-Taut by Lm5;
( P => q ) => (( P '&' P ) => ( P '&' q )) in IPC-Taut by Th49;
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 ) '&' q
in IPC-Taut by Lm6;
( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) in
IPC-Taut by Th33;
hence thesis by A1,Th26;
end;
Lm8: (p '&' q) '&' s => (p '&' s) in IPC-Taut
proof
set P = p '&' q;
A1: P => p in IPC-Taut by Def14;
( P => p ) => ((P '&' s) => (p '&' s)) in IPC-Taut by Th44;
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 in IPC-Taut by Lm8;
( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
hence thesis by A1,Def14;
end;
Lm10: (p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut
proof
A1: (p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut by Lm9;
(p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut by Lm7;
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 in IPC-Taut by Th46;
( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
hence thesis by A1,Def14;
end;
Lm12: (p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut
proof
A1: (p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut by Lm11;
(p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut by Lm10;
hence thesis by A1,Th26;
end;
Lm13: (p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut
proof
A1: (s '&' p) '&' q => (s '&' q) '&' p in IPC-Taut by Lm10;
(p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut by Lm12;
hence thesis by A1,Th26;
end;
Lm14: (p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut
proof
A1: (s '&' q) '&' p => p '&' (s '&' q) in IPC-Taut by Th46;
(p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut by Lm13;
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: s '&' q => q '&' s in IPC-Taut by Th46;
( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
hence thesis by A1,Def14;
end;
theorem
(p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut
proof
A1: p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut by Lm15;
(p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut by Lm14;
hence thesis by A1,Th26;
end;
Lm16: p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut
proof
A1: p '&' (s '&' q) => (s '&' q) '&' p in IPC-Taut by Th46;
p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm15;
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: s '&' q => q '&' s in IPC-Taut by Th46;
( P => Q ) => ((P '&' p) => (Q '&' p)) in IPC-Taut by Th44;
hence thesis by A1,Def14;
end;
Lm18: p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut
proof
A1: (s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut by Lm17;
p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut by Lm16;
hence thesis by A1,Th26;
end;
Lm19: p '&' (q '&' s) => (p '&' s) '&' q in IPC-Taut
proof
A1: (q '&' s) '&' p => (p '&' s) '&' q in IPC-Taut by Lm13;
p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut by Lm18;
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: q '&' s => s '&' q in IPC-Taut by Th46;
( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
hence thesis by A1,Def14;
end;
theorem
p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut
proof
A1: p '&' (s '&' q) => (p '&' q) '&' s in IPC-Taut by Lm19;
p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm20;
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
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;
end;
case
A3: q in IPC-Taut;
q => (p 'or' q) in IPC-Taut by Def14;
hence thesis by A3,Def14;
end;
end;
hence thesis;
end;
theorem Th56:
(p 'or' q) => (q 'or' p) in IPC-Taut
proof
A1: p => (q 'or' p) in IPC-Taut by Def14;
A2: q => (q 'or' p) in IPC-Taut by Def14;
(p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)))
in IPC-Taut by Def14;
then ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by A1
,Def14;
hence thesis by A2,Def14;
end;
theorem
(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 thesis by A2,Def14;
end;
theorem Th58:
(p => q) => (p => (q 'or' s)) in IPC-Taut
proof
A1: (q => (q 'or' s)) => ((p => q) => (p => (q 'or' s))) in IPC-Taut by Th22;
q => (q 'or' s) in IPC-Taut by Def14;
hence thesis by A1,Def14;
end;
theorem Th59:
(p => q) => (p => (s 'or' q)) in IPC-Taut
proof
A1: (q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22;
q => (s 'or' q) in IPC-Taut by Def14;
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;
A1: (p => q) => (p => Q) in IPC-Taut by Th58;
(p => Q) => ((s => Q) => (P => Q)) in IPC-Taut by Def14;
then
A2: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Th23;
s => Q in IPC-Taut by Def14;
then (p => Q) => (P => Q) in IPC-Taut by A2,Def14;
hence thesis by A1,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 in IPC-Taut by Def14;
A2: (p => q) => (p => Q) in IPC-Taut by Th59;
(s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Def14;
then (p => Q) => (P => Q) in IPC-Taut by A1,Def14;
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;
A1: P => (q 'or' P) in IPC-Taut by Def14;
p => P in IPC-Taut by Def14;
then p => (q 'or' P) in IPC-Taut by A1,Th26;
then
A2: ((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
A3: ((q 'or' P) 'or' p) => (q 'or' P) in IPC-Taut by A2,Th26;
s => P in IPC-Taut by Def14;
then (q 'or' s) => (q 'or' P) in IPC-Taut by Th63;
then
A4: (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 (p 'or' Q) => ((q 'or' P) 'or' p) in IPC-Taut by A4,Th26;
hence thesis by A3,Th26;
end;
theorem
( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut
proof
A1: (s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56;
(q 'or' s) => (s 'or' q) in IPC-Taut by Th56;
then
A2: (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 (p 'or' (q 'or' s)) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26;
hence thesis by A1,Th26;
end;
theorem
( (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) => (p 'or' q) in IPC-Taut by Th56;
then
A2: (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63;
((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56;
then ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1,Th26;
then
A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26;
(s 'or' q) => (q 'or' s) in IPC-Taut by Th56;
then
A4: (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63;
(s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64;
then ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3,Th26;
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
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
T is CPC_theory implies T is IPC_theory;
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[object] 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 object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0:
sch 1;
Y c= MC-wff
by A1;
then reconsider Z = Y as Subset of MC-wff;
take Z;
thus thesis 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 object holds a in Y iff a in Z
proof
let a be object;
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 thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func CPC-Taut -> Subset of MC-wff equals
CnCPC({}(MC-wff));
correctness;
end;
theorem Th68:
CnIPC (X) c= CnCPC (X)
proof
let a be object;
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;
hence thesis 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
A1: CnIPC(X) c= CnCPC(X) by Th68;
p => (q => p) in CnIPC (X) by Th1;
hence p => (q => p) in CnCPC (X) by A1;
A2: CnIPC(X) c= CnCPC(X) by Th68;
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X) by A2;
A3: CnIPC(X) c= CnCPC(X) by Th68;
p '&' q => p in CnIPC (X) by Th3;
hence p '&' q => p in CnCPC (X) by A3;
A4: CnIPC(X) c= CnCPC(X) by Th68;
p '&' q => q in CnIPC (X) by Th4;
hence p '&' q => q in CnCPC (X) by A4;
A5: CnIPC(X) c= CnCPC(X) by Th68;
p => (q => (p '&' q)) in CnIPC (X) by Th5;
hence p => (q => (p '&' q)) in CnCPC (X) by A5;
A6: CnIPC(X) c= CnCPC(X) by Th68;
p => (p 'or' q) in CnIPC (X) by Th6;
hence p => (p 'or' q) in CnCPC (X) by A6;
A7: CnIPC(X) c= CnCPC(X) by Th68;
q => (p 'or' q) in CnIPC (X) by Th7;
hence q => (p 'or' q) in CnCPC (X) by A7;
A8: CnIPC(X) c= CnCPC(X) by Th68;
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X) by A8;
A9: CnIPC(X) c= CnCPC(X) by Th68;
FALSUM => p in CnIPC (X) by Th9;
hence FALSUM => p in CnCPC (X) by A9;
T is CPC_theory & X c= T implies p 'or' (p => FALSUM) in T;
hence p 'or' (p => FALSUM) in CnCPC (X) by Def20;
end;
theorem Th70:
p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X)
proof
assume that
A1: p in CnCPC(X) and
A2: p => q in CnCPC(X);
T is CPC_theory & X c= T implies q in T
proof
assume that
A3: T is CPC_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def20;
p in T by A1,A3,A4,Def20;
hence thesis by A3,A5;
end;
hence thesis by Def20;
end;
theorem Th71:
T is CPC_theory & X c= T implies CnCPC(X) c= T
by Def20;
theorem Th72:
X c= CnCPC(X)
proof
let a be object;
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 thesis 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 object;
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;
hence thesis by A2,A3,Def20;
end;
hence thesis by Def20;
end;
end;
Lm21: CnCPC(CnCPC(X)) c= CnCPC(X)
proof
let a be object;
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 thesis by A1,A2,Def20;
end;
hence thesis by Def20;
end;
theorem
CnCPC(CnCPC(X)) = CnCPC(X)
proof
A1: CnCPC(X) c= CnCPC(CnCPC(X)) by Th72;
CnCPC(CnCPC(X)) c= CnCPC(X) by Lm21;
hence thesis by A1,XBOOLE_0:def 10;
end;
Lm22: CnCPC(X) is CPC_theory
by Th69,Th70;
registration
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: CnCPC(T) c= T
by A1,Def20;
T c= CnCPC(T) by Th72;
hence CnCPC(T) = T by A2,XBOOLE_0:def 10;
end;
thus thesis;
end;
theorem
T is CPC_theory implies CPC-Taut c= T
proof
assume
A1: T is CPC_theory;
CPC-Taut c= CnCPC(T) by Th73,XBOOLE_1:2;
hence thesis by A1,Th75;
end;
registration
cluster CPC-Taut -> CPC_theory;
coherence;
end;
theorem
IPC-Taut c= CPC-Taut by 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
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
T is S4_theory implies T is CPC_theory;
theorem
T is S4_theory implies T is IPC_theory;
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[object] 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 object holds a in Y iff a in MC-wff & P[a] from XBOOLE_0:
sch 1;
Y c= MC-wff
by A1;
then reconsider Z = Y as Subset of MC-wff;
take Z;
thus thesis 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 object holds a in Y iff a in Z
proof
let a be object;
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 thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func S4-Taut -> Subset of MC-wff equals
CnS4({}(MC-wff));
correctness;
end;
theorem Th80:
CnCPC (X) c= CnS4 (X)
proof
let a be object;
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;
hence thesis by A1,A3,Def20;
end;
hence thesis by Def23;
end;
theorem Th81:
CnIPC (X) c= CnS4 (X)
proof
A1: CnCPC (X) c= CnS4 (X) by Th80;
CnIPC (X) c= CnCPC (X) by Th68;
hence thesis by A1;
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
A1: CnIPC (X) c= CnS4 (X) by Th81;
p => (q => p) in CnIPC (X) by Th1;
hence p => (q => p) in CnS4 (X) by A1;
A2: CnIPC (X) c= CnS4 (X) by Th81;
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X) by A2;
A3: CnIPC (X) c= CnS4 (X) by Th81;
p '&' q => p in CnIPC (X) by Th3;
hence p '&' q => p in CnS4 (X) by A3;
A4: CnIPC (X) c= CnS4 (X) by Th81;
p '&' q => q in CnIPC (X) by Th4;
hence p '&' q => q in CnS4 (X) by A4;
A5: CnIPC (X) c= CnS4 (X) by Th81;
p => (q => (p '&' q)) in CnIPC (X) by Th5;
hence p => (q => (p '&' q)) in CnS4 (X) by A5;
A6: CnIPC (X) c= CnS4 (X) by Th81;
p => (p 'or' q) in CnIPC (X) by Th6;
hence p => (p 'or' q) in CnS4 (X) by A6;
A7: CnIPC (X) c= CnS4 (X) by Th81;
q => (p 'or' q) in CnIPC (X) by Th7;
hence q => (p 'or' q) in CnS4 (X) by A7;
A8: CnIPC (X) c= CnS4 (X) by Th81;
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X) by A8;
A9: CnIPC (X) c= CnS4 (X) by Th81;
FALSUM => p in CnIPC (X) by Th9;
hence FALSUM => p in CnS4 (X) by A9;
T is S4_theory & X c= T implies p 'or' (p => FALSUM) in T;
hence p 'or' (p => FALSUM) in CnS4 (X) by Def23;
end;
theorem Th83:
p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X)
proof
assume that
A1: p in CnS4 (X) and
A2: p => q in CnS4 (X);
T is S4_theory & X c= T implies q in T
proof
assume that
A3: T is S4_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def23;
p in T by A1,A3,A4,Def23;
hence thesis by A3,A5;
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;
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;
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;
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 that
A2: T is S4_theory and
A3: X c= T;
p in T by A1,A2,A3,Def23;
hence thesis by A2;
end;
hence thesis by Def23;
end;
theorem Th88:
T is S4_theory & X c= T implies CnS4(X) c= T
by Def23;
theorem Th89:
X c= CnS4(X)
proof
let a be object;
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 thesis 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 object;
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;
hence thesis by A2,A3,Def23;
end;
hence thesis by Def23;
end;
end;
Lm23: CnS4(CnS4(X)) c= CnS4(X)
proof
let a be object;
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 thesis by A1,A2,Def23;
end;
hence thesis by Def23;
end;
theorem
CnS4(CnS4(X)) = CnS4(X)
proof
A1: CnS4(X) c= CnS4(CnS4(X)) by Th89;
CnS4(CnS4(X)) c= CnS4(X) by Lm23;
hence thesis by A1,XBOOLE_0:def 10;
end;
Lm24: CnS4(X) is S4_theory
by Th82,Th84,Th85,Th86,Th83,Th87;
registration
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: CnS4(T) c= T
by A1,Def23;
T c= CnS4(T) by Th89;
hence CnS4(T) = T by A2,XBOOLE_0:def 10;
end;
thus thesis;
end;
theorem
T is S4_theory implies S4-Taut c= T
proof
assume
A1: T is S4_theory;
S4-Taut c= CnS4(T) by Th90,XBOOLE_1:2;
hence thesis by A1,Th92;
end;
registration
cluster S4-Taut -> S4_theory;
coherence;
end;
theorem
CPC-Taut c= S4-Taut by Th80;
theorem
IPC-Taut c= S4-Taut by Th81;