Expressing provability in PVS

[Giulia Sindoni]

Hi everyone,

I was wondering: 

Is there in PVS a way to express, within a theorem or lemma declaration, that a certain formula is provable from the empty set of assumption (i.e. it is a theorem)?

In a lemma, I want to say something like:

Given a boolean formula phi, if phi is provable from the empty set of assumptions, then …. (some conclusion).

I thought of using the symbol |- and write something like 

mylemma: LEMMA

FORALL (phi: bool):

|- phi IMPLIES ….

But it doesn’t seem possible to use the symbol |- as I am using it.

Initially, I though I could simply write 

mylemma1: LEMMA

FORALL (phi: bool):

 phi IMPLIES …

But I believe there is a difference between mylemma and mylemma1. For example, if phi is an atomic uninterpreted boolean formula, like p, that could therefore be interpreted both as True or as False,  |- phi means 

phi si true for all possible assignments of phi  to {True, False}

(which is of course never the case for an atom, as there is always an interpretation that assigns phi to False as well as an interpretation that assigns it to True). Whilst stating  phi simply means 

let’s assume that phi is True.

so in the latter case we assume we are working under a specific interpretation.

Has anyone come across the need of expressing something similar to this in PVS?

Giulia