First-Order Formulas

Formulas are built from tokens: variables, function symbols and predicate symbols, with the help of the propositional connectives, quantifiers and parentheses. You can also use Church's dot to group subformulas. We adopt the following notation (in parentheses, alternative names for connectives are shown):

Every token is an arbitrary sequence of latin letters, digits and underscores. Case is significant. Every token that occurs in some term and is not bound by a quantifier is considered as a constant.

Here are examples of well-formed formulas:

forall x . Nat(x) > (x = zero | exists y less(y,x))

@ x, y (sym_rel(x,y) iff sym_rel(y,x))


First-Order Texts

First-order texts accepted by SAD are sequences of dot-terminated first-order formulas. Note that we use the same character for Church's dot as this is unambiguous for well-formed formulas.

Formulas preceded by colon are goals and verifier tries to deduce them from the precedent formulas. If a goal is verified, it becomes an assumption for the following goals. Otherwise, the system stops. If a text ends with a colon, falsum is taken as a final goal. This can be used to search for a refutation of a set of formulas. Note that one-goal first-order sequents are thus valid texts. If you want to prove a sequent  P1, P2, P3 -> G  write  P1. P2. P3. : G. 

One-line comments starting with '#' can be used. Here is an example of a well-formed first-order text:

# Funny lemma from the group theory
forall x,y exists z P(x, y, z).
forall x,y,z,u,v,w . P(x, y, u) & P(y, z, v) & P(u, z, w) > P(x, v, w).
forall x,y,z,u,v,w . P(x, y, u) & P(y, z, v) & P(x, v, w) > P(u, z, w).
forall x . P(x, e, x) & P(e, x, x).
forall x . P(x, i(x), e) & P(i(x), x, e).
forall x P(x, x, e).
:   forall x,y,z . P(x, y, z) > P(y, x, z).
P(a, b, c).   :   P(b, a, c). # having the precedent goal proved
# the last goal is obviously entailed by the last premise


ForTheL texts

A ForTheL text is a sequence of sections, phrases, and special constructs like pattern introductors. Phrases are either assumptions (then they begin with "let" or "assume") or affirmations. Sections may be composed from sections of a lower level and phrases. Top-level sections are axioms, definitions, and propositions. Any top-level section is a sequence of assumptions finished by an affirmation. The affirmation of a proposition or an axiom may be an arbitrary ForTheL statement, whereas the affirmation of a definition must have one of several fixed forms. Low-level sections are proofs, proof blocks and proof cases. Any low-level section is a sequence of assumptions, low-level sections, and affirmations, finished by an affirmation.

The grammar of a ForTheL-phrase imitates the grammar of an English sentence. Phrases are built with nouns which denote notions (classes) or functions, with verbs and adjectives which denote predicates, with prepositions and conjunctions which define the logical meaning of a complex sentence. Here is a simple ForTheL-affirmation: "Every closed subset of every compact set is compact."

To know more about ForTheL, see the Reference Manual (gzipped PS or PDF) and examples of theorems and texts. One of those texts is given below (try this example).

A simple text about empty sets

[set/-s] [element/-s] [belong/-s] [subset/-s]

Signature SetSort. A set is a notion.
Let S,T denote sets.

Signature ElmSort. An element of S is a notion.
Let x belongs to X stand for x is an element of X.

Definition DefSubset. A subset of S is a set T
  such that every element of T belongs to S.

Definition DefEmpty. S is empty iff S has no elements.

Axiom ExEmpty. There exists an empty set.

Proposition.
  S is a subset of every set iff S is empty.
Proof.
  Case S is empty. Obvious.

  Case S is a subset of every set.
    Take an empty set E.
    Let z be an element of S.
    Then z is an element of E.
    We have a contradiction.
  end.
qed.