# Prove (-A=-A) = [-(-A => A) = (A=>-A)]

This is not homework I do this for fun. I tried using prover. The result is quite confusing.

I use the Logic Book This is the last problem I want to do in this section.

I have to it mostly in SD+ .

|- (-A=-A) = [-(-A => A) = (A=>-A)]

Here is my attempt

I will try a Negation Intro type proof.

0.|-(-A=-A) Assume

1.||(-A=-A) Assume ?

2.||(-A=>-A) &( -A=>-A) 1 equiv.?

3.||(-A=>-A) 2 &E ?

4.|| A=>A. 3 Trans ?

5.|(-A=-A) = [-(-A => A) = (A=>-A)] 1,5 -E ?

Any help or hints on how to do it would be appreciated.

BTW l can’t make mathjax work here. Ex v :$\lor$

• First thing, change implication on the right hand side to disjunction: [-(A v A) = (-A v -A)] Next, A v A is equivalent to A, and -A v -A is equivalent to -A. So now you have [-A = -A]. Apr 3 at 3:33
• Mathjax doesn't work here; only on math SE.
– Fizz
Apr 3 at 9:41
• I guess arguments using them are jpgs or something. Apr 4 at 14:21

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

• – Fizz
Apr 3 at 12:19
• That law isn’t mentioned in my text.ls there an equivalent to it @Fizz Apr 3 at 12:19
• @Eudoxus: if you post the rule system from your book (in a separate question), we could probably show you how it's derived.
– Fizz
Apr 3 at 12:23
• Apr 3 at 12:25
• Okay, I've updated the answer to reflect this system . @Eudoxus Apr 3 at 12:54