>
>
>
> 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.)
> On Jun 6, 2023, at 1:32 AM, Mario Carneiro <[email protected]> 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
--
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/9BA1807A-203C-4685-A7A8-D4A6BD83D6EE%40dwheeler.com.
