## 6.7.5 Line L01 of the proof

 Page 91 of 800 Search internet

Recall the proof of :

Line L01 says that follows from rule . Rule says

Line L01 comprises a label , an argumentation , and a conclusion bound together by a unification tactic .

The label is a variable. You can use arbitrary variables as labels, so feel free to name your lines or or whatever you like. The check page defines to as 100 individual variables.

Inside the proof, can be used as shorthand for the conclusion .

The unification tactic takes the argumentation and the conclusion and tries to prove the conclusion using the argumentation. The unification tactic returns an argumentation formulated as a Logiweb sequent term. At that time the conclusion has disappeared. The conclusion is merely used by the unification tactic to see what to do with the argumentation. Later on, when the proof checker evaluates the sequent term returned by the unification tactic, the proof checker will see that the sequent term indeed proves .

During proof checking, the following happens:

• Lgc(1) invokes the claim from the check page on the multzero page.
• The claim of the check page invokes and where the latter is the Logiweb proof checker.
• Among other, tactic expands each proof into Logiweb sequent terms and then evaluates the sequent terms to see what they prove.
• The tactic expander of invokes the tactics of each construct of the proof. Among other, when it sees the construct in Line it invokes the unification tactic.
• The unification tactic has its own system of 'unitac' tactics. The unitacs not only consider the argumentation they are supposed to expand but also consider a 'goal', i.e. they know what they should try to prove. In Line , the unification tactic unitac expands the argumentation with the goal of proving .

The unitac of knows that it is a unitac for a rule. So it first generates the Logiweb sequent operators needed for extracting the rule from the theory at hand. So now we have a proof of .

The unitac then compares with the expected conclusion and sees that it must eliminate a quantifier. Thus, it generates a suitable instance of rule :

plus a suitable instance of modus ponens:

The unification tactic uses unification to see that has to be instantiated to . Thus, the metavariable in rule is set to .

Rule says that for all object terms , , , and , the side condition endorses the conclusion . The side condition is true if is identical except for naming of bound variables to the result of replacing by in with suitable renaming of bound variables to avoid collisions. The is a meta-quantifier which quantifies over all object terms. The is an object quantifier which belongs to first order predicate calculus and Peano arithmetic.

Rule says that if one has proved and then one is allowed to conclude by modus ponens.

 Page 91 of 800 Search logiweb.eu