Description: In this proof, the use of the syntactic theorem bj-0 allows to reduce the total length by one (non-essential) step. See also the section comment and the comment of bj-0 . Since bj-0 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 as a theorem referencing it). The full proof reads $= wph wps wch bj-0 id $. (while, without using bj-0 , 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 or wel ). 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 is a special instance of id . (Contributed by BJ, 24-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-1 | ⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜒 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | ⊢ ( ( ( 𝜑 → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜒 ) ) |