let p be Element of HP-WFF ; :: thesis: ( p in HP_TAUT implies p is canonical )

set X = { q where q is Element of HP-WFF : q is canonical } ;

{ q where q is Element of HP-WFF : q is canonical } c= HP-WFF

X is Hilbert_theory

assume p in HP_TAUT ; :: thesis: p is canonical

then p in X by A2;

then ex q being Element of HP-WFF st

( p = q & q is canonical ) ;

hence p is canonical ; :: thesis: verum

set X = { q where q is Element of HP-WFF : q is canonical } ;

{ q where q is Element of HP-WFF : q is canonical } c= HP-WFF

proof

then reconsider X = { q where q is Element of HP-WFF : q is canonical } as Subset of HP-WFF ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Element of HP-WFF : q is canonical } or x in HP-WFF )

assume x in { q where q is Element of HP-WFF : q is canonical } ; :: thesis: x in HP-WFF

then ex p being Element of HP-WFF st

( p = x & p is canonical ) ;

hence x in HP-WFF ; :: thesis: verum

end;assume x in { q where q is Element of HP-WFF : q is canonical } ; :: thesis: x in HP-WFF

then ex p being Element of HP-WFF st

( p = x & p is canonical ) ;

hence x in HP-WFF ; :: thesis: verum

X is Hilbert_theory

proof

then A2:
HP_TAUT c= X
by HILBERT1:13;
thus
VERUM in X
; :: according to HILBERT1:def 10 :: thesis: for b_{1}, b_{2}, b_{3} being Element of HP-WFF holds

( b_{1} => (b_{2} => b_{1}) in X & (b_{1} => (b_{2} => b_{3})) => ((b_{1} => b_{2}) => (b_{1} => b_{3})) in X & (b_{1} '&' b_{2}) => b_{1} in X & (b_{1} '&' b_{2}) => b_{2} in X & b_{1} => (b_{2} => (b_{1} '&' b_{2})) in X & ( not b_{1} in X or not b_{1} => b_{2} in X or b_{2} in X ) )

let p, q, r be Element of HP-WFF ; :: thesis: ( p => (q => p) in X & (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus p => (q => p) in X ; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus (p => (q => r)) => ((p => q) => (p => r)) in X ; :: thesis: ( (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus (p '&' q) => p in X ; :: thesis: ( (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus (p '&' q) => q in X ; :: thesis: ( p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus p => (q => (p '&' q)) in X ; :: thesis: ( not p in X or not p => q in X or q in X )

assume p in X ; :: thesis: ( not p => q in X or q in X )

then A1: ex s being Element of HP-WFF st

( s = p & s is canonical ) ;

assume p => q in X ; :: thesis: q in X

then ex s being Element of HP-WFF st

( s = p => q & s is canonical ) ;

then q is canonical by A1, Th40;

hence q in X ; :: thesis: verum

end;( b

let p, q, r be Element of HP-WFF ; :: thesis: ( p => (q => p) in X & (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus p => (q => p) in X ; :: thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in X & (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus (p => (q => r)) => ((p => q) => (p => r)) in X ; :: thesis: ( (p '&' q) => p in X & (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus (p '&' q) => p in X ; :: thesis: ( (p '&' q) => q in X & p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus (p '&' q) => q in X ; :: thesis: ( p => (q => (p '&' q)) in X & ( not p in X or not p => q in X or q in X ) )

thus p => (q => (p '&' q)) in X ; :: thesis: ( not p in X or not p => q in X or q in X )

assume p in X ; :: thesis: ( not p => q in X or q in X )

then A1: ex s being Element of HP-WFF st

( s = p & s is canonical ) ;

assume p => q in X ; :: thesis: q in X

then ex s being Element of HP-WFF st

( s = p => q & s is canonical ) ;

then q is canonical by A1, Th40;

hence q in X ; :: thesis: verum

assume p in HP_TAUT ; :: thesis: p is canonical

then p in X by A2;

then ex q being Element of HP-WFF st

( p = q & q is canonical ) ;

hence p is canonical ; :: thesis: verum