Introduction

While we can use truth tables to check whether a set of premises entail a conclusion, this requires testing all possible truth assignments – of which there are exponentially many. In this chapter, we will learn the process of natural deduction in propositional logic. This will allow us to start with a set of known facts (premises) and apply a series of rules to see if we can reach some goal conclusion. Essentially, we will be able to see whether a given conclusion necessarily follows from a set of premises.

We will use the Logika tool to check whether our proofs correctly follow our deduction rules. HOWEVER, these proofs can and do exist outside of Logika. Different settings use slightly different syntaxes for the deduction rules, but the rules and proof system are the same. We will merely use Logika to help check our work.

Sequents, premises, and conclusions

A sequent is a mathematical term for an assertion. We use the notation:

p0, p1, ..., pm ⊢ c

The p0, p1, …, pm are called premises and c is called the conclusion. The ⊢ is called the turnstile operator, and we read it as “prove”. The full sequent is read as:

Statements p0, p1, ..., pm PROVE c

A sequent is saying that if we accept statements p0, p1, …, pm as facts, then we guarantee that c is a fact as well.

For example, in the sequent:

p → q , ¬ q  ⊢  ¬ p

The premises are: p → q and ¬q, and the conclusion is ¬p.

(Shortcut: we can use |- in place of the ⊢ turnstile operator.)

Sequent validity

A sequent is said to be valid if, for every truth assignment which make the premises true, then the conclusion is also true.

For example, consider the following sequent:

p → q , ¬ q  ⊢  ¬ p

To check if this sequent is valid, we must find all truth assignments for which both premises are true, and then ensure that those truth assignments also make the conclusion true.

Here is a (non-Logika syntax) type of truth table that combines all three statements:

p q | (p → q) | ( ¬q) |  ¬p
---------------------------
T T |    T     |  F   | F
T F |    F     |  T   | F
F T |    T     |  F   | T
F F |    T     |  T   | T

Examining each row in the above truth table, we see that only the truth assignment [F F] makes both premises (p → q and ¬q) true. We look right to see that the same truth assignment also makes the conclusion ( ¬p) true, which means that the sequent is valid.

Using Logika for proof verification

We can use the Logika tool to help check the correctness of our proofs. (Again, Logika is just a tool to help check our work – we could write the same argument in a different environment or on paper, and the meaning would be the same.)

Each Logika proof should be written in a separate file with a .logika extension. Logika verification knows each of the deduction rules we will see in the next few chapters, and will automatically check to ensure that your steps obey these deduction rules as you type your proof. If a proof is correct, you will see a purple checkmark in the lower right corner that says “Logika verified”. If you have logic errors, you will see them highlighted in red.

Sometimes, the Logika verification needs to be run manually. If you don’t see either red errors or a purple checkmark, right-click in the text area that contains the proof and select “Logika Check”.

Logika proof syntax

Sequents in Logika have the following form:

< 0 or more premises, separated by commas > ⊢ < 1 conclusion >

Proofs in Logika are structured in two columns, with claims on the left and their supporting justification on the right:

premises ⊢ conclusion
{
    1. claim_a          justification_a
    2. claim_b          justification_b
       ...              ...
    736. conclusion     justification_ef
}

Each claim is given a number, and these numbers are generally in order. However, the only rule is that claim numbers be unique (they may be out of order and/or non-consecutive). Once we have justified a claim in a proof, we will refer to it as a fact.

We will see more details of Logika proof syntax as we progress through chapter 4.

Premise justification

The most basic justification for a claim in a proof is “premise”. This justification is used when you pull in a premise from the sequent and introduce it into your proof. All, some or none of the premises can be introduced at any time in any order. Please note that only one premise may be entered per claim.

For example, we might bring in the premises from our sequent like this:

p, q,  ¬r |- p ∧ q
{
    1. p            premise
    2. q            premise
    3.  ¬r           premise
    ...
}

We could also bring in the same premise multiple times, if we wanted. We could also use non-sequential line numbers, as long as each line number was unique:

p, q,  ¬r |- p ∧ q
{
    7. p            premise
    10. q           premise
    2.  ¬r           premise
    8. p            premise
    ...
}

We could only bring in some portion of our premises, if we wanted:

p, q,  ¬r |- p ∧ q
{
    1. p            premise
    ...
}

But we can only list one premise in each claim. For example, the following is not allowed:

p, q,  ¬r |- p ∧ q
{
    //THIS IS WRONG ¬

    1. p, q,  ¬r         premise
    ...
}

Deduction rules

The logical operators (AND, OR, NOT, IMPLIES) are a kind of language for building propositions from basic, primitive propositional atoms. For this reason, we must have laws for constructing propositions and for disassembling them. These laws are called inference rules or deduction rules. A natural deduction system is a set of inference rules, such that for each logical operator, there is a rule for constructing a proposition with that operator (this is called an introduction rule) and there is a rule for disassembling a proposition with that operator (this is called an elimination rule).

For the sections that follow, we will see the introduction and elimination rules for each logical operator. We will then learn how to use these deduction rules to write a formal proof showing that a sequent is valid.