100 views

Skip to first unread message

Feb 10, 2017, 7:06:40 PM2/10/17

to metamath

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

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

Feb 13, 2017, 3:32:00 PM2/13/17

to meta...@googlegroups.com

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

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.

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

Feb 13, 2017, 4:52:06 PM2/13/17

to meta...@googlegroups.com, Giovanni Mascellani

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.
>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

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.

The text already notes that hypothesis can include definitions. Is that not clear enough? If not, how can we make it clearer?

Thanks!

--- David A.Wheeler

Feb 14, 2017, 12:43:58 PM2/14/17

to meta...@googlegroups.com

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.

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?

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.

Feb 14, 2017, 1:11:31 PM2/14/17

to metamath, metamath

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.
> >> * 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.

> 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...

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

Feb 14, 2017, 2:35:31 PM2/14/17

to metamath

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:Done; it's in the "develop" branch.

> >> * 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.

> 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) )

$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) )

$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 ) ) )

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

Feb 15, 2017, 1:04:46 PM2/15/17

to metamath, metamath

> 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...
> 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

This is useful information. I've copied and pasted it into mmnatded.html

so others can see it.

--- David A. Wheeler

Feb 17, 2017, 1:30:38 PM2/17/17

to Metamath, dwhe...@dwheeler.com

"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

Feb 17, 2017, 10:10:04 PM2/17/17

to metamath, Metamath

--- David A. Wheeler

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu