Logiweb(TM)

14.266 All-seqop catches variable which is free in condition

Prev Up Next Page 737 of 800 Search internet


Origin: check. Landing-place: diagnose.

All-seqop catches variable x which is free in the following condition: c

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 condition c' indicates that #x occurs free in c.

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 condition' typically occurs when a proof first assumes that a metavariable satisfies some side condition and then assumes the metavariable to be arbitrary. The All operator can implement the assumption that a metavariable is arbitrary whereas the Endorse operator can implement an assumption that a metavariable satisfies some side condition.

Prev Up Next Page 737 of 800 Search logiweb.eu

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