1

We were introduced to these rules during class and not sure how to grasp it. And what does this symbol mean ⊢?

enter image description here

UPDATE: Added rules 1a and 1b

Rule 1a: if the goal list has a proposition that is also in the hypothesis list, the conjecture is true.

Rule 1b: if both the goal list and hypothesis list contain propositions only, and no common propositions, the conjecture is disproven.

phoxd
  • 321
  • This https://math.stackexchange.com/questions/446178/math-logic-what-does-x-vdash-a-a-in-x-mean?rq=1 ? – Martin R Mar 21 '18 at 09:14
  • It means "is derivable" (in the "calculus" you are wroking with). – Mauro ALLEGRANZA Mar 21 '18 at 09:20
  • 1
    So the above rules must be read as follows: if we have a derivation of $G$ from $H$ and $\lnot F$, then we have a derivation of $G$ and $F$ from $H$. – Mauro ALLEGRANZA Mar 21 '18 at 09:22
  • Can you type out the rule 1a and 1b (presumably dealing with implication). Because depending on that the $\vdash$ can either be meant correctly as "derivation" or incorrectly as "under the assumption of" – DanielV Mar 21 '18 at 18:08
  • I updated and included 1a and 2b rule. This was used to describe Wang algorithm for theorem proving. Now I understand it a bit more. – phoxd Mar 25 '18 at 07:39

1 Answers1

2

These are the rules for Sequent calculus.

It formalizes the rules regarding the derivability relation: $\vdash$ (the symbol is called "the turnstile").

Each rule is expressed in terms of sequents: $A_1,\ldots, A_n \vdash B_1, \ldots B_k$.

The formulas to the left of the turnstile are called the antecedent, and the formulas on the right are called the succedent or consequent.

Mauro ALLEGRANZA
  • 94,169
  • 2
    Just to complete Mauro's answer: intuitively, a sequent $A_1,\ldots, A_n \vdash B_1, \ldots, B_k$ means that if you assume $A_1 \land \ldots \land A_n$ then $B_1 \lor \ldots \lor B_k$ follows by necessity. – Taroccoesbrocco Mar 21 '18 at 09:48
  • They're a rather curious sequent calculus, though, because they have the sequents with additional connectives in the premises rather than the conclusions. – hmakholm left over Monica Mar 21 '18 at 11:20