|Page 350 of 800||Search internet|
Recall the proofs of :
In Line L01 we use to prove . After tactic expansion, Line L01 proves . Axioms says:
Thus, the tactic expanded argumentation in Line L01 must add and must eliminate the object quantifier in Axiom .
The FOL tactic installs non-standard lemma, rule, and conclude unitacs. The FOL rule unitac has standard behavior on meta-terms but a non-standard behavior on object terms. The contents of is an object term and thus the FOL rule unitac applies its own, non-standard behavior and changes the argumentation into something like where is the following lemma:
In that way, the FOL rule unitac changes to .
Then the FOL conclude unitac takes over and sees that it has to instantiate object quantifiers. It does so using parallel instantiation. Parallelism is unimportant in this case where only one quantifier is instantiated. The Fol conclude unitac changes to something like where is the following lemma:
Thus, the proof until Line L01 tactic expands into something like the following:
Actually, the proof does not tactic expand to the proof above. Rather, it expands into a sequent proof which resembles what the proof above expands into.
|Page 350 of 800||Search logiweb.eu|