## A simple proof system

Now that we have defined semantic validity with ⊨ it is time to look at *syntactic* validity.
Syntactic validity, or derivability, is written ⊢ Γ.
This validity predicate is built up from axioms and proof rules.

### Axioms

Our three axioms can be written as

The True axiom states that ⊢ ⊤^{+}.
In other words, that ⊤^{+} is derivable.
We will later show the soundness and completeness,
⊢ Γ if and only if ⊨ Γ.

The assumption axiom states that any sequent containing both φ^{+} and φ^{-} is always true.
Recall that a sequent is a disjunction, so we are just saying that φ ∨ ¬φ.

### Rules

A complete *derivation of ⊢ Γ* will be a tree with ⊢ Γ at the root and axioms at the leafs.
The internal nodes will be formed by *rules*.

The simplest of these rules are the *negation rules*:

If it is possible to derive φ^{-}, then by applying this rule to the resulting sequent, ¬φ^{+} can be derived.
Note that the sequents contain a part Γ which the rule does not change, we call Γ the *context*.
The formulas that are actively used by the rule are called *principal* formulas.
Γ can stand for any sequent and φ for any formula.

The disjunction rules use the fact that a sequent is interpreted as a disjunction.
They just compose φ^{+} ∨ ψ^{+} into {φ^{+},ψ^{+}}.
Note that negative occurrences of ∧ also fall under the disjunction rule because of De Morgan's laws.

To derive a conjunction (or negative disjunction), for example φ∧ψ^{+}, two derivations are needed;
one for φ^{+} and one for ψ^{+}. If both of these are derivable, then so is their conjunction.

Each of these *logical rules* adds a connective when read from top to bottom.
And we now have rules for all logical connectives in our language.

### Example

Consider the formula (p ∨ ¬(p ∧ q)) ∧ ⊤. A possible derivation of that formula is:

Note that there are not many choices in our proof system; in fact there are no other ways to write a derivation of this formula.

## The proof search algorithm

But what do all these logic proofs have to do with semantic tableaux?

We can use the rules we have defined in a *proof search*.
In such a search we know what formula we are after, it will be at the root of the derivation tree.
Then we apply proof rules *bottom-up* until we reach an axiom.
So if we go back to the example above, we would start by writing:

This sequent can only be the result of the conjunction rule.
This rule will *take apart* the ∧ connective.

On the right we already have an axiom. On the left the outermost connective is a disjunction; and we have a rule for taking it apart. We can continue this until all branches reach an axiom, in which case the derivation is finished, or until no further rules can be applied, in which case the derivation fails, and we know the formula is not syntactically valid.

**Algorithm**proof search 1

**input:** A goal sequent

**output:** A derivation of that sequent if it exists

- If our current goal sequent matches an axiom, we are done.
- If our current goal ⊢ Γ,A matches the bottom of a logical rule then
- Apply the logical rule, giving one or more sequents Γ,A,B.
- Use a proof search to find a proof of the new sequent(s).

- If no rules can be applied then the search has failed.

## Keeping duplicates

Now consider the goal formula long → (long ∨ x) where long is a very long subformula.
During the proof search, after applying a rule for the implication we have the sequent
{long^{-}, long ∨ x^{+}}.
If we now take apart the disjunction we immediately arrive at an axiom.
However, if we first take apart the long formula the derivation will get larger, and there is no easy way to simplify it afterwards.
Similarly, if we encounter long ∨ long ∨ x^{+} both of the long subformulas will be taken apart.

The solution to these problems is to keep a copy of the formula. So for example the new disjunction rule would become

For readability we will not write the rules in +C form, because keeping track of all copies is tedious.
Instead we conceptually use a *meta-rule* for transforming all rules:

Where A and B are the principal formulas of the rule. From now on, all rules will be considered to keep copies.

### Termination

If we try to do a proof search we hit a minor problem: the algorithm does not terminate. The same rule can be applied over and over again. Clearly each formula should be taken apart only once.

**Algorithm**proof search 2

**input:** A goal sequent

**output:** A derivation of that sequent if it exists

- If our current goal sequent matches an axiom, we are done.
- If our current goal ⊢ Γ,A matches the bottom of a logical rule,
*and the principal formulas have not participated in this rule before*, then- Apply the logical rule, giving one or more sequents Γ,A,B.
- Use a proof search to find a proof of the new sequent(s).

- If no rules can be applied then the search has failed.

### Marks

To administer which formulas we have already inspected we mark them in the sequent.

**Definition:**
A *marked formula* is a signed formula that is marked as either *used* or as *unused*.
We will draw used formulas in grey and unused formulas in blue.

So again the disjunction rule, this time with marks:

The distinction between used and unused formulas is only made for the purpose of presentation,
it is just a way of administrating the information needed for the *proof search 2* algorithm.

### Does it work?

Let us go back to the problematic examples.

In the case of long → (long ∨ x) we can still take apart the long formula,
after which we end up with a sequent like {ContentsOfLong, long^{-}, long ∨ x^{+}}.
The only remaining rule that can be applied is the disjunction rule to the rightmost term, giving
{ContentsOfOld, long^{-}, long ∨ x^{+}, long^{+}, x^{+}}.
And this does match the assumption axiom.

In the second problematic case we had multiple copies of a long formula.
When used formulas are kept this no longer possible because the sequent is a set,
it can contain only one copy of any signed formula.
So for example when the disjunction rule is applied to the last formula of
{ContenstOfLong, long^{+}, long ∨ long^{+}}
The resulting sequent becomes simply {ContenstOfLong, long^{+}}.