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

Question

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 $

Answer 1

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