:: Suszko's Non-Fregean Logics, Part 1
:: by Taneli Huuskonen
::
:: Received December 2, 2025
:: Copyright (c) 2025-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 4.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/4.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_1, XXREAL_0, TARSKI, CARD_1,
ORDINAL4, FUNCT_1, XBOOLEAN, RELAT_1, NAT_1, ZF_LANG, POLNOT_1, POLNOT_2,
ZFMISC_1, FINSET_1, CQC_THE1, EQREL_1, SETFAM_1, FINSUB_1, BVFUNC_1,
FUNCOP_1, FUNCT_4, SUSZKO_1, AOFA_L00, CAT_1, ALGSPEC1, PROOFS_1,
FOMODEL1, FOMODEL3, FOMODEL4, WAYBEL20, METRIC_2, ALG_1, QUANTAL1;
notations ORDINAL1, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, NUMBERS, FINSEQ_1,
ENUMSET1, ZFMISC_1, POLNOT_1, FUNCT_2, BINOP_1, RELSET_1, XXREAL_0,
FINSET_1, FINSUB_1, SETFAM_1, FUNCOP_1, FUNCT_4, RELAT_1, EQREL_1,
FREEALG, PROOFS_1, POLNOT_2;
constructors ENUMSET1, RELSET_1, XREAL_0, FUNCT_4, FUNCOP_1, PROOFS_1,
POLNOT_2, ALG_1, FINSUB_1, POLNOT_1, FREEALG;
registrations ORDINAL1, RELSET_1, FINSEQ_1, XBOOLE_0, FUNCT_1, XREAL_0,
FINSET_1, POLNOT_1, FUNCOP_1, VALUED_0, POLNOT_2, SUBSET_1, PROOFS_1,
EQREL_1;
requirements REAL, NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, POLNOT_1;
expansions TARSKI, FINSEQ_1, POLNOT_2, SUBSET_1, PROOFS_1;
theorems TARSKI, FUNCT_1, FINSEQ_1, XBOOLE_0, XBOOLE_1, POLNOT_1, ENUMSET1,
ZFMISC_1, FUNCT_2, EQREL_1, RELSET_1, FUNCT_4, FINSUB_1, FUNCOP_1,
VALUED_0, PROOFS_1, POLNOT_2, GRFUNC_1, XTUPLE_0, RELAT_1;
schemes XBOOLE_0, EQREL_1, PROOFS_1;
begin
reserve k,m,n for Element of NAT,
i, j for Nat,
a, b, c for object,
y, z for set;
reserve p, q, r, s for FinSequence;
::
:: The Construction of Suszko's Sentential Calculus with Identity
::
definition
func VARS -> FinSequence-membered set equals
the set of all <*0,k*> where k is Element of NAT;
coherence
proof
set y = the set of all <*0,k*> where k is Element of NAT;
for a st a in y holds a is FinSequence
proof
let a;
assume a in y;
then consider k such that A1: a = <*0, k*>;
thus thesis by A1;
end;
hence thesis by FINSEQ_1:def 19;
end;
end;
registration
cluster VARS -> non empty antichain-like;
coherence
proof
<*0, the Element of NAT*> in VARS;
hence VARS is non empty;
for p st p in VARS holds dom p = { 1, 2 }
proof
let p;
assume p in VARS;
then consider k such that A2: p = <*0, k*>;
thus thesis by A2, FINSEQ_1:92;
end;
hence thesis by POLNOT_1:45;
end;
end;
definition
mode Variable is Element of VARS;
end;
Lm1:
for a being Variable holds 1 in dom a & a.1 = 0
proof
let a be Variable;
a in VARS;
then consider k such that A1: a = <* 0, k *>;
len a = 2 by A1, FINSEQ_1:44;
then dom a = Seg 2 by FINSEQ_1:def 3;
hence 1 in dom a by FINSEQ_1:2, TARSKI:def 2;
thus thesis by A1;
end;
:: definition
:: func TRUE -> FinSequence equals <*1*>;
:: coherence;
:: func FALSE -> FinSequence equals <*2*>;
:: coherence;
:: end;
definition
func 'not' -> FinSequence equals <*11*>;
coherence;
func '&&s' -> FinSequence equals <*21*>;
coherence;
func '||s' -> FinSequence equals <*22*>;
coherence;
end;
definition
func '->' -> FinSequence equals <*23*>;
coherence;
func '<->' -> FinSequence equals <*24*>;
coherence;
func '==' -> FinSequence equals <*25*>;
coherence;
end;
definition
func SCI-unops -> non empty FinSequence-membered set equals
{ 'not' };
coherence
proof
set y = { 'not' };
y is FinSequence-membered by TARSKI:def 1;
hence thesis;
end;
func SCI-binops -> non empty FinSequence-membered set equals
{ '&&s', '||s', '->', '<->', '==' };
coherence
proof
set y = { '&&s', '||s', '->', '<->', '==' };
y is non empty FinSequence-membered by ENUMSET1:def 3;
hence thesis;
end;
end;
theorem Th1:
for a holds (a in SCI-unops iff a = 'not') &
(a in SCI-binops iff a = '&&s' or a = '||s' or a = '->' or a = '<->'
or a = '==') by TARSKI:def 1, ENUMSET1:def 3;
registration
let F,G be non empty FinSequence-membered set;
cluster F \/ G -> non empty FinSequence-membered;
coherence;
end;
definition
func SCI-ops -> non empty FinSequence-membered set equals
SCI-unops \/ SCI-binops;
coherence;
end;
Lm3:
for a holds (a in SCI-ops iff
a = 'not' or a = '&&s' or a = '||s' or
a = '->' or a = '<->' or a = '==')
proof
let a;
A2: a in SCI-unops iff a = 'not' by TARSKI:def 1;
a in SCI-binops iff a = '&&s' or a = '||s' or a = '->' or a = '<->'
or a = '==' by ENUMSET1:def 3;
hence thesis by A2, XBOOLE_0:def 3;
end;
Lm4:
for p being Element of SCI-ops holds dom p = Seg 1 & p.1 <> 0
proof
let p be Element of SCI-ops;
per cases by XBOOLE_0:def 3;
suppose p in SCI-unops;
then p = 'not' by TARSKI:def 1;
hence thesis by FINSEQ_1:def 8;
end;
suppose p in SCI-binops;
then p = '&&s' or p = '||s' or p = '->' or p = '<->' or p = '=='
by ENUMSET1:def 3;
hence thesis by FINSEQ_1:def 8;
end;
end;
theorem
for p holds
(p = 'not' implies p.1 = 11) &
(p = '&&s' implies p.1 = 21) &
(p = '||s' implies p.1 = 22) &
(p = '->' implies p.1 = 23) &
(p = '<->' implies p.1 = 24) &
(p = '==' implies p.1 = 25);
registration
cluster SCI-ops -> non empty antichain-like;
coherence
proof
for p st p in SCI-ops holds dom p = Seg 1 by Lm4;
hence thesis by POLNOT_1:45;
end;
end;
definition
func SCI-symbols -> non empty FinSequence-membered set equals
VARS \/ SCI-ops;
coherence;
end;
definition
redefine func VARS -> non empty Subset of SCI-symbols; :: redefines VARS (SUSZKO_1, definition)
coherence by XBOOLE_1:7;
redefine func SCI-ops -> non empty Subset of SCI-symbols; :: redefines SCI-ops (SUSZKO_1, definition)
coherence by XBOOLE_1:7;
redefine func SCI-unops -> non empty Subset of SCI-symbols; :: redefines SCI-unops (SUSZKO_1, definition)
coherence by XBOOLE_1:7, XBOOLE_1:10;
redefine func SCI-binops -> non empty Subset of SCI-symbols; :: redefines SCI-binops (SUSZKO_1, definition)
coherence by XBOOLE_1:7, XBOOLE_1:10;
end;
definition
redefine func 'not' -> Element of SCI-symbols; :: redefines 'not' (SUSZKO_1, definition)
coherence
proof
'not' in SCI-unops by TARSKI:def 1;
hence thesis;
end;
redefine func '&&s' -> Element of SCI-symbols; :: redefines '&&s' (SUSZKO_1, definition)
coherence
proof
'&&s' in SCI-binops by ENUMSET1:def 3;
hence thesis;
end;
redefine func '||s' -> Element of SCI-symbols; :: redefines '||s' (SUSZKO_1, definition)
coherence
proof
'||s' in SCI-binops by ENUMSET1:def 3;
hence thesis;
end;
redefine func '->' -> Element of SCI-symbols; :: redefines '->' (SUSZKO_1, definition)
coherence
proof
'->' in SCI-binops by ENUMSET1:def 3;
hence thesis;
end;
redefine func '<->' -> Element of SCI-symbols; :: redefines '<->' (SUSZKO_1, definition)
coherence
proof
'<->' in SCI-binops by ENUMSET1:def 3;
hence thesis;
end;
redefine func '==' -> Element of SCI-symbols; :: redefines '==' (SUSZKO_1, definition)
coherence
proof
'==' in SCI-binops by ENUMSET1:def 3;
hence thesis;
end;
end;
Lm5:
for p being Element of SCI-symbols holds p.1 = 0 iff p in VARS
proof
let p be Element of SCI-symbols;
thus p.1 = 0 implies p in VARS
proof
assume p.1 = 0;
then not p in SCI-ops by Lm4;
hence thesis by XBOOLE_0:def 3;
end;
thus p in VARS implies p.1 = 0 by Lm1;
end;
Lm6:
not ex a st a in SCI-unops & a in SCI-binops
proof
A0: for p being FinSequence of NAT st p in SCI-binops holds p.1 > 20
proof
let p be FinSequence of NAT;
assume p in SCI-binops;
then p = '&&s' or p = '||s' or p = '->' or p = '<->' or p = '=='
by ENUMSET1:def 3;
hence thesis;
end;
given a such that A10: a in SCI-unops and A11: a in SCI-binops;
reconsider a as FinSequence of NAT by A10, TARSKI:def 1;
a = 'not' by A10, TARSKI:def 1;
then a.1 = 11;
hence contradiction by A0, A11;
end;
Lm7:
not ex a st a in VARS & a in SCI-ops
proof
given a such that A1: a in VARS and A2: a in SCI-ops;
reconsider p = a as Element of SCI-symbols by A1;
p.1 = 0 by A1, Lm1;
hence contradiction by A2, Lm4;
end;
registration
cluster SCI-symbols -> non trivial antichain-like;
coherence
proof
'&&s'.1 = 21 & '||s'.1 = 22;
then '&&s' <> '||s';
hence SCI-symbols is non trivial;
let p, q;
set r = p^q;
assume that A1: p in SCI-symbols and A2: r in SCI-symbols;
reconsider p as Element of SCI-symbols by A1;
reconsider r as Element of SCI-symbols by A2;
per cases;
suppose A3: p.1 = 0;
then A4: p in VARS by Lm5;
then 1 in dom p by Lm1;
then r.1 = 0 by A3, FINSEQ_1:def 7;
then r in VARS by Lm5;
hence thesis by A4, POLNOT_1:def 16;
end;
suppose A10: p.1 <> 0;
then not p in VARS by Lm5;
then A11: p in SCI-ops by XBOOLE_0:def 3;
then dom p = Seg 1 by Lm4;
then 1 in dom p by FINSEQ_1:1;
then r.1 = p.1 by FINSEQ_1:def 7;
then not r in VARS by A10, Lm5;
then r in SCI-ops by XBOOLE_0:def 3;
hence thesis by A11, POLNOT_1:def 16;
end;
end;
end;
definition
redefine func SCI-symbols -> non trivial Polish-language; :: redefines SCI-symbols (SUSZKO_1, definition)
coherence;
end;
definition
func SCI-op-arity -> Function of SCI-ops, NAT equals
(SCI-binops --> 2) +* (SCI-unops --> 1);
coherence
proof
set F1 = SCI-unops --> 1;
set F2 = SCI-binops --> 2;
set H = F2 +* F1;
A1: dom H = dom F2 \/ dom F1 by FUNCT_4:def 1 .= SCI-ops;
rng H c= NAT by VALUED_0:def 6;
hence thesis by A1, FUNCT_2:2;
end;
end;
Lm9:
SCI-op-arity.'not' = 1 & for a st a in SCI-binops holds SCI-op-arity.a = 2
proof
set F1 = SCI-unops --> 1;
set F2 = SCI-binops --> 2;
'not' in dom F1 by TARSKI:def 1;
hence SCI-op-arity.'not' = F1.'not' by FUNCT_4:13 .= 1 by Th1, FUNCOP_1:7;
let a;
assume A11: a in SCI-binops;
then not a in dom F1 by Lm6;
hence SCI-op-arity.a = F2.a by FUNCT_4:11 .= 2 by A11, FUNCOP_1:7;
end;
definition
func SCI-arity -> Polish-arity-function of SCI-symbols equals
SCI-op-arity +* (VARS --> 0);
coherence
proof
set F = VARS --> 0;
set G = SCI-op-arity +* F;
A1: dom G = dom F \/ dom SCI-op-arity by FUNCT_4:def 1
.= SCI-symbols by FUNCT_2:def 1;
ex a st a in dom G & G.a = 0
proof
take y = <*0,0*>;
A20: y in VARS;
hence y in dom G by A1;
y in dom F;
hence G.y = F.y by FUNCT_4:13 .= 0 by A20, FUNCOP_1:7;
end;
then 0 in rng G by FUNCT_1:3;
then G is with_zero;
then G is Polish-arity-function by A1, POLNOT_2:def 2;
hence G is Polish-arity-function of SCI-symbols by A1, POLNOT_2:1;
end;
end;
Lm10:
for a st a in SCI-ops holds SCI-arity.a = SCI-op-arity.a
proof
let a;
assume a in SCI-ops;
then not a in dom (VARS --> 0) by Lm7;
hence thesis by FUNCT_4:11;
end;
theorem Th6:
for a st a in VARS holds SCI-arity.a = 0
proof
set F = VARS --> 0;
let a;
assume A1: a in VARS;
then a in dom F;
hence SCI-arity.a = F.a by FUNCT_4:13 .= 0 by A1, FUNCOP_1:7;
end;
theorem Th7:
SCI-arity.'not' = 1 & for a st a in SCI-binops holds SCI-arity.a = 2
proof
'not' in SCI-ops by Lm3;
hence SCI-arity.'not' = 1 by Lm9, Lm10;
let a;
assume A1: a in SCI-binops;
then a in SCI-ops by XBOOLE_0:def 3;
hence SCI-arity.a = SCI-op-arity.a by Lm10 .= 2 by A1, Lm9;
end;
theorem Th9:
Polish-atoms(SCI-symbols, SCI-arity) = VARS
proof
set y = Polish-atoms(SCI-symbols, SCI-arity);
thus y c= VARS
proof
let a;
assume A11: a in y;
then SCI-arity.a = 0 & a in SCI-symbols by POLNOT_1:def 7;
then not a in SCI-unops & not a in SCI-binops by Th7, TARSKI:def 1;
then A13: not a in SCI-ops by XBOOLE_0:def 3;
a in SCI-symbols by A11, POLNOT_1:def 7;
hence thesis by A13, XBOOLE_0:def 3;
end;
let a;
assume a in VARS;
then a in SCI-symbols & SCI-arity.a = 0 by Th6;
hence a in y by POLNOT_1:def 7;
end;
definition
func SCI-formula-set -> full Polish-language of SCI-symbols equals
Polish-WFF-set(SCI-symbols, SCI-arity);
coherence;
end;
definition
mode SCI-formula is Polish-WFF of SCI-symbols, SCI-arity;
end;
registration
cluster non empty for Subset of SCI-formula-set;
existence
proof
set y = SCI-formula-set;
y c= y;
then reconsider y as Subset of SCI-formula-set;
take y;
thus thesis;
end;
end;
definition
let n;
func x.n -> SCI-formula equals
<*0, n*>;
coherence
proof
A1: <*0, n*> in Polish-atoms(SCI-symbols, SCI-arity)
by Th9;
Polish-atoms(SCI-symbols, SCI-arity)
c= Polish-expression-set(SCI-symbols, SCI-arity) by POLNOT_1:36;
hence thesis by A1;
end;
end;
reserve X for Extension of SCI-arity;
reserve L for Polish-ext-set of X;
reserve t, u, v, w for Formula of L;
theorem Th10:
for X holds SCI-symbols c= dom X
proof
let X;
X is SCI-arity -extending;
then dom SCI-arity c= dom X by GRFUNC_1:2;
hence thesis by FUNCT_2:def 1;
end;
theorem Th7x:
for X holds 'not' in dom X & X.'not' = 1
& for a st a in SCI-binops holds a in dom X & X.a = 2
proof
let X;
A1: dom SCI-arity = SCI-symbols by FUNCT_2:def 1;
A3: SCI-symbols c= dom X by Th10;
hence 'not' in dom X;
A4: X is SCI-arity-extending;
hence X.'not' = 1 by A1, Th7, GRFUNC_1:2;
let a;
assume A6: a in SCI-binops;
hence a in dom X by A3;
thus X.a = SCI-arity.a by A1, A4, A6, GRFUNC_1:2 .= 2 by A6, Th7;
end;
definition
let X, L, n;
func x.(n,L) -> Formula of L equals
x.n;
coherence
proof
SCI-formula-set c= L by POLNOT_1:37;
hence thesis;
end;
end;
theorem
for m, n st m <> n holds x.m <> x.n
proof
let m, n;
assume A1: m <> n;
(x.m).2 = m & (x.n).2 = n;
hence thesis by A1;
end;
definition
let p;
func 'not' p -> FinSequence equals
'not'^p;
coherence;
end;
definition
let p,q;
func p '&' q -> FinSequence equals
'&&s'^(p^q);
coherence;
func p 'or' q -> FinSequence equals
'||s'^(p^q);
coherence;
func p '->' q -> FinSequence equals
'->'^(p^q);
coherence;
func p '<->' q -> FinSequence equals
'<->'^(p^q);
coherence;
func p '==' q -> FinSequence equals
'=='^(p^q);
coherence;
end;
definition
let X, L, t;
redefine func 'not' t equals :: redefines 'not' (SUSZKO_1, definition)
Polish-unOp(X, L, 'not').t;
compatibility
proof
'not' in dom X & X.'not' = 1 by Th7x;
hence thesis by POLNOT_2:def 11;
end;
let u;
redefine func t '&' u equals :: redefines '&' (SUSZKO_1, definition)
Polish-binOp(X, L, '&&s').(t,u);
compatibility
proof
'&&s' in SCI-binops by ENUMSET1:def 3;
then '&&s' in dom X & X.'&&s' = 2 by Th7x;
hence thesis by POLNOT_2:def 12;
end;
redefine func t 'or' u equals :: redefines 'or' (SUSZKO_1, definition)
Polish-binOp(X, L, '||s').(t, u);
compatibility
proof
'||s' in SCI-binops by ENUMSET1:def 3;
then '||s' in dom X & X.'||s' = 2 by Th7x;
hence thesis by POLNOT_2:def 12;
end;
redefine func t '->' u equals :: redefines '->' (SUSZKO_1, definition)
Polish-binOp(X, L, '->').(t, u);
compatibility
proof
'->' in SCI-binops by ENUMSET1:def 3;
then '->' in dom X & X.'->' = 2 by Th7x;
hence thesis by POLNOT_2:def 12;
end;
redefine func t '<->' u equals :: redefines '<->' (SUSZKO_1, definition)
Polish-binOp(X, L, '<->').(t, u);
compatibility
proof
'<->' in SCI-binops by ENUMSET1:def 3;
then '<->' in dom X & X.'<->' = 2 by Th7x;
hence thesis by POLNOT_2:def 12;
end;
redefine func t '==' u equals :: redefines '==' (SUSZKO_1, definition)
Polish-binOp(X, L, '==').(t, u);
compatibility
proof
'==' in SCI-binops by ENUMSET1:def 3;
then '==' in dom X & X.'==' = 2 by Th7x;
hence thesis by POLNOT_2:def 12;
end;
end;
definition
let X, L, t;
redefine func 'not' t -> Formula of L; :: redefines 'not' (SUSZKO_1, definition)
coherence;
end;
definition
let X, L, t, u;
redefine func t '&' u -> Formula of L; :: redefines '&' (SUSZKO_1, definition)
coherence;
redefine func t 'or' u -> Formula of L; :: redefines 'or' (SUSZKO_1, definition)
coherence;
redefine func t '->' u -> Formula of L; :: redefines '->' (SUSZKO_1, definition)
coherence;
redefine func t '<->' u -> Formula of L; :: redefines '<->' (SUSZKO_1, definition)
coherence;
redefine func t '==' u -> Formula of L; :: redefines '==' (SUSZKO_1, definition)
coherence;
end;
definition
let X, L, t, u;
func t => u -> Formula of L equals
t '==' (t '&' u);
coherence;
end;
definition
let X, L, t;
let u be SCI-formula;
redefine func t '->' u -> Formula of L; :: redefines '->' (SUSZKO_1, definition)
coherence
proof
SCI-formula-set c= L by POLNOT_1:37;
then reconsider w = u as Formula of L;
t '->' u = t '->' w;
hence thesis;
end;
redefine func t '==' u -> Formula of L; :: redefines '==' (SUSZKO_1, definition)
coherence
proof
SCI-formula-set c= L by POLNOT_1:37;
then reconsider w = u as Formula of L;
t '==' u = t '==' w;
hence thesis;
end;
end;
definition
let X, L;
let u be SCI-formula;
let t;
redefine func u '->' t -> Formula of L; :: redefines '->' (SUSZKO_1, definition)
coherence
proof
SCI-formula-set c= L by POLNOT_1:37;
then reconsider w = u as Formula of L;
u '->' t = w '->' t;
hence thesis;
end;
redefine func u '==' t -> Formula of L; :: redefines '==' (SUSZKO_1, definition)
coherence
proof
SCI-formula-set c= L by POLNOT_1:37;
then reconsider w = u as Formula of L;
u '==' t = w '==' t;
hence thesis;
end;
end;
definition
let X, L, t;
attr t is atomic means
t in Polish-atoms(SCI-symbols, SCI-arity);
attr t is negative means
Polish-ext-head t = 'not';
attr t is conjunctive means
Polish-ext-head t = '&&s';
attr t is disjunctive means
Polish-ext-head t = '||s';
attr t is conditional means
Polish-ext-head t = '->';
attr t is biconditional means
Polish-ext-head t = '<->';
attr t is being_equality means
Polish-ext-head t = '==';
end;
theorem
for t holds t is atomic iff t in VARS by Th9;
theorem
for t holds t is negative iff ex u st t = 'not' u
proof
A1: 'not' in dom X & X.'not' = 1 by Th7x;
let t;
thus t is negative implies ex u st t = 'not' u
proof
assume t is negative;
then consider u such that
A3: t = Polish-unOp(X, L, 'not').u
by A1, POLNOT_2:10;
take u;
thus thesis by A3;
end;
thus thesis by A1, POLNOT_2:11;
end;
theorem
for t holds t is conjunctive iff ex u, v st t = u '&' v
proof
let t;
'&&s' in SCI-binops by ENUMSET1:def 3;
then A2: '&&s' in dom X & X.'&&s' = 2 by Th7x;
thus t is conjunctive implies ex u, v st t = u '&' v
proof
assume t is conjunctive;
then consider u, v such that
A3: t = Polish-binOp(X, L, '&&s').(u, v)
by A2, POLNOT_2:12;
take u, v;
thus thesis by A3;
end;
thus thesis by A2, POLNOT_2:13;
end;
definition
let X, L;
func SCI-prop-axioms L -> non empty Subset of L means
:Def10p:
for a holds a in it iff ex t, u, v st
a = t '->' (u '->' t) or
a = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or
a = (('not' t) '->' ('not' u)) '->' (u '->' t) or
a = (t '&' u) '->' ('not' (t '->' ('not' u))) or
a = ('not' (t '->' ('not' u))) '->' (t '&' u) or
a = (t 'or' u) '->' (('not' t) '->' u) or
a = (('not' t) '->' u) '->' (t 'or' u) or
a = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or
a = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u);
existence
proof
defpred P[ object ] means ex t, u, v st
$1 = t '->' (u '->' t) or
$1 = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or
$1 = (('not' t) '->' ('not' u)) '->' (u '->' t) or
$1 = (t '&' u) '->' ('not' (t '->' ('not' u))) or
$1 = ('not' (t '->' ('not' u))) '->' (t '&' u) or
$1 = (t 'or' u) '->' (('not' t) '->' u) or
$1 = (('not' t) '->' u) '->' (t 'or' u) or
$1 = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or
$1 = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u);
consider y being set such that A1: for a holds a in y iff a in L & P[ a ]
from XBOOLE_0:sch 1;
A2: x.(1,L) '->' (x.(1,L) '->' x.(1,L)) in y by A1;
y c= L by A1;
then reconsider y as non empty Subset of L by A2;
take y;
thus thesis by A1;
end;
uniqueness
proof
defpred P[ object ] means ex t, u, v st
$1 = t '->' (u '->' t) or
$1 = (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) or
$1 = (('not' t) '->' ('not' u)) '->' (u '->' t) or
$1 = (t '&' u) '->' ('not' (t '->' ('not' u))) or
$1 = ('not' (t '->' ('not' u))) '->' (t '&' u) or
$1 = (t 'or' u) '->' (('not' t) '->' u) or
$1 = (('not' t) '->' u) '->' (t 'or' u) or
$1 = (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) or
$1 = ((t '->' u) '&' (u '->' t)) '->' (t '<->' u);
let y1, y2 be non empty Subset of L such that
A1: a in y1 iff P[ a ] and A2: a in y2 iff P[ a ];
thus y1 = y2 from XBOOLE_0:sch 2(A1, A2);
end;
func SCI-id-axioms L -> non empty Subset of L means
:Def10i:
for a holds a in it iff ex t, u, v, w st
a = (t '==' t) or
a = (t '==' u) '->' (('not' t) '==' ('not' u)) or
a = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or
a = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or
a = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or
a = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or
a = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or
a = ((t '==' u) '->' (t '->' u));
existence
proof
defpred P[ object ] means ex t, u, v, w st
$1 = (t '==' t) or
$1 = (t '==' u) '->' (('not' t) '==' ('not' u)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or
$1 = ((t '==' u) '->' (t '->' u));
consider y being set such that A1: for a holds a in y iff a in L & P[ a ]
from XBOOLE_0:sch 1;
A2: x.(1,L) '==' x.(1,L) in y by A1;
y c= L by A1;
then reconsider y as non empty Subset of L by A2;
take y;
thus thesis by A1;
end;
uniqueness
proof
defpred P[ object ] means ex t, u, v, w st
$1 = (t '==' t) or
$1 = (t '==' u) '->' (('not' t) '==' ('not' u)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '&' v) '==' (u '&' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t 'or' v) '==' (u 'or' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '->' v) '==' (u '->' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '<->' v) '==' (u '<->' w)) or
$1 = ((t '==' u) '&' (v '==' w)) '->' ((t '==' v) '==' (u '==' w)) or
$1 = ((t '==' u) '->' (t '->' u));
let y1, y2 be non empty Subset of L such that
A1: a in y1 iff P[ a ] and A2: a in y2 iff P[ a ];
thus y1 = y2 from XBOOLE_0:sch 2(A1, A2);
end;
end;
registration
let X, L;
let B be Subset of L;
cluster B-extending for non empty Subset of L;
existence
proof
L c= L;
then reconsider K = L as non empty Subset of L;
take K;
thus thesis;
end;
end;
definition
let X, L;
func SCI-axioms L
-> (SCI-prop-axioms L)-extending Subset of L equals
SCI-prop-axioms L \/ SCI-id-axioms L;
coherence
proof
set y = SCI-prop-axioms L \/ SCI-id-axioms L;
reconsider y as Subset of L;
y is (SCI-prop-axioms L)-extending by XBOOLE_1:7;
hence thesis;
end;
end;
reserve R, R1, R2 for Rule of L;
definition
let X, L;
func SCI-MP L -> Rule of L equals
the set of all [{t,t '->' u}, u] where t, u is Formula of L;
coherence
proof
set Y = [: Fin L, L :];
set Z = the set of all [{t, t '->' u}, u] where t, u is Formula of L;
for a st a in Z holds a in Y
proof
let a;
assume a in Z;
then consider t, u being Formula of L such that
A2: a = [{t, t '->' u}, u];
set w = {t, t '->' u};
t in L & t '->' u in L;
then w c= L & w is finite by TARSKI:def 2;
then w in Fin L by FINSUB_1:def 5;
hence thesis by A2, ZFMISC_1:def 2;
end;
then Z c= Y;
then reconsider Z as Relation of Fin L, L;
A10: dom Z c= Fin L & rng Z c= L by RELAT_1:def 18, RELAT_1:def 19;
then Z is finitary by FINSUB_1:def 5;
hence thesis by A10, PROOFS_1:def 2;
end;
end;
definition
let X, L;
func SCI-rules L -> Rule of L equals
SCI-MP L;
coherence;
end;
definition
let X, L;
mode Formula-sequence of L is FinSequence of L;
mode Formula-finset of L is finite Subset of L;
end;
reserve A, A1, A2 for non empty Subset of L;
reserve B, B1, B2 for Subset of L;
reserve P, P1, P2 for Formula-sequence of L;
reserve S, S1, S2 for Formula-finset of L;
definition
let X, L, t;
redefine func { t } -> Formula-finset of L; :: redefines { (TARSKI, definition)
coherence
proof
set S = { t };
S c= L
proof
let a;
assume a in S;
then a = t by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
end;
definition
let X, L, B, a;
attr a is B-provable means :Def60:
a is (B, SCI-rules L)-provable;
end;
registration
let X, L, B;
cluster B-axiomatic -> B-provable for object;
coherence;
end;
theorem Th20:
for X, L, B, t, u st t is B-provable & t '->' u is B-provable holds
u is B-provable
proof
let X, L, B, t, u;
set R = SCI-rules L;
assume that
A1: t is B-provable and
A2: t '->' u is B-provable;
set S = {t, t '->' u};
for a st a in S holds a in L
proof
let a;
assume a in S;
then a = t or a = t '->' u by TARSKI:def 2;
hence thesis;
end;
then S c= L;
then reconsider S as Formula-finset of L;
t is (B,R)-provable & t '->' u is (B,R)-provable by A1, A2;
then A10: for a st a in S holds B, R |- a by TARSKI:def 2;
[S, u] in SCI-rules L;
then u is (B,R)-provable by A10, PROOFS_1:11;
hence thesis;
end;
definition
let X, L, a;
attr a is L-prop-axiomatic means
a is (SCI-prop-axioms L)-axiomatic;
attr a is L-id-axiomatic means
a is (SCI-id-axioms L)-axiomatic;
attr a is L-SCI-axiomatic means
a is (SCI-axioms L)-axiomatic;
attr a is L-SCI-provable means
a is (SCI-axioms L)-provable;
end;
registration
let X, L;
cluster -> L-prop-axiomatic for Element of SCI-prop-axioms L;
coherence by PROOFS_1:def 9;
cluster -> L-id-axiomatic for Element of SCI-id-axioms L;
coherence by PROOFS_1:def 9;
cluster -> L-SCI-axiomatic for Element of SCI-axioms L;
coherence by PROOFS_1:def 9;
cluster L-SCI-axiomatic -> L-SCI-provable for object;
coherence;
cluster L-prop-axiomatic -> L-SCI-axiomatic for object;
coherence;
cluster L-id-axiomatic -> L-SCI-axiomatic for object;
coherence
proof
let a;
assume a is L-id-axiomatic;
then a in SCI-id-axioms L by PROOFS_1:def 9;
then a in SCI-axioms L by XBOOLE_0:def 3;
hence thesis;
end;
end;
registration
let X, L, t;
cluster t '==' t -> L-id-axiomatic;
coherence
proof
t '==' t in SCI-id-axioms L by Def10i;
hence thesis;
end;
let u;
cluster t '->' (u '->' t) -> L-prop-axiomatic;
coherence
proof
t '->' (u '->' t) in SCI-prop-axioms L by Def10p;
hence thesis;
end;
cluster (('not' t) '->' ('not' u)) '->' (u '->' t) -> L-prop-axiomatic;
coherence
proof
(('not' t) '->' ('not' u)) '->' (u '->' t) in SCI-prop-axioms L
by Def10p;
hence thesis;
end;
cluster (t '&' u) '->' ('not' (t '->' ('not' u))) -> L-prop-axiomatic;
coherence
proof
(t '&' u) '->' ('not' (t '->' ('not' u))) in SCI-prop-axioms L by Def10p;
hence thesis;
end;
cluster ('not' (t '->' ('not' u))) '->' (t '&' u) -> L-prop-axiomatic;
coherence
proof
('not' (t '->' ('not' u))) '->' (t '&' u) in SCI-prop-axioms L by Def10p;
hence thesis;
end;
cluster (t 'or' u) '->' (('not' t) '->' u) -> L-prop-axiomatic;
coherence
proof
(t 'or' u) '->' (('not' t) '->' u) in SCI-prop-axioms L by Def10p;
hence thesis;
end;
cluster (('not' t) '->' u) '->' (t 'or' u) -> L-prop-axiomatic;
coherence
proof
(('not' t) '->' u) '->' (t 'or' u) in SCI-prop-axioms L by Def10p;
hence thesis;
end;
cluster (t '<->' u) '->' ((t '->' u) '&' (u '->' t)) -> L-prop-axiomatic;
coherence
proof
(t '<->' u) '->' ((t '->' u) '&' (u '->' t)) in SCI-prop-axioms L
by Def10p;
hence thesis;
end;
cluster ((t '->' u) '&' (u '->' t)) '->' (t '<->' u) -> L-prop-axiomatic;
coherence
proof
((t '->' u) '&' (u '->' t)) '->' (t '<->' u) in SCI-prop-axioms L
by Def10p;
hence thesis;
end;
cluster (t '==' u) '->' (('not' t) '==' ('not' u)) -> L-id-axiomatic;
coherence
proof
(t '==' u) '->' (('not' t) '==' ('not' u)) in SCI-id-axioms L by Def10i;
hence thesis;
end;
cluster (t '==' u) '->' (t '->' u) -> L-id-axiomatic;
coherence
proof
(t '==' u) '->' (t '->' u) in SCI-id-axioms L by Def10i;
hence thesis;
end;
let v;
cluster (t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v))
-> L-prop-axiomatic;
coherence
proof
(t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v))
in SCI-prop-axioms L by Def10p;
hence thesis;
end;
let w;
let O be Element of SCI-binops;
cluster ((t '==' u) '&' (v '==' w)) '->'
(Polish-binOp(X, L, O).(t,v)
'==' Polish-binOp(X, L, O).(u,w)) -> L-id-axiomatic;
coherence
proof
set F = (t '==' u) '&' (v '==' w);
set b = Polish-binOp(X, L, O);
set G = b.(t,v) '==' b.(u,w);
O = '&&s' or O = '||s' or O = '->' or O = '<->' or O = '=='
by ENUMSET1:def 3;
then G = (t '&' v) '==' (u '&' w)
or G = (t 'or' v) '==' (u 'or' w)
or G = (t '->' v) '==' (u '->' w)
or G = (t '<->' v) '==' (u '<->' w)
or G = (t '==' v) '==' (u '==' w);
then F '->' G in SCI-id-axioms L by Def10i;
hence thesis;
end;
end;
registration
let X, L;
cluster L-prop-axiomatic for Formula of L;
existence
proof
take x.(1,L) '->' (x.(1,L) '->' x.(1,L));
thus thesis;
end;
cluster L-id-axiomatic for Formula of L;
existence
proof
take x.(1,L) '==' x.(1,L);
thus thesis;
end;
end;
reserve C for (SCI-prop-axioms L)-extending Subset of L;
Lm20:
for X, L, C, t st t is L-prop-axiomatic holds t is C-provable;
registration
let X, L;
cluster L-prop-axiomatic -> (SCI-prop-axioms L)-provable for Formula of L;
coherence;
let C;
cluster non C-provable -> non (SCI-prop-axioms L)-provable for Formula of L;
coherence;
cluster C-provable for Formula of L;
existence
proof
take the Element of SCI-prop-axioms L;
thus thesis;
end;
end;
registration
let X, L, C, t;
let u be C-provable Formula of L;
cluster t '->' u -> C-provable;
coherence
proof
u '->' (t '->' u) is C-provable;
hence thesis by Th20;
end;
end;
Lm21:
for X, L, C, t, u, v st u '->' v is C-provable holds
(t '->' u) '->' (t '->' v) is C-provable
proof
let X, L, C, t, u, v;
assume A1: u '->' v is C-provable;
(t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v))
is C-provable;
hence (t '->' u) '->' (t '->' v) is C-provable by A1, Th20;
end;
theorem Th21:
for X, L, C, t, u, v st t '->' u is C-provable & u '->' v is C-provable
holds t '->' v is C-provable
proof
let X, L, C, t, u, v;
assume that
A2: t '->' u is C-provable and
A3: u '->' v is C-provable;
(t '->' u) '->' (t '->' v) is C-provable by A3, Lm21;
hence thesis by A2, Th20;
end;
theorem Th22:
for X, L, C, t holds t '->' t is C-provable
proof
let X, L, C, t;
set F1 = t '->' t;
set F2 = t '->' (F1 '->' t);
set F3 = t '->' F1;
F2 is C-provable & F2 '->' (F3 '->' F1) is C-provable;
then F3 is C-provable & F3 '->' F1 is C-provable by Th20;
hence F1 is C-provable by Th20;
end;
registration
let X, L, t;
cluster t '->' t -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th22;
end;
end;
registration
let X, L, C;
let t be C-provable Formula of L;
let u;
cluster (t '->' u) '->' u -> C-provable;
coherence
proof
set F = t '->' u;
(F '->' F) '->' ((F '->' t) '->' (F '->' u)) is C-provable;
then (F '->' t) '->' (F '->' u) is C-provable by Th20;
hence thesis by Th20;
end;
end;
registration
let X, L, C, t;
let u be C-provable Formula of L;
let v;
cluster (t '->' (u '->' v)) '->' (t '->' v) -> C-provable;
coherence
proof
set F1 = (t '->' (u '->' v));
set F2 = ((t '->' u) '->' (t '->' v));
set F3 = F1 '->' (t '->' u);
set F4 = F1 '->' (t '->' v);
(F1 '->' F2) '->' (F3 '->' F4) is C-provable;
then F3 '->' F4 is C-provable by Th20;
hence thesis by Th20;
end;
end;
Lm23:
for X, L, C, t, u holds (t '->' (t '->' u)) '->' (t '->' u) is C-provable
proof
let X, L, C, t, u;
set F1 = t '->' (t '->' u);
set F2 = t '->' t;
set F3 = F1 '->' (F2 '->' (t '->' u));
A1: F3 is C-provable;
F2 is C-provable;
then F3 '->' (F1 '->' (t '->' u)) is C-provable;
hence thesis by A1, Th20;
end;
theorem Th23:
for X, L, C, t, u st t '->' (t '->' u) is C-provable
holds t '->' u is C-provable
proof
let X, L, C, t, u;
assume A1: t '->' (t '->' u) is C-provable;
(t '->' (t '->' u)) '->' (t '->' u) is C-provable by Lm23;
hence thesis by A1, Th20;
end;
theorem Th24:
for X, L, C, t, u, v st t '->' (u '->' v) is C-provable
holds u '->' (t '->' v) is C-provable
proof
let X, L, C, t, u, v;
assume A1: t '->' (u '->' v) is C-provable;
(t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v))
is C-provable;
then A2: (t '->' u) '->' (t '->' v) is C-provable by A1, Th20;
u '->' (t '->' u) is C-provable;
hence thesis by A2, Th21;
end;
registration
let X, L, t, u;
cluster (t '->' (t '->' u)) '->' (t '->' u)
-> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Lm23;
end;
end;
Lm24:
for X, L, C, t, u st ('not' t) '->' ('not' u) is C-provable
holds u '->' t is C-provable
proof
let X, L, C, t, u;
assume A1: ('not' t) '->' ('not' u) is C-provable;
(('not' t) '->' ('not' u)) '->' (u '->' t) is C-provable;
hence thesis by A1, Th20;
end;
Lm25:
for X, L, C, t, u, v st t '->' (('not' u) '->' ('not' v)) is C-provable
holds t '->' (v '->' u) is C-provable
proof
let X, L, C, t, u, v;
assume A1: t '->' (('not' u) '->' ('not' v)) is C-provable;
(('not' u) '->' ('not' v)) '->' (v '->' u) is C-provable;
hence thesis by A1, Th21;
end;
theorem Th26:
for X, L, C, t holds ('not' 'not' t) '->' t is C-provable
proof
let X, L, C, t;
set F = 'not' 'not' t;
F '->' (('not' 'not' F) '->' F) is L-prop-axiomatic;
then F '->' (('not' t) '->' ('not' F)) is C-provable by Lm20, Lm25;
then A1: F '->' (F '->' t) is C-provable by Lm25;
(F '->' (F '->' t)) '->' (F '->' t) is C-provable;
hence thesis by A1, Th20;
end;
theorem Th27:
for X, L, C, t holds t '->' ('not' 'not' t) is C-provable
proof
let X, L, C, t;
('not' 'not' 'not' t) '->' ('not' t) is C-provable by Th26;
hence thesis by Lm24;
end;
Lm26:
for X, L, C, t, u, v st t '->' u is C-provable holds
(u '->' v) '->' (t '->' v) is C-provable
proof
let X, L, C, t, u, v;
assume A1: t '->' u is C-provable;
A2: (u '->' v) '->' (t '->' (u '->' v)) is C-provable;
(t '->' (u '->' v)) '->' ((t '->' u) '->' (t '->' v)) is C-provable;
then (u '->' v) '->' ((t '->' u) '->' (t '->' v)) is C-provable
by A2, Th21;
then (t '->' u) '->' ((u '->' v) '->' (t '->' v)) is C-provable by Th24;
hence thesis by A1, Th20;
end;
Lm27:
for X, L, C, t, u holds (t '->' u) '->' (('not' u) '->' ('not' t))
is C-provable
proof
let X, L, C, t, u;
A1: (('not' 'not' t) '->' ('not' 'not' u)) '->' (('not' u) '->' ('not' t))
is C-provable;
('not' 'not' t) '->' t is C-provable by Th26;
then A2: (t '->' u) '->' (('not' 'not' t) '->' u) is C-provable by Lm26;
u '->' ('not' 'not' u) is C-provable by Th27;
then (('not' 'not' t) '->' u) '->' (('not' 'not' t) '->' ('not' 'not' u))
is C-provable by Lm21;
then (t '->' u) '->' (('not' 'not' t) '->' ('not' 'not' u)) is C-provable
by A2, Th21;
hence thesis by A1, Th21;
end;
registration
let X, L, t;
cluster ('not' 'not' t) '->' t -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th26;
end;
cluster t '->' ('not' 'not' t) -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th27;
end;
let u;
cluster (t '->' u) '->' (('not' u) '->' ('not' t))
-> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Lm27;
end;
end;
theorem Th28:
for X, L, C, t, u holds ('not' t) '->' u is C-provable
implies ('not' u) '->' t is C-provable
proof
let X, L, C, t, u;
assume A1: ('not' t) '->' u is C-provable;
u '->' ('not' 'not' u) is C-provable;
then ('not' t) '->' ('not' 'not' u) is C-provable by A1, Th21;
hence thesis by Lm24;
end;
theorem
for X, L, C, t, u holds t '->' ('not' u) is C-provable
implies u '->' ('not' t) is C-provable
proof
let X, L, C, t, u;
assume A1: t '->' ('not' u) is C-provable;
('not' 'not' t) '->' t is C-provable;
then ('not' 'not' t) '->' ('not' u) is C-provable by A1, Th21;
hence thesis by Lm24;
end;
theorem Th30:
for X, L, C, t, u holds ('not' t) '->' ('not' u) is C-provable
iff u '->' t is C-provable
proof
let X, L, C, t, u;
thus ('not' t) '->' ('not' u) is C-provable implies u '->' t is C-provable
by Lm24;
assume A1: u '->' t is C-provable;
('not' 'not' u) '->' u is C-provable;
then A2: ('not' 'not' u) '->' t is C-provable by A1, Th21;
t '->' ('not' 'not' t) is C-provable;
then ('not' 'not' u) '->' ('not' 'not' t) is C-provable by A2, Th21;
hence thesis by Lm24;
end;
registration
let X, L, C, t;
let u be C-provable Formula of L;
cluster ('not' u) '->' t -> C-provable;
coherence
proof
('not' t) '->' u is C-provable;
hence thesis by Th28;
end;
end;
registration
let X, L, t;
cluster t '->' t -> L-SCI-provable;
coherence;
cluster t '->' ('not' 'not' t) -> L-SCI-provable;
coherence;
cluster ('not' 'not' t) '->' t -> L-SCI-provable;
coherence;
let u be L-SCI-provable Formula of L;
cluster t '->' u -> L-SCI-provable;
coherence
proof
u is L-SCI-provable & u '->' (t '->' u) is L-SCI-provable;
hence thesis;
end;
end;
theorem Th32:
for X, L, C, t, u holds ('not' t) '->' (t '->' u) is C-provable
proof
let X, L, C, t, u;
('not' t) '->' (('not' u) '->' ('not' t)) in SCI-prop-axioms L by Def10p;
hence thesis by Lm20, Lm25;
end;
registration
let X, L, t, u;
cluster ('not' t) '->' (t '->' u) -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th32;
end;
cluster t '->' (('not' t) '->' u) -> (SCI-prop-axioms L)-provable;
coherence
proof
A1: SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
A2: t '->' ('not' 'not' t) is (SCI-prop-axioms L)-provable;
('not' 'not' t) '->' (('not' t) '->' u) is (SCI-prop-axioms L)-provable;
hence thesis by A1, A2, Th21;
end;
end;
theorem
for X, L, C, t, u st 'not' t is C-provable holds t '->' u is C-provable
proof
let X, L, C, t, u;
assume 'not' t is C-provable;
then ('not' u) '->' ('not' t) is C-provable;
hence thesis by Lm24;
end;
registration
let X, L, t, u;
cluster t '->' ((t '->' u) '->' u) -> (SCI-prop-axioms L)-provable;
coherence
proof
set C = SCI-prop-axioms L;
A1: C is Extension of C by PROOFS_1:def 12;
(t '->' u) '->' (t '->' u) is C-provable;
hence thesis by A1, Th24;
end;
end;
theorem Th36:
for X, L, C, t, u, v holds t '->' (u '->' v) is C-provable
iff t '->' (('not' v) '->' ('not' u)) is C-provable
proof
let X, L, C, t, u, v;
thus t '->' (u '->' v) is C-provable
implies t '->' (('not' v) '->' ('not' u)) is C-provable
proof
set F1 = v '->' ('not' 'not' v);
set F2 = u '->' ('not' 'not' v);
assume A1: t '->' (u '->' v) is C-provable;
A2: F1 is C-provable;
(u '->' F1) '->' ((u '->' v) '->' F2) is C-provable;
then (u '->' v) '->' F2 is C-provable by A2, Th20;
then t '->' F2 is C-provable by A1, Th21;
then A4: u '->' (t '->' ('not' 'not' v)) is C-provable by Th24;
('not' 'not' u) '->' u is C-provable;
then ('not' 'not' u) '->' (t '->' ('not' 'not' v)) is C-provable
by A4, Th21;
then t '->' (('not' 'not' u) '->' ('not' 'not' v)) is C-provable by Th24;
hence thesis by Lm25;
end;
thus thesis by Lm25;
end;
theorem Th40:
for X, L, C, t, u holds
(t '&' u) '->' t is C-provable & (t '&' u) '->' u is C-provable
proof
let X, L, C, t, u;
set F = 'not' (t '->' ('not' u));
A1: (t '&' u) '->' F is C-provable;
('not' t) '->' (t '->' ('not' u)) is C-provable;
then F '->' t is C-provable by Th28;
hence (t '&' u) '->' t is C-provable by A1, Th21;
('not' u) '->' (t '->' ('not' u)) in SCI-prop-axioms L by Def10p;
then F '->' u is C-provable by Lm20, Th28;
hence thesis by A1, Th21;
end;
theorem Th41:
for X, L, C, t, u holds
t '->' (u '->' (t '&' u)) is C-provable
proof
let X, L, C, t, u;
set G = t '->' ('not' u);
('not' G) '->' (t '&' u) is L-prop-axiomatic;
then A1: ('not' (t '&' u)) '->' ('not' 'not' G) is C-provable by Lm20, Th30;
('not' 'not' G) '->' G is C-provable;
then ('not' (t '&' u)) '->' G is C-provable by Th21, A1;
then t '->' (('not' (t '&' u)) '->' ('not' u)) is C-provable by Th24;
hence thesis by Th36;
end;
registration
let X, L, t, u;
cluster (t '&' u) '->' t -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th40;
end;
cluster (t '&' u) '->' u -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th40;
end;
cluster t '->' (u '->' (t '&' u)) -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th41;
end;
end;
registration
let X, L, C, t;
let u be C-provable Formula of L;
cluster t '->' (t '&' u) -> C-provable;
coherence
proof
t '->' (u '->' (t '&' u)) is C-provable;
then u '->' (t '->' (t '&' u)) is C-provable by Th24;
hence thesis by Th20;
end;
cluster t '->' (u '&' t) -> C-provable;
coherence
proof
u '->' (t '->' (u '&' t)) is C-provable;
hence thesis by Th20;
end;
end;
registration
let X, L, C;
let t, u be C-provable Formula of L;
cluster t '&' u -> C-provable;
coherence
proof
u '->' (t '&' u) is C-provable;
hence thesis by Th20;
end;
end;
theorem
for X, L, C, t, u, v holds
(t '&' u) '->' v is C-provable iff t '->' (u '->' v) is C-provable
proof
let X, L, C, t, u, v;
thus (t '&' u) '->' v is C-provable
implies t '->' (u '->' v) is C-provable
proof
assume A1: (t '&' u) '->' v is C-provable;
(u '->' ((t '&' u) '->' v)) '->' ((u '->' (t '&' u)) '->' (u '->' v))
is C-provable;
then A2: (u '->' (t '&' u)) '->' (u '->' v) is C-provable by A1, Th20;
(t '->' ((u '->' (t '&' u)) '->' (u '->' v))) '->'
((t '->' (u '->' (t '&' u))) '->' (t '->' (u '->' v)))
is C-provable;
then A3: (t '->' (u '->' (t '&' u))) '->' (t '->' (u '->' v))
is C-provable by A2, Th20;
(t '->' (u '->' (t '&' u))) is C-provable;
hence thesis by A3, Th20;
end;
assume A10: t '->' (u '->' v) is C-provable;
(t '&' u) '->' t is C-provable;
then (t '&' u) '->' (u '->' v) is C-provable by A10, Th21;
then A11: u '->' ((t '&' u) '->' v) is C-provable by Th24;
(t '&' u) '->' u is C-provable;
then (t '&' u) '->' ((t '&' u) '->' v) is C-provable by A11, Th21;
hence thesis by Th23;
end;
theorem Th43:
for X, L, C, t, u holds
t '&' u is C-provable iff t is C-provable & u is C-provable
proof
let X, L, C, t, u;
thus t '&' u is C-provable implies t is C-provable & u is C-provable
proof
assume A1: t '&' u is C-provable;
(t '&' u) '->' t is C-provable & (t '&' u) '->' u is C-provable;
hence thesis by A1, Th20;
end;
thus thesis;
end;
theorem Th44:
for X, L, C, t, u, v holds t '->' (u '&' v) is C-provable iff
t '->' u is C-provable & t '->' v is C-provable
proof
let X, L, C, t, u, v;
thus t '->' (u '&' v) is C-provable implies
t '->' u is C-provable & t '->' v is C-provable
proof
assume A1: t '->' (u '&' v) is C-provable;
(u '&' v) '->' u is C-provable;
hence t '->' u is C-provable by A1, Th21;
(u '&' v) '->' v is C-provable;
hence thesis by A1, Th21;
end;
assume that A2: t '->' u is C-provable and A3: t '->' v is C-provable;
u '->' (v '->' (u '&' v)) is C-provable;
then t '->' (v '->' (u '&' v)) is C-provable by A2, Th21;
then v '->' (t '->' (u '&' v)) is C-provable by Th24;
then A5: t '->' (t '->' (u '&' v)) is C-provable by A3, Th21;
(t '->' (t '->' (u '&' v))) '->' (t '->' (u '&' v)) is C-provable;
hence thesis by A5, Th20;
end;
theorem Th45:
for X, L, C, t, u holds
t '->' (t 'or' u) is C-provable & u '->' (t 'or' u) is C-provable
proof
let X, L, C, t, u;
A1: (('not' t) '->' u) '->' (t 'or' u) is C-provable;
t '->' (('not' t) '->' u) is C-provable;
hence t '->' (t 'or' u) is C-provable by A1, Th21;
u '->' (('not' t) '->' u) is C-provable;
hence thesis by A1, Th21;
end;
registration
let X, L, t;
cluster t 'or' ('not' t) -> (SCI-prop-axioms L)-provable;
coherence
proof
(('not' t) '->' ('not' t)) '->' (t 'or' ('not' t))
is (SCI-prop-axioms L)-provable;
hence thesis by Th20;
end;
let u;
cluster t '->' (t 'or' u) -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th45;
end;
cluster u '->' (t 'or' u) -> (SCI-prop-axioms L)-provable;
coherence
proof
SCI-prop-axioms L is Extension of SCI-prop-axioms L by PROOFS_1:def 12;
hence thesis by Th45;
end;
end;
registration
let X, L, C;
let t be C-provable Formula of L;
let u;
cluster t 'or' u -> C-provable;
coherence
proof
t '->' (t 'or' u) is C-provable;
hence thesis by Th20;
end;
cluster u 'or' t -> C-provable;
coherence
proof
t '->' (u 'or' t) is C-provable;
hence thesis by Th20;
end;
end;
theorem Th46:
for X, L, C, t holds (('not' t) '->' t) '->' t is C-provable
proof
let X, L, C, t;
set u = the C-provable Formula of L;
(('not' t) '->' (t '->' ('not' u))) '->'
((('not' t) '->' t) '->' (('not' t) '->' ('not' u))) is C-provable;
then (('not' t) '->' t) '->' (('not' t) '->' ('not' u)) is C-provable
by Th20;
then A2: (('not' t) '->' t) '->' (u '->' t) is C-provable by Lm25;
(u '->' t) '->' t is C-provable;
hence thesis by A2, Th21;
end;
theorem Th47:
for X, L, C, t, u, v holds (t 'or' u) '->' v is C-provable
iff t '->' v is C-provable & u '->' v is C-provable
proof
let X, L, C, t, u, v;
thus (t 'or' u) '->' v is C-provable
implies t '->' v is C-provable & u '->' v is C-provable
proof
assume A1: (t 'or' u) '->' v is C-provable;
t '->' (t 'or' u) is C-provable;
hence t '->' v is C-provable by A1, Th21;
u '->' (t 'or' u) is C-provable;
hence u '->' v is C-provable by A1, Th21;
end;
assume that A10: t '->' v is C-provable and A11: u '->' v is C-provable;
A12: (t 'or' u) '->' (('not' t) '->' u) is C-provable;
A13: (('not' t) '->' u) '->' (('not' t) '->' v) is C-provable
by A11, Lm21;
('not' v) '->' ('not' t) is C-provable by A10, Th30;
then (('not' t) '->' v) '->' (('not' v) '->' v) is C-provable by Lm26;
then (('not' t) '->' u) '->' (('not' v) '->' v) is C-provable
by A13, Th21;
then A15: (t 'or' u) '->' (('not' v) '->' v) is C-provable by A12, Th21;
(('not' v) '->' v) '->' v is C-provable by Th46;
hence thesis by A15, Th21;
end;
theorem
for X, L, C, t, u, v, w st t '->' v is C-provable & u '->' w is C-provable
holds (t 'or' u) '->' (v 'or' w) is C-provable
& (t '&' u) '->' (v '&' w) is C-provable
proof
let X, L, C, t, u, v, w;
assume that A1: t '->' v is C-provable and A2: u '->' w is C-provable;
v '->' (v 'or' w) is C-provable;
then A3: t '->' (v 'or' w) is C-provable by A1, Th21;
w '->' (v 'or' w) is C-provable;
then u '->' (v 'or' w) is C-provable by A2, Th21;
hence (t 'or' u) '->' (v 'or' w) is C-provable by A3, Th47;
(t '&' u) '->' t is C-provable;
then A5: (t '&' u) '->' v is C-provable by A1, Th21;
(t '&' u) '->' u is C-provable;
then (t '&' u) '->' w is C-provable by A2, Th21;
hence thesis by A5, Th44;
end;
Lm50:
for X, L, C, t, u st u is (C \/ {t})-provable
holds t '->' u is C-provable
proof
let X, L, C, t, u;
set D = C \/ {t};
set R = SCI-rules L;
defpred P[object] means ex v st $1 = v & t '->' v is C-provable;
A4: for a st a in D holds P[a]
proof
let a;
assume A5: a in D;
then a is (C \/ {t})-axiomatic;
then A6: a is C-axiomatic or a = t by PROOFS_1:6;
reconsider v = a as Formula of L by A5;
t '->' v is C-provable by A6;
hence thesis;
end;
A10: for y, a st [y,a] in R & for b st b in y holds P[b] holds P[a]
proof
let y, a;
assume that A12: [y,a] in R and A13: for b st b in y holds P[b];
consider v, w being Formula of L such that
A14: [y,a] = [{v, v '->' w}, w] by A12;
A15: y = {v, v '->' w} & a = w by A14, XTUPLE_0:1;
v in y & v '->' w in y by A15, TARSKI:def 2;
then A17: P[v] & P[v '->' w] by A13;
(t '->' (v '->' w)) '->' ((t '->' v) '->' (t '->' w)) is C-provable;
then (t '->' v) '->' (t '->' w) is C-provable by A17, Th20;
hence P[a] by A15, A17, Th20;
end;
A20: for a st D, R |- a holds P[a] from PROOFS_1:sch 3(A4, A10);
assume u is D-provable;
then P[u] by A20, PROOFS_1:def 11;
hence thesis;
end;
theorem
for X, L, C, t, u holds
t '->' u is C-provable iff u is (C \/ {t})-provable
proof
let X, L, C, t, u;
set D = C \/ {t};
set R = SCI-rules L;
A1: D is C-extending & R is R-extending by XBOOLE_1:7;
thus t '->' u is C-provable implies u is D-provable
proof
assume t '->' u is C-provable;
then A2: t '->' u is D-provable by A1;
t is D-axiomatic by PROOFS_1:6;
hence thesis by A2, Th20;
end;
thus thesis by Lm50;
end;
reserve D for (SCI-axioms L)-extending Subset of L;
registration
let X, L, D;
cluster non D-provable -> non L-SCI-provable for Formula of L;
coherence by Def60;
cluster D-provable for Formula of L;
existence
proof
take x.(1,L) '==' x.(1,L);
thus thesis;
end;
end;
theorem Th60:
for X, L, D, t, u st t '==' u is D-provable
holds t '->' u is D-provable
proof
let X, L, D, t, u;
assume A2: t '==' u is D-provable;
(t '==' u) '->' (t '->' u) is D-provable;
hence thesis by A2, Th20;
end;
theorem Th61:
for X, L, D, t, u st t '==' u is D-provable
holds ('not' t) '==' ('not' u) is D-provable
proof
let X, L, D, t, u;
assume A2: t '==' u is D-provable;
(t '==' u) '->' (('not' t) '==' ('not' u)) is D-provable;
hence thesis by A2, Th20;
end;
theorem Th62:
for X, L, D, t, u holds (t '==' u) '->' (u '==' t) is D-provable
proof
let X, L, D, t, u;
set F1 = ((t '==' u) '&' (t '==' t)) '->' ((t '==' t) '==' (u '==' t));
F1 in SCI-id-axioms L by Def10i;
then A1: F1 is D-provable;
A2: t '==' t is D-provable;
then (t '==' u) '->' ((t '==' u) '&' (t '==' t)) is D-provable;
then A3: (t '==' u) '->' ((t '==' t) '==' (u '==' t)) is D-provable
by A1, Th21;
((t '==' t) '==' (u '==' t)) '->' ((t '==' t) '->' (u '==' t)) is D-provable;
then (t '==' u) '->' ((t '==' t) '->' (u '==' t)) is D-provable
by A3, Th21;
then (t '==' t) '->' ((t '==' u) '->' (u '==' t)) is D-provable
by Th24;
hence thesis by A2, Th20;
end;
theorem Th63:
for X, L, D, t, u st t '==' u is D-provable holds u '==' t is D-provable
proof
let X, L, D, t, u;
assume A1: t '==' u is D-provable;
(t '==' u) '->' (u '==' t) is D-provable by Th62;
hence thesis by A1, Th20;
end;
theorem
for X, L, D, t, u, v holds
((t '==' u) '&' (v '==' u)) '->' (t '==' v) is D-provable
proof
let X, L, D, t, u, v;
((t '==' u) '&' (v '==' u)) '->' ((t '==' v) '==' (u '==' u))
in SCI-id-axioms L by Def10i;
then A1: ((t '==' u) '&' (v '==' u)) '->' ((t '==' v) '==' (u '==' u))
is D-provable;
((t '==' v) '==' (u '==' u)) '->' ((u '==' u) '==' (t '==' v)) is D-provable
by Th62;
then A2: ((t '==' u) '&' (v '==' u)) '->' ((u '==' u) '==' (t '==' v))
is D-provable by A1, Th21;
((u '==' u) '==' (t '==' v)) '->' ((u '==' u) '->' (t '==' v)) is D-provable;
then ((t '==' u) '&' (v '==' u)) '->' ((u '==' u) '->' (t '==' v))
is D-provable by A2, Th21;
then A3: (u '==' u) '->' (((t '==' u) '&' (v '==' u)) '->' (t '==' v))
is D-provable by Th24;
u '==' u is D-provable;
hence thesis by A3, Th20;
end;
theorem
for X, L, D, t, u st t is D-provable & t => u is D-provable
holds u is D-provable
proof
let X, L, D, t, u;
assume that A1: t is D-provable and A2: t => u is D-provable;
t '->' (t '&' u) is D-provable by A2, Th60;
then t '&' u is D-provable by A1, Th20;
hence thesis by Th43;
end;
theorem Th66:
for X, L, D, t, u, v, w st t '==' u is D-provable & v '==' w is D-provable
holds (t '&' v) '==' (u '&' w) is D-provable &
(t '&' v) '->' (u '&' w) is D-provable &
(t '&' v is D-provable implies u '&' w is D-provable) &
(t 'or' v) '==' (u 'or' w) is D-provable &
(t 'or' v) '->' (u 'or' w) is D-provable &
(t 'or' v is D-provable implies u 'or' w is D-provable) &
(t '->' v) '==' (u '->' w) is D-provable &
(t '->' v) '->' (u '->' w) is D-provable &
(t '->' v is D-provable implies u '->' w is D-provable) &
(t '<->' v) '==' (u '<->' w) is D-provable &
(t '<->' v) '->' (u '<->' w) is D-provable &
(t '<->' v is D-provable implies u '<->' w is D-provable) &
(t '==' v) '==' (u '==' w) is D-provable &
(t '==' v) '->' (u '==' w) is D-provable &
(t '==' v is D-provable implies u '==' w is D-provable) &
(t => v) '==' (u => w) is D-provable &
(t => v) '->' (u => w) is D-provable &
(t => v is D-provable implies u => w is D-provable)
proof
let X, L, D, t, u, v, w;
set F = (t '==' u) '&' (v '==' w);
assume A1: t '==' u is D-provable & v '==' w is D-provable;
F '->' ((t '&' v) '==' (u '&' w)) in SCI-id-axioms L by Def10i;
then F '->' ((t '&' v) '==' (u '&' w)) is D-provable;
hence A2: (t '&' v) '==' (u '&' w) is D-provable by A1, Th20;
hence (t '&' v) '->' (u '&' w) is D-provable by Th60;
hence t '&' v is D-provable implies u '&' w is D-provable by Th20;
F '->' ((t 'or' v) '==' (u 'or' w)) in SCI-id-axioms L by Def10i;
then F '->' ((t 'or' v) '==' (u 'or' w)) is D-provable;
hence (t 'or' v) '==' (u 'or' w) is D-provable by A1, Th20;
hence (t 'or' v) '->' (u 'or' w) is D-provable by Th60;
hence t 'or' v is D-provable implies u 'or' w is D-provable by Th20;
F '->' ((t '->' v) '==' (u '->' w)) in SCI-id-axioms L by Def10i;
then F '->' ((t '->' v) '==' (u '->' w)) is D-provable;
hence (t '->' v) '==' (u '->' w) is D-provable by A1, Th20;
hence (t '->' v) '->' (u '->' w) is D-provable by Th60;
hence t '->' v is D-provable implies u '->' w is D-provable by Th20;
F '->' ((t '<->' v) '==' (u '<->' w)) in SCI-id-axioms L by Def10i;
then F '->' ((t '<->' v) '==' (u '<->' w)) is D-provable;
hence (t '<->' v) '==' (u '<->' w) is D-provable by A1, Th20;
hence (t '<->' v) '->' (u '<->' w) is D-provable by Th60;
hence t '<->' v is D-provable implies u '<->' w is D-provable by Th20;
F '->' ((t '==' v) '==' (u '==' w)) in SCI-id-axioms L by Def10i;
then F '->' ((t '==' v) '==' (u '==' w)) is D-provable;
hence (t '==' v) '==' (u '==' w) is D-provable by A1, Th20;
hence (t '==' v) '->' (u '==' w) is D-provable by Th60;
hence t '==' v is D-provable implies u '==' w is D-provable by Th20;
set G = (t '==' u) '&' ((t '&' v) '==' (u '&' w));
G '->' ((t => v) '==' (u => w)) in SCI-id-axioms L by Def10i;
then G '->' ((t => v) '==' (u => w)) is D-provable;
hence (t => v) '==' (u => w) is D-provable by A1, A2, Th20;
hence (t => v) '->' (u => w) is D-provable by Th60;
hence t => v is D-provable implies u => w is D-provable by Th20;
end;
theorem Th67:
for X, L, D, t, u, v holds
(t '==' u) '->' ((t '&' v) '==' (u '&' v)) is D-provable &
(t '==' u) '->' ((v '&' t) '==' (v '&' u)) is D-provable &
(t '==' u) '->' ((t 'or' v) '==' (u 'or' v)) is D-provable &
(t '==' u) '->' ((v 'or' t) '==' (v 'or' u)) is D-provable &
(t '==' u) '->' ((t '->' v) '==' (u '->' v)) is D-provable &
(t '==' u) '->' ((v '->' t) '==' (v '->' u)) is D-provable &
(t '==' u) '->' ((t '<->' v) '==' (u '<->' v)) is D-provable &
(t '==' u) '->' ((v '<->' t) '==' (v '<->' u)) is D-provable &
(t '==' u) '->' ((t '==' v) '==' (u '==' v)) is D-provable &
(t '==' u) '->' ((v '==' t) '==' (v '==' u)) is D-provable &
(t '==' u) '->' ((t => v) '==' (u => v)) is D-provable &
(t '==' u) '->' ((v => t) '==' (v => u)) is D-provable
proof
let X, L, D, t, u, v;
set U = t '==' u;
set V = v '==' v;
V is D-provable;
then A1: U '->' (U '&' V) is D-provable & U '->' (V '&' U) is D-provable;
(U '&' V) '->' ((t '&' v) '==' (u '&' v)) in SCI-id-axioms L by Def10i;
then (U '&' V) '->' ((t '&' v) '==' (u '&' v)) is D-provable;
hence A2: U '->' ((t '&' v) '==' (u '&' v)) is D-provable by A1, Th21;
(V '&' U) '->' ((v '&' t) '==' (v '&' u)) in SCI-id-axioms L by Def10i;
then (V '&' U) '->' ((v '&' t) '==' (v '&' u)) is D-provable;
hence A3: U '->' ((v '&' t) '==' (v '&' u)) is D-provable by A1, Th21;
(U '&' V) '->' ((t 'or' v) '==' (u 'or' v)) in SCI-id-axioms L by Def10i;
then (U '&' V) '->' ((t 'or' v) '==' (u 'or' v)) is D-provable;
hence U '->' ((t 'or' v) '==' (u 'or' v)) is D-provable by A1, Th21;
(V '&' U) '->' ((v 'or' t) '==' (v 'or' u)) in SCI-id-axioms L by Def10i;
then (V '&' U) '->' ((v 'or' t) '==' (v 'or' u)) is D-provable;
hence U '->' ((v 'or' t) '==' (v 'or' u)) is D-provable by A1, Th21;
(U '&' V) '->' ((t '->' v) '==' (u '->' v)) in SCI-id-axioms L by Def10i;
then (U '&' V) '->' ((t '->' v) '==' (u '->' v)) is D-provable;
hence U '->' ((t '->' v) '==' (u '->' v)) is D-provable by A1, Th21;
(V '&' U) '->' ((v '->' t) '==' (v '->' u)) in SCI-id-axioms L by Def10i;
then (V '&' U) '->' ((v '->' t) '==' (v '->' u)) is D-provable;
hence U '->' ((v '->' t) '==' (v '->' u)) is D-provable by A1, Th21;
(U '&' V) '->' ((t '<->' v) '==' (u '<->' v)) in SCI-id-axioms L by Def10i;
then (U '&' V) '->' ((t '<->' v) '==' (u '<->' v)) is D-provable;
hence U '->' ((t '<->' v) '==' (u '<->' v)) is D-provable by A1, Th21;
(V '&' U) '->' ((v '<->' t) '==' (v '<->' u)) in SCI-id-axioms L by Def10i;
then (V '&' U) '->' ((v '<->' t) '==' (v '<->' u)) is D-provable;
hence U '->' ((v '<->' t) '==' (v '<->' u)) is D-provable by A1, Th21;
(U '&' V) '->' ((t '==' v) '==' (u '==' v)) in SCI-id-axioms L by Def10i;
then (U '&' V) '->' ((t '==' v) '==' (u '==' v)) is D-provable;
hence U '->' ((t '==' v) '==' (u '==' v)) is D-provable by A1, Th21;
(V '&' U) '->' ((v '==' t) '==' (v '==' u)) in SCI-id-axioms L by Def10i;
then (V '&' U) '->' ((v '==' t) '==' (v '==' u)) is D-provable;
hence U '->' ((v '==' t) '==' (v '==' u)) is D-provable by A1, Th21;
set F = (t '&' v) '==' (u '&' v);
U '->' U is D-provable;
then A11: U '->' (U '&' F) is D-provable by A2, Th44;
(U '&' F) '->' ((t => v) '==' (u => v)) in SCI-id-axioms L by Def10i;
then (U '&' F) '->' ((t => v) '==' (u => v)) is D-provable;
hence U '->' ((t => v) '==' (u => v)) is D-provable by A11, Th21;
set G = (v '&' t) '==' (v '&' u);
U '->' V is D-provable;
then A12: U '->' (V '&' G) is D-provable by A3, Th44;
(V '&' G) '->' ((v => t) '==' (v => u)) in SCI-id-axioms L by Def10i;
then (V '&' G) '->' ((v => t) '==' (v => u)) is D-provable;
hence U '->' ((v => t) '==' (v => u)) is D-provable by A12, Th21;
end;
theorem Th68:
for X, L, D, t, u, v st t '==' u is D-provable holds
(t is D-provable iff u is D-provable) &
(t '&' v) '==' (u '&' v) is D-provable &
(t '&' v) '->' (u '&' v) is D-provable &
((t '&' v) is D-provable implies (u '&' v) is D-provable) &
(v '&' t) '==' (v '&' u) is D-provable &
(v '&' t) '->' (v '&' u) is D-provable &
((v '&' t) is D-provable implies (v '&' u) is D-provable) &
(t 'or' v) '==' (u 'or' v) is D-provable &
(t 'or' v) '->' (u 'or' v) is D-provable &
((t 'or' v) is D-provable implies (u 'or' v) is D-provable) &
(v 'or' t) '==' (v 'or' u) is D-provable &
(v 'or' t) '->' (v 'or' u) is D-provable &
((v 'or' t) is D-provable implies (v 'or' u) is D-provable) &
(t '->' v) '==' (u '->' v) is D-provable &
(t '->' v) '->' (u '->' v) is D-provable &
((t '->' v) is D-provable implies (u '->' v) is D-provable) &
(v '->' t) '==' (v '->' u) is D-provable &
(v '->' t) '->' (v '->' u) is D-provable &
((v '->' t) is D-provable implies (v '->' u) is D-provable) &
(t '<->' v) '==' (u '<->' v) is D-provable &
(t '<->' v) '->' (u '<->' v) is D-provable &
((t '<->' v) is D-provable implies (u '<->' v) is D-provable) &
(v '<->' t) '==' (v '<->' u) is D-provable &
(v '<->' t) '->' (v '<->' u) is D-provable &
((v '<->' t) is D-provable implies (v '<->' u) is D-provable) &
(t '==' v) '==' (u '==' v) is D-provable &
(t '==' v) '->' (u '==' v) is D-provable &
((t '==' v) is D-provable implies (u '==' v) is D-provable) &
(v '==' t) '==' (v '==' u) is D-provable &
(v '==' t) '->' (v '==' u) is D-provable &
((v '==' t) is D-provable implies (v '==' u) is D-provable) &
(t => v) '==' (u => v) is D-provable &
(t => v) '->' (u => v) is D-provable &
((t => v) is D-provable implies (u => v) is D-provable) &
(v => t) '==' (v => u) is D-provable &
(v => t) '->' (v => u) is D-provable &
((v => t) is D-provable implies (v => u) is D-provable)
proof
let X, L, D, t, u, v;
set U = t '==' u;
assume A1: U is D-provable;
then U is D-provable & u '==' t is D-provable by Th63;
then t '->' u is D-provable & u '->' t is D-provable by Th60;
hence t is D-provable iff u is D-provable by Th20;
U '->' ((t '&' v) '==' (u '&' v)) is D-provable by Th67;
hence ((t '&' v) '==' (u '&' v)) is D-provable by A1, Th20;
hence ((t '&' v) '->' (u '&' v)) is D-provable by Th60;
hence (t '&' v) is D-provable implies (u '&' v) is D-provable by Th20;
U '->' ((v '&' t) '==' (v '&' u)) is D-provable by Th67;
hence ((v '&' t) '==' (v '&' u)) is D-provable by A1, Th20;
hence ((v '&' t) '->' (v '&' u)) is D-provable by Th60;
hence (v '&' t) is D-provable implies (v '&' u) is D-provable by Th20;
U '->' ((t 'or' v) '==' (u 'or' v)) is D-provable by Th67;
hence ((t 'or' v) '==' (u 'or' v)) is D-provable by A1, Th20;
hence ((t 'or' v) '->' (u 'or' v)) is D-provable by Th60;
hence (t 'or' v) is D-provable implies (u 'or' v) is D-provable by Th20;
U '->' ((v 'or' t) '==' (v 'or' u)) is D-provable by Th67;
hence ((v 'or' t) '==' (v 'or' u)) is D-provable by A1, Th20;
hence ((v 'or' t) '->' (v 'or' u)) is D-provable by Th60;
hence (v 'or' t) is D-provable implies (v 'or' u) is D-provable by Th20;
U '->' ((t '->' v) '==' (u '->' v)) is D-provable by Th67;
hence ((t '->' v) '==' (u '->' v)) is D-provable by A1, Th20;
hence ((t '->' v) '->' (u '->' v)) is D-provable by Th60;
hence (t '->' v) is D-provable implies (u '->' v) is D-provable by Th20;
U '->' ((v '->' t) '==' (v '->' u)) is D-provable by Th67;
hence ((v '->' t) '==' (v '->' u)) is D-provable by A1, Th20;
hence ((v '->' t) '->' (v '->' u)) is D-provable by Th60;
hence (v '->' t) is D-provable implies (v '->' u) is D-provable by Th20;
U '->' ((t '<->' v) '==' (u '<->' v)) is D-provable by Th67;
hence ((t '<->' v) '==' (u '<->' v)) is D-provable by A1, Th20;
hence ((t '<->' v) '->' (u '<->' v)) is D-provable by Th60;
hence (t '<->' v) is D-provable implies (u '<->' v) is D-provable by Th20;
U '->' ((v '<->' t) '==' (v '<->' u)) is D-provable by Th67;
hence ((v '<->' t) '==' (v '<->' u)) is D-provable by A1, Th20;
hence ((v '<->' t) '->' (v '<->' u)) is D-provable by Th60;
hence (v '<->' t) is D-provable implies (v '<->' u) is D-provable by Th20;
U '->' ((t '==' v) '==' (u '==' v)) is D-provable by Th67;
hence ((t '==' v) '==' (u '==' v)) is D-provable by A1, Th20;
hence ((t '==' v) '->' (u '==' v)) is D-provable by Th60;
hence (t '==' v) is D-provable implies (u '==' v) is D-provable by Th20;
U '->' ((v '==' t) '==' (v '==' u)) is D-provable by Th67;
hence ((v '==' t) '==' (v '==' u)) is D-provable by A1, Th20;
hence ((v '==' t) '->' (v '==' u)) is D-provable by Th60;
hence (v '==' t) is D-provable implies (v '==' u) is D-provable by Th20;
U '->' ((t => v) '==' (u => v)) is D-provable by Th67;
hence ((t => v) '==' (u => v)) is D-provable by A1, Th20;
hence ((t => v) '->' (u => v)) is D-provable by Th60;
hence (t => v) is D-provable implies (u => v) is D-provable by Th20;
U '->' ((v => t) '==' (v => u)) is D-provable by Th67;
hence ((v => t) '==' (v => u)) is D-provable by A1, Th20;
hence ((v => t) '->' (v => u)) is D-provable by Th60;
hence (v => t) is D-provable implies (v => u) is D-provable by Th20;
end;
definition
let X, L;
mode Congruence of L -> Equivalence_Relation of L means
:Def100:
for t, u, v, w st [t,u] in it & [v,w] in it holds
['not' t, 'not' u] in it &
[t '&' v, u '&' w] in it &
[t 'or' v, u 'or' w] in it &
[t '->' v, u '->' w] in it &
[t '<->' v, u '<->' w] in it &
[t '==' v, u '==' w] in it;
existence
proof
reconsider E = nabla L as Equivalence_Relation of L;
take E;
for t,u holds [t,u] in E
proof
let t, u;
[t,u] in [: L, L :] by ZFMISC_1:87;
hence [t,u] in E by EQREL_1:def 1;
end;
hence thesis;
end;
end;
reserve E for Congruence of L;
registration
let X, L;
cluster non empty for Subset-Family of L;
existence
proof
reconsider t = bool L as Subset-Family of L;
take t;
thus thesis;
end;
end;
definition
let X, L, E;
mode Equivalence_Class of E is Element of Class E;
end;
definition
let X, L, E, t;
func E-class t -> Equivalence_Class of E equals
Class(E, t);
coherence by EQREL_1:def 3;
end;
theorem Th70:
for X, L, E, t, u holds [t,u] in E iff E-class t = E-class u
proof
let X, L, E, t, u;
thus [t,u] in E implies E-class t = E-class u
proof
assume [t,u] in E;
then u in E-class t by EQREL_1:18;
hence thesis by EQREL_1:23;
end;
assume E-class t = E-class u;
then u in E-class t by EQREL_1:23;
hence thesis by EQREL_1:18;
end;
reserve d,e for Equivalence_Class of E;
theorem Th71:
for X, L, E, d ex t st d = E-class t
proof
let X, L, E, d;
consider a such that
A1: a in L and
A2: d = Class(E, a) by EQREL_1:def 3;
reconsider t = a as Formula of L by A1;
take t;
thus thesis by A2;
end;
definition
let X, L, E, d;
func 'not' d -> Equivalence_Class of E means
:Def101:
ex t st d = E-class t & it = E-class 'not' t;
existence
proof
consider t such that A2: d = E-class t by Th71;
take E-class 'not' t;
thus thesis by A2;
end;
uniqueness
proof
let e1, e2 be Equivalence_Class of E;
given t1 being Formula of L such that
A1: d = E-class t1 and
A2: e1 = E-class 'not' t1;
given t2 being Formula of L such that
A3: d = E-class t2 and
A4: e2 = E-class 'not' t2;
[t1,t2] in E by A1, A3, Th70;
then ['not' t1, 'not' t2] in E by Def100;
hence e1 = e2 by A2, A4, Th70;
end;
let e;
func d '&' e -> Equivalence_Class of E means
:Def102:
ex t, u st d = E-class t & e = E-class u & it = E-class (t '&' u);
existence
proof
consider t such that A1: d = E-class t by Th71;
consider u such that A2: e = E-class u by Th71;
take E-class (t '&' u);
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be Equivalence_Class of E;
given t1, u1 being Formula of L such that
A1: d = E-class t1 and
A2: e = E-class u1 and
A3: z1 = E-class (t1 '&' u1);
given t2, u2 being Formula of L such that
A4: d = E-class t2 and
A5: e = E-class u2 and
A6: z2 = E-class (t2 '&' u2);
A7: [t1, t2] in E by A1, A4, Th70;
[u1, u2] in E by A2, A5, Th70;
then [t1 '&' u1, t2 '&' u2] in E by A7, Def100;
hence z1 = z2 by A3, A6, Th70;
end;
func d 'or' e -> Equivalence_Class of E means
:Def103:
ex t, u st d = E-class t & e = E-class u & it = E-class (t 'or' u);
existence
proof
consider t such that A1: d = E-class t by Th71;
consider u such that A2: e = E-class u by Th71;
take E-class (t 'or' u);
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be Equivalence_Class of E;
given t1, u1 being Formula of L such that
A1: d = E-class t1 and
A2: e = E-class u1 and
A3: z1 = E-class (t1 'or' u1);
given t2, u2 being Formula of L such that
A4: d = E-class t2 and
A5: e = E-class u2 and
A6: z2 = E-class (t2 'or' u2);
A7: [t1, t2] in E by A1, A4, Th70;
[u1, u2] in E by A2, A5, Th70;
then [t1 'or' u1, t2 'or' u2] in E by A7, Def100;
hence z1 = z2 by A3, A6, Th70;
end;
func d '->' e -> Equivalence_Class of E means
:Def104:
ex t, u st d = E-class t & e = E-class u & it = E-class (t '->' u);
existence
proof
consider t such that A1: d = E-class t by Th71;
consider u such that A2: e = E-class u by Th71;
take E-class (t '->' u);
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be Equivalence_Class of E;
given t1, u1 being Formula of L such that
A1: d = E-class t1 and
A2: e = E-class u1 and
A3: z1 = E-class (t1 '->' u1);
given t2, u2 being Formula of L such that
A4: d = E-class t2 and
A5: e = E-class u2 and
A6: z2 = E-class (t2 '->' u2);
A7: [t1, t2] in E by A1, A4, Th70;
[u1, u2] in E by A2, A5, Th70;
then [t1 '->' u1, t2 '->' u2] in E by A7, Def100;
hence z1 = z2 by A3, A6, Th70;
end;
func d '<->' e -> Equivalence_Class of E means
:Def105:
ex t, u st d = E-class t & e = E-class u & it = E-class (t '<->' u);
existence
proof
consider t such that A1: d = E-class t by Th71;
consider u such that A2: e = E-class u by Th71;
take E-class (t '<->' u);
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be Equivalence_Class of E;
given t1, u1 being Formula of L such that
A1: d = E-class t1 and
A2: e = E-class u1 and
A3: z1 = E-class (t1 '<->' u1);
given t2, u2 being Formula of L such that
A4: d = E-class t2 and
A5: e = E-class u2 and
A6: z2 = E-class (t2 '<->' u2);
A7: [t1, t2] in E by A1, A4, Th70;
[u1, u2] in E by A2, A5, Th70;
then [t1 '<->' u1, t2 '<->' u2] in E by A7, Def100;
hence z1 = z2 by A3, A6, Th70;
end;
func d '==' e -> Equivalence_Class of E means
:Def106:
ex t, u st d = E-class t & e = E-class u & it = E-class (t '==' u);
existence
proof
consider t such that A1: d = E-class t by Th71;
consider u such that A2: e = E-class u by Th71;
take E-class (t '==' u);
thus thesis by A1, A2;
end;
uniqueness
proof
let z1, z2 be Equivalence_Class of E;
given t1, u1 being Formula of L such that
A1: d = E-class t1 and
A2: e = E-class u1 and
A3: z1 = E-class (t1 '==' u1);
given t2, u2 being Formula of L such that
A4: d = E-class t2 and
A5: e = E-class u2 and
A6: z2 = E-class (t2 '==' u2);
A7: [t1, t2] in E by A1, A4, Th70;
[u1, u2] in E by A2, A5, Th70;
then [t1 '==' u1, t2 '==' u2] in E by A7, Def100;
hence z1 = z2 by A3, A6, Th70;
end;
end;
definition
let X, L, D;
func EqRel D -> Congruence of L means
:Def110:
for t, u holds [t,u] in it iff t '==' u is D-provable;
existence
proof
defpred P[object, object] means
ex v, w st v = $1 & w = $2 & v '==' w is D-provable;
A1: for a st a in L holds P[a, a]
proof
let a;
assume a in L;
then reconsider t = a as Formula of L;
t '==' t is D-provable;
hence thesis;
end;
A10: for a, b st P[a, b] holds P[b, a]
proof
let a, b;
assume P[a, b];
then consider v, w such that
A12: v = a & w = b and
A13: v '==' w is D-provable;
w '==' v is D-provable by A13, Th63;
hence thesis by A12;
end;
A20: for a, b, c st P[a, b] & P[b, c] holds P[a, c]
proof
let a, b, c;
assume P[a,b] & P[b,c];
then consider t, u, v, w such that
A22: t = a and
A23: u = b and
A24: t '==' u is D-provable and
A25: v = b and
A26: w = c and
A27: v '==' w is D-provable;
t '==' w is D-provable by A23, A24, A25, A27, Th68;
hence thesis by A22, A26;
end;
consider E being Equivalence_Relation of L such that
A30: for a, b holds [a,b] in E iff a in L & b in L & P[a,b]
from EQREL_1:sch 1(A1, A10, A20);
take E;
A31: for p, q being Formula of L holds [p,q] in E iff p '==' q is D-provable
proof
let p, q be Formula of L;
thus [p, q] in E implies p '==' q is D-provable
proof
assume [p,q] in E;
then consider r, s being Formula of L such that
A32: r = p & s = q & r '==' s is D-provable by A30;
thus thesis by A32;
end;
thus thesis by A30;
end;
thus E is Congruence of L
proof
let t, u, v, w;
assume [t,u] in E & [v,w] in E;
then A33: t '==' u is D-provable & v '==' w is D-provable by A31;
then ('not' t) '==' ('not' u) is D-provable by Th61;
hence ['not' t, 'not' u] in E by A31;
(t '&' v) '==' (u '&' w) is D-provable &
(t 'or' v) '==' (u 'or' w) is D-provable &
(t '->' v) '==' (u '->' w) is D-provable &
(t '<->' v) '==' (u '<->' w) is D-provable &
(t '==' v) '==' (u '==' w) is D-provable by A33, Th66;
hence thesis by A31;
end;
thus thesis by A31;
end;
uniqueness
proof
let E1, E2 be Congruence of L;
assume that
A1: for t,u holds [t,u] in E1 iff t '==' u is D-provable and
A2: for t,u holds [t,u] in E2 iff t '==' u is D-provable;
for t,u holds [t,u] in E1 iff [t,u] in E2
proof
let t, u;
[t,u] in E1 iff t '==' u is D-provable by A1;
hence thesis by A2;
end;
hence thesis by RELSET_1:def 2;
end;
end;
definition
let X, L, D;
mode Equivalence_Class of D is Equivalence_Class of EqRel D;
end;
definition
let X, L, D, t;
func D-class t -> Equivalence_Class of D equals
(EqRel D)-class t;
coherence;
end;
theorem Th80:
for X, L, D, t, u holds t '==' u is D-provable iff D-class t = D-class u
proof
let X, L, D, t, u;
[t,u] in EqRel D iff t '==' u is D-provable by Def110;
hence thesis by Th70;
end;
reserve x, y, z for Equivalence_Class of D;
theorem Th81:
for X, L, D, x ex t st x = D-class t
proof
let X, L, D, x;
consider t such that A1: x = (EqRel D)-class t by Th71;
take t;
thus thesis by A1;
end;
definition
let X, L, D, x;
attr x is D-provable means
ex t st x = D-class t & t is D-provable;
end;
theorem
for X, L, D, x, y holds
y = 'not' x iff ex t st x = D-class t & y = D-class 'not' t
proof
let X, L, D, x, y;
set E = EqRel D;
thus y = 'not' x implies ex t st x = D-class t & y = D-class 'not' t
proof
assume y = 'not' x;
then consider t such that A1: x = E-class t & y = E-class 'not' t
by Def101;
take t;
thus thesis by A1;
end;
thus thesis by Def101;
end;
registration
let X, L, D;
let t be D-provable Formula of L;
cluster D-class t -> D-provable;
coherence;
end;
registration
let X, L, D;
cluster D-provable for Equivalence_Class of D;
existence
proof
take D-class (the D-provable Formula of L);
thus thesis;
end;
end;
theorem Th90:
for X, L, D, t st D-class t is D-provable holds t is D-provable
proof
let X, L, D, t;
set x = D-class t;
assume x is D-provable;
then consider u such that A1: D-class u = x and A2: u is D-provable;
u '==' t is D-provable by A1, Th80;
then u '->' t is D-provable by Th60;
hence t is D-provable by A2, Th20;
end;
registration
let X, L, D;
let x be D-provable Equivalence_Class of D;
cluster -> D-provable for Element of x;
coherence
proof
let t be Element of x;
x is D-provable;
then consider u such that A2: D-class u = x and u is D-provable;
A4: u in x by A2, EQREL_1:23;
then t in x;
then reconsider t as Formula of L;
D-class t = x by A2, A4, EQREL_1:23;
hence thesis by Th90;
end;
end;
theorem
for x, y holds x '&' y is D-provable iff x is D-provable & y is D-provable
proof
let x, y;
consider t such that A1: x = D-class t by Th81;
consider u such that A2: y = D-class u by Th81;
A3: x '&' y = D-class t '&' u by A1, A2, Def102;
thus x '&' y is D-provable implies x is D-provable & y is D-provable
proof
assume x '&' y is D-provable;
then t '&' u is D-provable by A3, Th90;
then t is D-provable & u is D-provable by Th43;
hence thesis by A1, A2;
end;
assume x is D-provable & y is D-provable;
then t is D-provable & u is D-provable by A1, A2, Th90;
hence x '&' y is D-provable by A3;
end;
theorem
for x, y holds x '==' y is D-provable iff x = y
proof
let x, y;
consider t such that A1: x = D-class t by Th81;
consider u such that A2: y = D-class u by Th81;
x '==' y = D-class (t '==' u) by A1, A2, Def106;
hence thesis by A1, A2, Th80, Th90;
end;
theorem
for X, L, D, t, u holds
D-class 'not' t = 'not' (D-class t) &
D-class (t '&' u) = (D-class t) '&' (D-class u) &
D-class (t 'or' u) = (D-class t) 'or' (D-class u) &
D-class (t '->' u) = (D-class t) '->' (D-class u) &
D-class (t '<->' u) = (D-class t) '<->' (D-class u) &
D-class (t '==' u) = (D-class t) '==' (D-class u)
by Def101, Def102, Def103, Def104, Def105, Def106;
theorem
for X, L, D, x, y st x is D-provable holds
x 'or' y is D-provable & y 'or' x is D-provable
proof
let X, L, D, x, y;
consider t such that A1: x = D-class t by Th81;
consider u such that A2: y = D-class u by Th81;
A3: x 'or' y = D-class (t 'or' u) by A1, A2, Def103;
assume x is D-provable;
then A4: t is D-provable by A1, Th90;
hence x 'or' y is D-provable by A3;
y 'or' x = D-class (u 'or' t) by A1, A2, Def103;
hence y 'or' x is D-provable by A4;
end;
theorem Th96:
for X, L, D, t, u holds t '<->' u is D-provable
iff t '->' u is D-provable & u '->' t is D-provable
proof
let X, L, D, t, u;
thus t '<->' u is D-provable
implies t '->' u is D-provable & u '->' t is D-provable
proof
assume A1: t '<->' u is D-provable;
(t '<->' u) '->' ((t '->' u) '&' (u '->' t)) is D-provable;
then (t '->' u) '&' (u '->' t) is D-provable by A1, Th20;
hence thesis by Th43;
end;
assume A10: t '->' u is D-provable & u '->' t is D-provable;
((t '->' u) '&' (u '->' t)) '->' (t '<->' u) is D-provable;
hence thesis by A10, Th20;
end;
theorem
for X, L, D, t, u st t '<->' u is D-provable holds u '<->' t is D-provable
proof
let X, L, D, t, u;
assume t '<->' u is D-provable;
then t '->' u is D-provable & u '->' t is D-provable by Th96;
hence thesis by Th96;
end;