--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@...> wrote:
>
> Here are the axioms for the real numbers that users of DC Proof may
> find useful for doing proofs in real analysis (calculus). I will
> include it in the Samples directory of the next release due in the
> near future.
>
> http://www.dcproof.com/AxiomsRealNumbers.proof (DC Proof format)
>
> http://www.dcproof.com/AxiomsRealNumbers.html  (HTML format)
>

Corrected last line of "Field Axioms" (line 1)to include proviso that
~a=0. Thanks to Mark Hurd for pointing this out this error.

Dan

Here are the axioms for the real numbers that users of DC Proof may
find useful for doing proofs in real analysis (calculus). I will
include it in the Samples directory of the next release due in the
near future.

http://www.dcproof.com/AxiomsRealNumbers.proof (DC Proof format)

http://www.dcproof.com/AxiomsRealNumbers.html  (HTML format)

Dan Christensen

Dear members,

Here is my new version of the proof written with the new Subset Rule
(see line 37).

Down load in DC Proof format by clicking on:

http://www.dcproof.com/ConstructN2.proof


OR

View on your web browser at:

http://www.dcproof.com/ConstructN2.html

Thanks to Norman Megill of "Metamath" fame, as well as the list's
own Mark Hurd for their helpful suggestions and insights.

Dan


--- In dcproof@yahoogroups.com, "Dan Christensen" <dchris@...> wrote:
>
> Dear members,
>
> Here is another, considerably simpler approach to working with
real
> numbers in DC Proof. Rather than constructing the reals starting
> with Peano's Axioms for the natural numbers (a HUGE undertaking!),
> here we do the opposite -- we start with the axioms for real
numbers
> R, as presented in most introductory texts, and construct the
> natural numbers FROM them. We take a subset of R and prove that it
> uniquely exhibits properties equivalent to PA. The natural
numbers,
> it turns out, are already imbedded in any complete ordered field
> (like the real numbers). In my experience, this is not readily
> apparent in most texts.
>
> I will be including this proof, along with the proofs of the
various
> lemmas therein, and other samples of proofs about the real numbers
> in a future release of DC Proof.
>
> DC Proof format -- click to download:
>
> http://www.dcproof.com/ConstructN.proof
>
>
> HTML formal:
>
> http://www.dcproof.com/ConstructN.html
>
> Dan
>

Effectively Immediately

New release of DC Proof 1.0 dated 2006-02-15 includes:

1. Fixed bug in Subset Rule that could lead to invalid proofs as a
result of invalid selection criteria. Details available upon request.

Download at DC Proof Online at:

http://www.dcproof.com

OR

Download directly by clicking on:

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

Dan Christensen
dc@...

Effective Immediately

New Release of DC Proof 1.0 dated 2006-02-07

Includes:

1. Changed colour of system generated comments on main screen and in
HTML output for enhanced readability.

2. Streamlined insert mode to minimize scrolling and other
inconveniences. This should help in writing longer proofs. Affects
Hide/Show Details (F5, F6), and line deletions while in insert mode.

3. Changes to user documenation: Inserted missing page from Example
8 of Tutorial (line 5). (Oooops!) Added paragraph "Problems with
Dependency among Variables" to The Specification Rules page, and
addition links to this page.

Download at DC Proof Online at:
http://www.dcproof.com

OR

Download directly by clicking on:
http://www.dcproof.com/dcpsetup.exe

Dan Christensen

Dear members,

Here is another, considerably simpler approach to working with real
numbers in DC Proof. Rather than constructing the reals starting
with Peano's Axioms for the natural numbers (a HUGE undertaking!),
here we do the opposite -- we start with the axioms for real numbers
R, as presented in most introductory texts, and construct the
natural numbers FROM them. We take a subset of R and prove that it
uniquely exhibits properties equivalent to PA. The natural numbers,
it turns out, are already imbedded in any complete ordered field
(like the real numbers). In my experience, this is not readily
apparent in most texts.

I will be including this proof, along with the proofs of the various
lemmas therein, and other samples of proofs about the real numbers
in a future release of DC Proof.

DC Proof format -- click to download:

http://www.dcproof.com/ConstructN.proof


HTML formal:

http://www.dcproof.com/ConstructN.html

Dan

Effective Immediately

New Release of DC Proof 1.0

Includes:

1. Fixed bug in Universal Specification form that caused the form to
close in response to some syntax errors.

Download at DC Proof Online at:
http://www.dcproof.com

OR

Download directly by clicking on:
http://www.dcproof.com/dcpsetup

Dan Christensen
Toronto, Canada

Effective immediately

New release of DC Proof 1.0 dated 2005-12-10

Includes:

1. Fixed definition of pairwise intersection generated by Set
Operations option.

Download at DC Proof Online at:

http://www.dcproof.com


OR

Download directly by clicking on:

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


Dan Christensen

Effective immediately...

New release of DC Proof 1.0 dated 2005-8-8 includes:

1. Improved graphics (screen shots) in tutorial and user guide.

2. Larger fonts used on various forms/screens for improved
readability.

No change to functionality.

Download new version at DC Proof Online:

http://www.dcproof.com

OR download directly by clicking on:

http://www.dcproof.com/dcpsetup

Dan Christensen
Toronto, Canada

Dear members,

I received the following proof from Mark Hurd. Using the new SUM
shortcut, he proved that

x + x^2 + x^3 + ... + x^k = x*((x^k-1)/(x-1)) for x>1

Well done, Mark!

Download by clicking on:

http://www.dcproof.com/SumPowers.proof (130K)

Dan

PS: I will soon be releasing a new version of DC Proof with improved
graphics in the user documentation.


Mark wrote:

> Dan
>
> Here's a proof that Sum(i,1,k):x^i=x*(x^k-1)/(x-1)
>
> It was developed during beta testing of the release below.
>
> Some of the premises (and lemmas) are not used, I got sidetracked
> in a
> couple of places, and I'd approach it slightly differently if I
> started
> again.
>
> Regards,
> Mark Hurd, B.Sc.(Ma.) (Hons.)

Effective immeidately...

New version of DC Proof 1.0 dated 2005-08-5 includes

1. New shortcuts for SUM and PROD operators (on Numbers menu)

2. Minor bug fixes, cosmetic changes (details on request)


Download at DC Proof Online at:

http://www.dcproof.com

OR download directly by clicking on:

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


Dan Christensen
Toronto, Canada

Dear Members,

Following is a proof using the SUM operator for an arbritary number
of
constants:

http://www.dcproof.com/SUMconstants.proof  (DC Proof format)
http://www.dcproof.com/SUMconstants.html   (HTML format)

(Thanks for your help, Mark!)

Dan

Dear Members,

Here are two simple but essential results for working with SUM and
PROD operators to download.

Closure of the SUM operator:

http://www.dcproof.com/SUMclosure.proof (DC Proof format)
http://www.dcproof.com/SUMclosure.html  (HTML format)


Closure of the PROD operator:

http://www.dcproof.com/PRODclosure.proof (DC Proof format)
http://www.dcproof.com/PRODclosure.html  (HTML format)

To make use of these results in your own proofs, simply copy the
text of the last line in each, and paste it into the Premise text
box of your proof.

Dan

Effective Immediately

New release of DC Proof 1.0 dated 2005-06-20 includes:

1. Change to Delete All References (F3) that will, in some cases,
reduce the number of lines deleted. Could save re-entering some
lines.

2. Change to Delete All References (F3) that will preserve Insert
Mode in most cases. Now, Insert Mode will be switched off only when
the line before the insertion point is deleted.

3. Scroll position in the main text box will be preserved when
selecting menu options except when text is highlighted. In this
case, the main text box may be scrolled to the beginning of the
selected text and the highlighting will be removed.

Thanks to Mark Hurd for suggesting these changes.

Download from DC Proof Online at:

http://www.dcproof.com

OR

Download directly by clicking on:

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

Dan Christensen
Toronto, Canada

> >>>>...HOT KEYS...<<<<
>
> >>See the tool bar. The 'Det' button invokes Detachment, the 'U
Gen'
> button invokes Universal Generalization, etc.<<
>
> Understood, but the tool bar still involves a click, as opposed to
a
> keyboard combo.  No big deal, would just be a little more
convenient (for
> me, but can't
> speak for everyone else).
>

I forgot to mention that DC Proof makes extensive use of CTRL, ALT
and F key sequences, though not for all commands.  The CTRL and F
key sequences are shown in the menu options, e.g. Edit / Insert Mode
is F2. The ALT sequences are activated when you press the ALT key,
e.g. Logic / Detachment is ALT, L, D (in order). Hot keys are
indicated by undelining (only after pressing ALT). To reduce key-
strokes and to help you learn the notation, the Premise form (and
others) also make us of CTRL keys  for standard notation, e.g.
CTRL+A gives you the universal quantifier, "ALL( ):" The will also
be evident from the menu options.


>
>
> >>>>...POSSIBLE TRANSFORMATION PICKLIST...<<<<
>
> >>The number of possibilities are limitless. I wouldn't know where
to
> begin!<<
>
> Yeah, it sounded like the number of possibilities might be
unmanageable.
>
> >>...colour and font of the variables....<<
>
> That definitely helps, thanks for including that feature.
>
>
> >>>>USING CONCLUSIONS OF OTHER PROOFS AS GIVENS IN THE CURRENT
PROOF<<<<
>
> >>....copy the text of a conclusion or generalization from one
proof
> into the premise of another....several occurrences of DC Proof
open at
> once....<<
>
> Yep, but not quite the same as a global copying and pasting in one
shot.
>

When I say copy the text, I mean the usual copy and paste functions
of most text editors. Just highlight the text of a statement
(usually a generalization) in one proof, and copy it using the
Edit / Copy (or CTRL+C) function. Then open the Premise form in
another proof, and paste using Edit / Paste (or CTRL+V) function.

You can also creat a library of definitions, axioms, etc. in the
*.proof format. Open the file and save it to a new one, and starting
writing your new proof.


>
>
> >>>>....STRING SUBSTITUTION....<<<<
>
> >>....You can use any number of characters to make meaningful
names for
> predicates, propositions and variables....<<
>
> Yes, and that's helpful in a proof which is intended to be
readable and
> meaningful at first glance.  I was thinking about the possibility
of
> making a
> shorter proof - in the sense of the number of characters typed,
not in the
> sense of the number of lines - making it a bit more elegant but
only
> injecting
> the meaning at the beginning (in the definitions), and the end (in
the
> conclusion).
>

Perhaps it's my programming background, but I think you will find it
better to stick with meaningful (longer) variable names throughout.
If have  designed the system to minimize the number of key-strokes
throughout.  Once you have established a premise, most commands
require your to type only a single variable name, if that. And for
those, you can also use the copy and paste functions to reduce key-
strokes even further.

You can also create a legend for each variable name using the
Comment or Introduction functions.

.
>
> >>>>COMMAND LINE<<<<
> >>Sorry, I don't see any advantage in this. It would be like
playing
> chess in your head! Wouldn't you really rather use a nice
graphical
> interface?<<
>
> Doesn't have to be either-or.  For example, I use both Take
Command - a
> graphical command line - and Total Commander - an Explorer
replacement.
> They
> are both indispensable for me, at this point.
>
> Neither a graphical interface, nor a command-line interface are
ends in
> themselves, bur rather means to an end.  The end, for me in the
case of DC
> Proof, is the exploration and discovery of logical principles.
>
> I do indeed like DC Proof just the way it is, and am grateful that
you
> designed something I couldn't locate anywhere for several years.
But as a
> programmmer, it would be cool to be able to experiment with
generating
> statements and conclusions externally, while at the same time
making use
> of DC
> Proof's capabilities.  It might be possible to gain some insights -
  and do
> some things - that wouldn't be possible otherwise, but it's
impossible to
> predict this.  Of course, it would also open up a can of worms for
you,
> and maybe start to evolve your product in a direction you hadn't
planned
> on.
>

To say the least. :^)


> Actually, playing chess or working out long proofs mentally would
be kind
> of cool, a mental exercise which wouldn't require external
equipment.
> Probably
> some day that will be possible, after some breakthroughs in
affordable
> neural implants, but who knows when?
>
>
> >>Don't they have rather small screens, and no colour? For these
> reasons, I think they would be rather awkward to use for an
application
> like DC Proof.
> At times, you really do need to see the "big picture" -- the
bigger the
> better. At times, you may even want to use the smallest font to
view as
> many
> lines at once as possible.<<
>
> Yes, that may well be so, in the case of the graphical
calculators.  They
> do some amazing things nowadays - showing integrals and
derivatives in
> symbolic
> form, e.g.  But yeah, the screen size and monocolor might be
inappropriate
> for the kinds of symbolic representations which DC Proof does well.
>
>
> Anyway, thanks for the response, Dan.  My suggestions were
intended to
> demonstrate some of the initial thoughts which a first-time user
of DC
> Proof
> might have, and which would be forgotten after a few months of
experience.
> I'm very happy with the software, and thanks again for providing
it.
>

Thank you for your interest and your kind words.

Dan

(Reply e-mailed to me from iquine -- my reply to this to follow)


>>>>...HOT KEYS...<<<<

  >>See the tool bar. The 'Det' button invokes Detachment, the 'U
Gen' button invokes Universal Generalization, etc.<<

Understood, but the tool bar still involves a click, as opposed to a
keyboard combo.  No big deal, would just be a little more convenient
for me, but can't speak for everyone else).



  >>>>...POSSIBLE TRANSFORMATION PICKLIST...<<<<

  >>The number of possibilities are limitless. I wouldn't know where
to begin!<<

Yeah, it sounded like the number of possibilities might be
unmanageable.

  >>...colour and font of the variables....<<

That definitely helps, thanks for including that feature.


  >>>>USING CONCLUSIONS OF OTHER PROOFS AS GIVENS IN THE CURRENT
PROOF<<<<

  >>....copy the text of a conclusion or generalization from one
proof into the premise of another....several occurrences of DC Proof
open at once....<<

Yep, but not quite the same as a global copying and pasting in one
shot.



  >>>>....STRING SUBSTITUTION....<<<<

  >>....You can use any number of characters to make meaningful names
for predicates, propositions and variables....<<

Yes, and that's helpful in a proof which is intended to be readable
and meaningful at first glance.  I was thinking about the
possibility of making a shorter proof - in the sense of the number
of characters typed, not in the sense of the number of lines -
making it a bit more elegant but only injecting the meaning at the
beginning (in the definitions), and the end (in the conclusion).


  >>>>COMMAND LINE<<<<
  >>Sorry, I don't see any advantage in this. It would be like
playing chess in your head! Wouldn't you really rather use a nice
graphical interface?<<

Doesn't have to be either-or.  For example, I use both Take Command -
a graphical command line - and Total Commander - an Explorer
replacement. They are both indispensable for me, at this point.

Neither a graphical interface, nor a command-line interface are ends
in themselves, bur rather means to an end.  The end, for me in the
case of DC Proof, is the exploration and discovery of logical
principles.

I do indeed like DC Proof just the way it is, and am grateful that
you designed something I couldn't locate anywhere for several years.
But as a programmmer, it would be cool to be able to experiment with
generating statements and conclusions externally, while at the same
time making use of DC Proof's capabilities.  It might be possible to
gain some insights -and do some things - that wouldn't be possible
otherwise, but it's impossible to predict this.  Of course, it would
also open up a can of worms for you, and maybe start to evolve your
product in a direction you hadn't planned on.

Actually, playing chess or working out long proofs mentally would be
kind of cool, a mental exercise which wouldn't require external
equipment.  Probably some day that will be possible, after some
breakthroughs in affordable neural implants, but who knows when?


  >>Don't they have rather small screens, and no colour? For these
reasons, I think they would be rather awkward to use for an
application like DC Proof. At times, you really do need to see
the "big picture" -- the bigger the better. At times, you may even
want to use the smallest font to view as many lines at once as
possible.<<

Yes, that may well be so, in the case of the graphical calculators.
They do some amazing things nowadays - showing integrals and
derivatives in symbolic form, e.g.  But yeah, the screen size and
monocolor might be inappropriate for the kinds of symbolic
representations which DC Proof does well.


Anyway, thanks for the response, Dan.  My suggestions were intended
to demonstrate some of the initial thoughts which a first-time user
of DC Proof might have, and which would be forgotten after a few
months of experience.  I'm very happy with the software, and thanks
again for providing it.

>>...Here is the proof using Arbitrary Or Not rule the new and improved
Cases rule:...<<

Tried it, works, good, thanks.

Mark, thanks for the workaround alternate proof.


Regards,

Effective Immediately

New release of DC Proof 1.0 dated 2005-06-11 includes:

1. Fix to bug in Case Rule that, in some cases, would not recognize
valid consequents.

Download from DC Proof Online at:

http://www.dcproof.com


OR

Download directly by clicking on:

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


Dan Christensen
Toronto, Canada

--- In dcproof@yahoogroups.com, "Mark Hurd" <mhurd@m...> wrote:
> Hi Dan,
>
> The problem with your proof is that it uses Contra, which is
effectively the
> thing being proved.
>
> I agree that CASES should work. NB a workaround: if you apply
Imply-And to
> both of the B=>A's in 11 then Cases succeeds!
>
> BTW iquine, instead of starting a new Premise A|~A, use Or Not.
Then if
> Cases worked you'd be done.
>

Have just fixed this bug. Uploading now -- slow line.

Here is the proof using Arbitrary Or Not rule the new and improved
Cases rule:

	 1 ~A => ~B
		 Premise

		 2 ~A
			 Premise

		 3 ~B
			 Detach, 1, 2

		 4 ~~B => A
			 Arb Cons, 3

		 5 B => A
			 Rem DNeg, 4

	 6 ~A => [B => A]
		 Conclusion, 2

		 7 A
			 Premise

		 8 B => A
			 Arb Ante, 7

	 9 A => [B => A]
		 Conclusion, 7

	 10 [A => [B => A]] & [~A => [B => A]]
		 Join, 9, 6

	 11 A | ~A
		 Or Not

	 12 B => A
		 Cases, 11, 10

13 ~A => ~B => [B => A]
	 Conclusion, 1

Dan

>>There is a much easier way. See below.<<

Dan, thanks, I didn't realize you had a contrapositive
rule as one of the primitives, it will certainly help
in some circumstances.

Anyway, I wasn't really looking for an easier way - we
could just use a Proof by Contradiction to do that -
but rather some way of completing the proof the way it
was written, using CASES or something similar.  Is
that possible?


Regards,



__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around
http://mail.yahoo.com

Hi Dan,

The problem with your proof is that it uses Contra, which is effectively the
thing being proved.

I agree that CASES should work. NB a workaround: if you apply Imply-And to
both of the B=>A's in 11 then Cases succeeds!

BTW iquine, instead of starting a new Premise A|~A, use Or Not. Then if
Cases worked you'd be done.

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

---- Original Message ----
From: "Dan Christensen" <dchris@...>
To: <dcproof@yahoogroups.com>
Sent: Saturday, June 11, 2005 2:06 PM
Subject: [DC Proof] Re: How to finish this proof?

> There is a much easier way. See below.
>
> Dan
>
>
>         Prove: (~A=>~B)=>(B=>A)
>
> Suppose...
>
> 1 ~A => ~B
> Premise
>
> 2 ~~B => ~~A
> Contra, 1
>
<snip>
>
> --- In dcproof@yahoogroups.com, "iquine" <iquine@y...> wrote:
> > Dan,
> >
> > Thanks for the response to my wishlist, will respond to that over the
> > weekend.
> >
> > Haven't quite gotten the hang of DCProof yet, and am stuck on a proof
> > that could easily be done on paper, but can't see how to do it here.
> >
> > The thereom is an implication, which could easily be proved by
> > contradiction.
> >
> > My attempted approach was to prove that the consequent was true if A
> > was true, and that it also was true if ~A was true, and that therefore
> > it must be true.
> >
> > The problem is that, when I try to apply CASES, DCProof allows me to
> > click on the OR statement in 10 - but it won't allow me to click on
> > the AND statement in 11, probably because the consequent is not a
> > single statement letter, but rather an implication in itself.
> >
> > How would you complete the proof along these same lines?
> >
> >
> > Prove: (~A=>~B)=>(B=>A)
> >
> > 1 ~A => ~B
> > Premise
> >
> > 2 ~A
> > Premise
> >
> > 3 ~B
> > Detach, 1, 2
> >
> > 4 ~~B => A
> > Arb Cons, 3
> >
> > 5 B => A
> > Rem DNeg, 4
> >
> > 6 ~A => [B => A]
> > Conclusion, 2
> >
> > 7 A
> > Premise
> >
> > 8 B => A
> > Arb Ante, 7
> >
> > 9 A => [B => A]
> > Conclusion, 7
> >
> > 10 ~A | A
> > Premise
> >
> > 11 [~A => [B => A]] & [A => [B => A]]
> > Join, 6, 9

There is a much easier way. See below.

Dan


         Prove: (~A=>~B)=>(B=>A)

	 Suppose...

	 1 ~A => ~B
		 Premise

	 2 ~~B => ~~A
		 Contra, 1

	 3 B => ~~A
		 Rem DNeg, 2

	 4 B => A
		 Rem DNeg, 3

As Required:

5 ~A => ~B => [B => A]
	 Conclusion, 1



--- In dcproof@yahoogroups.com, "iquine" <iquine@y...> wrote:
> Dan,
>
> Thanks for the response to my wishlist, will respond to that over
the
> weekend.
>
> Haven't quite gotten the hang of DCProof yet, and am stuck on a
proof
> that could easily be done on paper, but can't see how to do it
here.
>
> The thereom is an implication, which could easily be proved by
> contradiction.
>
> My attempted approach was to prove that the consequent was true if
A
> was true, and that it also was true if ~A was true, and that
therefore
> it must be true.
>
> The problem is that, when I try to apply CASES, DCProof allows me
to
> click on the OR statement in 10 - but it won't allow me to click on
> the AND statement in 11, probably because the consequent is not a
> single statement letter, but rather an implication in itself.
>
> How would you complete the proof along these same lines?
>
>
> Prove: (~A=>~B)=>(B=>A)
>
> 1 ~A => ~B
>  Premise
>
>  2 ~A
> 	 Premise
>
>  3 ~B
> 	 Detach, 1, 2
>
>  4 ~~B => A
> 	 Arb Cons, 3
>
>  5 B => A
> 	 Rem DNeg, 4
>
> 6 ~A => [B => A]
>  Conclusion, 2
>
>  7 A
> 	 Premise
>
>  8 B => A
> 	 Arb Ante, 7
>
> 9 A => [B => A]
>  Conclusion, 7
>
> 10 ~A | A
>  Premise
>
> 11 [~A => [B => A]] & [A => [B => A]]
>  Join, 6, 9

Dan,

Thanks for the response to my wishlist, will respond to that over the
weekend.

Haven't quite gotten the hang of DCProof yet, and am stuck on a proof
that could easily be done on paper, but can't see how to do it here.

The thereom is an implication, which could easily be proved by
contradiction.

My attempted approach was to prove that the consequent was true if A
was true, and that it also was true if ~A was true, and that therefore
it must be true.

The problem is that, when I try to apply CASES, DCProof allows me to
click on the OR statement in 10 - but it won't allow me to click on
the AND statement in 11, probably because the consequent is not a
single statement letter, but rather an implication in itself.

How would you complete the proof along these same lines?


Prove: (~A=>~B)=>(B=>A)

1 ~A => ~B
	 Premise

	 2 ~A
		 Premise

	 3 ~B
		 Detach, 1, 2

	 4 ~~B => A
		 Arb Cons, 3

	 5 B => A
		 Rem DNeg, 4

6 ~A => [B => A]
	 Conclusion, 2

	 7 A
		 Premise

	 8 B => A
		 Arb Ante, 7

9 A => [B => A]
	 Conclusion, 7

10 ~A | A
	 Premise

11 [~A => [B => A]] & [A => [B => A]]
	 Join, 6, 9

Hi,

Thanks for the suggestions. Below, you will find some suggestions to help
you achieve at least some of the functionality you are looking for, using
the current version.

----- Original Message -----
From: "iquine" <iquine@...>
To: <dcproof@yahoogroups.com>
Sent: Wednesday, June 08, 2005 8:59 AM
Subject: [DC Proof] Wish list/suggested enhancement/silly ideas


> Wish list/suggested enhancements/silly ideas, from the point of view
> of someone who has just started using DC Proof
>
> 1) Hot Keys for the most common functions, such as the application of
> Modus Ponens/Detachment
>

See the tool bar. The 'Det' button invokes Detachment, the 'U Gen' button
invokes Universal Generalization, etc.


> 2) Picklist of possible transformations - the user jumps into some
> kind of SUGGEST TRANSFORMATIONS mode, and clicks on any number of
> statements.  The user is then presented with a picklist of relevant
> rules which could be applied to the given set of statements.
>

The number of possibilities are limitless. I wouldn't know where to begin!

The colour and font of the variables, however, do suggest some possibilites.
Or at least eliminate some. The colour of the variables indicate what kind
of generalizations are possible -- green for universal, and red for
existential generalizations. A variable in a bold font rules out an
immediate conclusion.


> 3) Ability to group sets of .Proof files, extract their conclusions
> (with/without associated comments), and join them all into a set of
> axioms, which are then auto-pasted to the top of the current file.
>

You can copy the text of a conclusion or generalization from one proof into
the premise of another. See 'Edit Menu Options.' You can have several
occurrences of DC Proof open at once, a different proof displayed in each
one.


> 4) String substitution in the conclusion - like substituting 'Socrates
> is mortal' for 'M(s)', or 'Politicians lie' for 'L(p)' at the end of
> the proof.
>

You can use any number of characters to make meaningful names for
predicates, propositions and variables. You could, to use your example,
have:

1 ALL(x):[Man(x) => Mortal(x)]
     Premise

2 Man(socrates)
    Premise

3 Man(socrates) => Mortal(socrates)
    U Spec, 1

4 Mortal(socrates)
    Detach, 3, 2


>
> 4a) Alternative to 4) - A separate definition file for any given
> proof, specifying the initial string substitutions mentioned in (4)
> above, and a separate conclusion file, which takes the conclusion at
> the end of the current .PROOF file, performs the string substitutions,
> and outputs the desired strings into the separate conclusion file.
>

See reply to number 3. If you copy in a generalization, you can apply it to
any free variables in another proof.


>
> 5 Command line capability - something like
>
> DCPROOFCMD.EXE <FileName>.PROOF ADDPREMISE "(A=>B)=>C"
> DCPROOFCMD.EXE <FileName>.PROOF ADDPREMISE "(A=>B)"
> DCPROOFCMD.EXE <FileName>.PROOF DETACH "1,2"  (Not sure how you would
> obtain the line numbers 1 and 2, but that's the general idea)
>
> 5a) Some means of returning various result values, e.g. line numbers,
> from each command line referenced in 5.  The idea would be that batch
> files could be used as a script language for DCPROOF.
>

Sorry, I don't see any advantage in this. It would be like playing chess in
your head! Wouldn't you really rather use a nice graphical interface?


>
> 6) A Pocket PC or Texas Instruments (e.g. TI-92 or Voyage 200) version
>

Don't they have rather small screens, and no colour? For these reasons, I
think they would be rather awkward to use for an application like DC Proof.
At times, you really do need to see the "big picture" -- the bigger the
better. At times, you may even want to use the smallest font to view as many
lines at once as possible.

Dan

Wish list/suggested enhancements/silly ideas, from the point of view
of someone who has just started using DC Proof

1) Hot Keys for the most common functions, such as the application of
Modus Ponens/Detachment

2) Picklist of possible transformations - the user jumps into some
kind of SUGGEST TRANSFORMATIONS mode, and clicks on any number of
statements.  The user is then presented with a picklist of relevant
rules which could be applied to the given set of statements.

3) Ability to group sets of .Proof files, extract their conclusions
(with/without associated comments), and join them all into a set of
axioms, which are then auto-pasted to the top of the current file.

4) String substitution in the conclusion - like substituting 'Socrates
is mortal' for 'M(s)', or 'Politicians lie' for 'L(p)' at the end of
the proof.


4a) Alternative to 4) - A separate definition file for any given
proof, specifying the initial string substitutions mentioned in (4)
above, and a separate conclusion file, which takes the conclusion at
the end of the current .PROOF file, performs the string substitutions,
and outputs the desired strings into the separate conclusion file.


5 Command line capability - something like

	 DCPROOFCMD.EXE <FileName>.PROOF ADDPREMISE "(A=>B)=>C"
	 DCPROOFCMD.EXE <FileName>.PROOF ADDPREMISE "(A=>B)"
	 DCPROOFCMD.EXE <FileName>.PROOF DETACH "1,2"  (Not sure how you would
obtain the line numbers 1 and 2, but that's the general idea)

5a) Some means of returning various result values, e.g. line numbers,
from each command line referenced in 5.  The idea would be that batch
files could be used as a script language for DCPROOF.


6) A Pocket PC or Texas Instruments (e.g. TI-92 or Voyage 200) version

Effective Immediately

New release of DC Proof 1.0, dated 2005-05-22

Includes:

1. Fixed bug in Make HTML File option that would occassionally drop
symbols "<" and ">" in HTML output. Affects only HTML output. No
effect on validity of proofs.

Download at DC Proof Online at:

http://www.dcproof.com

OR

Download directly by clicking on:

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


Dan Christensen
Toronto, Canada

Effective Immediately

New release of DC Proof 1.0 (dated 2005-05-17) includes:

1. Fixed minor bug in mouse-click processing. Occassionally, cursor
data would be lost, resulting in the wrong statements, variables or
expressions being inadvertently selected. No effect on validity of
proofs.

2. Added ability to unselect (deselect) highlighted text by pressing
the Escape key.

3. Changes to user documentation (Edit Menu) to reflect these
changes.


Download at DC Proof Online website at:

http://www.dcproof.com

OR

Download directly by clicking on:

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


Dan Christensen
Toronto, Canada

Effective Immediately

New release of DC Proof 1.0, dated 2005-04-24 (See Help/About)

Includes corrections to user documentation. Thanks again to Mark
Hurd for bringing these errors to my attention.

No changes to functionality are included.

Download latest version at DC Proof Online at:

http://www.dcproof.com

OR

Download directly by clicking on:

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

Dan Christensen
Toronto, Canada

PS: This is a reposting of the original release notice yesterday
which does not appear to have been sent out by Yahoo Groups. I
apologize for any duplication that may have resulted.

Effective immediately

New release of DC Proof 1.0 includes:

1. Fixed bug that, in some cases, did not set colours of free
variables correctly, i.e. did not recognize dependencies between
variables, and could have led to invalid generalizations.


Thanks to Mark Hurd for bringing this problem to my attention.


Download at the DC Proof website at:

http://www.dcproof.com

OR

Download directly by clicking on:

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


Dan

PS: I am in the process of moving and renovating. My responses to
your postings my be delayed somewhat.

Following is the rationale for the pairwise union operator || as
defined in DC Proof. (See "Set Theory" in the User Reference Guide.)

http://www.dcproof.com/PairwiseUnion.html  (HTML format)
http://www.dcproof.com/PairwiseUnion.proof (DC Proof format)

As a exercise, readers may want to provide similar rationales for
the pairwise intersection operator && and the set complement
operator ` as defined in DC Proof. I will post the first solution at
my website.

Dan
dc@...