I will try a Negation Intro type proof.
You do not seek to introduce a negation, but rather a biconditional. Biconditional statements are proven by proving the conditionals hold in each direction.
Further, there will clearly be nesting of another such subproof.
|_
| |_ -A = -A Assumption
| | |_ -(-A => A) Assumption
| | | |_ A Assumption
| | | | : :
| | | | : :
| | | | -A - Introduction
| | | A => -A => Introduction
| | -(-A => A) => (A => -A) => Introduction
| | |_ A => -A Assumption
| | | |_ -A => A Assumption
| | | | : :
| | | | : :
| | | | -A - Introduction
| | | | A => Elimination
| | | -(-A => A) - Introduction
| | (A => -A) => -(-A => A) => Introduction
| | -(-A => A) = (A => -A) = Introduction
| (-A = -A) => [-(-A => A) = (A => -A)] => Introduction
| |_ -(-A => A) = (A => -A) Assumption
| | : :
| | : :
| | -A = -A = Introduction
| [-(-A => A) = (A => -A)] => (-A = -A) => Introduction
| (-A = -A) = (-(-A => A) = (A => -A)) = Introduction
That law isn’t mentioned in my text.ls there an equivalent to it – @Eudoxus
https://archive.org/details/logicbook00berg/page/n1/mode/2up
Yes. The principle of explosion is that anything may be derived from a contradiction. Often a falsum symbol is used to explicitly indicate a contradiction, but the principle works whenever two contradictory statements are derived. Basically:
| Q Somehow derived
| -Q Somehow derived too
| P Explosion
The system in your text does not include a falsity constant, and as such implements negation elimination and introduction rules thus:
| |_ P Assumption
| | Q Somehow derived
| | -Q Somehow derived too
| -P -Introduction
| |_ -P Assumption
| | Q Somehow derived
| | -Q Somehow derived too
| P -Elimination
The principle of explosion is therefore simply an application of these. When contrary statements can be derived, that derivation can be lifted into a raised context (either by reiteration, or doing so in situ):
| Q Somehow derived
| -Q Somehow derived too
| |_ -P Assumption
| | Q Reiterate
| | -Q Reiterate
| P - Elimination
