Deductive Closure (Propositional Hilbert Calculus)

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 :

Extensivity

Definition

Extensivity of Deductive Closure (Propositional Hilbert Calculus)

Every propositional theory is contained in its deductive closure:

Every assumption is itself derivable from .

Link to original

Idempotence

Definition

Idempotence of Deductive Closure (Propositional Hilbert Calculus)

For every propositional theory , taking its deductive closure twice gives the same result as taking it once:

Using already derivable formulas as assumptions adds no further consequences.

Link to original

Monotonicity

Definition

Monotonicity of Deductive Closure (Propositional Hilbert Calculus)

For all propositional theories , deductive closure preserves inclusion:

Adding assumptions cannot remove derivable formulas.

Link to original