| Math | IFF | |||
|---|---|---|---|---|
| names | ||||
| a | o.i.a, inner context i, outer context o | |||
| atoms and terms | ||||
| set element | x ∈ X or X(x) | (X x) | ||
| predicate member | x ∈ p or p(x) | (p x) | ||
| relation member | (x, y) ∈ r or r(x, y) | (r x y) | ||
| function application | f(x) | (f x) | ||
| equations | ||||
| σ = τ or =(σ τ) | (= σ τ) | |||
| connectives | ||||
| conjunction | φ ⋀ ψ or ⋀(φ ψ) | (and P Q) | ||
| disjunction | φ ⋁ ψ or ⋁(φ ψ) | (or P Q) | ||
| implication | φ ⇒ ψ or ⇒(φ ψ) | (implies P Q) or (=> P Q) | ||
| equivalence | φ ⇔ ψ or ⇔(φ ψ) | (iff P Q) or (<=> P Q) | ||
| negation | ¬ φ or ¬(φ) | (not P) | ||
| quantifiers | ||||
| universal | ∀x0 ∈ X0, x1 ∈ X1 φ | |||
| or ∀(x0 ∈ X0, x1 ∈ X1) (φ) | (forall ((X0 x0) (X1 x1)) P) | |||
| existential | ∃x0 ∈ X0, x1 ∈ X1 φ | |||
| or ∃(x0 ∈ X0, x1 ∈ X1) (φ) | (exists ((X0 x0) (X1 x1)) P) |
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.