Symbol Reference: ¬ — Logical Negation Connective (¬, AST Constructor: TpNeg)

¬ \(\neg\) — Logical Negation Connective (¬, AST Constructor: TpNeg)

Unary logical negation connective ¬𝛂, governed by axioms A09, A10, and Law of Excluded Middle A12.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	¬ \(\neg\)
Category	Logical Connective (Unary Truth-Functional Symbol)
SML AST Constructor	`HP (TpNeg of 'Truth_EXP) [in datatype Truth_p, typetheory.ML:650]`
Constructor Arguments	1. Negated formula 𝛂 : Fm
Metatype / Signature	`Fm → Fm \| Bool → Bool`
Binder Status	No — Unary Logical Connective (Negation)
Defining Kernel Entries (ML Labels)	Axiom AxmPropNegElim (1.09): A09 (`#AxmPropNegElim` / `#label-a09`) · Axiom AxmPropNegIntro (1.10): A10 (`#AxmPropNegIntro` / `#label-a10`) · Axiom AxmPropExcludedMiddle (1.12): A12 (`#AxmPropExcludedMiddle` / `#label-a12`)
LaTeX Form	`\neg`
How to Understand It	SML AST Constructor: `HP (TpNeg of 'Truth_EXP)` in `Truth_p` (`typetheory.ML:650`). Takes one formula argument `𝛂 : Fm`.
Canonical Law / Usage	`𝛂 ∨ (¬𝛂)`
Related Symbols & Kernel Entries	Axiom AxmPropNegElim (1.09): A09 Axiom AxmPropNegIntro (1.10): A10 Axiom AxmPropExcludedMiddle (1.12): A12

Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)

Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.

# Formal Entity Specification

1.09

Title	A09 `#AxmPropNegElim` `#label-a09`
Classification	Axiom
Formula	0((¬⟦𝛂⟧)→(⟦𝛂⟧→⊥)) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \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}{)} \href{../symbols/impl-conn.html}{\rightarrow} \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/bot-const.html}{\bot} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA9_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}{]} \)
Kernel Note	Negation Elimination (Contradiction to Bottom): (¬⟦𝛂⟧) → (⟦𝛂⟧ → ⊥).
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmPropNegElim`) → · (1.09) · `#AxmPropNegElim`

1.10

Title	A10 `#AxmPropNegIntro` `#label-a10`
Classification	Axiom
Formula	0((⟦𝛂⟧→⟦𝛃⟧)→((⟦𝛂⟧→¬⟦𝛃⟧)→¬⟦𝛂⟧)) 0\(\href{../symbols/delimiters-brackets.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/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.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/neg-conn.html}{\neg} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \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}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA10_prf`
Scheme of Types	0`((⟦[𝛂@Fm.Expression]⟧→⟦[𝛃@Fm.Expression]⟧)→((⟦[𝛂@Fm.Expression]⟧→¬⟦[𝛃@Fm.Expression]⟧)→¬⟦[𝛂@Fm.Expression]⟧))`
Judgements	1[(𝛂 :Fm ), (𝛃 :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/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}{]} \)
Kernel Note	Negation Introduction (Reductio Ad Absurdum): (⟦𝛂⟧ → ⟦𝛃⟧) → ((⟦𝛂⟧ → ¬⟦𝛃⟧) → ¬⟦𝛂⟧).
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmPropNegIntro`) → · (1.10) · `#AxmPropNegIntro`

1.12

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`