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 (wellformed 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 1325 and wel 1327). 
Ref  Expression 

wph  wff φ 
Ref  Expression 

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