Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > wn | GIF version |
Description: If φ is a wff, so is ¬ φ or "not φ." Part of the recursive definition of a wff (well-formed formula). Traditionally, Greek letters are used to represent wffs, and we follow this convention. In propositional calculus, we define only wffs built up from other wffs, i.e. there is no starting or "atomic" wff. Later, in predicate calculus, we will extend the basic wff definition by including atomic wffs (weq 1389 and wel 1391). |
Ref | Expression |
---|---|
wph | wff φ |
Ref | Expression |
---|---|
wn | wff ¬ φ |
Colors of variables: wff set class |
Copyright terms: Public domain | W3C validator |