What does two-sided turnstile means in logic?

Question

I seem to not find this symbol on any other website or document and am struggling to find out its meaning: two-sided turnstile

The whole thing, for context purposes is: context

Or is it just another way to write double-turnstile?

Answer 1

First of all, that is a meta-logic symbol, not a logic symbol. That is, it expresses a connection between the logic statements $p \rightarrow q$ and $\neg p \lor q$.

One option is that it is used to express that using the rules of the system, the two statements can be derived from each other. As such, it would be equivalent to making the following two claims:

$p \rightarrow q \vdash \neg p \lor q$

and

$ \neg p \lor q \vdash p \rightarrow q$

However, I know I have also seen it expressing a rule of replacement, meaning that any $p \rightarrow q$ in any formula can be replaced by $\neg p \lor q$ and vice versa.

A rule of replacement is like a rule of inference, but different in two ways:

1. The inference goes both ways, rather than one way.

2. It can be applied to component statements.

EDIT

Now that you me the larger context, it is clear that the former is meant. So, you need to do two proofs: one where you infer $\neg p \lor q$ from $p \rightarrow q$, and one where you infer $p \rightarrow q$ from $\neg p \lor q$

Answer 2

A sequent logic is a set of rules for using existing statements to create new statements.

A turnstyle, $A \vdash B$, indicates that the rules allow for $B$ to be created from $A$.

A double turnstyle indicates that the above holds as well as $A$ can be created from $B$, that is, they both can be created from each other by the set of rules.

If the logic is sound, then a double turnstyle will be equivalent to the $\iff$ (if and only if) operator, but if a logic isn't sound then a turnstyle or double turnstyle might not indicate anything useful at all.