处所的顺序

Question

如何更改规则中的前提顺序？例如,在伊莎贝尔的自然演绎规则中:

mp: ?P ? ?Q ? ?P ? ?Q

我们可以将订单更改为:

?P ? ?P ? ?Q ? ?Q

我可以使用rev_mp或定义一个新的引理,但我要找的是是否有一个定理修饰符改变了前提的顺序.

Answer 1

定理的前提可以随属性一起旋转rotated.您还可以指定要旋转的场所数量,例如mp[rotated 1].AFAIK没有任何属性可以随意排列场地.