Logic

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.
[τ₀ ... τ_n]
Equational formulas are constructed with the usual equality symbol = “between” pairs of terms.
(= τ₀ τ₁)
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 τ₀ ... τ_n)
(or τ₀ ... τ_n)
(not φ)
(implies τ₀ τ₁) or (=> τ₀ τ₁)
(iff τ₀ τ₁) or (<=> τ₀ τ₁)
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) φ₀ ... φ_n) φ)
(forall ((A1 ?x1) ... (Am ?xm)) (implies (and φ₀ ... φ_n) φ)),
and the following existentially quantified expressions are equivalent
(exists ((A1 ?x1) ... (Am ?xm) φ₁ ... φ_n) φ)
(exists ((A1 ?x1) ... (Am ?xm)) (and φ₁ ... φ_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.