ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  wal Structured version   Unicode version

Syntax Definition wal 1267
Description: Extend wff definition to include the universal quantifier ('for all'). is read " (phi) is true for all ." Typically, in its final application would be replaced with a wff containing a (free) occurrence of the variable , for example . In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of . When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
Ref Expression
Ref Expression

This syntax is primitive. The first axiom using it is ax-5 1268.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator