FirstOrder 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):
@ (forall) 
universality 
$ (exists) 
existence 
~ (iff) 
equivalence 
> (implies) 
implication 
 (or) 
disjunction 
& (and) 
conjunction 
 (not) 
negation 
. 
Church's dot 
= 
equality 
!= 
disequality 
true 
verum 
false 
falsum 
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 wellformed formulas:
forall x . Nat(x) > (x = zero  exists y less(y,x))
@ x, y (sym_rel(x,y) iff sym_rel(y,x))
FirstOrder Texts
Firstorder texts accepted by SAD are sequences of dotterminated firstorder formulas.
Note that we use the same character for Church's dot as this is unambiguous for
wellformed 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 onegoal firstorder
sequents are thus valid texts. If you want to prove a sequent
P1, P2, P3 > G write P1. P2. P3. : G.
Oneline comments starting with '#' can be used.
Here is an example of a wellformed firstorder 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. Toplevel sections
are axioms, definitions, and propositions. Any toplevel 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. Lowlevel sections are
proofs, proof blocks and proof cases. Any lowlevel section is a sequence of
assumptions, lowlevel sections, and affirmations, finished by an affirmation.
The grammar of a ForTheLphrase 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 ForTheLaffirmation:
"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.
