Unclear logic notation for PFX program rules
The "fraction"-style notation is an inference rule in natural deduction style.  See What is this fraction-like &quot;discrete mathematics&quot;–style notation used for formal rules?.

$v_1,\dots,v_n\vdash \cdots$  means "in the environment $v_1,\dots,v_n$, such-and-such is true".  (It's not an "or", and it doesn't mean "implies".)  See What does ⊢ mean in operational semantics?.

I recommend finding a good textbook on programming language semantics, and reading it.  It will give you some background that will help you understand that notation.  It's probably too much to explain all of that in a single answer here.