1

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 $

3
  • 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].
    – causative
    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.
    – Eudoxus
    Apr 4 at 14:21
3

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
5

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.