Hilbert Calculus (Propositional Logic)

Definition

Hilbert Calculus ( Propositional Logic)

One Hilbert calculus for propositional logic has the following axiom schemata, for arbitrary formulas :

Its only inference rule is modus ponens. Here, denotes implication.

Inference Rules

The Hilbert calculus of propositional logic consists of only one inference rule:

Modus Ponens

Definition

Modus Ponens (Propositional Logic)

Modus ponens is the inference rule, for arbitrary formulas :

Here, denotes implication.

Link to original

Soundness

Definition

Sound Calculus

A calculus is sound (Korrektheit) if derivability implies entailment: for every set of formulas and every formula ,

Every permitted derivation must therefore establish a semantic consequence. The converse property is completeness.

Link to original

Completeness

Definition

Complete Calculus

A calculus is complete (Vollständigkeit) if entailment implies derivability: for every set of formulas and every formula ,

Every semantic consequence must therefore have a derivation. The converse property is soundness.

Link to original

Derived Inference Rules

Implication Introduction

Definition

Implication Introduction Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, the deduction theorem provides an introduction inference rule for implication. For any theory and formulas :

Here abbreviates ; the conclusion no longer requires as an additional assumption.

Link to original

Implication Elimination

Definition

Implication Elimination Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, implication has the following elimination inference rule, for arbitrary formulas :

This is the derivability form of modus ponens, which is already the calculus’s primitive inference rule.

Link to original

Conjunction Introduction

Definition

Conjunction Introduction Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, conjunction has the following derived introduction inference rule, for arbitrary formulas :

Link to original

Conjunction Elimination

Definition

Conjunction Elimination Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, conjunction has the following derived elimination inference rules, for arbitrary formulas :

Link to original

Disjunction Introduction

Definition

Disjunction Introduction Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, disjunction has the following derived introduction inference rules, for arbitrary formulas :

Link to original

Disjunction Elimination

Definition

Disjunction Elimination Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, proof by cases is the derived elimination inference rule for disjunction. For any theory and formulas :

Here abbreviates : if each case yields , the disjunction suffices to derive .

Link to original

Negation Introduction

Definition

Negation Introduction Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, negation has the following derived introduction inference rule, for any theory and formulas :

Here abbreviates : deriving a contradiction under the additional assumption allows us to discharge and conclude .

Link to original

Double Negation Elimination

Definition

Double Negation Elimination Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, double negation elimination is the following derived elimination inference rule, for any formula :

Link to original

Weak Negation Elimination

Definition

Weak Negation Elimination Inference Rule (Propositional Hilbert Calculus)

In the propositional Hilbert calculus, weak negation elimination is the following derived elimination inference rule, for arbitrary formulas :

This is the principle of explosion (ex falso sequitur quodlibet): a formula and its negation allow any conclusion.

Link to original

Proof

Definition

Proof (Propositional Hilbert Calculus)

A proof in the Hilbert calculus is a finite sequence of formulas, , where each is either:

• an instance of ; or
• obtained by modus ponens from earlier entries:

A formula is provable, written , iff such a proof ends with .

Link to original

Derivation

Definition

Derivation (Propositional Hilbert Calculus)

A derivation from a theory in the Hilbert calculus is a finite sequence of formulas, , where each is either:

• an instance of ;
• a premise ; or
• obtained by modus ponens from earlier entries:

Its conclusion is . For , it is an assumption-free proof.

Link to original

Deductive Closure

Definition

Deductive Closure (Propositional Hilbert Calculus)

In the propositional Hilbert calculus , the deductive closure of a theory is the set of all formulas derivable from :

Link to original

Consistency

Definition

Consistent Theory (Propositional Hilbert Calculus)

A propositional theory is consistent in the Hilbert calculus if falsum is not derivable from :

Link to original

Example