Logiweb(TM)

8.5.20 Cut

Prev Up Next Page 345 of 800 Search internet


The cut operator A ;; B proves the conclusion of B using the conclusion of A. In other words, the conclusion of A can be used as a premise in B.

The cut operator can be used both at tactic and at unitac level. At the tactic level, it is used after Line L02, L03, L04, and L05 in the proof below:

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

prepare proof indentation,proof of M1.8a : 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

The semicolons after those lines suggest that the cut operator is used there. The semicolon after Line L01 has nothing to do with the cut operator and is only included there to make line Line L01 look like the other lines. Line L01 represents in infer operator like Prop infer *** rather than a cut.

Here is a rather constructed example of use of a cut at unitac level:

lemma CutExample : #x infer ( ( #x oplus #x ) oplus ( #x oplus #x ) ) end lemma

prepare proof indentation,proof of CutExample : line L01 : #x infer ( ConsLemma Init Deref conclude #x oplus #x ;; ConsLemma Init Deref conclude ( ( #x oplus #x ) oplus ( #x oplus #x ) ) ) >> #x infer ( ( #x oplus #x ) oplus ( #x oplus #x ) ) qed

In the proof above, the first application of ConsLemma proves #x oplus #x from #x and the second application of ConsLemma builds on top of that by proving ( #x oplus #x ) oplus ( #x oplus #x ) from #x oplus #x.

Prev Up Next Page 345 of 800 Search logiweb.eu

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