7.1.4 Proofs in Hilbert Calculus

Continuation.

Proof

An occurence of a rule schema where all schematic formulae (like , etc.) have been replaced by actual formulae of the language is called an instance of that schema. A proof with our little calculus is simply a sequence of instances of the inference rule schema, such that the antecedents of each rule are succedents of rules earlier in the sequence. If we additionally allow formulae from a set into the sequence, we speak of a proof from the assumptions in . Any formula that occurs in a proof generated from our Hilbert calculus is provable (or provable from the assumptions in if it occurs in a proof from these assumptions). So intuitively, if we want to prove a formula, we take a (possibly empty) set of assumptions and apply the inference rules until we have produced our formula as the conclusion of some rule application.

Theorem

We will write if the formula is provable from the assumptions in in the calculus . We will call the relation the derivability or provability relation for .

We will simply write if is provable from the assumptions in (so a shorthand for ). A formula that is provable without any further assumptions is called a theorem .

An Example Proof

Let us look at an example to fortify our intuition. We will prove the theorem .

There are two things to note about this proof.

The last observation is negative. But it mainly has to do with the particular calculus we're using. We will discuss a more intuitive calculus (called semantic tableaux) later.

The Axiomatic Method

The first observation in contrast is a positive one. Indeed it is the great pro of using calculi (or the axiomatic method , as one also says): Instead of thinking about infinitely many models for validity , we can consider provability , which can be exhibited by pure syntactic formula manipulation. The only question that remains is how provability and validity relate to each other. In other words: We want to justify our calculus in terms of semantics again.


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