Hi all, I wanted to share a simple remark, which is probably known to some.
Megill's completeness theorem [Megill, Thm. 9.7] proves that all true schemes with DV conditions of the form DV(x,y) and DV(x,ph) are provable from ax-mp, ax-gen, ax-1--13. One can ask about schemes with DV conditions of the form DV(ph,ps). If such a scheme is provable from that axiom system, then the same scheme without that DV condition is also provable. Indeed, such a DV condition cannot be produced from DV conditions of the form DV(x,y) or DV(x,ph). Therefore, the question is equivalent to the existence of true schemes with DV(ph,ps) which are false without it. An example is ( ( E. x ph -> A. x ph ) \/ ( E. x ps -> A. x ps ) ) , DV(ph,ps) It is true because the DV condition implies that x does not occur in at least one of ph and ps. Therefore, at least one of the two disjuncts is true. Without the DV condition, it is false: for instance, substitute x=y for both ph and ps. I added it to my mathbox (locally) and reproved ax-5 from it. I do not know whether the java tool will complain. Maybe I'll do a git pull request and see. Benoit -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/188db4a5-23d4-45be-a8bb-5296c87d6856n%40googlegroups.com.
