From 5c6da425a6ba7dbe2865805f03e2d4d5a008a043 Mon Sep 17 00:00:00 2001 From: "David A. Wheeler" Date: Wed, 10 Jan 2024 10:24:36 -0500 Subject: [PATCH] Explain why $d is used on its first use Explain why $d is used when $d is first used. This text is tweaked from an email by Mario Carneiro on 2024-01-01 titled "Re: [Metamath] Results about ax-13 usage". I thought it was a great point and that the information belonged somewhere in set.mm itself. Signed-off-by: David A. Wheeler --- set.mm | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index d5608d2bda..689dfed984 100644 --- a/set.mm +++ b/set.mm @@ -15580,8 +15580,28 @@ only postulated (that is, axiomatic) rule of inference of predicate This axiom essentially says that if ` x ` does not occur in ` ph ` , i.e. ` ph ` does not depend on ` x ` in any way, then we can add the quantifier ` A. x ` to ` ph ` with no further assumptions. By ~ sp , we - can also remove the quantifier (unconditionally). (Contributed by NM, - 10-Jan-1993.) $) + can also remove the quantifier (unconditionally). + + This is our first use of a disjoint variable restriction aka distinct + variables ($d in the Metamath language). It would be possible to + express our axioms without $d but there are good reasons we do it this + way. The "obvious" way of truthfully expressing this axiom (and other + similar axioms) without distinct variable constraints ($d statements) + would lead to situations where even after the variable is done being + used you still can't discharge the distinctor. This would mean its + logical equivalent would permanently stick around. Effectively all + proofs would end up saying "provided there are at least N variables in + the metalogic, the following theorem holds" because you actually can't + prove anything about whether variables exist in this setting. This + admits models where e.g. the object logic only has three variables v0 v1 + v2 and so you can't write any expression containing four or more forall + or exists quantifiers without being degenerate in some way, so the + undischargeable assumptions that pile up are saying that the object + logic is at least nondegenerate enough to perform the proof in question. + The $d provisos provide a simple mechanism to eliminate the problem in + general. + + (Contributed by NM, 10-Jan-1993.) $) ax-5 $a |- ( ph -> A. x ph ) $. $}