Definition:Tableau Proof (Propositional Tableaus)/Proof System

From ProofWiki
Jump to navigation Jump to search

Proof System

Tableau proofs form a proof system $\mathrm{PT}$ for the language of propositional logic $\mathcal L_0$.

It consists solely of axioms, in the following way:

A WFF $\mathbf A$ is a $\mathrm{PT}$-axiom if and only if there exists a tableau proof of $\mathbf A$.

Likewise, we can define the notion of provable consequence for $\mathrm{PT}$:

A WFF $\mathbf A$ is a $\mathrm{PT}$-provable consequence of a collection of WFFs $\mathbf H$ if there exists a tableau proof of $\mathbf A$ from $\mathbf H$.

Although formally $\mathrm{PT}$ has no rules of inference, the rules for the definition of propositional tableaus can informally be regarded as such.