AxmPropExFalso (1.11, Axiom): A11

Standalone kernel entity record from 1. Propositional Logic (1.01–1.14) — View in Complete Entity Database (#AxmPropExFalso) →

Formula Display:
Proof Trees:

AxmPropExFalso (1.11) — A11

Classical propositional calculus axiom schemas (A01–A13) and Modus Ponens.

Num Entity Database Record (Vertical Field Table)
1.11
Title A11 #AxmPropExFalso #label-a11
Classification Axiom
Formula
0(⊥→⟦𝛂⟧)
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/bot-const.html}{\bot} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST PA11_prf
Scheme of Types 0(⊥→⟦[𝛂@Fm.Expression]⟧)
Judgements
1[(𝛂:Fm)]
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/image-op.html}{]} \)
Verification Postulated (Kernel Axiom) · Standalone Entry (AxmPropExFalso) → · (1.11) · #AxmPropExFalso