>
> Another more thing: it may be more correct to use the universal closures
>> of the $e hypotheses above (as I did in the current bj-df-clel and
>> bj-df-cleq). This does not change much, since one can go back and forth
>> between them by ax-gen/sp, but sentences (closed formulas) are easier to
>> understand than open formulas
>
>
> Why do you think universal closures are easier to understand? Personally
> I don't find them easier, if nothing else because the formula is longer and
> thus takes slightly more effort to parse mentally.
>
I think we generally do not see a difference in difficulty because we got
so used to the (very standard) convention, "a formula holds exactly when
its universal closure holds", so we mentally do the translation, so for us
open formulas are as easy as their universal closures. But you can see
from the mere statement of this convention that the objects whose truth we
first define unambiguously are sentences, and then we posit the above
convention to give a truth value to open formulas as well. This convention
is not always the most convenient (for instance on the empty domain of
discourse (see Leblanc, Meyer, Open formulas and the empty domain, Arch.
math. Logik 12 (1969), 78--84), or in free logic, that is, with a domain
with non-denoting, or non-existent, objects). Of course, in set.mm there
is no difference, and on the proof theoretic side, ax-gen/spi allow us to
go back and forth. In general, ax-gen holds, but spi may not hold, so the
universal closure is weaker. An example of this in set.mm is ax6vsep,
which proves ax6v from {propcalc, ax-ext, ax-sep}. To me, this shows that
ax-sep is too strong, and should be replaced by its universal closure (for
ax-ext, this is less important, since we then posit class extensionality
and there is no quantification over classes).
> Moreover, instantiating the $e from the $a in your ax-cleq is an immediate
> and obvious substitution, whereas with universal closure in bj-df-cleq we
> also need applications of ax-gen.
>
Indeed. I was a bit torn to weaken the similarity of the $e and $a
statements in e.g. bj-df-cleq. But I think we should give this up because
of the above paragraph. Additionally, the lesser similarity is due to the
fact that we cannot quantify over classes, so this is an occasion to ponder
why this is so, especially in the context of free logic (I found the
articles of the online Stanford Encyclopedia of Phylosophy very
interesting: articles "Free logic" and "Nonexistent objects").
> Also, if we require the universal closures of the hypotheses, for
> consistency shouldn't we also require the universal closure of the
> conclusion? That would be awkward: for bj-df-clel we would have to prefix
> the $p with "A. x1 ... A. xn" along with the side condition "where
> x1,...,xn are the free variables in A and B", and of course the current
> set.mm doesn't even have a notation that allows us to express that.
>
No, I think bj-df-clel is OK as is. As I wrote above, classes cannot be
quantified over anyway. I do not aim to have only closed formulas, far
from it. Axioms would preferably be expressed in closed form, but then we
can make free use of spi to remove initial quantifiers. See e.g.
ileuni/ax-strcoll immediately followed by ileuni/strcoll2 ---
unfortunately, I did two things at once there, but the idea would be to
have "ax-ext $a |- A. x A. y ( A. z ( z e. x <-> z e. y ) -> x = y ) $."
(with correct dv's), immediately followed by "axext $p |- ( A. z ( z e. x
<-> z e. y ) -> x = y ) $= [using spi twice] $.".
I'm not saying you are wrong, only that I don't understand the reasoning or
> advantage and need to be educated. :) I know that many books show ZFC
> axioms and even FOL axiomatizations with universal closures, and I've never
> understood why. Requiring all proof steps to be universally closed (as some
> FOL axiomatizations do) can make them quite tedious to work with. There are
> "Quine closures" and "Berry closures", each with a set of rules to add,
> drop, and reorder the quantifiers in universal closures as we apply ax-mp
> etc. These seem like a major distraction and complication vs. using simple
> open formulas, particularly when schemes are involved.
>
Some books want to have only sentences and avoid use of generalization
(like in one section of Tarski's article that serves as our foundation).
Again, this is not my aim at all here. And like you, I'm not sure why they
go into so much trouble to do so. Note that most proofs of Godel's
completeness theorem found in textbooks allow only sentences; some (minor)
work has to be done to extend it to open formulas as well. This may be one
of the reasons.
> Maybe there are advantages to universal closures (sentences) for some
> theoretical purposes, but I don't see any advantage for set.mm.
>
I mostly agree, which is why I propose to do as I wrote above with ax-ext
followed by axext. The advantage I see is being closer to textbook axioms,
and especially not stating stronger axioms (again, ax6vsep is a good
example).
> (and the problem of having specific instances as hypotheses creeps up in
>> the conservativity theorem, it seems).
>>
>
> Where do you see this? In any case, can't we just apply ax-gen as needed
> if open formulas are problematic?
>
Mario's proof of the conservativity theorem above in this thread
(https://groups.google.com/g/metamath/c/xdHB0oW0aZ4/m/8Rfzy_lWAQAJ) is for
hypotheses-free theorems. In the first paragraph, where he concludes "so
ax-ext is a theorem of S \cup \{df-clab\}", we need to change it, when
there are hypotheses, to "so ax-ext is a theorem of S \cup \{df-clab\} or
is a hypothesis of Phi" [actually, we have to be more precise that it is
"that" particular instance of ax-ext]. But two sentences later in his
proof, one sees that other instances of ax-ext may be needed. Therefore, it
is more convenient to have a sentence for ax-ext, since then another
instance is simply obtained by alpha renaming. Maybe one can do without
this, but at the price of more complexity, I think.
Benoît
--
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/bd8a59b1-5954-410e-a4ed-eadc90a33e02n%40googlegroups.com.
