Syntax

Overview

Gentzen's syntax is defined by the following context-free grammer:

<prop>     ::= <var>|<unary><var>|(<prop>)|<unary>(<prop>)|<prop><binary><prop>
<var>      ::= <alpha>{<alnum>}*
<binary>   ::= <and>|<or>|<imp>
<unary>    ::= <not>
<not>      ::= !
<and>      ::= &&
<or>       ::= ||
<imp>      ::= ->
<alnum>    ::= <alpha>|<digit>
<digit>    ::= 0|1|2|3|4|5|6|7|8|9
<alpha>    ::= <upper>|<lower>
<upper>    ::= A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z
<lower>    ::= a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z

Operators

Gentzen's operators are defined in the following table:

Operator	Character
NOT	!
AND	&&
OR	||
IMPLIES	->

The table is sorted by operator precedence, though parentheses trump all other operators. Thus, !A && B translates to "Not A and B", while !(A && B) reads "Not A and not B".

Variables

Variables begin with a letter, and may be followed by letters or digits.

Examples of valid variable names

a
A1
Apple
apple5
q84ljs

Well-Formed Formulae (Propositions)

From the Internet Encyclopedia of Philosophy:

Definition: A well-formed formula (hereafter abbrevated as wff) of PL is defined recursively as follows:

1. Any statement letter is a well-formed formula.
2. If α is a well-formed formula, then so is '¬α'.
3. If α and β are well-formed formulas, then so is '(α & β)'.
4. If α and β are well-formed formulas, then so is '(α v β)'.
5. If α and β are well-formed formulas, then so is '(α → β)'.
6. If α and β are well-formed formulas, then so is '(α ↔ β)'.
7. Nothing that cannot be constructed by successive steps of (1)-(6) is a well-formed formula.

In other words, a WFF is a statement, a negated statement, a negated WFF, or two WFFs joined by a binary operator.

A note about negation

Because negation is the highest-precedence operator, a WFF must be wrapped in parentheses to be negated. However, a variable does not need to be wrapped in parentheses to be negated. For example:

!A
!(A -> B)