14.262 Infer-seqop used on non-meta term

Prev Up Next Page 733 of 800 Search internet

Origin: check. Landing-place: diagnose.

Infer-seqop used on non-meta term: x

The Infer sequent operator applied to a sequent << P ,, C ,, x >> and a metaterm h yields << P setminus {{ h }} ,, C ,, h infer x >>. Thus, the Infer operator allows to move a hypothesis h from the set of premisses to the conclusion. The Infer operator can be used for hypothetical reasoning like 'Assume the axioms of Peano arithmetic, prove some lemma, conclude that the axioms of Peano arithmetic infer the lemma'. In this case the axioms of Peano arithmetic serve as hypothesis h.

The 'Infer-seqop used on non-meta term' indicates that the hypothesis h was illformed. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 733 of 800 Search logiweb.eu

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