If I were to build a first order logic parser could I do it using a context free parser generator (like bison)?

I found some articles where First Order Logic Syntax is described with EBNF notation, usually like this:

<Formula> := <PrimitiveFormula> |
             (¬<Formula>) |
             (<Formula> <Connective> <Formula>) |
             <Quantifier> <Variable> <Formula>

<PrimitiveFormula> := <Predicate>(<Term>,...,<Term>)

<Term> := <Constant> |

<Connective> := -> | ∧ | ∨ | <->

<Quantifier> := ∀ | ∃

<Constant> := c0 | c1 | ... 

<Variable> := x0 | x1 | ...

But it seems that this grammar is blind to the fact that the number of arguments that predicates take must match their arity.

Moreover if we would consider only closed formulas to be well formed, could some BNF-based grammar cope with variable scoping/binding?

  • $\begingroup$ If you have a finite number of predicate symbols, then you can always make a specific rule for each of them $\endgroup$ – Maxime Ramzi Jan 22 '18 at 17:52

You are right that as usually presented, the grammar of first-order formulas assumes that each predicate symbol "knows" its own arity and requires the number of actual arguments to the predicate to match that. This cannot be expressed purely with a finite context-free grammar.

But it is even worse than that, because the standard assumption is also that we have an infinity of predicate symbols of each arity (as well as an infinity of variable letters and constant symbols). So even your

<Constant> ::= c0 | c1 | ...

is problematic for the completely formal presentation of context-free grammars you see in formal language theory texts. The underlying alphabet is supposed to be finite!

There are several ways to react to that:

The computer-sciency way: Just don't care. There are an infinity of symbols of each kind, the lexer can distinguish them somehow, and we're free to put additional restrictions on top of the syntax as part of our parser actions.

The Turing-machine way: Insist that the alphabet must be finite. Predicate symbols cannot be single symbols; in order to say something like "the fifth predicate symbol with four argument" we need to write something like p'''''[iiii] which the grammar must match one character at a time. In that case we can make a context-free grammar that matches the iiii subscript with arguments:

<PrimitiveFormula> ::= p <Primes> [ <PrimitiveMiddle> )
<PrimitiveMiddle> ::= i ] ( <Term>
                   |  i <PrimitiveMiddle> , <Term>
<Primes> ::= <empty>
          |  <Primes> '

This is not particularly exciting, though, and works only "by accident" because there's only one count we have to match (and I presciently decided to express the arity in unary notation).

The minimalist way: Still don't care. For each predicate symbol $p$ the grammar will accept both $p(t_1,t_2)$ and $p(t_1,t_2,t_3)$ -- but we shrug and simply decide that these are semantically two different predicates! Our proof system will happily work with that convention, and when the time comes to define structures we just have to say that the meaning of $p$ is a subset of all finite sequences of the universe, rather than a set of (say) ordered tuples from the universe.

The parochial way: Declare that you need to fix a particular logical language before you start writing down grammars. The language will give you a finite number of predicates; let each of them be a symbol of its own and write a grammar production for each of them.

It is not common to insist that only closed formulas are well-formed. Indeed, almost every text you come across will define "well-formed formula" as something that can contain free variables. So matching up variable instances to variable binders is not usually viewed as the job of the grammar.

  • 1
    $\begingroup$ I agree with you when you say that almost every text in logic defines "well-formed formula" as something that can contain free variables. But I don't agree when you say that "matching up variable instances to variable binders is not usually viewed as the job of the grammar", if you intend that it is a matter of semantics and not of syntax. Especially in proof theory, it is crucial to identify formulas up to renaming of bind variables: it is implicit in every inference rule concerning quantifiers (think of natural deduction or sequent calculus). $\endgroup$ – Taroccoesbrocco Jan 23 '18 at 10:23
  • 1
    $\begingroup$ @Taroccoesbrocco: I agree with you that such things belong on the "syntax" side of the syntax/semantics boundary. But not all syntactical properties are necessarily captured by a grammar (in the formal-languages sense of "grammar"), and resolving variable bindings is one of those. $\endgroup$ – hmakholm left over Monica Jan 23 '18 at 12:40
  • 1
    $\begingroup$ (In practical computer-science jargon there is a tradition of calling this kind of not-in-the-grammar rules "static semantics", but that's not the terminology that's usually used in logic). $\endgroup$ – hmakholm left over Monica Jan 23 '18 at 13:09
  • 1
    $\begingroup$ I hope someone is still reading this thread! I am a set theorist, mainly teaching CS. It occurs to me to wonder whether or not the set of wffs of the language of set theory (just $\in$ and =) is context-free. I seem to remember that it is, tho' i don't remember seeing a proof anywhere. My follow-up question is: is the set of stratifiable wffs CF (stratifiable is as in Quine/NF)? I am not suff fluent with pumping lemmas for CF languages to be able to write out the proof (whose existence i suspect) that it isn't. It could make a nice exercise for my CS students. Anyone tho'rt about this? $\endgroup$ – Thomas Forster Mar 30 '20 at 1:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.