How are typecodes used/enforced by the Metamath program?

[Humanities Clinic]

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.)

(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?

(3) And, am I right to say that a type code can just be *any* constant? ie declared in $c statement? 

[Humanities Clinic]

Hi is there an answer to this question?

[Mario Carneiro]

On Mon, Jun 5, 2023 at 1:43 AM Humanities Clinic <humaniti...@gmail.com> 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 .)

[David A. Wheeler]

>
>
>
> On Mon, Jun 5, 2023 at 1:43 AM Humanities Clinic <humaniti...@gmail.com> 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.)

> On Jun 6, 2023, at 1:32 AM, Mario Carneiro <di....@gmail.com> wrote:
> 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".

As always, Mario gave a fantastic answer. Here are a few additional notes that may help you understand it.

A Metamath proof *always* includes the steps necessary to create the expressions (statements & parts of statements) used in the proof. The verification process checks those steps to ensure that the types are correct in all cases. These steps are sometimes called "inessential". The HTML published proofs normally don't show the inessential steps for theorems, but these steps *do* show for axioms (since for an axiom there are no other steps to show). You can easily use the metamath-exe program to show every step, even the inessential ones, at your option. The development version of metamath-lamp can also show the inessential steps or not (at your option).

You might look at axiom ax-ext in set.mm:
https://us.metamath.org/mpeuni/ax-ext.html
Steps 1 & 2 let us introduce set variables z and x, which are type setvar.
Step 3 uses the justification "wel" to create "z e. x" *and* allows the verifier
to determine it's a wff.

--- David A. Wheeler