AxmPropExcludedMiddle (1.12, Axiom): A12

AxmPropExcludedMiddle (1.12) — A12

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

Num Entity Database Record (Vertical Field Table)

Title	A12 `#AxmPropExcludedMiddle` `#label-a12`
Classification	Axiom
Formula	0(⟦𝛂⟧∨¬⟦𝛂⟧) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/or-conn.html}{\lor} \href{../symbols/neg-conn.html}{\neg} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA12_prf`
Scheme of Types	0`(⟦[𝛂@Fm.Expression]⟧∨¬⟦[𝛂@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 (`AxmPropExcludedMiddle`) → · (1.12) · `#AxmPropExcludedMiddle`