Symbol Reference: ∨ — Logical Disjunction Connective (∨, AST Constructor: TpOr)

∨ \(\lor\) — Logical Disjunction Connective (∨, AST Constructor: TpOr)

Binary inclusive logical disjunction connective 𝛂 ∨ 𝛃, governed by axioms A06, A07, and A08.

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	∨ \(\lor\)
Category	Logical Connective (Binary Truth-Functional Symbol)
SML AST Constructor	`HP (TpOr of ('Truth_EXP * 'Truth_EXP)) [in datatype Truth_p, typetheory.ML:654]`
Constructor Arguments	1. Left disjunct 𝛂 : Fm; 2. Right disjunct 𝛃 : Fm
Metatype / Signature	`Fm × Fm → Fm \| Bool × Bool → Bool`
Binder Status	No — Binary Logical Connective (Disjunction)
Defining Kernel Entries (ML Labels)	Axiom AxmPropDisjLeft (1.06): A06 (`#AxmPropDisjLeft` / `#label-a06`) · Axiom AxmPropDisjRight (1.07): A07 (`#AxmPropDisjRight` / `#label-a07`) · Axiom AxmPropDisjElim (1.08): A08 (`#AxmPropDisjElim` / `#label-a08`)
LaTeX Form	`\lor`
How to Understand It	SML AST Constructor: `HP (TpOr of ('Truth_EXP * 'Truth_EXP))` in `Truth_p` (`typetheory.ML:654`). Takes left disjunct `𝛂 : Fm` and right disjunct `𝛃 : Fm`.
Canonical Law / Usage	`𝛂 → (𝛂 ∨ 𝛃)`
Related Symbols & Kernel Entries	Axiom AxmPropDisjLeft (1.06): A06 Axiom AxmPropDisjRight (1.07): A07 Axiom AxmPropDisjElim (1.08): A08

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

Title	A06 `#AxmPropDisjLeft` `#label-a06`
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{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/or-conn.html}{\lor} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA6_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 (`AxmPropDisjLeft`) → · (1.06) · `#AxmPropDisjLeft`

1.07

Title	A07 `#AxmPropDisjRight` `#label-a07`
Classification	Axiom
Formula	0(⟦𝛃⟧→(⟦𝛂⟧∨⟦𝛃⟧)) 0\(\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/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/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PA7_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 (`AxmPropDisjRight`) → · (1.07) · `#AxmPropDisjRight`

1.08

Title	A08 `#AxmPropDisjElim` `#label-a08`
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{\gamma}} \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{\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/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/or-conn.html}{\lor} \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/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	`PA8_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 (`AxmPropDisjElim`) → · (1.08) · `#AxmPropDisjElim`