On Mon, Jun 5, 2023 at 1:43 AM Humanities Clinic <[email protected]> wrote:
> Hihi, I have read most of Dr Megill/Wheeler's Metamath book, as well as > most of the MPE pages, and I understand that typecodes are used to specify > the type of a variable in $f statements. > > (1) How and when does Metamath ensure the types are "enforced"? When does > it throw an error? (Oh, please do let me know which part of Dr > Megill/Wheeler's book has the answer if I have missed it.) > Most theorem applications involve subproofs showing that the substitutions are well typed. For example if you apply ax-mp, this has two main premises |- ph and |- ( ph -> ps ), but also two syntax subproofs "wff ph" and "wff ps". So you have to prove that your substitution is in fact a well formed formula before you can apply it, and the $f hypotheses can be used as the base case here - if your formula is a variable like "ch" then you can apply wch $f wff ch $. to prove "wff ch". > (2) Also, I know $e, $a, $p statements all have typecodes as well. Are > their type codes enforced/used in the same way as $f statements? > Yes. Whenever you apply a hypothesis or theorem the typecode has to match just like any other part of the statement. (3) And, am I right to say that a type code can just be *any* constant? ie > declared in $c statement? > Yes, there is no explicit declaration for typecodes, any constant symbol can act like a typecode. (I regard this as somewhat unfortunate, and the dialect of MM used by set.mm includes typecode declarations in the form of "syntax" commands inside $j comments, like syntax 'wff'; syntax '|-' for 'wff'; which say respectively that 'wff' is a syntax typecode and '|-' is a logical typecode whose main argument is of type 'wff'. More information can be found at https://github.com/metamath/set.mm/blob/develop/j-commands.html .) -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuXAiBQc6wvT7eR2Pmcfn-%2BkUY5gKbhFv1t56yG6xXaeg%40mail.gmail.com.
