1

Source: p 446, A Concise Introduction to Logic (12 Ed, 2014) by Patrick Hurley

Here is another example of an argument having a tautology as its conclusion. In this case, since the conclusion is a conditional statement, conditional proof is the easier alternative:enter image description here

I see that line 2 is the Assumption for the Conditional Proof, but it already provides you with "T". So why write lines 3 and 4, which appear completely redundant?

I would have written only:

1. S
   | 2. T     ACP     
3. T → T      2-2, CP    
Improve this question

2 Answers 2

Reset to default
0

The proof is a derivation, by CP, of :

S ⊢ T ⊃ T.

If you rewrite it as :

1) S --- premise

2) T --- ACP

3) at this point, there is no rule allowing you to derive a "new" T from 2) in order to conclude with :

4) T ⊃ T --- 2,3 CP.

Improve this answer
2
  • Thank you, but I am still confused. Why is a 'new' T needed? You already assumed, and so possess, T!
    – user8572
    Commented Jan 1, 2016 at 20:28
  • 1
    @LePressentiment - in 1) you have a premise (i.e. an assumption) S; in 2) you ave a new assumption T. At that point, you have only two assumptions and you have proved nothing ...
    – Mauro ALLEGRANZA
    Commented Jan 2, 2016 at 13:05
0

This is only a partial answer since I have the same question as the OP does about lines 3 and 4, however, I am presenting it to show how this could be proven.

The question is why this proof cannot be completed in three steps? That would depend on the rules that one has available which are programmed into the proof checker one is using.

For the proof checker associated with forall x one can do exactly as the OP suggests doing and get a valid proof using conditional introduction (→I) on a sequence of lines starting and ending at line 2 and discharging the assumption made on line 2:

enter image description here

One could also use reiteration (R) which allows one to add a line with what one has from a previous line. This makes the sequence of lines start with 2 and end with 3:

enter image description here

Reiteration is a derived rule based on the basic rules defined in forall x. One could avoid this derived rule and use the more basic rules. (See page 136 for a derivation of the reiteration rule.)

Here is how it would look using conjunction introduction (∧I) and conjunction elimination (∧E):

enter image description here

Note that this used conjunction ("and") introduction rather than disjunction ("or") introduction as in the OP's quoted example. The "Taut" rule for line 4 is not one that I think I have, or I am unaware of it.

From the perspective of the proof checker I am using I would come to the same conclusion and ask "So why write 3 and 4, which appear completely redundant?" The answer may appear somewhere in Hurley's text where the basic rules for that text are defined.

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/ Wikipedia, "Fitch notation" https://en.wikipedia.org/wiki/Fitch_notation

Improve this answer

You must log in to answer this question.