Formation Rules for System IV ['Gentzen']

Formation Rules for System IV

10/8/09 Under construction

Terms, constants, variables, propositions, and predicates


<constant> ::= (['0'-'9']) |'∅'| 'U'|'{ }'
<subscript> ::=  ['₁'-'₉']
<functor> ::=  ['a'-'v'](< subscript >)*
<variable> ::=  ['w'-'z'](< subscript >)*
<term> ::=

<functor>((<term>)+ (,<term>)*)+|
{((<term>)+ (,<term>)*)+}|
℘ (<term>)|

For example, 5, ∅, a, w, b₁₂, z₁₂₁₂, f(abc), f(a,b,c), {a,b,c},  (5),  ℘(x), 5''' , 1+2, 2-3, x.2, a∪b, x∩y, <a,b>,  {x:Px}, {x|Px&Qy}   are all terms.

(Atomic) constants

<atomicConstant> ::= <constant>|<functor>

That is 'a' through 'v' , possibly with subscripts, and the numerals and some set theory constants.


 'w' through 'z' , possibly with subscripts.



 'a' through 'v' , possibly with subscripts.


Propositions and Predicates

<predicator> ::= ['A'-'Z'](< subscript >)*
<proposition> ::=

<predicator>(< term >)*|


The predicate letters are upper case A-Z, possibly with subscripts. Then propositions are these followed by zero or more terms, for example, P, Q₁₂f(abc), or X12 . There is also 'top' ⊤ and 'bottom' ⊥ which are pre-defined propositions for true and false.

Well Formed Formulas (WFFs) 

<wff> ::=

<term1> = <term2>|
<term1> < <term2>|
<term1> > <term2>|
<term1> ε <term2>|
<wff1> ∧<wff2>|
<wff1> ∨<wff2>|
<wff1> ⊃ <wff2>
<wff1> ≡<wff2>|
(∀<variable>) <wff>|
∀<variable> <wff>|
(∃<variable>) <wff>|
(∃<variable>!) <wff>|
|∀<variable>:<type>) <wff>|
(∃<variable>:<type>) <wff>|
Κ<term> <wff>| 
Ρ<term> <wff>| 

For example, P, Pa, Qbv, (∀x)Hxy are all well-formed formulas and so too are a=b and (∃x)(x=d).

Brackets are used to clarify or disambiguate expressions.