| Description: In this proof, the use of
the syntactic theorem bj-0 34722 allows to reduce
the total length by one (non-essential) step. See also the section
comment and the comment of bj-0 34722. Since bj-0 34722
is used in a
non-essential step, this use does not appear on this webpage (but the
present theorem appears on the webpage for bj-0 34722
as a theorem referencing
it). The full proof reads $= wph wps wch bj-0 id $. (while, without
using bj-0 34722, it would read $= wph wps wi wch wi id $.).
Now we explain why syntactic theorems are not useful in set.mm. Suppose
that the syntactic theorem thm-0 proves that PHI is a well-formed formula,
and that thm-0 is used to shorten the proof of thm-1. Assume that PHI
does have proper non-atomic subformulas (which is not the case of the
formula proved by weq 1966 or wel 2107). Then, the proof of thm-1 does not
construct all the proper non-atomic subformulas of PHI (if it did, then
using thm-0 would not shorten it). Therefore, thm-1 is a special instance
of a more general theorem with essentially the same proof. In the present
case, bj-1 34723 is a special instance of id 22.
(Contributed by BJ,
24-Sep-2019.) (Proof modification is discouraged.)
(New usage is discouraged.) |
