A Grammar for IFF FOL Languages

The EBNF for IFF-FOL languages follows the EBNF for the Simple Common Logic (SCL) standard. The following syntax is written using Extended Backus-Naur Form (EBNF), as specified by International Standard ISO/IEC 14977. Literal characters use quotes '…', sequences of items are separated by commas …,…,…, a vertical bar | indicates alternatives, braces {…} indicate repetition, subtraction – indicates exceptions, brackets […] are used for optional items, and parentheses (…) group items together. Productions are terminated with a semicolon ;.

There are two approaches to the design of an IFF-FOL grammar, the categorical logic (CAT) approach and the assumed KIF approach (KIF). The CAT approach corresponds to the endomorphic or kernel aspect of the IFF-FOL, whereas the KIF approach corresponds to the exomorphic or shell aspect of the IFF-FOL. An indicia is a subset of variables. The CAT approach is oriented towards expression arity, where arity is an indicia; particularly substitution between expression arity fibers. Hence, it requires that all connectives (negations, conjunctions, disjunctions, implications and equivalences) operate on a fixed fiber. This means, for example, that all conjuncts must have the same arity. Because of this inflexibility, when variables are embedded as (elementary) terms, they must have an attached indicia that functions as the arity of the elementary term. The KIF approach is not so strongly oriented towards substitution and expression arity fibers. In fact, arity as indicia is not very explicit in traditional KIF (of course arity as natural number is explicit, but we use the term "valence" for this notion). Hence, KIF is more flexible, in the sense that all connectives are unrestricted on argument arities. The arity of the result is the union of the set of argument arities. Because of this flexibility, variables can be embedded as terms using their singleton as an implicit arity. The present grammar for the IFF-FOL is KIF-oriented. The example below demonstrates the inductive definition of expression arity. An extension grammar for the IFF-FOL will be CAT-oriented.

The syntax is presented here in two parts. The first part called lexical syntax deals with the parsing of character streams into lexical items. The second part called grammatical syntax is the logical syntax of the IFF-FOL kernel, which assumes that lexical items have been recognized by a lexical analyzer.

Lexical Syntax

Parentheses are lexical tokens that denote pairs, tuples, and subsets. They are the only delimiter (grouping device) in the IFF-FOL syntax.

A character is any other ASCII non-control character, which can all be used to form lexical tokens (with some restrictions based on the first character of the lexical token). This includes all the alphanumeric characters listed here in keyboard order, where the alphabetic characters are indicated by ellipses.

A reserved-word consists of the lexical tokens used to indicate the syntactic structure of the IFF-FOL. These must not be used as names in IFF-FOL text.

A name is a lexical token which is not reserved.

A variable, a function symbol or a relation symbol is a name.

Kernel Grammatical Syntax

Terms

For both indicia and tuples, sets are used instead of sequences in the IFF-FOL axiomatics. Natural numbers and sequences have been carefully eliminated from the IFF-FOL for simplicity of the axiomatics. Implicit indicia and maps represent natural numbers and sequences used in surface syntax. An indicia-variable is a pair consisting of an indicia (the arity) and a variable. Indicia-variables represent variables as the simplest terms in the IFF-FOL. The indicia component is used to attach an arity to the variable. The semantics of indicia-variables is Cartesian product projection. In an indicia-variable, the variable is required to be a member of the indicia. Indicia-variables correspond to variable cases in the IFF-FOL axiomatics. The arity of an expression can be used to construct the arity of its included variables.

Tuples can be substituted into function symbols. A function symbol and a tuple are a substitutable pair when the arity of the function symbol is the same as the index of the term tuple. In a function-tuple the function symbol arity must equal the tuple index.

A term is either a variable or a function-tuple. A variable is an elementary term; that is, a term is elementary when it is constructed from a variable. A function-tuple or a term-tuple is a composite term: that is, a term is composite when it is constructed by substitution.

A tuple is a map from an indicia, its index, to the set of terms of a particular arity, its arity. Both terms and atomic expressions use the notion of a tuple of terms, which represents a vector of arguments to a function or relation, respectively. There are operations in the IFF-FOL axiomatics for describing several ways to construct tuples: either as the empty tuple for a particular arity, or as an indexed-term, or as an insertible-pair, or as a tuplable-pair. For any indicia regarded as an arity, there is an empty-tuple with empty index and with arity that indicia. Terms are tuples. An indexed-term is a pair consisting of a variable and a term. There are no constraints between the variable component and the term component. An indexed-term becomes a singleton tuple, whose index is the singleton of the variable component of the indexed-term and whose arity is the arity of the term component of the indexed-term. Terms can be inserted breadth-wise into tuples. An indexed-term and a tuple are an insertible pair when the arity of the term component of the indexed-term is the arity of the tuple. Hence, such a pair is insertible iff the singleton tuple of the indexed-term and the tuple are pairable. Any insertible pair is an insertion tuple defined as the pairing of the singleton tuple of the indexed-term and the tuple. The index of the insertion tuple is the result of inserting the variable component of the indexed-term into the index of the tuple. The arity of the insertion tuple is the common arity. Insertion of an indexed-pair into the empty tuple is the singleton of the indexed-term. A pair of tuples is a tuplable-pair or pairable when they share a common arity. Any tuplable pair defines a pairing tuple, whose index is the disjoint union of indices and whose arity is the common arity. Here we just describe a tuple as a sequence of terms, and use the implicit canonical indicia to represent the underlying map.

Expressions

An equation is used to assert the equality of two terms. The two terms involved must have the same arity.

A relation-tuple consists of two components, a relation symbol and a tuple, where the arity of the relation symbol is equal to the index of the tuple. Relations are embedded as relation-tuples, hence atoms, with identity tuple.

An atom is either an equation or a relation-tuple.

A conjunction is a subset of expressions labeled by the conjunction symbol. The conjunction of any subset of expressions is a conjunctive expression.

 A negation is an expression labeled by the negation symbol. The negation of any expression is a negative expression.

An expression-variable is a pair consisting of an expression and a variable. In an expression-variable, the variable is required to be a member of the arity of the expression. Expression-variables correspond to expression cases in the IFF-FOL axiomatics. Structurally, it would have been better to place the close-paren after the expression, and we did this at first; but we have switched these two items in order to be closer to traditional KIF.

A (existential) quantification is an expression-variable labeled with the (existential) quantification symbol. The (existential) quantification of any expression-variable is a  (existentially) quantified expression.

An expression is either an atom or a conjunction or a negation or an (existential) quantification. Any atom is an atomic expression. The negation of any expression is a negative expression. The conjunction of any subset of expressions is a conjunctive expression. The (existential) quantification of any expression case is a quantified expression. Nothing else is an expression.

Example

The same logical expression can be rendered in a variety of different syntactic external surface forms: connectives can be written as infix, postfix or prefix, groupings indicated by brackets, groups of dots or graphically by enclosing circles, etc. For example, consider the simple logical expression "all boys have been kissed by some girls" taken from the SCL standard. This can be written in the following surface forms. Note that (1) the IFF-FOL core form is almost identical to the SCL core form (they differ in their kernel forms by a quantifier exchange, since they use different quantifiers as primitive), (2) the IFF-FOL kernel form is close to the existential graph form, since they both use the same primitive operations: conjunction (implicit in EGs), negation and existential quantification.

[Traditional logical form:]

(∀x)(Boy(x) → (∃y)(Girl(y) & Kissed(x, y)))

[Conceptual Graph interchange form:]

[@every *x] 
    [If: (Boy ?x) 
         [Then: [*y] 
             (Girl ?y) (Kissed ?x ?y) ]]

[SCL core form:]

(forall (x) 
    (implies (Boy x) 
             (exists (y) 
                 (and (Girl y) (Kissed x y)))))

[SCL kernel form:]

(forall (x) 
    (not (and (Boy x) 
              (forall (y) 
                  (not (and (Girl y) (Kissed x y)))))))

[IFF-FOL core form:]

(forall (x)
    (implies Boy(x)
             (exists (y) 
                 (and Girl(y) Kissed(x y)))))

[IFF-FOL kernel form:]

(not (exists (x)
         (and Boy(x)
              (not (exists (y) 
                       (and Girl(y) Kissed(x y)))))))

[Existential Graph form:]

( Boy[x] 
    ( Girl[y] Kissed[x y] ) )