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."

The grammar can be extended with the special top-level constructs called pattern introductors. Here is a pattern introductor for an unary notion: "[an element/elements of x]". If a word used in a pattern has several possible forms, you can list them all with slashes. One can introduce a new pattern as an alias of some expression of the same kind, using an introductor of the form "[pattern @ meaning]". The only predefined pattern is a predicate pattern "[x is equal to y]".

Another special constructs are instructions for the verifier: "[full]", "[none]", and "[quit]". They set the verification mode for the following ForTheL-text. The starting mode is "full". That means that every proposition and stand-alone affirmation in the text must be checked to be provable from the precedent text.

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

[a set/sets] [an element/elements of x]
[x is in/from y @ x is an element of y]
[x belongs/belong to y @ x is in y]
[a subset/subsets of x] [x is empty]

Definition DefSubset. Let S be a set.
  A subset of S is a set with no elements not in S.

Definition DefEmpty. Let S be a set.
  S is empty iff S has no elements.

Axiom ExEmpty. There exists an empty set.

Proposition. Let S be a set.
  S is a subset of every set iff S is empty.
Proof.
  First assume S is a subset of every set.
    Then S is empty.
    Indeed
      Let z be in S and E be an empty set.
      Then z is an element of E.
      We have a contradiction.
    end.
  end.
  Now assume S is empty.
    Let T be a set.
    Every element of S is in T (by DefEmpty).
    Hence S is a subset of T (by DefSubset).
  end.
qed.