A language for first order logic

The language has been described informally above but here is a formal grammar for it.

%start statement

%%

statement      : expression
               ;

expression     : atomic_expression
               | ( expression binop expression )
               | [ expression binop expression ]
               | { expression binop expression }
               | ( ¬ expression )
               | [ ¬ expression ]
               | { ¬ expression }
               | ( quantifier variable . expression )
               | [ quantifier variable . expression ]
               | { quantifier variable . expression }
               ;

atomic_expression : ( atom )
                  | [ atom ]
                  | { atom }
                  ;

atom           : predicate
               | atom variable
               | atom paramater
               ;

binop          : ∧ | ∨ | ⊃ | ⊼ | ⊻ | ≡ | ≢ | ⊂
               ;

quantifier     : ∀ | ∃
               ;

predicate      : pred_letter
               | predicate !
               ;

pred_letter    : f | g | h | i | j
               ;

parameter      : param_letter
               | parameter !
               ;

param_letter   : a | b | c | d | e
               ;

variable       : var_letter
               | variable !
               ;

var_letter     : v | w | x | y | z
               ;

As in the zeroeth order calculus, exclamation points can be used to generate an infinite number of predicates, variables and parameters, but we will never actually need them in examples.

As with zeroeth order logic it’s useful to have symbols which don’t belong to the language but which are used for talking about the language. We’ll continue to use \({ P }\), \({ Q }\), etc. to represent expresions but we’ll add \({ A }\), \({ B }\), etc. for parameters, \({ F }\), \({ G }\), etc. for predicates, and \({ V }\), \({ W }\), etc. for variables. The same convention about different types of brackets being interchangeable applies.