8.5.1 Argumentation proof lines

Prev Up Next Page 326 of 800 Search internet

Recall that the most common lines in proofs are ones which argue in favor of a conclusion. The constructs

   line L : A >> C ; N
   line L : A >> C ;
   line L : A >> C qed

use the argumentation A to prove the conclusion C. As an example, the constructs are used for expressing Line L02-L06 of the proof of Lemma 1.8 in Mendelson: 'Introduction to mathematical logic':

Prop lemma M1.8b : #x imply #x end lemma

prepare proof indentation,proof of M1.8b : line L01 : Premise >> Prop ; line L02 : A2 >> ( #x imply ( #y imply #x ) imply #x ) imply newline ( #x imply #y imply #x ) imply #x imply #x ; line L03 : A1 >> #x imply ( #y imply #x ) imply #x ; line L04 : MP ponens L02 ponens L03 >> ( #x imply #y imply #x ) imply #x imply #x ; line L05 : A1 >> #x imply #y imply #x ; line L06 : MP ponens L04 ponens L05 >> #x imply #x qed

We use the word argumentation in place of argument to avoid confusion with arguments of a function.

Lemma M1.8a, M1.8b, M1.8c, and so on all refer to Lemma 1.8 in Mendelson. That is a technicality. The proofs in the present notes are all checked by Logiweb. I have given M1.8a, M1.8b, and so on different names to make sure they are all checked.

Prev Up Next Page 326 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05