--- In dcproof@yahoogroups.com, "Mark Hurd" <markhurd@o...> wrote:
> Currently the Cases rule corresponds to:
>
> [P | Q] & [[P => R] & [Q => R]] => R
>
> However this can be generalised to:
>
> [P | Q] & [[P => R] & [Q => S]] => R | S
>

And interesting possibility, but does this really come up that
often? I'm sure there are hundreds of PC theorems I could implement.
For pedagogical reasons, however, I really need to draw the line
somewhere.


> And the above result then needs R | R => R, which does not seem as
> trivial as it should be with DC Proof's current rules.
>

I don't like this approach. If I were to implement a generalized
Cases, I would make it entirely separate from the Cases rule I have
now.


> I suggest Dan changes cases to the general version and adds a rule
that
> helps prove P | P => P when needed.
>

The latter would be easy to implement, but again, is it used all
that often?

Dan

Homepage: www.dcproof.com

I will implement an XOR operator.

Any suggestions for notation? I don't want to use "XOR" or "xor"
because these are currently interpreted as a proposition and a
variable respectively. Mark has suggested <>. This has the advantage
of being easy to implement. But it is also used in Basic for "not
equal." It might be confusing to CS students. What about *| ? I will
inquire in other forums as well.

My proposed rule, along the lines of the DeMorgan rule, would be:

A xor B  <-->  [A | B] & ~[A & B]

Would other xor rules be useful?

Dan

Homepage: www.dcproof.com


--- In dcproof@yahoogroups.com, "Mark Hurd" <markhurd@o...> wrote:
> Dan might have a different point of view in this case, but he
mostly chooses to implement features corresponding to basic teaching
of logic as he observes, interprets, and prefers it.
>
> Thus, AFAIK there is no commonly used XOr operator in written
logic (other than <> perhaps) and so I don't expect Dan would be
interested.
>
> Nevertheless, I too have dealt with [P & ~Q] | [~P & Q] a lot (and
changing from this form to your's below is NOT trivial...) and as
programmer, wouldn't mind an XOr operator, and corresponding rules
of logic.
>
> Regards,
> Mark Hurd, B.Sc.(Ma.) (Hons.)
> ----- Original Message -----
> From: michaelg_lew
> To: dcproof@yahoogroups.com
> Sent: Wednesday, March 24, 2004 5:33 AM
> Subject: [dcproof] Exclusive OR (XOR)
>
>
> How can I use XOR or an equivalent function in DCProof?
>
> I could not find it.  An equivalent can be written as
>
>   A XOR B = [A | B ] & ~ [ A & B ]
>
> One could use that to write a logical function which is okay with
> me but if that is possible in DCProof, I did not understand it and
> kept getting errors in the premises window.
>
> I think cases is an application derived from XOR, and in some
> logics, such as in QBasic, XOR is not even included among the
> logical operators.
>
> Mike Lewis
>
>
>
>
> -------------------------------------------------------------------
-------------
> Yahoo! Groups Links
>
>   a.. To visit your group on the web, go to:
>   http://groups.yahoo.com/group/dcproof/
>
>   b.. To unsubscribe from this group, send an email to:
>   dcproof-unsubscribe@yahoogroups.com
>
>   c.. Your use of Yahoo! Groups is subject to the Yahoo! Terms of
Service.
>
>
>
> [Non-text portions of this message have been removed]

Here are the promised definitions of symmetric difference (delta) as
promised:

www.dcproof.com/delta.proof  (DC Proof format)

www.dcproof.com/delta.html   (HTML format)

Dan


--- In dcproof@yahoogroups.com, "michaelg_lew" <mglewis@q...> wrote:
> How can I use XOR or an equivalent function in DCProof?
>
> I could not find it.  An equivalent can be written as
>
>   A XOR B = [A | B ] & ~ [ A & B ]
>
> One could use that to write a logical function which is okay with
> me but if that is possible in DCProof, I did not understand it and
> kept getting errors in the premises window.
>
> I think cases is an application derived from XOR, and in some
> logics, such as in QBasic, XOR is not even included among the
> logical operators.
>
> Mike Lewis

Currently the Cases rule corresponds to:

[P | Q] & [[P => R] & [Q => R]] => R

However this can be generalised to:

[P | Q] & [[P => R] & [Q => S]] => R | S

And the above result then needs R | R => R, which does not seem as
trivial as it should be with DC Proof's current rules.

I suggest Dan changes cases to the general version and adds a rule that
helps prove P | P => P when needed.

Regards,
Mark Hurd, B.Sc.(Ma.) (Hons.)

Dan might have a different point of view in this case, but he mostly chooses to
implement features corresponding to basic teaching of logic as he observes,
interprets, and prefers it.

Thus, AFAIK there is no commonly used XOr operator in written logic (other than
<> perhaps) and so I don't expect Dan would be interested.

Nevertheless, I too have dealt with [P & ~Q] | [~P & Q] a lot (and changing from
this form to your's below is NOT trivial...) and as programmer, wouldn't mind an
XOr operator, and corresponding rules of logic.

Regards,
Mark Hurd, B.Sc.(Ma.) (Hons.)
----- Original Message -----
From: michaelg_lew
To: dcproof@yahoogroups.com
Sent: Wednesday, March 24, 2004 5:33 AM
Subject: [dcproof] Exclusive OR (XOR)


How can I use XOR or an equivalent function in DCProof?

I could not find it.  An equivalent can be written as

   A XOR B = [A | B ] & ~ [ A & B ]

One could use that to write a logical function which is okay with
me but if that is possible in DCProof, I did not understand it and
kept getting errors in the premises window.

I think cases is an application derived from XOR, and in some
logics, such as in QBasic, XOR is not even included among the
logical operators.

Mike Lewis




--------------------------------------------------------------------------------
Yahoo! Groups Links

   a.. To visit your group on the web, go to:
   http://groups.yahoo.com/group/dcproof/

   b.. To unsubscribe from this group, send an email to:
   dcproof-unsubscribe@yahoogroups.com

   c.. Your use of Yahoo! Groups is subject to the Yahoo! Terms of Service.



[Non-text portions of this message have been removed]

Mike,

You cannot define your own logical operators in DC Proof. You can,
however, define symmetric difference -- the set theoretic equivalent
of XOR. To get an idea of how to do this, see the Set Operators
option of the Sets menu. This defines the interestion (&&), union
(||), and complement (`) operators. I will post a suitable
definition in a day or two.

Dan

Homepage: http://wwww.dcproof.com



--- In dcproof@yahoogroups.com, "michaelg_lew" <mglewis@q...> wrote:
> How can I use XOR or an equivalent function in DCProof?
>
> I could not find it.  An equivalent can be written as
>
>   A XOR B = [A | B ] & ~ [ A & B ]
>
> One could use that to write a logical function which is okay with
> me but if that is possible in DCProof, I did not understand it and
> kept getting errors in the premises window.
>
> I think cases is an application derived from XOR, and in some
> logics, such as in QBasic, XOR is not even included among the
> logical operators.
>
> Mike Lewis

How can I use XOR or an equivalent function in DCProof?

I could not find it.  An equivalent can be written as

   A XOR B = [A | B ] & ~ [ A & B ]

One could use that to write a logical function which is okay with
me but if that is possible in DCProof, I did not understand it and
kept getting errors in the premises window.

I think cases is an application derived from XOR, and in some
logics, such as in QBasic, XOR is not even included among the
logical operators.

Mike Lewis

Substitution should also work:

       DC Proof 1.0 - Subst Test
	 1 x=y
		 Premise

	 2 x=x
		 Substitute, 1, 1

	 3 y=x
		 Substitute, 1, 2

4 x=y => y=x
	 Conclusion, 1

5 ALL(y):[x=y => y=x]
	 U Gen, 4

6 ALL(x):ALL(y):[x=y => y=x]
	 U Gen, 5

	 7 x+y=z
		 Premise

	 8 x+y=x+y
		 Substitute, 7, 7

	 9 z=x+y
		 Substitute, 7, 8

10 x+y=z => z=x+y
	 Conclusion, 7

11 ALL(z):[x+y=z => z=x+y]
	 U Gen, 10

12 ALL(y):ALL(z):[x+y=z => z=x+y]
	 U Gen, 11

13 ALL(x):ALL(y):ALL(z):[x+y=z => z=x+y]
	 U Gen, 12



The tricks are to understand what order you need to click each side of the equal
statement and to only apply the substitution to one of the sides of expr=expr
line.

Regards,
Mark Hurd, B.Sc.(Ma.) (Hons.)

--------------------------------------------------------------------------------

----- Original Message -----
From: Rafael Pe%ffaloza
To: dcproof@yahoogroups.com
Sent: Saturday, March 20, 2004 4:15 AM
Subject: [dcproof] Change of Equality order


I have a new petition or suggestion on improvement.

Suppose I want to prove that a<b => b>a

Given your definitions of '<' and '>', there is a point in the proof
where I have

a+k=b

but I need

b=a+k

The simplest way to do the needed change should be to use the
Substitution, but for a reason I don't understand, no matter if I
click the right or left side of the expresions, after I do the two
substitutions, I end up again with

a+k=b

Is there a way to change this?

Thanks
Rafael


[Non-text portions of this message have been removed]

--- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
<rpenalozan@y...> wrote:
> I have a new petition or suggestion on improvement.
>
> Suppose I want to prove that a<b => b>a
>
> Given your definitions of '<' and '>', there is a point in the
proof
> where I have
>
> a+k=b
>
> but I need
>
> b=a+k
>
> The simplest way to do the needed change should be to use the
> Substitution, but for a reason I don't understand, no matter if I
> click the right or left side of the expresions, after I do the two
> substitutions, I end up again with
>
> a+k=b
>
> Is there a way to change this?
>

Yes. Use the Symmetry option of the Sets menu.

Dan

Homepage: http://www.dcproof.com

Effective: March 20, 2004  1:45 AM

New beta release including fix of bugs in Set Operations option of
Sets menu, and other modules that did not recognize set operators:
intersection (&&), union (||) and complement (`).

Download from DC Proof Online at

http://www.dcproof.com


Or download directly from

http://www.dcproof.com/dcpsetup.exe


Dan Christensen
Toronto, Canada

The Set Operations option on the Set menu does not work at all.
There may sometimes be a problem parsing the set intersection (&&)
and set union (||) operators (when linebreaks are inserted). This
problem will probably be fixed this weekend. I apologize for the
inconvenience.

Dan

--- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
<rpenalozan@y...> wrote:
> Maybe I'm not making myself clear enough. Forget about group theory
> and 0, and suppose I have a new operator, which is no more than a
> closed funcion, I want to use (just as an example) which is
different
> to those given in the definitions you have of sum, difference, etc.
> (Just to give a motivation to this, suppose I want to use the
absolute
> value of a number; THIS IS NOT THE ONLY THING I WANT, I'M JUST
GIVING
> AN EXAMPLE).

I understood that the group theoretic 0 was just an example. I
mentioned it again only to show that it could be handled in two
different ways.


Then, I can post the definition as a premise, but doing
> that will force me to put that definition EACH AND EVERY TIME I
use it
> (for the method the program uses block every used premise). On the
> other hand, if there was a way to give that as a definition (or as
an
> axiom), I wouldn't need to do that.
>
>   That is what I want, nothing more. And I don't think it should
be a
> big problem to include that.
>

It is not a big problem to implement, but I don't see how this would
save you any time. Either way, a user data file must be maintained,
and you must find the definition/file in a list, somehow open that
file and load it into the main text box. The only advantage I can
see, is that you wouldn't have to, declare all your definitions,
etc. at the beginning of your proof. But wouldn't you do this
normally anyway? As much as possible, it's good to see all your
assumptions declared explicitly up front in a formal proof, don't
you think? Have I missed something obvious?

Dan

Homepage: http://www.dcproof.com

I have a new petition or suggestion on improvement.

Suppose I want to prove that a<b => b>a

Given your definitions of '<' and '>', there is a point in the proof
where I have

a+k=b

but I need

b=a+k

The simplest way to do the needed change should be to use the
Substitution, but for a reason I don't understand, no matter if I
click the right or left side of the expresions, after I do the two
substitutions, I end up again with

a+k=b

Is there a way to change this?

Thanks
Rafael

Maybe I'm not making myself clear enough. Forget about group theory
and 0, and suppose I have a new operator, which is no more than a
closed funcion, I want to use (just as an example) which is different
to those given in the definitions you have of sum, difference, etc.
(Just to give a motivation to this, suppose I want to use the absolute
value of a number; THIS IS NOT THE ONLY THING I WANT, I'M JUST GIVING
AN EXAMPLE). Then, I can post the definition as a premise, but doing
that will force me to put that definition EACH AND EVERY TIME I use it
(for the method the program uses block every used premise). On the
other hand, if there was a way to give that as a definition (or as an
axiom), I wouldn't need to do that.

   That is what I want, nothing more. And I don't think it should be a
big problem to include that.

Thanks,
Rafael


--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@n...> wrote:
> --- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
> <rpenalozan@y...> wrote:
> > The definition of 0 was just a simple example. I am dealing right
> now
> > with Bayesian Networks. I know that DCProof isn't intended for this
> > kind of applications, but I want to try out the program in this
> kind
> > of environments, as this will probably show some improvements that
> > could be made.
> >
> > I don't think that the solution could be for you to add all kinds
> of
> > definitions as they are needed (for this may be a hard work for
> you,
> > and too slow for people like me), rather give a way to write
> > definitions of our own, that may act as your definition of group.
>
> [snip]
>
> Definitions such as I provide for group theory -- with modifications
> if desired -- can easily be put in a file, along with previously
> obtained results (theorems, lemmas, etc.). It is no more difficult
> or time consuming to open such a file than it is to click a menu
> option for a built-in definition. You can even post such files at
> your own homepage to let others download and play around with them --
> just upload your *.proof file to your website and create a hyperlink
> to it using the .proof extension.
>
> Dan
>
> http://www.dcproof.com

--- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
<rpenalozan@y...> wrote:
> The definition of 0 was just a simple example. I am dealing right
now
> with Bayesian Networks. I know that DCProof isn't intended for this
> kind of applications, but I want to try out the program in this
kind
> of environments, as this will probably show some improvements that
> could be made.
>
> I don't think that the solution could be for you to add all kinds
of
> definitions as they are needed (for this may be a hard work for
you,
> and too slow for people like me), rather give a way to write
> definitions of our own, that may act as your definition of group.

[snip]

Definitions such as I provide for group theory -- with modifications
if desired -- can easily be put in a file, along with previously
obtained results (theorems, lemmas, etc.). It is no more difficult
or time consuming to open such a file than it is to click a menu
option for a built-in definition. You can even post such files at
your own homepage to let others download and play around with them --
just upload your *.proof file to your website and create a hyperlink
to it using the .proof extension.

Dan

http://www.dcproof.com

Raphael,

Would you please give me an example of a formal defintion that you
have found to be problematic. Is it a question of notation?

Dan


--- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
<rpenalozan@y...> wrote:
> The definition of 0 was just a simple example. I am dealing right
now
> with Bayesian Networks. I know that DCProof isn't intended for this
> kind of applications, but I want to try out the program in this
kind
> of environments, as this will probably show some improvements that
> could be made.
>
> I don't think that the solution could be for you to add all kinds
of
> definitions as they are needed (for this may be a hard work for
you,
> and too slow for people like me), rather give a way to write
> definitions of our own, that may act as your definition of group.
> This may be useful for beginners also, as they may be able
to "play"
> with the definition of (for example) natural numbers, and see which
> properties are changed; this may lead to find out and understand
other
> numerical entities.
>
> Thanks
> RPN
>
> --- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@n...>
wrote:
> > --- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
> > <rpenalozan@y...> wrote:
> > > --- In dcproof@yahoogroups.com, "Dan Christensen"
<dchris@n...>
> > wrote:
> > > > I received this question a few days ago:
> > > >
> > > > I have a question on DCProof; is there a way to make
definitions
> > > > (for example, define how will a predicate or a function
should
> > be
> > > > interpreted)? I know I may use the iff as a premise to
create a
> > > > definition, but in that case, I would have to make that
premise
> > > > every time I need to use my definition (for the premise
becomes
> > > > inactive). And on the other hand, the use of the iff becomes
a
> > > > little problematic (in definitions).
> > > >
> > > >
> > > > Here was my reply:
> > > >
> > > > There are two ways to bring definitions over to a new proof:
> > > >
> > > > 1. You can copy and paste the text of individual statements
from
> > > one
> > > > proof to another. In DC Proof, open the old proof file that
has
> > the
> > > > definition you want. Highlight the text of the statement and
> > click
> > > > edit/copy. Then open your new proof, click Premise, paste
the
> > old
> > > > text into the text box of the Premise form, etc. You can
also
> > copy
> > > > the result (theorem or lemma) from one proof to be a Premise
in
> > > > another.
> > > >
> > > > 2. You can also create a proof file containing one of more
> > > > definitions (or axioms), along with comments, etc. When you
want
> > to
> > > > start a new proof using those definitions, open that file
and
> > > > immediately save it under your new proof file name. This
will
> > leave
> > > > your definitions file unchanged.
> > > >
> > > > Dan
> > >
> > >   This approach isn't convenient for the developments I am
> > intending
> > > to use. Let me give you an example: I want to prove (or check
out)
> > > all the distinct properties of the element 0 in a group. Then
I
> > have
> > > to define what 0 means (the additive neutro). Now, what is the
> > > problem?, that every simple property I want to prove, I have
to
> > > define 0, while if I could just have a Definition, I could use
> > this
> > > simbol to prove all the properties in a row, without needing
to
> > copy
> > > or do stuff like that.
> > >   I hope you could help me with this
> > > RPN
> >
> > In this particular case, I do have the defintion of 0 (for
groups)
> > built into the  program. Click on the Numbers menu and select
the
> > Group Axioms option. This will generate a Premise containing the
5
> > axioms for groups. Likewise, I have Peano's Axioms for the
natural
> > numbers, definitions for the various arithmetic operators on N
and
> > the axioms of ring theory. If readers have suggestions for other
> > suitable definitions, please write to me here, and I will
consider
> > incorporating them in a future release.
> >
> > Dan
> >
> > DC Proof homepage: http://www.dcproof.com

The definition of 0 was just a simple example. I am dealing right now
with Bayesian Networks. I know that DCProof isn't intended for this
kind of applications, but I want to try out the program in this kind
of environments, as this will probably show some improvements that
could be made.

I don't think that the solution could be for you to add all kinds of
definitions as they are needed (for this may be a hard work for you,
and too slow for people like me), rather give a way to write
definitions of our own, that may act as your definition of group.
This may be useful for beginners also, as they may be able to "play"
with the definition of (for example) natural numbers, and see which
properties are changed; this may lead to find out and understand other
numerical entities.

Thanks
RPN

--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@n...> wrote:
> --- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
> <rpenalozan@y...> wrote:
> > --- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@n...>
> wrote:
> > > I received this question a few days ago:
> > >
> > > I have a question on DCProof; is there a way to make definitions
> > > (for example, define how will a predicate or a function should
> be
> > > interpreted)? I know I may use the iff as a premise to create a
> > > definition, but in that case, I would have to make that premise
> > > every time I need to use my definition (for the premise becomes
> > > inactive). And on the other hand, the use of the iff becomes a
> > > little problematic (in definitions).
> > >
> > >
> > > Here was my reply:
> > >
> > > There are two ways to bring definitions over to a new proof:
> > >
> > > 1. You can copy and paste the text of individual statements from
> > one
> > > proof to another. In DC Proof, open the old proof file that has
> the
> > > definition you want. Highlight the text of the statement and
> click
> > > edit/copy. Then open your new proof, click Premise, paste the
> old
> > > text into the text box of the Premise form, etc. You can also
> copy
> > > the result (theorem or lemma) from one proof to be a Premise in
> > > another.
> > >
> > > 2. You can also create a proof file containing one of more
> > > definitions (or axioms), along with comments, etc. When you want
> to
> > > start a new proof using those definitions, open that file and
> > > immediately save it under your new proof file name. This will
> leave
> > > your definitions file unchanged.
> > >
> > > Dan
> >
> >   This approach isn't convenient for the developments I am
> intending
> > to use. Let me give you an example: I want to prove (or check out)
> > all the distinct properties of the element 0 in a group. Then I
> have
> > to define what 0 means (the additive neutro). Now, what is the
> > problem?, that every simple property I want to prove, I have to
> > define 0, while if I could just have a Definition, I could use
> this
> > simbol to prove all the properties in a row, without needing to
> copy
> > or do stuff like that.
> >   I hope you could help me with this
> > RPN
>
> In this particular case, I do have the defintion of 0 (for groups)
> built into the  program. Click on the Numbers menu and select the
> Group Axioms option. This will generate a Premise containing the 5
> axioms for groups. Likewise, I have Peano's Axioms for the natural
> numbers, definitions for the various arithmetic operators on N and
> the axioms of ring theory. If readers have suggestions for other
> suitable definitions, please write to me here, and I will consider
> incorporating them in a future release.
>
> Dan
>
> DC Proof homepage: http://www.dcproof.com

Effective: March 17, 2004 4:30PM EST

New beta release including:

1. Change to enable use of Copy and Find functions at any point in
processing, the only exception being the invoking of the Existential
Generalization rule.

2. Updated User Manual -- "Edit Menu Options" -- to reflect this.


Download at DC Proof Online website at

http://www.dcproof.com


Or download directly from

http://www.dcproof.com/dcpsetup.exe

Dan Christensen
Toronto, Canada

If you downloaded DC Proof yesterday, you may have the wrong
version -- one that still contains a bug in Find form. To ensure you
have the correct version, download the latest version date March 13
at DC Proof Online at

http://www.dcproof.com

Or click

http://www.dcproof.com/dcpsetup.exe

I apologize for any inconvenience.

Dan

Effective: 2004-03-11

New Beta release for DC Proof 1.0 with the following update:

1. Fixed error in Find form that did not properly process special
character, epsilon


Download new version at DC Proof homepage

http://www.dcproof.com


Or download directly by clicking on

http://www.dcproof.com/dcpsetup.exe


Dan

--- In dcproof@yahoogroups.com, "Rafael Pe%ffaloza"
<rpenalozan@y...> wrote:
> --- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@n...>
wrote:
> > I received this question a few days ago:
> >
> > I have a question on DCProof; is there a way to make definitions
> > (for example, define how will a predicate or a function should
be
> > interpreted)? I know I may use the iff as a premise to create a
> > definition, but in that case, I would have to make that premise
> > every time I need to use my definition (for the premise becomes
> > inactive). And on the other hand, the use of the iff becomes a
> > little problematic (in definitions).
> >
> >
> > Here was my reply:
> >
> > There are two ways to bring definitions over to a new proof:
> >
> > 1. You can copy and paste the text of individual statements from
> one
> > proof to another. In DC Proof, open the old proof file that has
the
> > definition you want. Highlight the text of the statement and
click
> > edit/copy. Then open your new proof, click Premise, paste the
old
> > text into the text box of the Premise form, etc. You can also
copy
> > the result (theorem or lemma) from one proof to be a Premise in
> > another.
> >
> > 2. You can also create a proof file containing one of more
> > definitions (or axioms), along with comments, etc. When you want
to
> > start a new proof using those definitions, open that file and
> > immediately save it under your new proof file name. This will
leave
> > your definitions file unchanged.
> >
> > Dan
>
>   This approach isn't convenient for the developments I am
intending
> to use. Let me give you an example: I want to prove (or check out)
> all the distinct properties of the element 0 in a group. Then I
have
> to define what 0 means (the additive neutro). Now, what is the
> problem?, that every simple property I want to prove, I have to
> define 0, while if I could just have a Definition, I could use
this
> simbol to prove all the properties in a row, without needing to
copy
> or do stuff like that.
>   I hope you could help me with this
> RPN

In this particular case, I do have the defintion of 0 (for groups)
built into the  program. Click on the Numbers menu and select the
Group Axioms option. This will generate a Premise containing the 5
axioms for groups. Likewise, I have Peano's Axioms for the natural
numbers, definitions for the various arithmetic operators on N and
the axioms of ring theory. If readers have suggestions for other
suitable definitions, please write to me here, and I will consider
incorporating them in a future release.

Dan

DC Proof homepage: http://www.dcproof.com

--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@n...> wrote:
> I received this question a few days ago:
>
> I have a question on DCProof; is there a way to make definitions
> (for example, define how will a predicate or a function should be
> interpreted)? I know I may use the iff as a premise to create a
> definition, but in that case, I would have to make that premise
> every time I need to use my definition (for the premise becomes
> inactive). And on the other hand, the use of the iff becomes a
> little problematic (in definitions).
>
>
> Here was my reply:
>
> There are two ways to bring definitions over to a new proof:
>
> 1. You can copy and paste the text of individual statements from
one
> proof to another. In DC Proof, open the old proof file that has the
> definition you want. Highlight the text of the statement and click
> edit/copy. Then open your new proof, click Premise, paste the old
> text into the text box of the Premise form, etc. You can also copy
> the result (theorem or lemma) from one proof to be a Premise in
> another.
>
> 2. You can also create a proof file containing one of more
> definitions (or axioms), along with comments, etc. When you want to
> start a new proof using those definitions, open that file and
> immediately save it under your new proof file name. This will leave
> your definitions file unchanged.
>
> Dan

   This approach isn't convenient for the developments I am intending
to use. Let me give you an example: I want to prove (or check out)
all the distinct properties of the element 0 in a group. Then I have
to define what 0 means (the additive neutro). Now, what is the
problem?, that every simple property I want to prove, I have to
define 0, while if I could just have a Definition, I could use this
simbol to prove all the properties in a row, without needing to copy
or do stuff like that.
   I hope you could help me with this
RPN

Effective: 2004-03-07

New Beta release for DC Proof 1.0 with the following updates:

1. Fixed error message in the Premise Rule that pointed to the wrong
line number when inserting a Premise mid-proof.

2. Modified user documentation for the Premise Rule to clarify the
meaning of these error messages.


Download new version at DC Proof homepage

http://www.dcproof.com


Or download directly by clicking on

http://www.dcproof.com/dcpsetup.exe

I received this question a few days ago:

I have a question on DCProof; is there a way to make definitions
(for example, define how will a predicate or a function should be
interpreted)? I know I may use the iff as a premise to create a
definition, but in that case, I would have to make that premise
every time I need to use my definition (for the premise becomes
inactive). And on the other hand, the use of the iff becomes a
little problematic (in definitions).


Here was my reply:

There are two ways to bring definitions over to a new proof:

1. You can copy and paste the text of individual statements from one
proof to another. In DC Proof, open the old proof file that has the
definition you want. Highlight the text of the statement and click
edit/copy. Then open your new proof, click Premise, paste the old
text into the text box of the Premise form, etc. You can also copy
the result (theorem or lemma) from one proof to be a Premise in
another.

2. You can also create a proof file containing one of more
definitions (or axioms), along with comments, etc. When you want to
start a new proof using those definitions, open that file and
immediately save it under your new proof file name. This will leave
your definitions file unchanged.

Dan

See the DC Proof 1.0, Beta Test Status Report at

http://www.dcproof.com/StatusReport.htm

Dan

Question received by e-mail today:

How stable and safe do you think the current version is?

My reply:

Quite stable. Today's release had only minor changes, as did the
last release on Feb. 15.  I have been using it quite a bit to write
several proofs, hundreds of lines each. Since I first released it in
December, DC Proof hasn't crashed or hung up the system on my XP
machine. It is written in Visual Basic 6. It's really quite low
tech. Apart from the help files, it's just text and simple binary
files. A completely standard MS setup. It's compact too. The exe
file is only 724 KB. (Several other standard MS/VB run-time modules
are downloaded with it.)

I have had about three hundred downloads in February alone. There
have been no serious complaints since that intial probelm with the
help screen. That's a good sign, I guess.

Dan

One reader at a math newsgroup suggested:

I would suggest to use the COMMON quantifiers

(Ax)   and   (Ex)

instead of the extremely uncommon and rather irritating

ALL(x):   and   EXISTS(x):

A quantifier is not a function, mind that! (In addition this would
*improve* readability [of complex statements] a good deal!)


Same for the connective "or", the symbole here definitely SHOULD BE

v

and NOT

|.


Moreover imho it would be a good idea to use the simple symbols

->   and   <->

instead of the more complicated and less clear

=>   and   <=>.

Note that there are approaches in logic where the latter symbols are
used either at meta-level or to express some semantical relation(s).

[End of quote]


The intended user of DC Proof is the non-specialist undergraduate or
advanced high school student. My guiding principles on the use of
notation are that it should be:

1. as close as practical (given the standard keyboard characters) to
that used in mathematics textbooks and classrooms,

2. easy to learn, and

3. make use of meaningful variable names on any length.


On my use of the quantifiers "ALL" and "EXIST":

Every undergraduate algebra and calculus textbook that if have seen
makes use of expressions like "for all x" and "there exists a y."
The use of quantifiers "ALL" and "EXIST," therefore, will be more
familiar and more meaningful to the intended user.

And since variables names of any length are allowed, there must be
some delimiter (round brackets) at the beginning and end of the
variable.

"ALL" and "EXIST" are key words in DC Proof. As such these
quantifiers are not likely to be confused with functions or
predicates.

Note that the user need not memorize the notation. On the Premise
form, for example, there is a Notation menu with Ctrl-key shortcuts.
Ctrl-e inserts the string "EXIST( ):" at the cursor and repositions
the cursor between the brackets for the user to key in the variable
name.


On my use of "|" rather than "v" for the OR-operator:

In DC Proof, "v" can be used as a variable name. It can also be
embedded in a variable, proposition or predicate. The string "AvB",
for example, would be interpreted as a logical proposition. So, some
non-alphabetic symbol for the OR-operator was required. I chose "|"
as the most esthetic alternative, and because it is used as an OR-
operator in some programming languages.


On the use of "=>" and "<=>" rather than "->" and "<->":

It has been my experience that "=>" is used by instructors in
mathematics classrooms for "implies". They use "->" to indicate a
mapping or correspondence. Thus, the intended user will be more
familiar with the use of "=>" for "implies." Similarly with the use
of "<=>" for "if and only if". In my experience, the intended user
will not be very much concerned with meta-levels, semantical
relations etc.


What do readers here think? I would appreciate your comments.

Dan

Effective: 2004-03-03

New Beta release for DC Proof 1.0 with the following updates:

1. Added industry standard Ctrl-key shortcuts for Undo, Redo, Cut,
Copy, Paste in various forms.

2. Fixed minor bug in Open command. Error message on status line now
blanked out on successful retry after attempting to open an a
invalid proof file.


Download new version at DC Proof homepage

http://www.dcproof.com


Or download directly by clicking on

http://www.dcproof.com/dcpsetup.exe


Dan Christensen

PS: What do you think of DC Proof? Your comments and suggestions
would really be appreciated. Let's try to get some discussion going
at the DC Proof Users' Group.

One user has written to me to suggest:

"A big feature could be to allow any propositional calculus lemma to
be used as new axioms. Eg. The tutorial proves P&Q=>Q&P, but
currently that doesn't help to change S&R to R&S later in the same
proof or in another proof.

"Also, it would be good if the final line of any saved proof with no
open premises could be introduced into another proof."


What to you think? Here was my reply to him:

"It was difficult to strike a balance between austerity for
educational purposes and useability. (This was especially true for
the rules/axioms of set theory.)  Rather than using every theorem in
PC as another axiom, my preference is to identify a small number of
them that will be used time and again (e.g. the Contrapositive,
Detachment and Cases rules, etc.), and hard-code them into my
program.

"As for using the results of one proof in another, you can
accomplish this by simply copying the text of the result and
introducing it as a premise in subsequent proofs."


Dan

Effective: 2004-02-15

New Beta release with the following updates:

1. Added Alt-key shortcuts for menus
2. Reorganized Logic menu
3. Revised User Manual - Rules of Inference / Logic

Dan Christensen
dc@...
Visit DC Proof Online at http://www.dcproof.com