Logic, from the Greek word λογος, studies the structure of statements and arguments in both formal systems and natural language. The logic metalanguage of the metashell is a simple lisp-like syntactic framework that allows logical expression via a set of logical symbols.
- The logic metalanguage uses parentheses for general delimiters.
( ... )
- Tuples of terms are formed by using a tuple notation (special delimiters) inherited from KIF.
[τ0 ... τn]
- Equational formulas are constructed with the usual equality symbol = “between” pairs of terms.
(= τ0 τ1)
- For propositional expression, the logical symbols contain the connectives for conjunction &, disjunction |, negation ¬, implication ⇒ and equivalence ≡. These operate on formulas (called here expressions). There are special abbreviations for implication and equivalence.
(and τ0 ... τn)
(or τ0 ... τn)
(implies τ0 τ1) or (=> τ0 τ1)
(iff τ0 τ1) or (<=> τ0 τ1)
- For predicative expression, the logical symbols contain the two quantification symbols ∀ and ∃. The standard notation is restricted quantification (thus enforcing restricted or limited comprehension): all quantified variables should be sorted (restricted to particular sets).
(forall ((A ?x) (B ?y)) ...)
(exists ((A ?x) (B ?y) (C ?z)) ...)
- For convenience of expression, the logic metalanguage allows for guard exspressions at the end of the list of bound variables. The following universally quantified expressions are equivalent
(forall ((A1 ?x1) ... (Am ?xm) φ0 ... φn) φ)
(forall ((A1 ?x1) ... (Am ?xm)) (implies (and φ0 ... φn) φ)),and the following existentially quantified expressions are equivalent
(exists ((A1 ?x1) ... (Am ?xm) φ1 ... φn) φ)
(exists ((A1 ?x1) ... (Am ?xm)) (and φ1 ... φn φ)).
The logic metalanguage is closely related to the grammer, which specifies the correct form for IFF expressions.
Some IFF documents such as this one contain a lot of unicode characters, and so require a recent browser. But even some recent browsers fail to render it properly. Two browsers that do render these documents correctly are Firefox and Opera.