Menu
How to change the order of premises in a rule? For instance, in Isabelle's natural deduction rule:
mp: ?P ⟶ ?Q ⟹ ?P ⟹ ?Q
Can we change the order to:
?P ⟹ ?P ⟶ ?Q ⟹ ?Q
I can use rev_mp or define a new lemma, but what I am looking for is whether there is a theorem modifier that changes the order of premises.
850
In classical logic, and indeed in most logics, the order of the premises does not matter. This is encoded in the fact that classical logic, as do most logics, contain commutativity as a structural rule (which basically says order doesn't matter).
In logical argument, a premise is a statement or assumption on which an argument is based. For example, if a person looks at a green apple and says, "this apple is sour," the premises of this argument could be: 1) Green apples are sour.
A premise is a statement in an argument that provides reason or support for the conclusion. There can be one or many premises in a single argument. A conclusion is a statement in an argument that indicates of what the arguer is trying to convince the reader/listener.
one or more propositions, called premises, to a new proposition, usually called the conclusion. A rule of inference is said to be truth-preserving if the conclusion derived from the application of the rule is true whenever the premises are true.
The premises of a theorem can be rotated with the attribute rotated. You can also specify the number of premises to rotate, e.g., mp[rotated 1]. AFAIK there's no attribute for arbitrarily permuting the premises.
65
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
