Predicate calculus

[Jeremy Weissmann]

Hello all,

I came across this problem today, which is annoying me. Here let x and y be of the same nonempty type. We wish to show:

(*) (Ax : (Ey :: f.y) => f.x : g.x) => (Ex :: g.x) .

Being out of practice, I could only proceed by interpreting as follows: If f.x holds for some x , then (Ey :: f.y) => f.x holds, and hence g.x holds. So (Ex :: g.x) holds. Otherwise (Ey :: f.y) is false, in which case (Ey :: f.y) => f.x holds for every x , in which case g.x holds for every x , and since x’s type is nonempty, this means that (Ex :: g.x) holds.

Can someone help me calculate this?!

+j

[Jeremy Weissmann]

At the very least, I could figure out a calculation using a method I once called Skolemization or Case Analysis, which says that if I can calculate X using a property p.c , then to show X it suffices to show (Ec :: p.c) .

In the context of my problem, I wanted to show:

(*) (Ax : (Ey :: f.y) => f.x : g.x) => (Ex :: g.x) .

I can do this by putting the antecedent into the context and proving the consequent:

|[ (Ax : (Ey :: f.y) => f.x : g.x)

true
== { ** using (Ey :: f.y) => f.x }
g.x
=> { predicate calculus }
(Ex :: g.x)

]|

By Skolemization, it suffices to prove (Ex :: (Ey :: f.y) => f.x)) , which is a walkover:

(Ex :: (Ey :: f.y) => f.x))
== { x’s type is nonempty }
(Ey :: f.y) => (Ex :: f.y)
== { pred. calc. }
true .

[Jeremy Weissmann]

For the record, I have also called this the Heuristic of Auxiliary Symbols:

http://mathmeth.com/jaw/main/jaw0xx/jaw77.pdf

http://mathmeth.com/jaw/main/jaw0xx/jaw72.pdf

http://mathmeth.com/jaw/main/jaw1xx/jaw109.pdf

On Oct 2, 2024, at 17:20, Jeremy Weissmann <plusj...@gmail.com> wrote:

[Diethard Michaelis]

Hi Jeremy,

From the DS book near the end of chapter 5 (I renamed f into g ...)
(119) [(Ex::r.x)=>((Ax: r.x: g.x)=>Y == (Ex: r.x: g.x=>Y)))]

Substituting
. Y := (Ex::g.x)
. r.x := (Ey::f.y)=>f.x
the desideratum becomes the middle subexpression
. (Ax: r.x: g.x)=>Y
where range r is not empty i.e.
. [(Ex::r.x)]
on behalf of
. (Ex::(Ey::f.y)=>f.x)
. == { P=> over (Ex::) (non empty range true) }
. (Ey::f.y)=>(Ex::f.x)
. == {}
. true
and (on behalf of instantiation) we have
. [g.x=>Y]
and consequently (non empty r)
. [(Ex: r.x: g.x=>Y)]
the right subexpression is true, too.
Thus from (119) we conclude
. [true=>(desideratum == true)]
and we are done.

Cheers, Diethard.

[Jeremy Weissmann]

Hi all,

   Here is a new effort inspired by Diethard's work.  Of course we are saying very similar things, but in different ways.  I enjoy feeling out the slight differences in these presentations.

   We are asked to show:

     (Ax : (Ey :: f.y) => f.x : g.x)  =>  (Ex :: g.x)         .

Let us suppress some detail and rewrite this as:

(*)     (Ax : r.x : g.x)  =>  (Ex :: g.x)       ,

where  [ r.x  ==  (Ey :: f.y) => f.x ]  holds for all  x .

   But  (*)  is practically a theorem of predicate calculus, namely:

(0)   For nonempty range,  'for all'  implies  'there exists' .    (See Appendix.)

Thus  (*)  is established by:

     (Ax : r.x : g.x)

=>   {  (0) ,  provided  [ (Ex :: r.x) ]  }

     (Ex : r.x : g.x)

=>   { monotonicity of  E  }

     (Ex :: g.x)       ,

and the deferred proof obligation:

     (Ex :: r.x)

==   { unfolding  r  }

     (Ex :: (Ey :: f.y) => f.x)

==   {  (X =>)  over  E  for nonempty type }

     (Ey :: f.y) => (Ex :: f.x)

==   { predicate calculus }

     true     .

Appendix

   As for a proof of  (0) ,  we formalize it as:

(0)    (Ex :: r.x)  =>  ( (Ax : r.x : f.x) => (Ex : r.x : f.x) )     ,

and establish this as follows:

     (Ax : r.x : f.x) => (Ex : r.x : f.x)

==   {  =>  into  ¬  and  \/  }

     ¬(Ax : r.x : f.x)  \/  (Ex : r.x : f.x)

==   { de Morgan }

     (Ex : r.x : ¬f.x)  \/  (Ex : r.x : f.x)

==   { combining the term }

     (Ex : r.x : ¬f.x \/ f.x )

==   { excluded middle, shunting  r.x  to the term }

     (Ex :: r.x)     ,

which even shows the stronger:

(0')     (Ex :: r.x)   ==   (Ax : r.x : f.x) => (Ex : r.x : f.x)     .

Not only is  (0')  stronger than  (0) ,  but it requires one fewer parenthesis pair.

PS. There is a nagging feeling I have that some of my work from 20 years ago on unbracketed results could come into play here, but it was so long ago that I can't be sure.

[Diethard Michaelis]

The problem kept me busy for several hours spread over the last days.
There arose a proof using generalized "punctual" Leibniz for universal
(and existential) quantification, see DS book chapter 5 (101).
I refreshed my understanding of Skolemization a la WF278.

BUT FINALLY
I realized that I had once more missed to
USE PUNCTUALITY!

(J) (Ax : (Ey :: f.y) => f.x : g.x) => (Ex :: g.x)

is a punctual function of its subexpression "(Ey :: f.y)" as

Theorem: (Ax :: f.x.Z) and (Ex :: f.x.Z) are punctual in Z
provided for all x f.x.Z is, as function of predicate Z,
a punctual predicate transformer. END Theorem

A fact I know by heart and for decades.
(see EWD1187, "Boolean connectives yield punctual expressions")
https://www.cs.utexas.edu/~EWD/ewd11xx/EWD1187.PDF

Further I have the (my) "punctual = linear" theorem:
For punctual predicate transformer F
[F.X == F.true == X\/(F.true == F.false)]
(see DMGM.2001.Dez.25,
"Arithmetic, Linear Algebra, and Predicate Calculus").

Substituting false for (Ey :: f.y) in (J) yields
. (Ax :: g.x) => (Ex :: g.x)
which is a well known theorem and thus true.
And so is the more elaborate variant with (non empty) range
(A=>E) [ (Ex :: f.x) => ( (Ax : f.x : g.x) => (Ex : f.x : g.x) ) ].

Substituting true for (Ey :: f.y) in (J) yields
. ( (Ax : f.x : g.x) => (Ex :: g.x) ).

By elementary predicate calculus [(A => B == B == A\/B]
. [F.false] => [F.X == X => F.true]
and thus (J) becomes
. (Ey :: f.y) => ( (Ax : f.x : g.x) => (Ex :: g.x) )
which is
by the monotonicity of existential quantifiers and (P=>)
a consequence of (A=>E).

All this was done w/o paper and pen in my head.

Diethard.

> *Appendix*