On Thu, Sep 26, 2019 at 9:49 AM Benoit <[email protected]> wrote:
> * I think that Rule 3 is not necessary. It's true that a definition not
> satisfying Rule 3 is a bit strange, but Rules 1,2,4,5 seem to suffice for
> conservativity and eliminability.
>
Rule 3 is not necessary for it to be a conservative extension, but it is
required for it to be a definitional extension, in the same way that the
"definition"
cfoo $a class Foo $.
(with no associated definitional theorem) posits the existence of a
constant but does not pin it down. This does not lead to contradiction or
the ability to prove new theorems, because you can always just replace Foo
with (/) everywhere it appears, but you do not have eliminability, in that
there are propositions which contain Foo that are not provably equal to any
proposition in the original language (for example "(/) e. Foo").
If you leave out rule 3, you can define something like
cbar $a wff Bar x y $.
${ $d x y $. df-bar $a |- ( Bar x y <-> x = y ) $. $}
and now "Bar x x" is one of these unmentionables: there is no way to prove
that it means anything in particular, because the definitional theorem that
is supposed to be responsible for connecting it to the original language
wants nothing to do with this expression, even though it is well formed.
You could go further and make it not even well formed:
${ $d x y $.
cbar $a wff Bar x y $.
df-bar $a |- ( Bar x y <-> x = y ) $.
$}
but now the grammar is not context free because the term formers have side
conditions, so parsing becomes harder. (If it's just $d preconditions
appearing in syntax axioms then you can probably get a reasonable method by
generating all parse trees and rejecting all those that violate a DV
condition, but if you add hypotheses then it becomes outright undecidable.)
On Thu, Sep 26, 2019 at 10:56 AM 'ookami' via Metamath <
[email protected]> wrote:
> The definition df-bust-verifier is not per se "crazy", it becomes so in
> the presence of ax-5. Should you ever strive for a set.mm without
> distinct variable constraints, usage of df-bust-verifier is at your
> discretion. Distinct variable constraints are in FOL (without sets) a
> convenience extension, because requiring two variables be distinct can be
> achieved by a distinctor hypothesis -. A. x x x = y, and x be distinct from
> ph is replaceable with a F/ x ph hypothesis (I leave out the boring special
> case of a one-object universe).
>
I believe this is false. While I don't think you can derive false, you can
at least derive that the universe has one element and hence distinctors
don't work:
$d x y $d x z
1 |- ( BustVerifier <-> x = y )
2 |- ( BustVerifier <-> x = z )
3:1,2 |- ( x = y <-> x = z )
4 |- ( x = y -> x = y )
5:3 |- ( x = y -> x = z )
6:4,5 |- ( x = y -> y = z )
7:6 |- ( E. x x = y -> y = z )
8 |- E. x x = y
9:7,8 |- y = z
10:9 |- A. y y = z
I haven't carefully analyzed these supporting theorems for ax-5 usage, in
particular step 7 (exlimiv), but it's a bit weird to have $d hypotheses
from df-bust-verifier when the axiom system itself doesn't deal with them.
This gives rise to the question, how the definitionChecker works: Does it
> assume the current axiomatic foundation in place, or does it really do a
> semantic check of axioms it finds in the file and individually derives
> requirements for soundness? In other words: If I remove ax-5 from set.mm
> and discard theorems based on it, is df-bust-verifier accepted then?
>
Deleting theorems will only make more definitions be rejected, because the
theorem prover that discharges side conditions will be able to prove less
things. The reasoning in the mmj2 definition checker is tailored to set.mm
theorems (for example, step 1 - "every definition must have <-> or = at the
head" - is very specific to set.mm). The next generation of definition
checker will be based on the $j annotations, which attempt to define
generically properties of certain constants which suffice for the equality
metatheorem ( x = y -> P(x) ~ P(y) ) mentioned in df-cdeq (
http://us2.metamath.org/mpeuni/mmtheorems32.html#mm3162s).
On Thu, Sep 26, 2019 at 11:29 AM Benoit <[email protected]> wrote:
> The definition checker does not assume an axiomatic foundation: it reads
> the provided mm database (which has to be similar to set.mm, in terms of
> typecodes (e.g. "|-" and "setvar") but it also works e.g. on iset.mm).
> It checks Rules 1--5 I gave in the post above because we can prove, outside
> of Metamath, that a definition respecting these rules is conservative and
> eliminable (a similar metatheorem is proved for instance in Kleene's
> Introduction to metamathematics).
>
This proof relies on the database being significantly set.mm-like, down to
the names of certain constants (and especially their types). You can
probably fool the definition checker or cause it to crash if you define
"wb" to have three arguments, or not act like an equivalence relation, or
other things like that.
Mario
--
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/CAFXXJSugYCmGsikd%2BuZHkkG4aJbFWFM7UrzqXHHNzO71K22%2BGg%40mail.gmail.com.
