Logiweb(TM)

14.265 All-seqop catches variable which is free in premise

Prev Up Next Page 736 of 800 Search internet


Origin: check. Landing-place: diagnose.

All-seqop catches variable x which is free in the following premise: p

The All sequent operator applied to a sequent << P ,, C ,, A >> and a metavariable #x yields << P ,, C ,, All #x : A >> provided #x does not occur free in any premise or side condition. The 'All-seqop catches variable which is free in premise p' indicates that #x occurs free in p.

Users typically read proofs start to end whereas the sequent evaluator typically evaluates proofs end to start. The 'All-seqop catches variable which is free in premise' typically occurs when a proof first assumes that a metavariable satisfies some statement and then assumes the metavariable to be arbitrary. The All operator can implement the assumption that a metavariable is arbitrary whereas the Infer operator can implement an assumption that a metavariable satisfies some statement.

Prev Up Next Page 736 of 800 Search logiweb.eu

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