Discussion:
NOT NOT p |- p
(too old to reply)
Roman
2011-10-05 03:11:33 UTC
Permalink
Since we proved the above today, can we just use that end result
anywhere on our assignment for when we substitute a negation of
something into a negation?
Omer Beg
2011-10-05 14:16:27 UTC
Permalink
Since we proved the above today, can we just use that end result anywhere on
our assignment for when we substitute a negation of something into a
negation?
No.
Since you do not have substitution as a rule you cannot do a substitution
within a formula.
But, the proof does imply that

|- (NOT NOT p -> p)

So you can use this tautology like any of the axioms, and when you do,
give the reference to the proof (i.e. lecture notes or the book etc.).

-Omer
Jonathan Buss
2011-10-06 13:55:05 UTC
Permalink
Post by Omer Beg
Post by Roman
Since we proved the above today, can we just use that end result
anywhere on our assignment for when we substitute a negation of
something into a negation?
No.
Since you do not have substitution as a rule you cannot do a
substitution within a formula.
But, the proof does imply that
|- (NOT NOT p -> p)
So you can use this tautology like any of the axioms, and when you do,
give the reference to the proof (i.e. lecture notes or the book etc.).
-Omer
Note, however, that Question 2 of Assignment 2 requires the full formal
proofs. Thus you should give the proof implied by the above -- not just
cite the result. For Question 3, just a citation will do fine.

(Actually, I don't think that "¬¬p ⊢ p" will be useful for either
question -- but feel free to demonstrate otherwise.)

Jonathan Buss
Roman
2011-10-06 16:29:13 UTC
Permalink
Post by Jonathan Buss
Post by Omer Beg
Post by Roman
Since we proved the above today, can we just use that end result
anywhere on our assignment for when we substitute a negation of
something into a negation?
No.
Since you do not have substitution as a rule you cannot do a
substitution within a formula.
But, the proof does imply that
|- (NOT NOT p -> p)
So you can use this tautology like any of the axioms, and when you do,
give the reference to the proof (i.e. lecture notes or the book etc.).
-Omer
Note, however, that Question 2 of Assignment 2 requires the full formal
proofs. Thus you should give the proof implied by the above -- not just
cite the result. For Question 3, just a citation will do fine.
(Actually, I don't think that "¬¬p ⊢ p" will be useful for either
question -- but feel free to demonstrate otherwise.)
Jonathan Buss
I don't understand how this should be done... where am I supposed to
"give the proof implied by the above" if I don't site it?
Roman
2011-10-06 20:44:56 UTC
Permalink
Post by Roman
Post by Jonathan Buss
Post by Omer Beg
Post by Roman
Since we proved the above today, can we just use that end result
anywhere on our assignment for when we substitute a negation of
something into a negation?
No.
Since you do not have substitution as a rule you cannot do a
substitution within a formula.
But, the proof does imply that
|- (NOT NOT p -> p)
So you can use this tautology like any of the axioms, and when you do,
give the reference to the proof (i.e. lecture notes or the book etc.).
-Omer
Note, however, that Question 2 of Assignment 2 requires the full formal
proofs. Thus you should give the proof implied by the above -- not just
cite the result. For Question 3, just a citation will do fine.
(Actually, I don't think that "¬¬p ⊢ p" will be useful for either
question -- but feel free to demonstrate otherwise.)
Jonathan Buss
I don't understand how this should be done... where am I supposed to
"give the proof implied by the above" if I don't site it?
In class you gave a formal proof of |- (NOT p -> NOT q) -> (q -> p)
(contra positive of Ax3).
In the example right after this one, you proved NOT NOT p |- p, in which
you used the previous result as an axiom and wrote down "prev example"
on the right hand side.

Is this what needs to be done?...
Jonathan Buss
2011-10-07 19:24:04 UTC
Permalink
Post by Roman
Post by Roman
Post by Jonathan Buss
Post by Omer Beg
Post by Roman
Since we proved the above today, can we just use that end result
anywhere on our assignment for when we substitute a negation of
something into a negation?
No.
Since you do not have substitution as a rule you cannot do a
substitution within a formula.
But, the proof does imply that
|- (NOT NOT p -> p)
So you can use this tautology like any of the axioms, and when you do,
give the reference to the proof (i.e. lecture notes or the book etc.).
-Omer
Note, however, that Question 2 of Assignment 2 requires the full formal
proofs. Thus you should give the proof implied by the above -- not just
cite the result. For Question 3, just a citation will do fine.
(Actually, I don't think that "¬¬p ⊢ p" will be useful for either
question -- but feel free to demonstrate otherwise.)
Jonathan Buss
I don't understand how this should be done... where am I supposed to
"give the proof implied by the above" if I don't site it?
List the formulae that constitute the (formal) proof.

A citation says, "you can look over there". It's not the actual thing
itself.


(By the way, "site" and "cite" are quite different.)
Post by Roman
In class you gave a formal proof of |- (NOT p -> NOT q) -> (q -> p)
(contra positive of Ax3).
In the example right after this one, you proved NOT NOT p |- p, in which
you used the previous result as an axiom and wrote down "prev example"
on the right hand side.
Is this what needs to be done?...
I believe that I put a "..." just above that line. The full proof fills
in the "..." with the actual lines.
Curtis Bright
2011-10-07 22:59:34 UTC
Permalink
Post by Jonathan Buss
Note, however, that Question 2 of Assignment 2 requires the full formal
proofs. Thus you should give the proof implied by the above -- not just
cite the result.
I was told citing results and using the deduction theorem were fine,
even in question 2's "formal proof". I don't see how this squares with
the question as written, but on the other hand, I compiled full explicit
proofs and it's not something I would recommend (at least for the proofs
I did, your mileage may vary).

Curtis

Continue reading on narkive:
Loading...