Syntax of formulas
Grammar
<phi>,
<psi>... ::= bottom | <atomphi> | (<phi> and
<psi>) | (<phi> or <psi>) | (not <phi>) |
(<phi> imply <psi>) | (<phi> equiv <psi>) |
(forall <var> <phi>) | (exists <var> <phi>)
<atomphi> ::= <proposition> | (<predicate> <term> <term> <term> .....)
<term> ::= <constant> | <var> | (<function> <term> <term> <term>....)
<proposition> ::= p, q, etc. (any symbol)
<predicate> ::= p, q etc. (any symbol)
<function> ::= f, g, etc. (any symbol)
<var> ::= x, y, etc. (any symbol)
<constant> ::= s, t, etc. (any symbol)
Example
(p x)
(p x y)
((p x) and (forall x (q x (f x))))