Definition:Complete Proof System

From ProofWiki
Jump to navigation Jump to search

This page is about Complete Proof System. For other uses, see Complete.

Definition

Let $\LL$ be a logical language.

Let $\mathscr P$ be a proof system for $\LL$, and let $\mathscr M$ be a formal semantics for $\LL$.


Then $\mathscr P$ is said to be complete for $\mathscr M$ if and only if:

Every $\mathscr M$-tautology is a $\mathscr P$-theorem.

Symbolically, this can be expressed as the statement that, for every logical formula $\phi$ of $\LL$:

$\models_{\mathscr M} \phi$ implies $\vdash_{\mathscr P} \phi$


Strongly Complete Proof System

$\mathscr P$ is strongly complete for $\mathscr M$ if and only if:

Every $\mathscr M$-semantic consequence is a $\mathscr P$-provable consequence.

Symbolically, this can be expressed as the statement that, for every collection $\FF$ of logical formulas, and every logical formula $\phi$ of $\LL$:

$\FF \models_{\mathscr M} \phi$ implies $\FF \vdash_{\mathscr P} \phi$


Also known as

Many sources obfuscate the distinction between complete and strongly complete.


Also see


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Definition:Complete_Proof_System&oldid=644361"