| Title |
Modus Ponens #RulModusPonens #label-modus-ponens |
| Classification |
Inference Rule |
| Formula |
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/turnstile-derivability.html}{\vdash} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
PMP_prf |
| Scheme of Types |
0(โฆ[๐@Fm.Expression]โง, (โฆ[๐@Fm.Expression]โงโโฆ[๐@Fm.Expression]โง) โข โฆ[๐@Fm.Expression]โง) |
| Judgements |
1\(\href{../symbols/image-op.html}{[} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/image-op.html}{]} \)
|
| Side Condition |
1\(\href{../symbols/top-const.html}{\top} \)
|
| Verification |
Primitive / Derived Rule (Kernel) · Standalone Entry (RulModusPonens) → · (1.14) · #RulModusPonens |