Symbol Reference: → — Material Implication Connective (→, AST Constructor: TpImpl)

→ \(\to\) — Material Implication Connective (→, AST Constructor: TpImpl)

Primitive binary logical connective of material implication (𝛂 → 𝛃), governed by Hilbert axioms A01, A02 and Modus Ponens (Rule RulModusPonens (1.14)).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	→ \(\to\)
Category	Logical Connective (Binary Truth-Functional Symbol)
SML AST Constructor	`HP (TpImpl of ('Truth_EXP * 'Truth_EXP)) [in datatype Truth_p, typetheory.ML:651]`
Constructor Arguments	1. Antecedent formula 𝛂 : Fm; 2. Consequent formula 𝛃 : Fm
Metatype / Signature	`Fm × Fm → Fm \| Bool × Bool → Bool`
Binder Status	No — Binary Logical Connective (Truth-Functional Symbol)
Defining Kernel Entries (ML Labels)	Axiom AxmPropWeakening (1.01): A01 (`#AxmPropWeakening` / `#label-a01`) · Axiom AxmPropFrege (1.02): A02 (`#AxmPropFrege` / `#label-a02`) · Inference Rule RulModusPonens (1.14): Modus Ponens (`#RulModusPonens` / `#label-modus-ponens`)
LaTeX Form	`\to`
How to Understand It	SML AST Constructor: `HP (TpImpl of ('Truth_EXP * 'Truth_EXP))` in `Truth_p` (`typetheory.ML:651`). Takes two formula arguments `(𝛂 : Fm, 𝛃 : Fm)`.
Canonical Law / Usage	`𝛂 → (𝛃 → 𝛂)`
Related Symbols & Kernel Entries	Axiom AxmPropWeakening (1.01): A01 Axiom AxmPropFrege (1.02): A02 Inference Rule RulModusPonens (1.14): Modus Ponens

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.01

Title	A01 `#AxmPropWeakening` `#label-a01`
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/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \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}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA1_prf`
Scheme of Types	0`(⟦[𝛂@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}{]} \)
Verification	Postulated (Kernel Axiom) · Standalone Entry (`AxmPropWeakening`) → · (1.01) · `#AxmPropWeakening`

1.02

Title	A02 `#AxmPropFrege` `#label-a02`
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/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\gamma}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.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/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/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{\gamma}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA2_prf`
Scheme of Types	0`((⟦[𝛂@Fm.Expression]⟧→(⟦[𝛃@Fm.Expression]⟧→⟦[𝛄@Fm.Expression]⟧))→((⟦[𝛂@Fm.Expression]⟧→⟦[𝛃@Fm.Expression]⟧)→(⟦[𝛂@Fm.Expression]⟧→⟦[𝛄@Fm.Expression]⟧)))`
Judgements	1[(𝛂 :Fm ), (𝛃 :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/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\gamma}} \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 (`AxmPropFrege`) → · (1.02) · `#AxmPropFrege`

1.14

Title	Modus Ponens `#RulModusPonens` `#label-modus-ponens`
Classification	Inference Rule
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/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[(𝛂: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}{]} \)
Side Condition	1⊤ 1\(\href{../symbols/top-const.html}{\top} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulModusPonens`) → · (1.14) · `#RulModusPonens`