Left-hand side does not contain formula φ

[pgimalac]

Hello, I'm trying to prove ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))), I tried using Trivial, but I get the error message "Left-hand side does not contain formula φ", what does this error mean ?

    have("(∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))") by Hypothesis
    andThen("∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)))") by Trivial

Trivial seems to find a (big) proof by itself, but one of the steps fails:

The given proof is incorrect: Left-hand side does not contain formula φ
   0       Hypo.         (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
   1       Subproof 0    ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
     -1    Import 0      (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
      0    Rewrite -1    ⊢ ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))) ⇒ ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)))
      1    Subproof      ∀'x. 'P('x) ∧ 'R('x, 'x); ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))) ⇒ ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
->       0 Hypo.         ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ∀'x. 'P('x)
         1 Hypo.         ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ∀'x. 'P('x); ∀'x. 'R('x, 'x)
         2 Right ∧ 0, 1  ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ∀'x. 'P('x); (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
         3 Right ∧ 2     ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)); ∀'x. 'P('x)
         4 Hypo.         ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ∀'x. 'R('x, 'x); ∀'x. 'P('x)
         5 Hypo.         ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ∀'x. 'R('x, 'x)
         6 Right ∧ 4, 5  ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ ∀'x. 'R('x, 'x); (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
         7 Right ∧ 6     ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)); ∀'x. 'R('x, 'x)
         8 Right ∧ 3, 7  ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)); (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
         9 Hypo.         ∀'x. 'P('x) ∧ 'R('x, 'x); ∀'x. 'P('x); ∀'x. 'R('x, 'x) ⊢ ∀'x. 'P('x)
        10 Hypo.         ∀'x. 'P('x) ∧ 'R('x, 'x); ∀'x. 'P('x); ∀'x. 'R('x, 'x) ⊢ ∀'x. 'R('x, 'x)
        11 Right ∧ 9, 10 ∀'x. 'P('x) ∧ 'R('x, 'x); ∀'x. 'P('x); ∀'x. 'R('x, 'x) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
        12 Left ∧ 11     ∀'x. 'P('x) ∧ 'R('x, 'x); (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
        13 Left ∨ 12     ∀'x. 'P('x) ∧ 'R('x, 'x); (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x)) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
        14 Left → 8, 13  ∀'x. 'P('x) ∧ 'R('x, 'x); ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))) ⇒ ((∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
      2    Cut 0, 1      ∀'x. 'P('x) ∧ 'R('x, 'x) ⊢ (∀'x. 'P('x)) ∧ (∀'x. 'R('x, 'x))
Proof checker has reported an error at line 1.1.0: Left-hand side does not contain formula φ

Is it because it's using Hypothesis on something which is not in the form φ ⊢ φ ?

I managed to prove step 1.1.0 myself, is there a way to insert that into Trivial's proof or do I have to do the whole proof by hand ?

Thanks.

[pgimalac]

I managed to prove what I wanted by proving 1.1.0 and 1.1.5, then performing a RightAnd, so nevermind the last question, but I'm still curious as to what Left-hand side does not contain formula φ means.

[SimonGuilloud]

Good question! The answer is rather simple. Trivial is only able to do reasonning about propositional logic and knows nothing of formulas. Hence, the proposition, you're trying to prove is not provable by Trivial.

Then, Trivial has a gready technique. When it comes down to a sequent with no top level propositional symbols, it simply assumes "Hypothesis" will work and there will be a non-empty intersection between the left and right of the sequent (This is indeed always true if the sequent we are trying to prove is a propositional tautology!).

It is certainly true that this "least effort" tentative is very unhelpful when the tactics fails, and we are currently building a better error report system :)

[pgimalac]

Thanks for the answer :)