:: LUKASI_1 semantic presentation
begin
theorem Th1: :: LUKASI_1:1
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => q) => ((q => r) => (p => r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p => q) => ((q => r) => (p => r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: (p => q) => ((q => r) => (p => r)) in TAUT A
(p => q) => (('not' (q '&' ('not' r))) => ('not' (p '&' ('not' r)))) in TAUT A by CQC_THE1:44;
then (p => q) => ((q => r) => ('not' (p '&' ('not' r)))) in TAUT A by QC_LANG2:def_2;
hence (p => q) => ((q => r) => (p => r)) in TAUT A by QC_LANG2:def_2; ::_thesis: verum
end;
theorem Th2: :: LUKASI_1:2
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(q => r) => (p => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A holds
(q => r) => (p => r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A implies (q => r) => (p => r) in TAUT A )
assume A1: p => q in TAUT A ; ::_thesis: (q => r) => (p => r) in TAUT A
(p => q) => ((q => r) => (p => r)) in TAUT A by Th1;
hence (q => r) => (p => r) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
theorem Th3: :: LUKASI_1:3
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q in TAUT A & q => r in TAUT A holds
p => r in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q in TAUT A & q => r in TAUT A holds
p => r in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A & q => r in TAUT A implies p => r in TAUT A )
assume that
A1: p => q in TAUT A and
A2: q => r in TAUT A ; ::_thesis: p => r in TAUT A
(p => q) => ((q => r) => (p => r)) in TAUT A by Th1;
then (q => r) => (p => r) in TAUT A by A1, CQC_THE1:46;
hence p => r in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;
theorem Th4: :: LUKASI_1:4
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p => p in TAUT A
let p be Element of CQC-WFF A; ::_thesis: p => p in TAUT A
( (('not' p) => p) => p in TAUT A & p => (('not' p) => p) in TAUT A ) by CQC_THE1:42, CQC_THE1:43;
hence p => p in TAUT A by Th3; ::_thesis: verum
end;
Lm1: for A being QC-alphabet
for q, r, p, s being Element of CQC-WFF A holds (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, r, p, s being Element of CQC-WFF A holds (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT A
let q, r, p, s be Element of CQC-WFF A; ::_thesis: (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT A
(p => q) => ((q => r) => (p => r)) in TAUT A by Th1;
hence (((q => r) => (p => r)) => s) => ((p => q) => s) in TAUT A by Th2; ::_thesis: verum
end;
Lm2: for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A holds (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A holds (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT A
let p, q, r, s be Element of CQC-WFF A; ::_thesis: (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT A
( ((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in TAUT A & (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in TAUT A ) by Lm1;
hence (p => (q => r)) => ((s => q) => (p => (s => r))) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm3: for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A holds (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A holds (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT A
let p, q, r, s be Element of CQC-WFF A; ::_thesis: (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT A
( ((q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s)) in TAUT A & (((q => r) => (p => r)) => (((p => r) => s) => ((q => r) => s))) => ((p => q) => (((p => r) => s) => ((q => r) => s))) in TAUT A ) by Lm1, Th1;
hence (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm4: for A being QC-alphabet
for t, p, r, s, q being Element of CQC-WFF A holds (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for t, p, r, s, q being Element of CQC-WFF A holds (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT A
let t, p, r, s, q be Element of CQC-WFF A; ::_thesis: (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT A
( (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT A & ((p => q) => (((p => r) => s) => ((q => r) => s))) => ((t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s)))) in TAUT A ) by Lm2, Lm3;
hence (t => ((p => r) => s)) => ((p => q) => (t => ((q => r) => s))) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm5: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((('not' p) => q) => r) => (p => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((('not' p) => q) => r) => (p => r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((('not' p) => q) => r) => (p => r) in TAUT A
p => (('not' p) => q) in TAUT A by CQC_THE1:43;
hence ((('not' p) => q) => r) => (p => r) in TAUT A by Th2; ::_thesis: verum
end;
Lm6: for A being QC-alphabet
for p, r, s, q being Element of CQC-WFF A holds p => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, r, s, q being Element of CQC-WFF A holds p => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT A
let p, r, s, q be Element of CQC-WFF A; ::_thesis: p => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT A
( (('not' p) => q) => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT A & ((('not' p) => q) => (((('not' p) => r) => s) => ((q => r) => s))) => (p => (((('not' p) => r) => s) => ((q => r) => s))) in TAUT A ) by Lm3, Lm5;
hence p => (((('not' p) => r) => s) => ((q => r) => s)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm7: for A being QC-alphabet
for q, p being Element of CQC-WFF A holds (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A holds (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT A
let q, p be Element of CQC-WFF A; ::_thesis: (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT A
( (('not' p) => p) => p in TAUT A & ((('not' p) => p) => p) => (((('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((q => ((('not' p) => p) => p)) => ((('not' p) => p) => p))) in TAUT A ) by Lm6, CQC_THE1:42;
then ( (('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT A & ((('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((q => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) in TAUT A ) by CQC_THE1:42, CQC_THE1:46;
hence (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm8: for A being QC-alphabet
for t, p being Element of CQC-WFF A holds t => ((('not' p) => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for t, p being Element of CQC-WFF A holds t => ((('not' p) => p) => p) in TAUT A
let t, p be Element of CQC-WFF A; ::_thesis: t => ((('not' p) => p) => p) in TAUT A
( (('not' t) => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT A & ((('not' t) => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => (t => ((('not' p) => p) => p)) in TAUT A ) by Lm5, Lm7;
hence t => ((('not' p) => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm9: for A being QC-alphabet
for p, q, t being Element of CQC-WFF A holds (('not' p) => q) => (t => ((q => p) => p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, t being Element of CQC-WFF A holds (('not' p) => q) => (t => ((q => p) => p)) in TAUT A
let p, q, t be Element of CQC-WFF A; ::_thesis: (('not' p) => q) => (t => ((q => p) => p)) in TAUT A
( t => ((('not' p) => p) => p) in TAUT A & (t => ((('not' p) => p) => p)) => ((('not' p) => q) => (t => ((q => p) => p))) in TAUT A ) by Lm4, Lm8;
hence (('not' p) => q) => (t => ((q => p) => p)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm10: for A being QC-alphabet
for t, q, p, r being Element of CQC-WFF A holds ((t => ((q => p) => p)) => r) => ((('not' p) => q) => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for t, q, p, r being Element of CQC-WFF A holds ((t => ((q => p) => p)) => r) => ((('not' p) => q) => r) in TAUT A
let t, q, p, r be Element of CQC-WFF A; ::_thesis: ((t => ((q => p) => p)) => r) => ((('not' p) => q) => r) in TAUT A
( (('not' p) => q) => (t => ((q => p) => p)) in TAUT A & ((('not' p) => q) => (t => ((q => p) => p))) => (((t => ((q => p) => p)) => r) => ((('not' p) => q) => r)) in TAUT A ) by Lm9, Th1;
hence ((t => ((q => p) => p)) => r) => ((('not' p) => q) => r) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm11: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => q) => ((q => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) => q) => ((q => p) => p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) => q) => ((q => p) => p) in TAUT A
( (('not' ((q => p) => p)) => ((q => p) => p)) => ((q => p) => p) in TAUT A & ((('not' ((q => p) => p)) => ((q => p) => p)) => ((q => p) => p)) => ((('not' p) => q) => ((q => p) => p)) in TAUT A ) by Lm10, CQC_THE1:42;
hence (('not' p) => q) => ((q => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm12: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => ((q => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds p => ((q => p) => p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: p => ((q => p) => p) in TAUT A
( (('not' p) => q) => ((q => p) => p) in TAUT A & ((('not' p) => q) => ((q => p) => p)) => (p => ((q => p) => p)) in TAUT A ) by Lm5, Lm11;
hence p => ((q => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th5: :: LUKASI_1:5
for A being QC-alphabet
for q, p being Element of CQC-WFF A holds q => (p => q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A holds q => (p => q) in TAUT A
let q, p be Element of CQC-WFF A; ::_thesis: q => (p => q) in TAUT A
( q => ((('not' p) => q) => q) in TAUT A & (q => ((('not' p) => q) => q)) => ((p => (('not' p) => q)) => (q => (p => q))) in TAUT A ) by Lm2, Lm12;
then ( p => (('not' p) => q) in TAUT A & (p => (('not' p) => q)) => (q => (p => q)) in TAUT A ) by CQC_THE1:43, CQC_THE1:46;
hence q => (p => q) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th6: :: LUKASI_1:6
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p => q) => r) => (q => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p => q) => r) => (q => r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p => q) => r) => (q => r) in TAUT A
( q => (p => q) in TAUT A & (q => (p => q)) => (((p => q) => r) => (q => r)) in TAUT A ) by Th1, Th5;
hence ((p => q) => r) => (q => r) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th7: :: LUKASI_1:7
for A being QC-alphabet
for q, p being Element of CQC-WFF A holds q => ((q => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A holds q => ((q => p) => p) in TAUT A
let q, p be Element of CQC-WFF A; ::_thesis: q => ((q => p) => p) in TAUT A
( (('not' p) => q) => ((q => p) => p) in TAUT A & ((('not' p) => q) => ((q => p) => p)) => (q => ((q => p) => p)) in TAUT A ) by Lm11, Th6;
hence q => ((q => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th8: :: LUKASI_1:8
for A being QC-alphabet
for s, q, p being Element of CQC-WFF A holds (s => (q => p)) => (q => (s => p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for s, q, p being Element of CQC-WFF A holds (s => (q => p)) => (q => (s => p)) in TAUT A
let s, q, p be Element of CQC-WFF A; ::_thesis: (s => (q => p)) => (q => (s => p)) in TAUT A
( q => ((q => p) => p) in TAUT A & (q => ((q => p) => p)) => ((s => (q => p)) => (q => (s => p))) in TAUT A ) by Lm2, Th7;
hence (s => (q => p)) => (q => (s => p)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th9: :: LUKASI_1:9
for A being QC-alphabet
for q, r, p being Element of CQC-WFF A holds (q => r) => ((p => q) => (p => r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, r, p being Element of CQC-WFF A holds (q => r) => ((p => q) => (p => r)) in TAUT A
let q, r, p be Element of CQC-WFF A; ::_thesis: (q => r) => ((p => q) => (p => r)) in TAUT A
( (p => q) => ((q => r) => (p => r)) in TAUT A & ((p => q) => ((q => r) => (p => r))) => ((q => r) => ((p => q) => (p => r))) in TAUT A ) by Th1, Th8;
hence (q => r) => ((p => q) => (p => r)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm13: for A being QC-alphabet
for q, s, p, r being Element of CQC-WFF A holds ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, s, p, r being Element of CQC-WFF A holds ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT A
let q, s, p, r be Element of CQC-WFF A; ::_thesis: ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT A
( (s => (q => p)) => (q => (s => p)) in TAUT A & ((s => (q => p)) => (q => (s => p))) => (((q => (s => p)) => r) => ((s => (q => p)) => r)) in TAUT A ) by Th1, Th8;
hence ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm14: for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ((p => q) => p) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ((p => q) => p) => p in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ((p => q) => p) => p in TAUT A
( (('not' p) => (p => q)) => (((p => q) => p) => p) in TAUT A & ((('not' p) => (p => q)) => (((p => q) => p) => p)) => ((p => (('not' p) => q)) => (((p => q) => p) => p)) in TAUT A ) by Lm11, Lm13;
then ( p => (('not' p) => q) in TAUT A & (p => (('not' p) => q)) => (((p => q) => p) => p) in TAUT A ) by CQC_THE1:43, CQC_THE1:46;
hence ((p => q) => p) => p in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm15: for A being QC-alphabet
for p, r, s, q being Element of CQC-WFF A holds ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, r, s, q being Element of CQC-WFF A holds ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT A
let p, r, s, q be Element of CQC-WFF A; ::_thesis: ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT A
( (p => q) => (((p => r) => s) => ((q => r) => s)) in TAUT A & ((p => q) => (((p => r) => s) => ((q => r) => s))) => (((p => r) => s) => ((p => q) => ((q => r) => s))) in TAUT A ) by Lm3, Th8;
hence ((p => r) => s) => ((p => q) => ((q => r) => s)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm16: for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds ((p => q) => r) => ((r => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds ((p => q) => r) => ((r => p) => p) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ((p => q) => r) => ((r => p) => p) in TAUT A
( ((p => q) => p) => p in TAUT A & (((p => q) => p) => p) => (((p => q) => r) => ((r => p) => p)) in TAUT A ) by Lm14, Lm15;
hence ((p => q) => r) => ((r => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm17: for A being QC-alphabet
for r, p, s, q being Element of CQC-WFF A holds (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for r, p, s, q being Element of CQC-WFF A holds (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT A
let r, p, s, q be Element of CQC-WFF A; ::_thesis: (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT A
( ((p => q) => r) => ((r => p) => p) in TAUT A & (((p => q) => r) => ((r => p) => p)) => ((((r => p) => p) => s) => (((p => q) => r) => s)) in TAUT A ) by Lm16, Th1;
hence (((r => p) => p) => s) => (((p => q) => r) => s) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm18: for A being QC-alphabet
for q, r, p being Element of CQC-WFF A holds ((q => r) => p) => ((q => p) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, r, p being Element of CQC-WFF A holds ((q => r) => p) => ((q => p) => p) in TAUT A
let q, r, p be Element of CQC-WFF A; ::_thesis: ((q => r) => p) => ((q => p) => p) in TAUT A
( ((p => q) => q) => ((q => p) => p) in TAUT A & (((p => q) => q) => ((q => p) => p)) => (((q => r) => p) => ((q => p) => p)) in TAUT A ) by Lm16, Lm17;
hence ((q => r) => p) => ((q => p) => p) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th10: :: LUKASI_1:10
for A being QC-alphabet
for q, r being Element of CQC-WFF A holds (q => (q => r)) => (q => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, r being Element of CQC-WFF A holds (q => (q => r)) => (q => r) in TAUT A
let q, r be Element of CQC-WFF A; ::_thesis: (q => (q => r)) => (q => r) in TAUT A
( (q => r) => (q => r) in TAUT A & ((q => r) => (q => r)) => ((q => (q => r)) => (q => r)) in TAUT A ) by Lm18, Th4;
hence (q => (q => r)) => (q => r) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm19: for A being QC-alphabet
for q, s, r, p being Element of CQC-WFF A holds (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, s, r, p being Element of CQC-WFF A holds (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT A
let q, s, r, p be Element of CQC-WFF A; ::_thesis: (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT A
( ((q => r) => p) => ((q => p) => p) in TAUT A & (((q => r) => p) => ((q => p) => p)) => ((q => s) => (((q => r) => p) => ((s => p) => p))) in TAUT A ) by Lm4, Lm18;
hence (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm20: for A being QC-alphabet
for q, r, p, s being Element of CQC-WFF A holds ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, r, p, s being Element of CQC-WFF A holds ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT A
let q, r, p, s be Element of CQC-WFF A; ::_thesis: ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT A
( (q => s) => (((q => r) => p) => ((s => p) => p)) in TAUT A & ((q => s) => (((q => r) => p) => ((s => p) => p))) => (((q => r) => p) => ((q => s) => ((s => p) => p))) in TAUT A ) by Lm19, Th8;
hence ((q => r) => p) => ((q => s) => ((s => p) => p)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm21: for A being QC-alphabet
for q, s, p, r being Element of CQC-WFF A holds (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, s, p, r being Element of CQC-WFF A holds (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT A
let q, s, p, r be Element of CQC-WFF A; ::_thesis: (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT A
( (q => r) => (p => (q => r)) in TAUT A & ((q => r) => (p => (q => r))) => ((q => s) => ((s => (p => (q => r))) => (p => (q => r)))) in TAUT A ) by Lm20, Th5;
hence (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
Lm22: for A being QC-alphabet
for s, p, q, r being Element of CQC-WFF A holds (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for s, p, q, r being Element of CQC-WFF A holds (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT A
let s, p, q, r be Element of CQC-WFF A; ::_thesis: (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT A
( (q => s) => ((s => (p => (q => r))) => (p => (q => r))) in TAUT A & ((q => s) => ((s => (p => (q => r))) => (p => (q => r)))) => ((s => (p => (q => r))) => ((q => s) => (p => (q => r)))) in TAUT A ) by Lm21, Th8;
hence (s => (p => (q => r))) => ((q => s) => (p => (q => r))) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th11: :: LUKASI_1:11
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p => q) => (p => r)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p => q) => (p => r)) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in TAUT A
( (q => r) => ((p => q) => (p => r)) in TAUT A & ((q => r) => ((p => q) => (p => r))) => ((p => (q => r)) => ((p => q) => (p => r))) in TAUT A ) by Lm22, Th9;
hence (p => (q => r)) => ((p => q) => (p => r)) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th12: :: LUKASI_1:12
for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' (VERUM A)) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds ('not' (VERUM A)) => p in TAUT A
let p be Element of CQC-WFF A; ::_thesis: ('not' (VERUM A)) => p in TAUT A
(VERUM A) => (('not' (VERUM A)) => p) in TAUT A by CQC_THE1:43;
hence ('not' (VERUM A)) => p in TAUT A by CQC_THE1:41, CQC_THE1:46; ::_thesis: verum
end;
theorem Th13: :: LUKASI_1:13
for A being QC-alphabet
for q, p being Element of CQC-WFF A st q in TAUT A holds
p => q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, p being Element of CQC-WFF A st q in TAUT A holds
p => q in TAUT A
let q, p be Element of CQC-WFF A; ::_thesis: ( q in TAUT A implies p => q in TAUT A )
q => (p => q) in TAUT A by Th5;
hence ( q in TAUT A implies p => q in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:14
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p in TAUT A holds
(p => q) => q in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p in TAUT A holds
(p => q) => q in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p in TAUT A implies (p => q) => q in TAUT A )
assume A1: p in TAUT A ; ::_thesis: (p => q) => q in TAUT A
p => ((p => q) => q) in TAUT A by Th7;
hence (p => q) => q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
theorem Th15: :: LUKASI_1:15
for A being QC-alphabet
for s, q, p being Element of CQC-WFF A st s => (q => p) in TAUT A holds
q => (s => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for s, q, p being Element of CQC-WFF A st s => (q => p) in TAUT A holds
q => (s => p) in TAUT A
let s, q, p be Element of CQC-WFF A; ::_thesis: ( s => (q => p) in TAUT A implies q => (s => p) in TAUT A )
assume A1: s => (q => p) in TAUT A ; ::_thesis: q => (s => p) in TAUT A
(s => (q => p)) => (q => (s => p)) in TAUT A by Th8;
hence q => (s => p) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
theorem Th16: :: LUKASI_1:16
for A being QC-alphabet
for s, q, p being Element of CQC-WFF A st s => (q => p) in TAUT A & q in TAUT A holds
s => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for s, q, p being Element of CQC-WFF A st s => (q => p) in TAUT A & q in TAUT A holds
s => p in TAUT A
let s, q, p be Element of CQC-WFF A; ::_thesis: ( s => (q => p) in TAUT A & q in TAUT A implies s => p in TAUT A )
assume s => (q => p) in TAUT A ; ::_thesis: ( not q in TAUT A or s => p in TAUT A )
then q => (s => p) in TAUT A by Th15;
hence ( not q in TAUT A or s => p in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:17
for A being QC-alphabet
for s, q, p being Element of CQC-WFF A st s => (q => p) in TAUT A & q in TAUT A & s in TAUT A holds
p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for s, q, p being Element of CQC-WFF A st s => (q => p) in TAUT A & q in TAUT A & s in TAUT A holds
p in TAUT A
let s, q, p be Element of CQC-WFF A; ::_thesis: ( s => (q => p) in TAUT A & q in TAUT A & s in TAUT A implies p in TAUT A )
assume ( s => (q => p) in TAUT A & q in TAUT A ) ; ::_thesis: ( not s in TAUT A or p in TAUT A )
then s => p in TAUT A by Th16;
hence ( not s in TAUT A or p in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:18
for A being QC-alphabet
for q, r being Element of CQC-WFF A st q => (q => r) in TAUT A holds
q => r in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for q, r being Element of CQC-WFF A st q => (q => r) in TAUT A holds
q => r in TAUT A
let q, r be Element of CQC-WFF A; ::_thesis: ( q => (q => r) in TAUT A implies q => r in TAUT A )
(q => (q => r)) => (q => r) in TAUT A by Th10;
hence ( q => (q => r) in TAUT A implies q => r in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem Th19: :: LUKASI_1:19
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A holds
(p => q) => (p => r) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A holds
(p => q) => (p => r) in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) in TAUT A implies (p => q) => (p => r) in TAUT A )
assume A1: p => (q => r) in TAUT A ; ::_thesis: (p => q) => (p => r) in TAUT A
(p => (q => r)) => ((p => q) => (p => r)) in TAUT A by Th11;
hence (p => q) => (p => r) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
theorem Th20: :: LUKASI_1:20
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A & p => q in TAUT A holds
p => r in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A & p => q in TAUT A holds
p => r in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) in TAUT A & p => q in TAUT A implies p => r in TAUT A )
assume p => (q => r) in TAUT A ; ::_thesis: ( not p => q in TAUT A or p => r in TAUT A )
then (p => q) => (p => r) in TAUT A by Th19;
hence ( not p => q in TAUT A or p => r in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:21
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A & p => q in TAUT A & p in TAUT A holds
r in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) in TAUT A & p => q in TAUT A & p in TAUT A holds
r in TAUT A
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) in TAUT A & p => q in TAUT A & p in TAUT A implies r in TAUT A )
assume ( p => (q => r) in TAUT A & p => q in TAUT A ) ; ::_thesis: ( not p in TAUT A or r in TAUT A )
then p => r in TAUT A by Th20;
hence ( not p in TAUT A or r in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem Th22: :: LUKASI_1:22
for A being QC-alphabet
for p, q, r, s being Element of CQC-WFF A st p => (q => r) in TAUT A & p => (r => s) in TAUT A holds
p => (q => s) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q, r, s being Element of CQC-WFF A st p => (q => r) in TAUT A & p => (r => s) in TAUT A holds
p => (q => s) in TAUT A
let p, q, r, s be Element of CQC-WFF A; ::_thesis: ( p => (q => r) in TAUT A & p => (r => s) in TAUT A implies p => (q => s) in TAUT A )
assume that
A1: p => (q => r) in TAUT A and
A2: p => (r => s) in TAUT A ; ::_thesis: p => (q => s) in TAUT A
p => ((q => r) => ((r => s) => (q => s))) in TAUT A by Th1, Th13;
then p => ((r => s) => (q => s)) in TAUT A by A1, Th20;
hence p => (q => s) in TAUT A by A2, Th20; ::_thesis: verum
end;
theorem :: LUKASI_1:23
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => (VERUM A) in TAUT A by Th13, CQC_THE1:41;
Lm23: for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' p) => (p => ('not' (VERUM A))) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds ('not' p) => (p => ('not' (VERUM A))) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: ('not' p) => (p => ('not' (VERUM A))) in TAUT A
p => (('not' p) => ('not' (VERUM A))) in TAUT A by CQC_THE1:43;
hence ('not' p) => (p => ('not' (VERUM A))) in TAUT A by Th15; ::_thesis: verum
end;
Lm24: for A being QC-alphabet
for p being Element of CQC-WFF A holds (('not' p) => ('not' (VERUM A))) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds (('not' p) => ('not' (VERUM A))) => p in TAUT A
let p be Element of CQC-WFF A; ::_thesis: (('not' p) => ('not' (VERUM A))) => p in TAUT A
( ('not' p) => (('not' (VERUM A)) => p) in TAUT A & (('not' p) => (('not' (VERUM A)) => p)) => ((('not' p) => ('not' (VERUM A))) => (('not' p) => p)) in TAUT A ) by Th11, Th12, Th13;
then A1: (('not' p) => ('not' (VERUM A))) => (('not' p) => p) in TAUT A by CQC_THE1:46;
(('not' p) => p) => p in TAUT A by CQC_THE1:42;
hence (('not' p) => ('not' (VERUM A))) => p in TAUT A by A1, Th3; ::_thesis: verum
end;
theorem Th24: :: LUKASI_1:24
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => ('not' q)) => (q => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) => ('not' q)) => (q => p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) => ('not' q)) => (q => p) in TAUT A
( q => (('not' q) => ('not' (VERUM A))) in TAUT A & (('not' q) => ('not' (VERUM A))) => ((('not' p) => ('not' q)) => (('not' p) => ('not' (VERUM A)))) in TAUT A ) by Th9, CQC_THE1:43;
then A1: q => ((('not' p) => ('not' q)) => (('not' p) => ('not' (VERUM A)))) in TAUT A by Th3;
q => ((('not' p) => ('not' (VERUM A))) => p) in TAUT A by Lm24, Th13;
then q => ((('not' p) => ('not' q)) => p) in TAUT A by A1, Th22;
hence (('not' p) => ('not' q)) => (q => p) in TAUT A by Th15; ::_thesis: verum
end;
theorem Th25: :: LUKASI_1:25
for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' ('not' p)) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds ('not' ('not' p)) => p in TAUT A
let p be Element of CQC-WFF A; ::_thesis: ('not' ('not' p)) => p in TAUT A
( ('not' ('not' p)) => (('not' p) => ('not' (VERUM A))) in TAUT A & (('not' p) => ('not' (VERUM A))) => ((VERUM A) => p) in TAUT A ) by Lm23, Th24;
then ('not' ('not' p)) => ((VERUM A) => p) in TAUT A by Th3;
then (VERUM A) => (('not' ('not' p)) => p) in TAUT A by Th15;
hence ('not' ('not' p)) => p in TAUT A by CQC_THE1:41, CQC_THE1:46; ::_thesis: verum
end;
Lm25: now__::_thesis:_for_A_being_QC-alphabet_
for_p_being_Element_of_CQC-WFF_A_holds_(p_=>_('not'_(VERUM_A)))_=>_('not'_p)_in_TAUT_A
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds (p => ('not' (VERUM A))) => ('not' p) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: (p => ('not' (VERUM A))) => ('not' p) in TAUT A
('not' ('not' p)) => p in TAUT A by Th25;
then A1: (p => ('not' (VERUM A))) => (('not' ('not' p)) => ('not' (VERUM A))) in TAUT A by Th2;
(('not' ('not' p)) => ('not' (VERUM A))) => ('not' p) in TAUT A by Lm24;
hence (p => ('not' (VERUM A))) => ('not' p) in TAUT A by A1, Th3; ::_thesis: verum
end;
theorem Th26: :: LUKASI_1:26
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => q) => (('not' q) => ('not' p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => q) => (('not' q) => ('not' p)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p => q) => (('not' q) => ('not' p)) in TAUT A
( ('not' q) => (q => ('not' (VERUM A))) in TAUT A & (q => ('not' (VERUM A))) => ((p => q) => (p => ('not' (VERUM A)))) in TAUT A ) by Lm23, Th9;
then A1: ('not' q) => ((p => q) => (p => ('not' (VERUM A)))) in TAUT A by Th3;
('not' q) => ((p => ('not' (VERUM A))) => ('not' p)) in TAUT A by Lm25, Th13;
then ('not' q) => ((p => q) => ('not' p)) in TAUT A by A1, Th22;
hence (p => q) => (('not' q) => ('not' p)) in TAUT A by Th15; ::_thesis: verum
end;
theorem Th27: :: LUKASI_1:27
for A being QC-alphabet
for p being Element of CQC-WFF A holds p => ('not' ('not' p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds p => ('not' ('not' p)) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: p => ('not' ('not' p)) in TAUT A
( ((VERUM A) => p) => (('not' p) => ('not' (VERUM A))) in TAUT A & (('not' p) => ('not' (VERUM A))) => ('not' ('not' p)) in TAUT A ) by Lm25, Th26;
then A1: ((VERUM A) => p) => ('not' ('not' p)) in TAUT A by Th3;
p => ((VERUM A) => p) in TAUT A by Th5;
hence p => ('not' ('not' p)) in TAUT A by A1, Th3; ::_thesis: verum
end;
theorem Th28: :: LUKASI_1:28
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (('not' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => q) in TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( (('not' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => q) in TAUT A )
let p, q be Element of CQC-WFF A; ::_thesis: ( (('not' ('not' p)) => q) => (p => q) in TAUT A & (p => q) => (('not' ('not' p)) => q) in TAUT A )
p => ('not' ('not' p)) in TAUT A by Th27;
hence (('not' ('not' p)) => q) => (p => q) in TAUT A by Th2; ::_thesis: (p => q) => (('not' ('not' p)) => q) in TAUT A
('not' ('not' p)) => p in TAUT A by Th25;
hence (p => q) => (('not' ('not' p)) => q) in TAUT A by Th2; ::_thesis: verum
end;
theorem Th29: :: LUKASI_1:29
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( (p => ('not' ('not' q))) => (p => q) in TAUT A & (p => q) => (p => ('not' ('not' q))) in TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( (p => ('not' ('not' q))) => (p => q) in TAUT A & (p => q) => (p => ('not' ('not' q))) in TAUT A )
let p, q be Element of CQC-WFF A; ::_thesis: ( (p => ('not' ('not' q))) => (p => q) in TAUT A & (p => q) => (p => ('not' ('not' q))) in TAUT A )
( (p => (('not' ('not' q)) => q)) => ((p => ('not' ('not' q))) => (p => q)) in TAUT A & p => (('not' ('not' q)) => q) in TAUT A ) by Th11, Th13, Th25;
hence (p => ('not' ('not' q))) => (p => q) in TAUT A by CQC_THE1:46; ::_thesis: (p => q) => (p => ('not' ('not' q))) in TAUT A
( (p => (q => ('not' ('not' q)))) => ((p => q) => (p => ('not' ('not' q)))) in TAUT A & p => (q => ('not' ('not' q))) in TAUT A ) by Th11, Th13, Th27;
hence (p => q) => (p => ('not' ('not' q))) in TAUT A by CQC_THE1:46; ::_thesis: verum
end;
theorem Th30: :: LUKASI_1:30
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (p => ('not' q)) => (q => ('not' p)) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (p => ('not' q)) => (q => ('not' p)) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (p => ('not' q)) => (q => ('not' p)) in TAUT A
( (p => ('not' q)) => (('not' ('not' q)) => ('not' p)) in TAUT A & (('not' ('not' q)) => ('not' p)) => (q => ('not' p)) in TAUT A ) by Th26, Th28;
hence (p => ('not' q)) => (q => ('not' p)) in TAUT A by Th3; ::_thesis: verum
end;
theorem Th31: :: LUKASI_1:31
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds (('not' p) => q) => (('not' q) => p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds (('not' p) => q) => (('not' q) => p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: (('not' p) => q) => (('not' q) => p) in TAUT A
( (('not' p) => q) => (('not' q) => ('not' ('not' p))) in TAUT A & (('not' q) => ('not' ('not' p))) => (('not' q) => p) in TAUT A ) by Th26, Th29;
hence (('not' p) => q) => (('not' q) => p) in TAUT A by Th3; ::_thesis: verum
end;
theorem :: LUKASI_1:32
for A being QC-alphabet
for p being Element of CQC-WFF A holds (p => ('not' p)) => ('not' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds (p => ('not' p)) => ('not' p) in TAUT A
let p be Element of CQC-WFF A; ::_thesis: (p => ('not' p)) => ('not' p) in TAUT A
( (('not' ('not' p)) => ('not' p)) => ('not' p) in TAUT A & (p => ('not' p)) => (('not' ('not' p)) => ('not' p)) in TAUT A ) by Th28, CQC_THE1:42;
hence (p => ('not' p)) => ('not' p) in TAUT A by Th3; ::_thesis: verum
end;
theorem :: LUKASI_1:33
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds ('not' p) => (p => q) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds ('not' p) => (p => q) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ('not' p) => (p => q) in TAUT A
( ('not' p) => (('not' ('not' p)) => q) in TAUT A & (('not' ('not' p)) => q) => (p => q) in TAUT A ) by Th28, CQC_THE1:43;
hence ('not' p) => (p => q) in TAUT A by Th3; ::_thesis: verum
end;
theorem Th34: :: LUKASI_1:34
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff ('not' q) => ('not' p) in TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff ('not' q) => ('not' p) in TAUT A )
let p, q be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A iff ('not' q) => ('not' p) in TAUT A )
(p => q) => (('not' q) => ('not' p)) in TAUT A by Th26;
hence ( p => q in TAUT A implies ('not' q) => ('not' p) in TAUT A ) by CQC_THE1:46; ::_thesis: ( ('not' q) => ('not' p) in TAUT A implies p => q in TAUT A )
(('not' q) => ('not' p)) => (p => q) in TAUT A by Th24;
hence ( ('not' q) => ('not' p) in TAUT A implies p => q in TAUT A ) by CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:35
for A being QC-alphabet
for p, q being Element of CQC-WFF A st ('not' p) => ('not' q) in TAUT A holds
q => p in TAUT A by Th34;
theorem :: LUKASI_1:36
for A being QC-alphabet
for p being Element of CQC-WFF A holds
( p in TAUT A iff 'not' ('not' p) in TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds
( p in TAUT A iff 'not' ('not' p) in TAUT A )
let p be Element of CQC-WFF A; ::_thesis: ( p in TAUT A iff 'not' ('not' p) in TAUT A )
thus ( p in TAUT A implies 'not' ('not' p) in TAUT A ) ::_thesis: ( 'not' ('not' p) in TAUT A implies p in TAUT A )
proof
assume A1: p in TAUT A ; ::_thesis: 'not' ('not' p) in TAUT A
p => ('not' ('not' p)) in TAUT A by Th27;
hence 'not' ('not' p) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
assume A2: 'not' ('not' p) in TAUT A ; ::_thesis: p in TAUT A
('not' ('not' p)) => p in TAUT A by Th25;
hence p in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:37
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff p => ('not' ('not' q)) in TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff p => ('not' ('not' q)) in TAUT A )
let p, q be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A iff p => ('not' ('not' q)) in TAUT A )
thus ( p => q in TAUT A implies p => ('not' ('not' q)) in TAUT A ) ::_thesis: ( p => ('not' ('not' q)) in TAUT A implies p => q in TAUT A )
proof
assume A1: p => q in TAUT A ; ::_thesis: p => ('not' ('not' q)) in TAUT A
(p => q) => (p => ('not' ('not' q))) in TAUT A by Th29;
hence p => ('not' ('not' q)) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
assume A2: p => ('not' ('not' q)) in TAUT A ; ::_thesis: p => q in TAUT A
(p => ('not' ('not' q))) => (p => q) in TAUT A by Th29;
hence p => q in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:38
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff ('not' ('not' p)) => q in TAUT A )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p => q in TAUT A iff ('not' ('not' p)) => q in TAUT A )
let p, q be Element of CQC-WFF A; ::_thesis: ( p => q in TAUT A iff ('not' ('not' p)) => q in TAUT A )
thus ( p => q in TAUT A implies ('not' ('not' p)) => q in TAUT A ) ::_thesis: ( ('not' ('not' p)) => q in TAUT A implies p => q in TAUT A )
proof
assume A1: p => q in TAUT A ; ::_thesis: ('not' ('not' p)) => q in TAUT A
(p => q) => (('not' ('not' p)) => q) in TAUT A by Th28;
hence ('not' ('not' p)) => q in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
assume A2: ('not' ('not' p)) => q in TAUT A ; ::_thesis: p => q in TAUT A
(('not' ('not' p)) => q) => (p => q) in TAUT A by Th28;
hence p => q in TAUT A by A2, CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:39
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p => ('not' q) in TAUT A holds
q => ('not' p) in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p => ('not' q) in TAUT A holds
q => ('not' p) in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( p => ('not' q) in TAUT A implies q => ('not' p) in TAUT A )
assume A1: p => ('not' q) in TAUT A ; ::_thesis: q => ('not' p) in TAUT A
(p => ('not' q)) => (q => ('not' p)) in TAUT A by Th30;
hence q => ('not' p) in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
theorem :: LUKASI_1:40
for A being QC-alphabet
for p, q being Element of CQC-WFF A st ('not' p) => q in TAUT A holds
('not' q) => p in TAUT A
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st ('not' p) => q in TAUT A holds
('not' q) => p in TAUT A
let p, q be Element of CQC-WFF A; ::_thesis: ( ('not' p) => q in TAUT A implies ('not' q) => p in TAUT A )
assume A1: ('not' p) => q in TAUT A ; ::_thesis: ('not' q) => p in TAUT A
(('not' p) => q) => (('not' q) => p) in TAUT A by Th31;
hence ('not' q) => p in TAUT A by A1, CQC_THE1:46; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
clusterK170(A,(p => q),((q => r) => (p => r))) -> valid ;
coherence
(p => q) => ((q => r) => (p => r)) is valid
proof
thus (p => q) => ((q => r) => (p => r)) in TAUT A by Th1; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:41
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(q => r) => (p => r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid holds
(q => r) => (p => r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies (q => r) => (p => r) is valid )
assume A1: p => q is valid ; ::_thesis: (q => r) => (p => r) is valid
(p => q) => ((q => r) => (p => r)) is valid ;
hence (q => r) => (p => r) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem Th42: :: LUKASI_1:42
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid & q => r is valid holds
p => r is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid & q => r is valid holds
p => r is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid & q => r is valid implies p => r is valid )
assume ( p => q is valid & q => r is valid ) ; ::_thesis: p => r is valid
then ( p => q in TAUT A & q => r in TAUT A ) by CQC_THE1:def_10;
hence p => r in TAUT A by Th3; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p be Element of CQC-WFF A;
clusterK170(A,p,p) -> valid ;
coherence
p => p is valid
proof
thus p => p in TAUT A by Th4; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,p,(q => p)) -> valid ;
coherence
p => (q => p) is valid
proof
thus p => (q => p) in TAUT A by Th5; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:43
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is valid holds
q => p is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p is valid holds
q => p is valid
let p, q be Element of CQC-WFF A; ::_thesis: ( p is valid implies q => p is valid )
assume p is valid ; ::_thesis: q => p is valid
then p in TAUT A by CQC_THE1:def_10;
hence q => p in TAUT A by Th13; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q, s be Element of CQC-WFF A;
clusterK170(A,(s => (q => p)),(q => (s => p))) -> valid ;
coherence
(s => (q => p)) => (q => (s => p)) is valid
proof
thus (s => (q => p)) => (q => (s => p)) in TAUT A by Th8; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem Th44: :: LUKASI_1:44
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
q => (p => r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
q => (p => r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid implies q => (p => r) is valid )
assume p => (q => r) is valid ; ::_thesis: q => (p => r) is valid
then p => (q => r) in TAUT A by CQC_THE1:def_10;
hence q => (p => r) in TAUT A by Th15; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
theorem :: LUKASI_1:45
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid & q is valid holds
p => r is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid & q is valid holds
p => r is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid & q is valid implies p => r is valid )
assume p => (q => r) is valid ; ::_thesis: ( not q is valid or p => r is valid )
then q => (p => r) is valid by Th44;
hence ( not q is valid or p => r is valid ) by CQC_THE1:65; ::_thesis: verum
end;
theorem :: LUKASI_1:46
for A being QC-alphabet
for p being Element of CQC-WFF A holds
( p => (VERUM A) is valid & ('not' (VERUM A)) => p is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds
( p => (VERUM A) is valid & ('not' (VERUM A)) => p is valid )
let p be Element of CQC-WFF A; ::_thesis: ( p => (VERUM A) is valid & ('not' (VERUM A)) => p is valid )
thus p => (VERUM A) in TAUT A by Th13, CQC_THE1:41; :: according to CQC_THE1:def_10 ::_thesis: ('not' (VERUM A)) => p is valid
thus ('not' (VERUM A)) => p in TAUT A by Th12; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,p,((p => q) => q)) -> valid ;
coherence
p => ((p => q) => q) is valid
proof
thus p => ((p => q) => q) in TAUT A by Th7; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
registration
let A be QC-alphabet ;
let q, r be Element of CQC-WFF A;
clusterK170(A,(q => (q => r)),(q => r)) -> valid ;
coherence
(q => (q => r)) => (q => r) is valid
proof
thus (q => (q => r)) => (q => r) in TAUT A by Th10; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:47
for A being QC-alphabet
for q, r being Element of CQC-WFF A st q => (q => r) is valid holds
q => r is valid
proof
let A be QC-alphabet ; ::_thesis: for q, r being Element of CQC-WFF A st q => (q => r) is valid holds
q => r is valid
let q, r be Element of CQC-WFF A; ::_thesis: ( q => (q => r) is valid implies q => r is valid )
assume A1: q => (q => r) is valid ; ::_thesis: q => r is valid
(q => (q => r)) => (q => r) is valid ;
hence q => r is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
clusterK170(A,(p => (q => r)),((p => q) => (p => r))) -> valid ;
coherence
(p => (q => r)) => ((p => q) => (p => r)) is valid
proof
thus (p => (q => r)) => ((p => q) => (p => r)) in TAUT A by Th11; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem Th48: :: LUKASI_1:48
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(p => q) => (p => r) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid holds
(p => q) => (p => r) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid implies (p => q) => (p => r) is valid )
assume A1: p => (q => r) is valid ; ::_thesis: (p => q) => (p => r) is valid
(p => (q => r)) => ((p => q) => (p => r)) is valid ;
hence (p => q) => (p => r) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem :: LUKASI_1:49
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => (q => r) is valid & p => q is valid holds
p => r is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => (q => r) is valid & p => q is valid holds
p => r is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => (q => r) is valid & p => q is valid implies p => r is valid )
assume that
A1: p => (q => r) is valid and
A2: p => q is valid ; ::_thesis: p => r is valid
(p => q) => (p => r) is valid by A1, Th48;
hence p => r is valid by A2, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
clusterK170(A,((p => q) => r),(q => r)) -> valid ;
coherence
((p => q) => r) => (q => r) is valid
proof
thus ((p => q) => r) => (q => r) in TAUT A by Th6; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:50
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p => q) => r is valid holds
q => r is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st (p => q) => r is valid holds
q => r is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( (p => q) => r is valid implies q => r is valid )
assume A1: (p => q) => r is valid ; ::_thesis: q => r is valid
((p => q) => r) => (q => r) is valid ;
hence q => r is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q, r be Element of CQC-WFF A;
clusterK170(A,(p => q),((r => p) => (r => q))) -> valid ;
coherence
(p => q) => ((r => p) => (r => q)) is valid
proof
thus (p => q) => ((r => p) => (r => q)) in TAUT A by Th9; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:51
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r => p) => (r => q) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r => p) => (r => q) is valid
let p, q, r be Element of CQC-WFF A; ::_thesis: ( p => q is valid implies (r => p) => (r => q) is valid )
assume A1: p => q is valid ; ::_thesis: (r => p) => (r => q) is valid
(p => q) => ((r => p) => (r => q)) is valid ;
hence (r => p) => (r => q) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,(p => q),(('not' q) => ('not' p))) -> valid ;
coherence
(p => q) => (('not' q) => ('not' p)) is valid
proof
thus (p => q) => (('not' q) => ('not' p)) in TAUT A by Th26; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,(('not' p) => ('not' q)),(q => p)) -> valid ;
coherence
(('not' p) => ('not' q)) => (q => p) is valid
proof
thus (('not' p) => ('not' q)) => (q => p) in TAUT A by Th24; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:52
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ('not' p) => ('not' q) is valid iff q => p is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( ('not' p) => ('not' q) is valid iff q => p is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( ('not' p) => ('not' q) is valid iff q => p is valid )
thus ( ('not' p) => ('not' q) is valid implies q => p is valid ) ::_thesis: ( q => p is valid implies ('not' p) => ('not' q) is valid )
proof
assume A1: ('not' p) => ('not' q) is valid ; ::_thesis: q => p is valid
(('not' p) => ('not' q)) => (q => p) is valid ;
hence q => p is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
assume A2: q => p is valid ; ::_thesis: ('not' p) => ('not' q) is valid
(q => p) => (('not' p) => ('not' q)) is valid ;
hence ('not' p) => ('not' q) is valid by A2, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p be Element of CQC-WFF A;
clusterK170(A,p,('not' ('not' p))) -> valid ;
coherence
p => ('not' ('not' p)) is valid
proof
thus p => ('not' ('not' p)) in TAUT A by Th27; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
registration
let A be QC-alphabet ;
let p be Element of CQC-WFF A;
clusterK170(A,('not' ('not' p)),p) -> valid ;
coherence
('not' ('not' p)) => p is valid
proof
thus ('not' ('not' p)) => p in TAUT A by Th25; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:53
for A being QC-alphabet
for p being Element of CQC-WFF A holds
( 'not' ('not' p) is valid iff p is valid )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A holds
( 'not' ('not' p) is valid iff p is valid )
let p be Element of CQC-WFF A; ::_thesis: ( 'not' ('not' p) is valid iff p is valid )
thus ( 'not' ('not' p) is valid implies p is valid ) ::_thesis: ( p is valid implies 'not' ('not' p) is valid )
proof
assume A1: 'not' ('not' p) is valid ; ::_thesis: p is valid
('not' ('not' p)) => p is valid ;
hence p is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
assume A2: p is valid ; ::_thesis: 'not' ('not' p) is valid
p => ('not' ('not' p)) is valid ;
hence 'not' ('not' p) is valid by A2, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,(('not' ('not' p)) => q),(p => q)) -> valid ;
coherence
(('not' ('not' p)) => q) => (p => q) is valid
proof
thus (('not' ('not' p)) => q) => (p => q) in TAUT A by Th28; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:54
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ('not' ('not' p)) => q is valid iff p => q is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( ('not' ('not' p)) => q is valid iff p => q is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( ('not' ('not' p)) => q is valid iff p => q is valid )
thus ( ('not' ('not' p)) => q is valid implies p => q is valid ) ::_thesis: ( p => q is valid implies ('not' ('not' p)) => q is valid )
proof
assume A1: ('not' ('not' p)) => q is valid ; ::_thesis: p => q is valid
(('not' ('not' p)) => q) => (p => q) is valid ;
hence p => q is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
assume A2: p => q is valid ; ::_thesis: ('not' ('not' p)) => q is valid
('not' ('not' p)) => p is valid ;
hence ('not' ('not' p)) => q is valid by A2, Th42; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,(p => ('not' ('not' q))),(p => q)) -> valid ;
coherence
(p => ('not' ('not' q))) => (p => q) is valid
proof
thus (p => ('not' ('not' q))) => (p => q) in TAUT A by Th29; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:55
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p => ('not' ('not' q)) is valid iff p => q is valid )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A holds
( p => ('not' ('not' q)) is valid iff p => q is valid )
let p, q be Element of CQC-WFF A; ::_thesis: ( p => ('not' ('not' q)) is valid iff p => q is valid )
thus ( p => ('not' ('not' q)) is valid implies p => q is valid ) ::_thesis: ( p => q is valid implies p => ('not' ('not' q)) is valid )
proof
assume A1: p => ('not' ('not' q)) is valid ; ::_thesis: p => q is valid
(p => ('not' ('not' q))) => (p => q) is valid ;
hence p => q is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
assume A2: p => q is valid ; ::_thesis: p => ('not' ('not' q)) is valid
q => ('not' ('not' q)) is valid ;
hence p => ('not' ('not' q)) is valid by A2, Th42; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,(p => ('not' q)),(q => ('not' p))) -> valid ;
coherence
(p => ('not' q)) => (q => ('not' p)) is valid
proof
thus (p => ('not' q)) => (q => ('not' p)) in TAUT A by Th30; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:56
for A being QC-alphabet
for p, q being Element of CQC-WFF A st p => ('not' q) is valid holds
q => ('not' p) is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st p => ('not' q) is valid holds
q => ('not' p) is valid
let p, q be Element of CQC-WFF A; ::_thesis: ( p => ('not' q) is valid implies q => ('not' p) is valid )
assume A1: p => ('not' q) is valid ; ::_thesis: q => ('not' p) is valid
(p => ('not' q)) => (q => ('not' p)) is valid ;
hence q => ('not' p) is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
registration
let A be QC-alphabet ;
let p, q be Element of CQC-WFF A;
clusterK170(A,(('not' p) => q),(('not' q) => p)) -> valid ;
coherence
(('not' p) => q) => (('not' q) => p) is valid
proof
thus (('not' p) => q) => (('not' q) => p) in TAUT A by Th31; :: according to CQC_THE1:def_10 ::_thesis: verum
end;
end;
theorem :: LUKASI_1:57
for A being QC-alphabet
for p, q being Element of CQC-WFF A st ('not' p) => q is valid holds
('not' q) => p is valid
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A st ('not' p) => q is valid holds
('not' q) => p is valid
let p, q be Element of CQC-WFF A; ::_thesis: ( ('not' p) => q is valid implies ('not' q) => p is valid )
assume A1: ('not' p) => q is valid ; ::_thesis: ('not' q) => p is valid
(('not' p) => q) => (('not' q) => p) is valid ;
hence ('not' q) => p is valid by A1, CQC_THE1:65; ::_thesis: verum
end;
theorem :: LUKASI_1:58
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q holds
X |- (q => r) => (p => r)
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q holds
X |- (q => r) => (p => r)
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => q holds
X |- (q => r) => (p => r)
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => q implies X |- (q => r) => (p => r) )
assume A1: X |- p => q ; ::_thesis: X |- (q => r) => (p => r)
X |- (p => q) => ((q => r) => (p => r)) by CQC_THE1:59;
hence X |- (q => r) => (p => r) by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem Th59: :: LUKASI_1:59
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q & X |- q => r holds
X |- p => r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => q & X |- q => r holds
X |- p => r
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => q & X |- q => r holds
X |- p => r
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => q & X |- q => r implies X |- p => r )
assume that
A1: X |- p => q and
A2: X |- q => r ; ::_thesis: X |- p => r
X |- (p => q) => ((q => r) => (p => r)) by CQC_THE1:59;
then X |- (q => r) => (p => r) by A1, CQC_THE1:55;
hence X |- p => r by A2, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:60
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds X |- p => p by CQC_THE1:59;
theorem :: LUKASI_1:61
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p holds
X |- q => p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p holds
X |- q => p
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p holds
X |- q => p
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p implies X |- q => p )
assume A1: X |- p ; ::_thesis: X |- q => p
X |- p => (q => p) by CQC_THE1:59;
hence X |- q => p by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:62
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p holds
X |- (p => q) => q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p holds
X |- (p => q) => q
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p holds
X |- (p => q) => q
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p implies X |- (p => q) => q )
assume A1: X |- p ; ::_thesis: X |- (p => q) => q
X |- p => ((p => q) => q) by CQC_THE1:59;
hence X |- (p => q) => q by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem Th63: :: LUKASI_1:63
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) holds
X |- q => (p => r)
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) holds
X |- q => (p => r)
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => (q => r) holds
X |- q => (p => r)
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => (q => r) implies X |- q => (p => r) )
assume A1: X |- p => (q => r) ; ::_thesis: X |- q => (p => r)
X |- (p => (q => r)) => (q => (p => r)) by CQC_THE1:59;
hence X |- q => (p => r) by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:64
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) & X |- q holds
X |- p => r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) & X |- q holds
X |- p => r
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => (q => r) & X |- q holds
X |- p => r
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => (q => r) & X |- q implies X |- p => r )
assume X |- p => (q => r) ; ::_thesis: ( not X |- q or X |- p => r )
then X |- q => (p => r) by Th63;
hence ( not X |- q or X |- p => r ) by CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:65
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (p => q) holds
X |- p => q
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (p => q) holds
X |- p => q
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => (p => q) holds
X |- p => q
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => (p => q) implies X |- p => q )
assume A1: X |- p => (p => q) ; ::_thesis: X |- p => q
X |- (p => (p => q)) => (p => q) by CQC_THE1:59;
hence X |- p => q by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:66
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- (p => q) => r holds
X |- q => r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- (p => q) => r holds
X |- q => r
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- (p => q) => r holds
X |- q => r
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- (p => q) => r implies X |- q => r )
assume A1: X |- (p => q) => r ; ::_thesis: X |- q => r
X |- ((p => q) => r) => (q => r) by CQC_THE1:59;
hence X |- q => r by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem Th67: :: LUKASI_1:67
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) holds
X |- (p => q) => (p => r)
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) holds
X |- (p => q) => (p => r)
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => (q => r) holds
X |- (p => q) => (p => r)
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => (q => r) implies X |- (p => q) => (p => r) )
assume A1: X |- p => (q => r) ; ::_thesis: X |- (p => q) => (p => r)
X |- (p => (q => r)) => ((p => q) => (p => r)) by CQC_THE1:59;
hence X |- (p => q) => (p => r) by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:68
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) & X |- p => q holds
X |- p => r
proof
let A be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => (q => r) & X |- p => q holds
X |- p => r
let p, q, r be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => (q => r) & X |- p => q holds
X |- p => r
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => (q => r) & X |- p => q implies X |- p => r )
assume X |- p => (q => r) ; ::_thesis: ( not X |- p => q or X |- p => r )
then X |- (p => q) => (p => r) by Th67;
hence ( not X |- p => q or X |- p => r ) by CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:69
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- ('not' p) => ('not' q) iff X |- q => p )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- ('not' p) => ('not' q) iff X |- q => p )
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) holds
( X |- ('not' p) => ('not' q) iff X |- q => p )
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- ('not' p) => ('not' q) iff X |- q => p )
thus ( X |- ('not' p) => ('not' q) implies X |- q => p ) ::_thesis: ( X |- q => p implies X |- ('not' p) => ('not' q) )
proof
assume A1: X |- ('not' p) => ('not' q) ; ::_thesis: X |- q => p
X |- (('not' p) => ('not' q)) => (q => p) by CQC_THE1:59;
hence X |- q => p by A1, CQC_THE1:55; ::_thesis: verum
end;
assume A2: X |- q => p ; ::_thesis: X |- ('not' p) => ('not' q)
X |- (q => p) => (('not' p) => ('not' q)) by CQC_THE1:59;
hence X |- ('not' p) => ('not' q) by A2, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:70
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- 'not' ('not' p) iff X |- p )
proof
let A be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- 'not' ('not' p) iff X |- p )
let p be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) holds
( X |- 'not' ('not' p) iff X |- p )
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- 'not' ('not' p) iff X |- p )
thus ( X |- 'not' ('not' p) implies X |- p ) ::_thesis: ( X |- p implies X |- 'not' ('not' p) )
proof
assume A1: X |- 'not' ('not' p) ; ::_thesis: X |- p
X |- ('not' ('not' p)) => p by CQC_THE1:59;
hence X |- p by A1, CQC_THE1:55; ::_thesis: verum
end;
assume A2: X |- p ; ::_thesis: X |- 'not' ('not' p)
X |- p => ('not' ('not' p)) by CQC_THE1:59;
hence X |- 'not' ('not' p) by A2, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:71
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- p => ('not' ('not' q)) iff X |- p => q )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- p => ('not' ('not' q)) iff X |- p => q )
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) holds
( X |- p => ('not' ('not' q)) iff X |- p => q )
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => ('not' ('not' q)) iff X |- p => q )
thus ( X |- p => ('not' ('not' q)) implies X |- p => q ) ::_thesis: ( X |- p => q implies X |- p => ('not' ('not' q)) )
proof
assume A1: X |- p => ('not' ('not' q)) ; ::_thesis: X |- p => q
X |- (p => ('not' ('not' q))) => (p => q) by CQC_THE1:59;
hence X |- p => q by A1, CQC_THE1:55; ::_thesis: verum
end;
assume A2: X |- p => q ; ::_thesis: X |- p => ('not' ('not' q))
X |- q => ('not' ('not' q)) by CQC_THE1:59;
hence X |- p => ('not' ('not' q)) by A2, Th59; ::_thesis: verum
end;
theorem :: LUKASI_1:72
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- ('not' ('not' p)) => q iff X |- p => q )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) holds
( X |- ('not' ('not' p)) => q iff X |- p => q )
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) holds
( X |- ('not' ('not' p)) => q iff X |- p => q )
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- ('not' ('not' p)) => q iff X |- p => q )
thus ( X |- ('not' ('not' p)) => q implies X |- p => q ) ::_thesis: ( X |- p => q implies X |- ('not' ('not' p)) => q )
proof
assume A1: X |- ('not' ('not' p)) => q ; ::_thesis: X |- p => q
X |- (('not' ('not' p)) => q) => (p => q) by CQC_THE1:59;
hence X |- p => q by A1, CQC_THE1:55; ::_thesis: verum
end;
assume A2: X |- p => q ; ::_thesis: X |- ('not' ('not' p)) => q
X |- ('not' ('not' p)) => p by CQC_THE1:59;
hence X |- ('not' ('not' p)) => q by A2, Th59; ::_thesis: verum
end;
theorem Th73: :: LUKASI_1:73
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => ('not' q) holds
X |- q => ('not' p)
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => ('not' q) holds
X |- q => ('not' p)
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => ('not' q) holds
X |- q => ('not' p)
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => ('not' q) implies X |- q => ('not' p) )
assume A1: X |- p => ('not' q) ; ::_thesis: X |- q => ('not' p)
X |- (p => ('not' q)) => (q => ('not' p)) by CQC_THE1:59;
hence X |- q => ('not' p) by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem Th74: :: LUKASI_1:74
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- ('not' p) => q holds
X |- ('not' q) => p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- ('not' p) => q holds
X |- ('not' q) => p
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- ('not' p) => q holds
X |- ('not' q) => p
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- ('not' p) => q implies X |- ('not' q) => p )
assume A1: X |- ('not' p) => q ; ::_thesis: X |- ('not' q) => p
X |- (('not' p) => q) => (('not' q) => p) by CQC_THE1:59;
hence X |- ('not' q) => p by A1, CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:75
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => ('not' q) & X |- q holds
X |- 'not' p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- p => ('not' q) & X |- q holds
X |- 'not' p
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- p => ('not' q) & X |- q holds
X |- 'not' p
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- p => ('not' q) & X |- q implies X |- 'not' p )
assume X |- p => ('not' q) ; ::_thesis: ( not X |- q or X |- 'not' p )
then X |- q => ('not' p) by Th73;
hence ( not X |- q or X |- 'not' p ) by CQC_THE1:55; ::_thesis: verum
end;
theorem :: LUKASI_1:76
for A being QC-alphabet
for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- ('not' p) => q & X |- 'not' q holds
X |- p
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st X |- ('not' p) => q & X |- 'not' q holds
X |- p
let p, q be Element of CQC-WFF A; ::_thesis: for X being Subset of (CQC-WFF A) st X |- ('not' p) => q & X |- 'not' q holds
X |- p
let X be Subset of (CQC-WFF A); ::_thesis: ( X |- ('not' p) => q & X |- 'not' q implies X |- p )
assume X |- ('not' p) => q ; ::_thesis: ( not X |- 'not' q or X |- p )
then X |- ('not' q) => p by Th74;
hence ( not X |- 'not' q or X |- p ) by CQC_THE1:55; ::_thesis: verum
end;