[set.mm] The conditional operator for propositions

[Benoit]

Hi all,

A few months ago, I added the "conditional operator for propositions" to my mathbox (currently Section 21.29.1.6, beginning at http://us2.metamath.org/mpeuni/wif.html).  I propose to move it to the main part for the following reasons:
* it is a pretty natural operator
* it is analogous to the conditional operator for classes, which is already in the main part (see ~df-if)
* it is actually more fundamental than the conditional operator for classes, and the latter could be defined from it (~bj-df-ifc) in a way which is in line with the treatment of classes in set.mm (i.e. as extensions of predicates), and is similar to ~df-csb in terms of ~df-sbc and ~df-nfc in terms of ~df-nf; this would improve consistency of set.mm
* I recently noticed that it is implicitly used in theorems related to the weak deduction theorem (~elimh, ~dedt), and I added the corresponding theorems expressed using "if" (~bj-elimhyp, ~bj-dedthm); I think that this makes them easier to understand
* I just noticed that it appears in Mario's latest slides, among the first definitions in peano.mm0.

In a first step, I would only move the staple theorems (i.e., not the theorems related to the weak deduction theorem, and not the new definition of the conditional operator for classes), by creating a subsection just before "1.2.8  Abbreviated conjunction and disjunction of three wff's".

For the labeling/token/symbol: I would like to parallel the conventions for df-sb/~df-csb or df-nf/df-nfc, that is:
* tokens: ` if ` and ` if_ `
* symbol: "if" and "underlined if"
* inside labels: "if" (e.g., wif, df-if, iftru, ifor...) and "ifc" (e.g., cifc, df-ifc, ifctru...).

Finally, there are several possible definitions (~df-bj-if, ~bj-dfif2 through ~bj-dfif7).  Which one to take as *the* definition ?  The current one might be the easiest to understand.  On the other hand, I think that one should take one for which the two theorems ~bj-iftru and ~bj-iffal still hold intuitionistically.  I haven't checked all variants, but I think this works for ~bj-dfif2, which furthermore has no negation in it.  This would favor that one.

Thanks for any remarks and suggestions.
Benoît

[Jim Kingdon]

On 10/5/19 3:53 AM, Benoit wrote:

> Finally, there are several possible definitions (~df-bj-if, ~bj-dfif2
> through ~bj-dfif7).  Which one to take as *the* definition ?  The
> current one might be the easiest to understand. On the other hand, I
> think that one should take one for which the two theorems ~bj-iftru
> and ~bj-iffal still hold intuitionistically.  I haven't checked all
> variants, but I think this works for ~bj-dfif2, which furthermore has
> no negation in it.  This would favor that one.

Using bj-difif2 would (intuitionistically) gain bj-iffal but (I think)
lose bj-casesif (and probably a lot of other ways of demonstrating
if(ph, ps, ch)).

I suspect that none of this is very useful intuitionistically unless ph
is decidable (see for example
http://us2.metamath.org:88/ileuni/pm2.54dc.html ). Which probably makes
me lean towards the more straightforward df-bj-if

[Mario Carneiro]

Only definitions dfif6 and dfif7 fail the true/false theorems: you can prove ( -. ph -> ( if- ( ph , ps , ch ) <-> -. -. ch ) ) in these cases. As Jim says none of the different variations are particularly useful unless ph is decidable, but I have a preference for dfif5 because it is the only one that *implies* that ph is decidable, so you can put it to use in negative position as well.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/afb962aa-8b41-cdad-2ffa-e6dd4f6e8c93%40panix.com.

[Norman Megill]

On Saturday, October 5, 2019 at 6:53:27 AM UTC-4, Benoit wrote:

Hi all,

A few months ago, I added the "conditional operator for propositions" to my mathbox (currently Section 21.29.1.6, beginning at http://us2.metamath.org/mpeuni/wif.html).  I propose to move it to the main part for the following reasons:
* it is a pretty natural operator
* it is analogous to the conditional operator for classes, which is already in the main part (see ~df-if)
* it is actually more fundamental than the conditional operator for classes, and the latter could be defined from it (~bj-df-ifc) in a way which is in line with the treatment of classes in set.mm (i.e. as extensions of predicates), and is similar to ~df-csb in terms of ~df-sbc and ~df-nfc in terms of ~df-nf; this would improve consistency of set.mm

I agree it is more fundamental.  My main concern is how useful would it be.  Unlike the present df-if, where the need arises frequently, I don't think we have encountered much need for a predicate version.  Does anyone know what existing theorems or proofs would benefit from it?

In any case, I wouldn't like to see the present df-if defined in terms of it.  I find bj-df-ifc somewhat confusing at first, at least for me, requiring that I unwrap a couple of layers of abstraction in my head to understand the otherwise simple idea.  At a minimum it requires unnecessarily learning an extra definition that the reader probably won't encounter otherwise.
 

* I recently noticed that it is implicitly used in theorems related to the weak deduction theorem (~elimh, ~dedt), and I added the corresponding theorems expressed using "if" (~bj-elimhyp, ~bj-dedthm); I think that this makes them easier to understand

I agree they would make these easier to understand.  However, these theorems are just for illustration and used for anything, so it wouldn't make much difference to set.mm as a whole.  Even the more useful class versions (~elimhyp, ~dedth) are falling out of favor and used less and less.
 

* I just noticed that it appears in Mario's latest slides, among the first definitions in peano.mm0.

Mario, do you use it much, and in what situations?
 

In a first step, I would only move the staple theorems (i.e., not the theorems related to the weak deduction theorem, and not the new definition of the conditional operator for classes), by creating a subsection just before "1.2.8  Abbreviated conjunction and disjunction of three wff's".

For the labeling/token/symbol: I would like to parallel the conventions for df-sb/~df-csb or df-nf/df-nfc, that is:
* tokens: ` if ` and ` if_ `
* symbol: "if" and "underlined if"
* inside labels: "if" (e.g., wif, df-if, iftru, ifor...) and "ifc" (e.g., cifc, df-ifc, ifctru...).

Finally, there are several possible definitions (~df-bj-if, ~bj-dfif2 through ~bj-dfif7).  Which one to take as *the* definition ?  The current one might be the easiest to understand.  On the other hand, I think that one should take one for which the two theorems ~bj-iftru and ~bj-iffal still hold intuitionistically.  I haven't checked all variants, but I think this works for ~bj-dfif2, which furthermore has no negation in it.  This would favor that one.

If we do adopt it, I think bj-dfif5 is better (classically at least), for the same reason that the present df-if is more intuitive than dfif2 even though df-if has one more symbol.  I would have to think hard and maybe even write down a truth table to figure out what bj-dfif2 is saying. The negation is important for the intuitive "alternation" idea:  when ph is true it is this, or when ph is not true it is that.  While df-bj-if is closer to the intuitive idea, we still have that if ph is false then (ph -> ps) is true, yet the final result is ch, a kind of counter-intuitive inversion. To me, the pure ANDs and ORs of bj-dfif5 are clearer.

Let us hear what others think before deciding.

Norm

[Mario Carneiro]

On Sat, Oct 5, 2019 at 6:16 PM Norman Megill <n...@alum.mit.edu> wrote:

On Saturday, October 5, 2019 at 6:53:27 AM UTC-4, Benoit wrote:

* I just noticed that it appears in Mario's latest slides, among the first definitions in peano.mm0.

Mario, do you use it much, and in what situations?

Here's an example from peano.mm0:

theorem elwrite:

$ x <> y e. write F a b <-> ifp (x = a) (y = b) (x <> y e. F) $ =

 

In metamath notation that would be something like:

|- ( <. X , Y >. e. write F A B <-> ifp ( X = A , Y = B , <. X , Y >. e. F ) )

This modifies the value of the function or relation F at a particular point a, setting the value to b, and the theorem says that if x = a then it is true exactly at y = b, otherwise it is true where F is defined. (The nearest equivalent set.mm function is sSet.)

Personally, I think it's a good idea to have a notation, and for that notation to be as near to identical to "if" as possible, because it's basically circumventing a restriction of the type system that we can't just write if ( ph , foo , bar ) whenever foo and bar live in the same sort S to give something in sort S. You will not be mislead by thinking they are one and the same operation.

It can also be used together with bitwise type logical operations, such as df-cad and df-had.

In any case, I wouldn't like to see the present df-if defined in terms of it.  I find bj-df-ifc somewhat confusing at first, at least for me, requiring that I unwrap a couple of layers of abstraction in my head to understand the otherwise simple idea.  At a minimum it requires unnecessarily learning an extra definition that the reader probably won't encounter otherwise.

I think that if df-ifp exists, it is a given that df-if will be rewritten in terms of it. It would be totally in keeping with other similar definitions that define a class operation in terms of the logical analogue, e.g. df-un, df-in, df-v etc. (Actually df-v is an exception; it should probably read { x | T. } and I guess the use of x = x is a historical accident?) If df-ifp exists but df-if doesn't use it, then that means people will have to go through the mental gymnastics of understanding df-ifp twice (with the attendant worry that somehow it can't be reused and maybe this use is different). df-if is basically mixing two concerns, the lifting to classes and the logical operation, and if df-ifp exists then these concerns are cleanly separated.

My understanding has been that the reason df-ifp doesn't exist is because it isn't used often enough to warrant definition. I think I anticipated that it would show up more in MM0 due to the more computer science bent, but we will see; currently the only uses are in the "write" function and in the definition of "if" for nat (which basically serves the same purpose as set.mm's if for classes).

Mario

[Benoit]

 (Actually df-v is an exception; it should probably read { x | T. } and I guess the use of x = x is a historical accident?)

This has been proposed in https://groups.google.com/d/msg/metamath/V3jmbWUd_mM/RAk2DEA3FQAJ, with explanations that I still stand by.  With the new definition df-tru, I think there is even less of a reason to keep "x = x" (which by the way evaluates to false in one of the two semantics on the empty domain -- granted, in this case, the universal class is the empty class anyway!).

To answer one of Norm's questions: I don't think the conditional operator on definitions would benefit many theorems in the current version of set.mm, I haven't really checked.  My main motivation is actually to improve consistency, to be able to say, for instance: "if_" is to "if" what "F/_" is to "F/" and what "[_ / ]_" is to "[. / ].", and to emphasize that classes are defined as extensions of predicates, which has concrete consequences on proof structures.

As for the definitions, there are indeed two groups: dfif1--4 and dfif5--7 (dfif1 being the current ~df-bj-if), and the easiest to understand are the first of each group (dfif1 and dfif5).  I did put dfif1 as the main definition because the "if... then" is akin to the implication used in dfif1.   Norm and Mario prefer dfif5, because in intuitionistic logic, it has the advantage of implying decidability of phi (obvious).

 

Benoît

[Benoit]

On Sunday, October 6, 2019 at 12:50:37 AM UTC+2, Mario Carneiro wrote:

It can also be used together with bitwise type logical operations, such as df-cad and df-had.

To give an example, I added http://us.metamath.org/mpeuni/bj-cadif.html

  bj-cadif    |- (cadd ( ph , ps , ch ) <-> if- ( ch , ( ph \/ ps ) , ( ph /\ ps ) ) )

which groups cad0 and cad1.

 

I think that if df-ifp exists, it is a given that df-if will be rewritten in terms of it. It would be totally in keeping with other similar definitions that define a class operation in terms of the logical analogue, e.g. df-un, df-in, df-v etc. (Actually df-v is an exception; it should probably read { x | T. } and I guess the use of x = x is a historical accident?)

I added http://us.metamath.org/mpeuni/bj-df-v.html (and also bj-df-nul and bj-nul).

Benoît