AxmDiscourseNonEmpty (2.01, Axiom): Discourse domain is non-empty

Standalone kernel entity record from 2. Predicate Logic (2.01–2.06) — View in Complete Entity Database (#AxmDiscourseNonEmpty) →

Formula Display:
Proof Trees:

AxmDiscourseNonEmpty (2.01) — Discourse domain is non-empty

First-order quantifier instantiation, abstraction rules, and non-empty discourse domain over Classes.

Num Entity Database Record (Vertical Field Table)
2.01
Title Discourse domain is non-empty #AxmDiscourseNonEmpty #label-discourse-domain-is-non-empty
Classification Axiom
Formula
0(∃(K:Class)⊤)
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/exists-binder.html}{\exists} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/top-const.html}{\top} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST PA0_prf
Scheme of Types 0(∃([K@Variable]:[Class@Type])⊤)
Verification Postulated (Kernel Axiom) · Standalone Entry (AxmDiscourseNonEmpty) → · (2.01) · #AxmDiscourseNonEmpty