|Page 343 of 800||Search internet|
The Curry operator modifies a conclusion of form to and the uncurry operator does the opposite. As examples of use, consider the following three lemmas and proofs:
defines the statement aspect of to be . That defines as a lemma directly in the Logiweb sequent calculus.
A lemma like
defines the statement aspect of as and also defines the unitac aspect of suitably. The latter allows to use directly in argumentations. In contrast,
does not define a unitac aspect for . Thus, one cannot use directly in argumentations but must include it using suitable operations as described in the next section.
|Page 343 of 800||Search logiweb.eu|