Deduction form and natural deduction

[David A. Wheeler]

The "develop" branch now has a new mmnatded.html file.
This explains, and cross-references with examples, Mario's approach to natural deduction.

My thanks to Mario for creating the examples, which really helped me understand his approach much better than I did before.

--- David A. Wheeler

[Giovanni Mascellani]

Hi.

Il 11/02/2017 01:06, David A. Wheeler ha scritto:
> The "develop" branch now has a new mmnatded.html file. This explains,
> and cross-references with examples, Mario's approach to natural
> deduction.

Nice to read, thanks you.

A couple of typos (unless I am mistaken) and a question:

* In [1] the last row of the table has (twice) chi instead of theta,
which is the thesis.

[1] http://us.metamath.org/mpegif/ex-natded5.2.html

* In [2], paragraph "Current approach to deductions", a conjunction is
mentioned, but the symbol of a disjunction is written between parentheses.

[2] http://us.metamath.org/mpegif/mmnatded.html

* And at last the question: in some deduction-styled theorems (for
example lhop[3], but many others do) there are a few hypotheses that do
not have the usual "ph ->" construct at the beginning. Why is that? What
is different with those hypotheses? Maybe it is a potential FAQ that
deserves a general answer in mmnatded.html.

[3] http://us.metamath.org/mpegif/lhop.html

Regards, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
PhD Student - Scuola Normale Superiore, Pisa, Italy

http://poisson.phc.unipi.it/~mascellani

[David A. Wheeler]

On February 13, 2017 3:31:57 PM EST, Giovanni Mascellani <g.masc...@gmail.com> wrote:
>Hi.
>
>Il 11/02/2017 01:06, David A. Wheeler ha scritto:
>> The "develop" branch now has a new mmnatded.html file. This explains,
>> and cross-references with examples, Mario's approach to natural
>> deduction.
>
>Nice to read, thanks you.
>
>A couple of typos (unless I am mistaken) and a question:
>
> * In [1] the last row of the table has (twice) chi instead of theta,
>which is the thesis.
>
> [1] http://us.metamath.org/mpegif/ex-natded5.2.html

Definitely a typo. Fixed in my local copy, I'll push later today.

> * In [2], paragraph "Current approach to deductions", a conjunction is
>mentioned, but the symbol of a disjunction is written between
>parentheses.
>
> [2] http://us.metamath.org/mpegif/mmnatded.html

Another typo. Fixed locally.

Thanks for reporting these!

> * And at last the question: in some deduction-styled theorems (for
>example lhop[3], but many others do) there are a few hypotheses that do
>not have the usual "ph ->" construct at the beginning. Why is that?
>What
>is different with those hypotheses? Maybe it is a potential FAQ that
>deserves a general answer in mmnatded.html.

In lhop there is only one statement not beginning with ph -> ..., It is a definition, D = ...
The text already notes that hypothesis can include definitions. Is that not clear enough? If not, how can we make it clearer?

>
> [3] http://us.metamath.org/mpegif/lhop.html
>
>Regards, Giovanni.

Thanks!


--- David A.Wheeler

[Giovanni Mascellani]

Hi.

Il 13/02/2017 22:51, David A. Wheeler ha scritto:
>> * And at last the question: in some deduction-styled theorems (for
>> example lhop[3], but many others do) there are a few hypotheses
>> that do not have the usual "ph ->" construct at the beginning. Why
>> is that? What is different with those hypotheses? Maybe it is a
>> potential FAQ that deserves a general answer in mmnatded.html.
> In lhop there is only one statement not beginning with ph -> ..., It
> is a definition, D = ... The text already notes that hypothesis can
> include definitions. Is that not clear enough? If not, how can we
> make it clearer?

Yes, you are right, I had missed that point.

Maybe it could be useful to specify that "definition" means in this
context. Is it something of the form "A = ..." or "ch <-> ..."? Sorry if
the question is trivial, but I am a newbie here and I have not yet
really mastered how is natural deduction to be used.

Also, I am curious why one does not need "ph ->" for the definitions.
However I understand that probably my lack of experience with natural
deduction is what is preventing me from getting a more complete view on
the whole thing. In other words, do not lose too much time with me here...

Thanks again, Giovanni.

[David A. Wheeler]

On Tue, 14 Feb 2017 18:43:49 +0100, Giovanni Mascellani <g.masc...@gmail.com> wrote:
> >> * And at last the question: in some deduction-styled theorems (for
> >> example lhop[3], but many others do) there are a few hypotheses
> >> that do not have the usual "ph ->" construct at the beginning. Why
> >> is that? What is different with those hypotheses? Maybe it is a
> >> potential FAQ that deserves a general answer in mmnatded.html.

> Il 13/02/2017 22:51, David A. Wheeler ha scritto:
> > In lhop there is only one statement not beginning with ph -> ..., It
> > is a definition, D = ... The text already notes that hypothesis can
> > include definitions. Is that not clear enough? If not, how can we
> > make it clearer?
>
> Yes, you are right, I had missed that point.
>
> Maybe it could be useful to specify that "definition" means in this
> context. Is it something of the form "A = ..." or "ch <-> ..."? Sorry if
> the question is trivial, but I am a newbie here and I have not yet
> really mastered how is natural deduction to be used.

Done; it's in the "develop" branch.

> Also, I am curious why one does not need "ph ->" for the definitions.
> However I understand that probably my lack of experience with natural
> deduction is what is preventing me from getting a more complete view on
> the whole thing. In other words, do not lose too much time with me here...

I think the definitions are indirectly covered by "ph ->".
Ignoring the definitions, all the hypotheses and the conclusions have "ph ->" prefixed to them.
The definitions don't need it, because they're simply reused and expanded within the
"ph -> ..." statements as needed. You could rewrite an assertion without the definitions
by substitution, but it'd be a pain to work with.

Mario may correct me here...

--- David A. Wheeler

[Mario Carneiro]

On Feb 14, 2017 1:11 PM, "David A. Wheeler" <dwhe...@dwheeler.com> wrote:

On Tue, 14 Feb 2017 18:43:49 +0100, Giovanni Mascellani <g.masc...@gmail.com> wrote:
> >> * And at last the question: in some deduction-styled theorems (for
> >> example lhop[3], but many others do) there are a few hypotheses
> >> that do not have the usual "ph ->" construct at the beginning. Why
> >> is that? What is different with those hypotheses? Maybe it is a
> >> potential FAQ that deserves a general answer in mmnatded.html.

> Il 13/02/2017 22:51, David A. Wheeler ha scritto:
> > In lhop there is only one statement not beginning with ph -> ..., It
> > is a definition, D = ... The text already notes that hypothesis can
> > include definitions. Is that not clear enough? If not, how can we
> > make it clearer?
>
> Yes, you are right, I had missed that point.
>
> Maybe it could be useful to specify that "definition" means in this
> context. Is it something of the form "A = ..." or "ch <-> ..."? Sorry if
> the question is trivial, but I am a newbie here and I have not yet
> really mastered how is natural deduction to be used.

Done; it's in the "develop" branch.

> Also, I am curious why one does not need "ph ->" for the definitions.
> However I understand that probably my lack of experience with natural
> deduction is what is preventing me from getting a more complete view on
> the whole thing. In other words, do not lose too much time with me here...

The actual purpose of the "ph ->" is to introduce a hypothesis that may not always be satisfiable without some assumptions (and the exact nature of those assumptions is not known inside the theorem, so the generic "ph" is used). If we are dealing with a true abbreviation, just a short way to write some symbols, then the "D = ..." hypothesis will either be satisfied by a similar hypothesis, or by theorem eqid, which will force the substitution of "..." for "D" in the rest of the theorem. Since in any case, the hypothesis can be discharged with no assumptions, the "ph" is not necessary.

Sometimes, we wish to discharge these hypotheses with something that isn't just an abbreviation. For example, if "J e. ( TopOn ` X )", then X is the base set of the topology J, so X = U. J (toponuni), but since X = U. J is not always true in this situation, we can't prove it without the hypothesis "J e. ( TopOn ` X )". What you have to do here, if you want to use a theorem that has the hypothesis "|- X = U. J" (to prove some statement |- P(X)), is use eqid anyway, producing a proof of P(U. J), then use ( ph -> X = U. J ) and equality theorems to get ( ph -> ( P(X) <-> P(U. J) ) ), then use the proof of |- P(U. J) to yield |- ( ph -> P(X) ). An example of this procedure is the derivation of ishaus2 (which has X = U. J given the context) from ishaus (which assumes X = U. J with no context).

The above procedure is always possible to do, but it is not always convenient since many steps may be needed for the equality proof. In cases where we specifically intend to discharge the assumption with something other than eqid, we sometimes add ph -> to the equalities as well. A common example of this is in structure builder theorems, where we want to use a self-referential expression for the left hand side. For example, we might define a group by

$e |- ( ph -> B = my-base-set )
$e |- ( ph -> .+ = my-group-op(B) )

mygroupval $p |- ( ph -> MyGroup = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. } )

Suppose that my-base-set is a complicated expression, and my-group-op(B) has a lot of references to B, so the fully expanded my-group-op(my-base-set) is really big, and we don't want to use it too many times. In the same context, we then prove:

$e |- ( ph -> B = my-base-set )
$e |- ( ph -> .+ = my-group-op(B) )
mygroupbaslem $p |- ( ph -> ( Base ` MyGroup ) = my-base-set )
mygroupaddlem $p |- ( ph -> ( +g ` MyGroup ) = my-group-op(B) )

and now we can bootstrap the whole thing:

mygroupbas $p |- ( ph -> ( Base ` MyGroup ) = my-base-set ) $=

1::eqid |- ( ph -> my-base-set = my-base-set )
2::eqid |- ( ph -> my-group-op = my-group-op(my-base-set) )
qed:1,2:mygroupbaslem |- ( ph -> ( Base ` MyGroup ) = my-base-set )

mygroupadd $p |- ( ph -> ( +g ` MyGroup ) = my-base-set ) $=

1::mygroupbas |- ( ph -> ( Base ` MyGroup ) = my-base-set )
2::eqid |- ( ph -> my-group-op( ( Base ` MyGroup ) ) = my-group-op( ( Base ` MyGroup ) ) )
qed:1,2:mygroupbaslem |- ( ph -> ( +g ` MyGroup ) = my-group-op( ( Base ` MyGroup ) ) )

Note that the contained references of my-group-op are now referencing ( Base ` MyGroup ), which makes this "definition" of a component of MyGroup self-referential. But that was the goal, and we have mygroupbas to expand it as necessary. A more elaborate version of this idea is done in prdsval, with prdsbas, prdsplusg, prdsmulr, etc pulling off components and bootstrapping using the previous theorems.

Finally, there are a few places where ( ph -> X = ... ) definitions are used by convention, specifically grppropd and other *propd theorems, and isgrpd and other is*d theorems for structures.

As a rule of thumb: Use X = ... abbreviations unless you need to use a non-identity abbreviation for X later.

Mario

[Giovanni Mascellani]

Il 14/02/2017 20:35, Mario Carneiro ha scritto:
> As a rule of thumb: Use X = ... abbreviations unless you need to use a
> non-identity abbreviation for X later.

Very nice explanation, thank you!

[David A. Wheeler]

> On Tue, 14 Feb 2017 18:43:49 +0100, Giovanni Mascellani

> > Also, I am curious why one does not need "ph ->" for the definitions.

On Tue, 14 Feb 2017 14:35:25 -0500, Mario Carneiro <di....@gmail.com> wrote:
> The actual purpose of the "ph ->" is to introduce a hypothesis that may not
> always be satisfiable without some assumptions (and the exact nature of
> those assumptions is not known inside the theorem, so the generic "ph" is
> used). If we are dealing with a true abbreviation, just a short way to
> write some symbols, then the "D = ..." hypothesis will either be satisfied
> by a similar hypothesis, or by theorem eqid, which will force the
> substitution of "..." for "D" in the rest of the theorem. Since in any
> case, the hypothesis can be discharged with no assumptions, the "ph" is not

> necessary...

This is useful information. I've copied and pasted it into mmnatded.html
so others can see it.

--- David A. Wheeler

[fl]

"Notationally this system ends up being awkward for practical use. "

Hi David,

can you remove this sentence? I stopped for other reasons. Practically the system
is equivalent to Mario Carneiro's work.

--
FL

[David A. Wheeler]

Sure! Done. Thanks.

--- David A. Wheeler