8
$\begingroup$

How close can you get to introducing and discharging hypotheses in metamath?

I'm trying to define a symbol formal system for the $\land$-only fragment of classical propositional logic.

It has the following rules.

$$ \frac{A \;\;\text{and}\;\; B}{A \land B} \;\;\text{and}\;\; \frac{A\land B}{A} \;\; \text{and} \;\; \frac{A \land B}{B} \;\; \text{are the inference rules} $$

I'm interested in proving a simple statement $P \land Q \vdash Q \land P$.

Here's my attempt to prove it so far in metamath. It is semi-syntactically correct, failing at the verify proof step in the command line interface.

I'm working using demo0.mm as an example.

Here's what I have so far.

$( define 1 (top) 0 (bottom) and * (conjunction)
   Also define |- entailment $)

$c 1 0 * wff |- ( ) $.

$( define metavariables P,Q,R $)

$v P Q R $.

wff-P $f wff P $.
wff-Q $f wff Q $.
wff-R $f wff R $.

wff-conj-P-Q $a wff ( * P Q ) $.

$( inference rule 1: conjunction intro:

   A and B
   -------
    * A B
$)

${
   conj-intro-min  $e |- P $.
   conj-intro-maj  $e |- Q $.
   conj-intro      $a |- ( * P Q ) $.
$}

$( inference rules 2 and 3 : conjunction elim $)

${
   pi1-prem   $e |- ( * P Q ) $.
   pi1        $a |- P $.
$}
${
   pi2-prem   $e |- ( * P Q ) $.
   pi2        $a |- Q $.
$}

$( prove that ( ( * P Q ) ) |- ( * Q P ) $)
commutative-conj $p ( ( * P Q ) ) |- ( * Q P ) $=
wff-P
wff-Q
wff-conj-P-Q
$.

The proof of commutative-conj is very, very incomplete and does not work.

I know that metamath is vaguely Hilbert-style and ... I'm pretty sure I can't just introduce a hypothesis.

So, I tried to do the next best thing and write a rule that contains a free variable in its conclusion that wouldn't unify with anything.

$( An extremely weak form of monotonicity of entailment

If  |- A  holds, then  B |- A  holds.

$)
${
   weak-mono-entailment-prem $e       |- P $.
   weak-mono-entailment      $a ( Q ) |- P $.
$}

However, this approach seems to require me to assert more and more ad hoc facts about $\vdash$ in order to make any progress at all ...

Is there a better, more idiomatic way to mimic introduction and discharge of hypotheses?

$\endgroup$
1
  • $\begingroup$ If it helps, I completely rewrote my answer to get more to your core issue. $\endgroup$
    – Jason Rute
    Feb 13, 2022 at 12:30

2 Answers 2

7
$\begingroup$

I rewrote my answer, but still I don't really know Metamath per se. I'm just going off of your logic. If you tell me I'm completely misunderstanding, I'll delete my answer.

So far it looks like you have implemented the following three rules:

|- P    |- Q        |- ( * P Q )        |- ( * P Q )
------------        ------------        ------------
 |- ( * P Q )          |- P                |- Q

and you are trying to prove

----------------------
( * Q P ) |- ( * P Q )

This is not possible since all of your rules have nothing on the left side of |-.

Using your axioms, you can however prove this:

|- ( * P Q )
------------
|- ( * Q P )

Based on a bit of Googling, I think you would write this theorem as:

${
  commutative-conj.1  $e |- ( * P Q )$.
  commutative-conj  $p |- ( * Q P )$= ...
}$

However, if you really want exactly ( * P Q ) |- ( * Q P ) you can use a different axiom system which let's you put hypotheses on the left. Here is a common one, which you can find in my course notes. You currently only need the rules:

          R |- P    R |- Q       R |- ( * P Q )       R |- ( * P Q )
------    ----------------       --------------       ------------
P |- P     R |- ( * P Q )        R |- P               R |- Q

Then you start with the assumption rule (* P Q) |- (* P Q). From that you apply your two elimination rules to get (* P Q) |- P and (* P Q) |- Q. Then you put those together with your intro rule to get (* P Q) |- (* Q P). However, that is just having exactly one hypothesis on the left which isn't what you want in the long run. I don't know how to deal in MM with an arbitrary list of them. Another expert can answer that.

$\endgroup$
3
  • $\begingroup$ That's great! Reuse the mechanism used for expressing an inference rule to express a conditional theorem (/ derivable inference rule I guess). I'm starting to think that, in metamath, |- may really be a dummy symbol whose sole job is to force the expression to begin with a terminal symbol. $\endgroup$ Feb 13, 2022 at 23:47
  • $\begingroup$ An examination of set.mm (warning, 41M file) reveals that this is indeed the case. Thanks again. $\endgroup$ Feb 14, 2022 at 0:01
  • 1
    $\begingroup$ @GregoryNisbet The turnstile |- can indeed be seen some kind of marker. In this minimal database, there are two such type codes: wff , which means "is a well-formed formula", not giving any assessment about its provability, and |- , which means "is provable". $\endgroup$ Feb 14, 2022 at 2:29
8
$\begingroup$

Concerning your actual proof attempt:

Here is the completed proof:

${
   commutative-conj-prem $e |- ( * P Q ) $.
   $( prove that ( ( * P Q ) ) |- ( * Q P ) $)
   commutative-conj $p |- ( * Q P ) $=
     wff-Q wff-P wff-P wff-Q commutative-conj-prem pi2 wff-P wff-Q
     commutative-conj-prem pi1 conj-intro $.
$}

Jason has already explained the changes needed to the theorem statement itself.

Here is how the Metamath program displays the proof:

MM-PA> SHOW PROOF commutative-conj
 5     pi2-prem=commutative-conj-prem $e |- ( * P Q )
 6   conj-intro-min=pi2             $a |- Q
 9     pi1-prem=commutative-conj-prem $e |- ( * P Q )
10   conj-intro-maj=pi1             $a |- P
11 commutative-conj=conj-intro    $a |- ( * Q P )
  • Step 5, it invokes commutative-conj-prem,
  • Step 6, it invokes pi2, with step 5 as a premise,
  • Step 9, it invokes again commutative-conj-prem,
  • Step 10, it invokes pi1, with step 9 as a premise,
  • Step 11, if finally invokes conj-intro, with steps 6 and 10 as premises.

You'll notice some steps are not shown. These are used to build the expressions which are used as substitutions. In your case, those are invocations of wff-p and wff-q. They can be shown using the SHOW PROOF commutative-conj / ALL command.

Here is the way the proof can be built with metamath-exe:

MM> PROVE commutative-conj
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT commutative-conj"):
21 commutative-conj-prem $e |- ( * P Q ) $.
22 commutative-conj $p |- ( * Q P ) $= ... $.
Unknown step summary (from "SHOW NEW_PROOF / UNKNOWN"):
1    commutative-conj=? $? |- ( * Q P )
MM-PA> ASSIGN 1 conj-intro
3 -1   conj-intro-min=?            $? |- Q
4      conj-intro-maj=?            $? |- P
MM-PA> ASSIGN 3 pi2
5 -1     pi2-prem=?                  $? |- ( * $4 Q )
7      conj-intro-maj=?            $? |- P
MM-PA> ASSIGN 5 commutative-conj-prem
7      conj-intro-maj=?               $? |- P
MM-PA> ASSIGN 7 pi1
 9        pi1-prem=?                     $? |- ( * P $6 )
MM-PA> ASSIGN 9 commutative-conj-prem
MM-PA> IMPROVE ALL
A proof of length 1 was found for step 8.
A proof of length 1 was found for step 7.
A proof of length 1 was found for step 4.
A proof of length 1 was found for step 3.
A proof of length 1 was found for step 2.
A proof of length 1 was found for step 1.
Steps 1 and above have been renumbered.
CONGRATULATIONS!  The proof is complete.  Use SAVE NEW_PROOF to save it.
Note:  The Proof Assistant does not detect $d violations.  After saving
the proof, you should verify it with VERIFY PROOF.

(this is the full output, the necessary commands are those after the interactive prompt MM-PA>)

More generally:

If you would like a proof format which has hypotheses one the left, before the turnstile, it is also possible to define it, see for example Mario's HOL database, where your statement would be written something like:

ancom $p |- ( R , S ) |= ( S , R ) $=

That's probably as close as you can get.

In practice, in the set.mm database, it common to use a "deduction style" format for proofs, where the implication -> takes the role of the inference rules, and a generic ph takes the role of the context. Then pm3.22 would correspond to your theorem. Its statement is written:

pm3.22 $p |- ( ( ph /\ ps ) -> ( ps /\ ph ) ) $=

But of course, from a proof theoretical point of view, that's a different statement.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.