Formation Rules for System IV ['Gentzen']

Formation Rules for System IV

10/8/09 Under construction

Terms, constants, variables, propositions, and predicates

Terms

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

<constant>|
<functor>|
<variable>|
<functor>((<term>)+)|
<functor>((<term>)+ (,<term>)*)+|
{((<term>)+ (,<term>)*)+}|
(<term>)|
℘ (<term>)|
<term>(''')+|
<term>+<term>|
<term>-<term>|
<term>.<term>|
<term>∪<term>|
<term>∩<term>|
<<term>,<term>>|
{<variable>:<wff>}
{<variable>|<wff>}

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.

Variables

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

Types

 '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> ::=

<proposition>|
<term1> = <term2>|
<term1> < <term2>|
<term1> > <term2>|
<term1> ε <term2>|
(<wff>)|
∼<wff>|
<wff1> ∧<wff2>|
<wff1> ∨<wff2>|
<wff1> ⊃ <wff2>
<wff1> ≡<wff2>|
(∀<variable>) <wff>|
∀<variable> <wff>|
(∃<variable>) <wff>|
(∃<variable>!) <wff>|
|∀<variable>:<type>) <wff>|
(∃<variable>:<type>) <wff>|
□<wff>| 
◊<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.