Category:Provable Consequences
Jump to navigation
Jump to search
This category contains results about Provable Consequences.
Definitions specific to this category can be found in Definitions/Provable Consequences.
Let $\mathscr P$ be a proof system for a formal language $\LL$.
Let $\FF$ be a collection of WFFs of $\LL$.
Denote with $\map {\mathscr P} \FF$ the proof system obtained from $\mathscr P$ by adding all the WFFs from $\FF$ as axioms.
Let $\phi$ be a theorem of $\map {\mathscr P} \FF$.
Then $\phi$ is called a provable consequence of $\FF$, and this is denoted as:
- $\FF \vdash_{\mathscr P} \phi$
Note in particular that for $\FF = \O$, this notation agrees with the notation for a $\mathscr P$-theorem:
- $\vdash_{\mathscr P} \phi$
This category currently contains no pages or media.