This document describes a lightweight KIF-oriented grammar for the IFF-FOL. An associated document describes a heavyweight CAT-oriented grammar for the IFF-FOL. The syntax is presented 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.
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 ;. This document was inspired
by the work on the Simple
Common Logic (SCL) standard. The EBNF for the IFF-FOL is very close
to the EBNF for the conventional first order logic aspect
of the SCL.
Parentheses are lexical tokens that denote pairs, tuples, subsets, etc. They are the only delimiter (grouping device) in the IFF-FOL syntax.
| open | = | '(' |
| close | = | ')' |
A character is any other ASCII non-control character, which can all be used to form lexical tokens. This includes all the alphanumeric characters listed here in keyboard order, where the alphabetic characters are indicated by ellipses.
| digit | = | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' ; |
| char | = | digit | '~' | '!' | '#' | '$' | '%' | '^' | '&' | '*' | '_' | '+' | '{' | '}' | '|' | ':' | '"' | '<' | '>' | '?' | '`' | '-' | '=' | '[' | ']' | '\' | ';' | ',' | '.' | '/' | 'A' | … | 'Z' | 'a' | … | 'z' ; |
A reserved-word is a lexical token that represents a logical symbol in the IFF-FOL and is used to indicate the syntactic structure of expressions in the IFF-FOL languages. These must not be used as names.
| reserved-word | = | '=' | 'and' | 'or' | 'not' | 'implies' | 'iff' | 'exists' | 'forall' | 'iff:theory' |
A name is a lexical token which is not reserved.
| character-sequence | = | ( char , { char } ) |
| name | = | character-sequence – reserved-word |
Non-logical symbols in the IFF-FOL
include constants, variables, function symbols and relation symbols. An
individual constant
represents a specific individual and corresponds
to a proper noun in natural languages. A variable represents a
specific, but unspecified (or arbitrary) individual and corresponds to
a pronoun in natural languages. A function
symbol represents an operation or map, which has an input and an
output. The input is provided by a list of n arguments, where n is called the valence of the function (the term arity is used for a difference, but
related, notion in the IFF-FOL). A relation
or predicate symbol represents a class of individuals or a relationship
among individuals and corresponds
to a common noun in natural languages. For each natural number n, we introduce a set of n-place relation symbols (relation
symbols of valence n).
Zero-place or nullary relation symbols are called "sentence symbols".
They correspond to independent sentences whose internal structure does
not matter. One-place or unary relation symbols correspond to
linguistic items denoting properties, like "being human", "being loud",
or "being a prime number". Two-place or binary relation symbols
correspond to linguistic items denoting binary relations, such as "is a
child of" or "is less than". Three-place or ternary relation symbols
are less common directly. Examples include "x lies between y and z", etc. However, the IFF-FOL
regards expressions as complex relation symbols, and the valence of
expressions can be arbitrarily large. The two-place or binary equality
or identity relation "=" is
treated specially in the IFF-FOL – as a logical symbol. For simplicity,
in some logical
languages used for general discourse the only terms are constants and
variables corresponding to proper nouns and pronouns. However, the
logic languages used for a more mathematical discourse require the use
of function symbols. These allow use of complex terms such as the
constant terms "the wife of John Kerry" and "8+3",
or terms containing variables, such as "((x×2)−y)"
or "the brother of x".
Function symbols in logical languages allow greater expressiveness,
but increase formal complexity. The IFF-FOL languages include
function symbols, and constants are regarded in the IFF-FOL as function
symbols of
valence 0.
A variable, a function symbol or a relation symbol is a name.
| variable | = | name |
| function | = | name |
| relation | = | name |
The IFF-FOL Core is the syntactic form of the IFF-FOL that is
closest to standard logical form. The central difference between the
core syntax of the light (here) and heavy IFF-FOL grammars is in the
presentation of IFF-FOL terms.
A term is a linguistic item that denotes an individual thing. Terms are constructed out of two basic constituents: variables and function symbols. A variable can be embedded as an elementary term.
| elementary-term | = | variable ; |
Function symbols can be applied to tuples to form composite terms. This is an elementary form of substitution. A function symbol can be applied to tuple of terms, and a composite term formed, when the valence of the function symbol is the same as the length of the tuple.
| composite-term | = | function , tuple ; |
A term is either an elementary term or a composite term, but nothing else.
| term | = | elementary-term | composite-term ; |
A tuple is a list of terms. Tuples are used in terms and atomic expressions, representing a list of arguments to a function or relation, respectively.
| tuple | = | open , { term } , close ; |
An expression or formula is a linguistic item that represents a logical proposition and corresponds to a declarative sentence in natural language. An equation or equational expression is used to assert the equality of two terms.
| equation | = | open , '=' , term , term , close ; |
An atom or atomic expression asserts that a relation holds for a tuple of terms. Hence, an atom consists of two components, a relation symbol and a tuple, where the valence of the relation symbol is equal to the length of the tuple.
| atom | = | 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 disjunction is a subset of expressions labeled by the disjunction symbol. The disjunction of any subset of expressions is a disjunctive expression.
| expression-subset | = | { expression } ; |
| conjunction-disjunction | = | open , ( 'and' | 'or' ) , expression-subset , close ; |
A negation is an expression labeled by the negation symbol. The negation of any expression is a negative expression.
| negation | = | open , 'not' , expression , close ; |
An implication is a pair of expressions labeled by the implication symbol. The implication of any pair of expressions is an implicative expression. An equivalence is a pair of expressions labeled by the equivalence symbol. The equivalence of any pair of expressions is an equivalence expression.
| expression-pair | = | expression , expression ; |
| implication-equivalence | = | open , ( 'implies' | 'iff' ) , expression-pair , close ; |
A (existential) quantification or an (existentially) quantified expression is an expression-variable pair labeled with the (existential) quantification symbol. A (universal) quantification or an (universally) quantified expression is an expression-variable pair labeled with the (universal) quantification symbol.
| expression-variable | = | open , variable , close , expression ; |
| quantification | = | open , ( 'exists' | 'forall' ) , expression-variable , close ; |
An expression is either an equation, an atom, a conjunction, a disjunction, a negation, an implication, an equivalence, an (existential) quantification, or a (universal) quantification, but nothing else.
| expression | = | equation | atom | conjunction-disjunction | negation | implication-equivalence | quantification ; |
An IFF
theory is a named subset of expressions.
| theory | = | open , 'iff:theory' , name , expression-subset , close ; |
For several reasons it is desirable to present a distinguish subset of the IFF-FOL core syntax, called the IFF-FOL kernel syntax, which is minimal and just sufficient to define the meanings of all the other logical constructions in the IFF-FOL core. Terms, term tuples, equations and atoms in the kernel syntax are handled in the same fashion as in the core syntax. The kernel syntax has only two connectives, conjunction and negation, and only one quantifier. For flexibility, the choice of quantifier could be left unspecified. In the simple common logic version of the IFF-FOL kernel syntax, the universal quantifier could be chosen. In the existential graphs version of the IFF-FOL kernel syntax, the existential quantifier could be chosen. We present the latter case here. The IFF-FOL semantics can be defined in terms of the IFF kernel syntax. The meanings of the additional core constructions can be defined by a systematic translation to the kernel.
| elementary-term | = | variable ; |
| composite-term | = | function , tuple ; |
| term | = | elementary-term | composite-term ; |
| tuple | = | open , { term } , close ; |
| equation | = | open , '=' , term , term , close ; |
| atom | = | relation , tuple ; |
| expression-subset | = | { expression } ; |
| conjunction | = | open , 'and' , expression-subset , close ; |
| negation | = | open , 'not' , expression , close ; |
| expression-variable | = | open , variable , close , expression ; |
| quantification | = | open , 'exists' , expression-variable , close ; |
| expression | = | equation | atom | conjunction | negation | quantification ; |
The IFF-FOL semantics can be defined in terms of the IFF kernel syntax. The meanings of the additional IFF-FOL core constructions can be defined by a standard translation to the IFF-FOL kernel syntax.
T
: IFF-FOL Core
→ IFF-FOL Kernel
This translation is indicated by the following table.
|
Construction |
Core |
Kernel |
| disjuntion | '(' 'or' ε1 … εn ')' | '(' 'not' '(' 'and' '(' 'not' T[ε1] ')' … '(' 'not' T[εn] ')' ')' ')' |
| implication | '(' 'implies' ε1 ε2 ')' | '(' 'not' '(' 'and' T[ε1] '(' 'not' T[ε2] ')' ')' ')' |
| equivalence | '(' 'iff' ε1 ε2 ')' | '(' 'and' T['(' 'implies' ε1 ε2) ] T[ '(' 'implies' ε2 ε1 ')' ] ')' |
| universal-quantification | '(' 'forall' '(' x ) ε ')' | '(' 'not' T[ '(' 'exists' '(' x ) '(' 'not' T[ε] ')' ')' ] ')' |
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. The IFF-FOL core form is almost identical to the SCL core form, and the IFF kernel form differs from the SCL kernel form by a quantifier exchange, since they use different quantifiers as primitive. 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) ]]
(forall (x)
(implies (Boy x)
(exists (y)
(and (Girl y) (Kissed x y)))))
(forall (x)
(not (and (Boy x)
(forall (y)
(not (and (Girl y) (Kissed x y)))))))
(forall (x)
(implies Boy(x)
(exists (y)
(and Girl(y) Kissed(x y)))))
(not (exists (x)
(and Boy(x)
(not (exists (y)
(and Girl(y) Kissed(x y)))))))
( Boy[x]
( Girl[y] Kissed[x y] ) )
Arity is one of the notions that separates the lightweght version of the IFF-FOL grammar from the heavyweight version. The arity of any basic linguistic element (function symbol, relation symbol, term or tuple) is the indicia (variable subset) of n free variables that serve as the locations or indices for the arguments of that element, where n is its valence. Can arity be defined and constructed in the lightweight version of the IFF-FOL grammar? The answer is yes! To demonstrate, let us analyze and construct the arity for the IFF-FOL kernel form of the above example expression. The arity of a variable, embedded as a term, is its singleton. The arity of a tuple of terms is the union of the term arities. The arity of an atom is the arity of the tuple component. The arity of a conjunction is the union of the arities of the conjunct expressions. The arity of a negation is the arity of the expression being negated. A quantification subtracts the quantified variable from the arity of the expression being quantified. Here is the arity construction.
| Tuple
or Expression |
Arity |
|
| (y) |
{y} |
|
| Girl(y) |
{y} |
|
| (x
y) |
{x,
y} |
|
| Kissed(x
y) |
{x,
y} |
|
| (and
Girl(y) Kissed(x y)) |
{x,
y} |
|
| (exists
(y) (and Girl(y) Kissed(x y))) |
{x} |
|
| (not
(exists (y) (and Girl(y) Kissed(x y)))) |
{x} |
|
| (x) |
{x} | |
| Boy(x) |
{x} |
|
| (and Boy(x) (not
(exists (y) (and Girl(y) Kissed(x y))))) |
{x} |
|
| (exists (x) (and
Boy(x) (not (exists (y) (and Girl(y) Kissed(x y)))))) |
{} |
|
| (not
(exists (x) (and Boy(x) (not (exists (y) (and Girl(y) Kissed(x y))))))) |
{} |
The SUO-IFF documents contain many unicode characters, and so require a recent browser. But even some recent browsers fail to render SUO-IFF properly. You can test your browser here.