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

Syntax Definition wn 3
Description: If  ph is a wff, so is  -.  ph or "not  ph." 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 1392 and wel 1394).
Hypothesis
Ref Expression
wph  wff  ph
Assertion
Ref Expression
wn  wff  -.  ph

This syntax is primitive. The first axiom using it is ax-in1 544.

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