# Introduction to Philosophy/Logic/A More Formal Approach to Sentential Logic

Introduction to Philosophy > Logic > A More Formal Approach to Sentential Logic
Our truth table analysis has revealed something interesting about the logical connectives. In particular, that they behave in some ways like + and . on ordinary numbers. Our journey into the world of abstraction has dealt some dividends, so now we shall go a little bit further down the path of abstraction.
What we are going to do is to define the propositional calculus as a formal language, rather like a computer programming language. We will use English, together with one or two Greek letters, to define and talk about the formal language of propositional calculus. Thus English is the metalanguage, and propositional calculus is the object language.

## Well-Formed Formulae

We have introduced logical formulae. Some strings of logical symbols make sense and some do not; ' p ∨ ' is nonsense as it wants something after the connective. The ones that do make sense are called well formed formulas or wffs for short. We can introduce some rules for distinguishing wffs from gobbledegook:
* Any sentence letter is a wff.
    So far we have been using p, q and r as sentence letters. In reality, there is an infinite supply of them. We could write p$_1$, p$_2$, p$_3$, and so forth, but we shall stay with p, q, and r.
* If φ is a wff, then ¬ φ is a wff.
* If φ and ψ are wffs, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ) and (φ ↔ ψ)are wffs.
    In our formal treatment we always write the brackets.
* Closure Clause: Nothing else is a wff.
This rules out nonsense strings. Note that, though the rules are to distinguish that which could be meaningful from that which is not, the rules are purely syntactic.
The other thing to note is that the rules have inverses, which is handy for deciding whether something that has already been written is a wff or not. We just apply these inverse rules until either we are left with nothing or get stuck. So we have an effective procedure for generating wffs, and an effective procedure for deciding whether a string is a wff.
We now introduce some rules of inference for propositional calculus. In some ways these rules are unnecessary, as we could take truth tables as as fundamental and prove the following rules using truth tables. However, when we get to predicate calculus, we won't have truth tables to help us, and will have to rely entirely on rules of inference.

## Rules of Inference

We now introduce some rules of inference for propositional calculus. In some ways these rules are unnecessary, as we could take truth tables as as fundamental and prove the following rules using truth tables. However, when we get to predicate calculus, we won't have truth tables to help us, and will have to rely entirely on rules of inference.
* Double Negative Elimination: From the wff ¬ ¬ φ, we may infer φ.
* Conjunction Introduction: From any wff φ and any wff ψ, we may infer ( φ ∧ ψ ).
* Conjunction Elimination: From any wff ( φ ∧ ψ ), we may infer φ and ψ
* Disjunction Introduction: From any wff φ, we may infer (φ ∨ ψ) and (ψ ∨ φ), where ψ is any wff.
* Disjunction Elimination: From wffs of the form ( φ ∨ ψ ), ( φ → χ ), and ( ψ → χ ), we may infer χ.
* Bi conditional Introduction: From wffs of the form ( φ → ψ ) and ( ψ → φ ), we may infer ( φ ↔ ψ ).
* Bi conditional Elimination: From the wff ( φ ↔ ψ ), we may infer ( φ → ψ ) and ( ψ → φ ).
* Modus Ponens: From wffs of the form φ and ( φ → ψ ), we may infer ψ.
* Conditional Proof: If ψ can be derived while assuming the hypothesis φ, we may infer ( φ → ψ ).
* Reductio ad Absurdum: If we can derive both ψ and ¬ ψ while assuming the hypothesis φ, we may infer ¬ φ.

## Interdefinability of operators

It is possible to define some logic operators in terms of others. For example, the truth table for the formula (φ → ψ) is equal to that of ¬(φ ∧ ¬ψ), so we might want to consider (φ → ψ) nothing more than an abbreviated notation for ¬(φ ∧ ¬ψ). The interesting point here is that all logic operators in propositional calculus can be expressed in terms of ¬ and ∧. This fact allows us to express the rules for well-formed formulae in a very simple way:
* If φ is a wff, then ¬ φ is a wff.
* If φ and ψ are wffs, then (φ ∧ ψ) is a wff.
* Nothing else is a well formed formula.
We can then define the other operators in terms of these two:
* (φ → ψ) is, by definition, ¬(φ ∧ ¬ψ).
* (φ ↔ ψ) is, by definition, (φ → ψ) ∧ (ψ → φ).
* (φ ∨ ψ) is, by definition, ¬(¬φ ∧ ¬ψ).
If we take into account these definitions (three additional rules), it may seem that we have not gained much by reducing the number of primitive operators. However, when the system of propositional calculus is considered as a whole (as, for example, when we are studying the properties of the system) it is useful to have a description of the system in terms of a very small number of rules. In cases like this we are not interested in particular formulae, so we can drop the additional rules which define the other operators. It is also possible to prove that all logical operators can be defined in terms of ¬ and ∨.