1. By Modus Ponens only

Give a formal proof of the sentence p from the single premise ¬¬p using only Modus Ponens and the standard axiom schemata. Warning: This is surprisingly difficult. Though it takes no more than about ten steps, the proof is non-obvious.

2. The post above is solved.

3. I am interested in how you solved it. When a derivation involves the third axiom (not B -> not A) -> (A -> B), which is responsible for double-negation elimination and classical logic, I know of only one systematic way of doing this. One can construct a derivation using the Deduction Theorem, which is usually much simpler. Since the proof of the theorem is constructive, one can then emulate it in this concrete instance to get a complete derivation.

4. I got the question from internet—I don't remember where, but it's quite interesting. I was taken by the warning, but it turned out to be a bluff.

As I understood it, only in the execution of a new line, Modus Ponens is required. The negation of an atomic formula is not an issue, particularly when used in the assumptions, so I did it as follows:
Given Argument: ~~P |- P

Proof:
1. P.................................Hypotheses
2. ~ ~ P...........................Premise
3. P.................................Hypotheses
4....... ~ P........................Assumption
5...... ~~P -->~~P............Hypotheses
6..............~~P.................Assumption
7. ......~~P.......................2,5, Modus ponens

Explanations:
Line 6 satisfies the hypotheses on line 5—cross out line 6. Line 5 becomes a premise.
Line 4 and 7 satisfy the hypotheses on line 3—cross out lines 4,5, and 7. Line 3 becomes a premise.
Line 3 satisfies the hypotheses on line 1. Lines 1 and 2 make up a valid argument.

If you don't like the contradiction for an inference, you can try this:

1. P.................................Hypotheses
2. ~ ~ P...........................Premise
3. P-->~~P.......................Hypotheses
4. P..................................Assumption
5...... ~~P -->~~P............Hypotheses
6..............~~P.................Assumption
7. ......~~P.......................2,4, Modus ponens

Line 6 satisfies line 5.
7 satisfies 3
4 satisfies 1

5. I am now more confused than before. What deductive system are you using: natural deduction, Hilbert system, or something else? In my usage, hypothesis, assumption and premise are all synonyms.

6. Originally Posted by emakarov
What deductive system are you using: natural deduction, Hilbert system, or something else? In my usage, hypothesis, assumption and premise are all synonyms.
Sorry, brother. I don't have the slightest idea.

Will this help now?

1.Show P
..|------------------------------|
2|. ~ ~ P...........................|
3|. Show P........................|
..|.|-------------------------|....|
4|.|~ P.........................|....|
5|.|Show ~~P -->~~P.|....|
..|.|...|--------|...............|....|
6|.|.. |.~~P..|...............|....|
..|.|...|--------|...............|....|
7|.|.~~P......................|....|
..|.|------------------------|....|
..|------------------------------|

7. This looks like Fitch variant of Natural Deduction, but I still can't recognize it. For one, one does not write what one needs to prove (like "Show P") in natural deduction derivations; all formulas are either assumptions or have already been proven.

Bit that's OK if the solution works for you.

8. Originally Posted by emakarov
For one, one does not write what one needs to prove (like "Show P") in natural deduction derivations; all formulas are either assumptions or have already been proven.

Bit that's OK if the solution works for you.
I have learned the method you mentioned, but with only one given it will not take you any where.

This method I have just begun learning is more powerful.

A free book for you:

Philosophy 110 on-line text