Symbol Reference: ∧ — Logical Conjunction Connective (∧, AST Constructor: TpAnd)

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

∧ \(\land\) — Logical Conjunction Connective (∧, AST Constructor: TpAnd)

Binary logical conjunction connective 𝛂 ∧ 𝛃, governed by axioms A03, A04, and A05.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
∧
\(\land\)
Category Logical Connective (Binary Truth-Functional Symbol)
SML AST Constructor HP (TpAnd of ('Truth_EXP * 'Truth_EXP)) [in datatype Truth_p, typetheory.ML:653]
Constructor Arguments 1. Left conjunct 𝛂 : Fm; 2. Right conjunct 𝛃 : Fm
Metatype / Signature Fm × Fm → Fm | Bool × Bool → Bool
Binder Status No — Binary Logical Connective (Conjunction)
Defining Kernel Entries (ML Labels) Axiom AxmPropConjLeft (1.03): A03 (#AxmPropConjLeft / #label-a03) · Axiom AxmPropConjRight (1.04): A04 (#AxmPropConjRight / #label-a04) · Axiom AxmPropConjIntro (1.05): A05 (#AxmPropConjIntro / #label-a05)
LaTeX Form \land
How to Understand It

SML AST Constructor: HP (TpAnd of ('Truth_EXP * 'Truth_EXP)) in Truth_p (typetheory.ML:653). Takes left conjunct 𝛂 : Fm and right conjunct 𝛃 : Fm.
Canonical Law / Usage (𝛂 ∧ 𝛃) → 𝛂
Related Symbols & Kernel Entries

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.03
Title A03 #AxmPropConjLeft #label-a03
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/and-conn.html}{\land} \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{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST PA3_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 (AxmPropConjLeft) → · (1.03) · #AxmPropConjLeft
1.04
Title A04 #AxmPropConjRight #label-a04
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/and-conn.html}{\land} \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{\beta}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST PA4_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 (AxmPropConjRight) → · (1.04) · #AxmPropConjRight
1.05
Title A05 #AxmPropConjIntro #label-a05
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/delimiters-brackets.html}{(} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\alpha}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/and-conn.html}{\land} \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}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST PA5_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}{]} \)
Verification Postulated (Kernel Axiom) · Standalone Entry (AxmPropConjIntro) → · (1.05) · #AxmPropConjIntro