7.1.3 A simple Logical System: Propositional Logic with Hilbert-Calculus

An example logical system.

In this section we will discuss the simplest non-trivial fragment of first-order logic imaginable: A formal language which has only one constant symbol, and where atomic formulae have been abbreviated to propositional variables. We will call this logic PH.

We have chosen this logic so that talking about it is simple, not that it covers any interesting fragment of natural language. We want to make clear certain concepts that will become important later, but we don't want to go through the exercise of formulating a calculus for a more expressive logic yet. Still you needn't worry, we will do so soon!

As discussed above, a logic has three components:

Syntax

The set of well-formed formulae of PH is built from propositional variables: and the logical operator of implication:

Semantics

The semantics of PH is determined by the following rules:

Calculus

The calculus is given by specifying its inference rules. Inference rules are generally written as schemata of the following form:

Here the and are (schematic) formulae and is the name of the inference rule. The rule signifies that whenever all of the formulae (the so-called called antecedent s or premise s) have already been derived, the formula (the succedent or conclusion ) can also be derived.

Here are the four inference rules of our calculus:

The first two inference rules are special cases, where the antecedents are empty. Such inference rules are commonly called axiom s. What makes them special is that their conclusions can be derived without assumptions, that is at any time. The rule is sometimes called modus ponens ; it codifies our intuition about the implication operator. The rule allows to substitute arbitrary well-formed formulae for propositional variables. We will use the notation , for the application of the substitution , to the formula . This replaces all occurrences of the propositional variable in with the formula . For example is .


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)