Summary Human-oriented Theorem Proving
           (c) 2004-04-24 Fabian M. Suchanek

This is a summary of the first part of the course "Human-oriented
Theorem-Proving" held by Dr. Claus-Peter Wirth in the WS 2003 at
Saarland University. Its topics are:
 * Sets                  * Proofs                * Sequent calculus
 * Tuples                * First-Order-Logic     * Disjunctive sequents
 * Relations             * Improved Logic        * Tableau calculus
 * Functions             * Semantics             * ND calculus
 * Decidability          * Q0                    * Variables
 * Languages             * Equality              * Matrix calculus
 * Logic                 * Modal Logic           * Induction
Furthermore, the summary contains a rough and not well-founded
overview over the second part of the lecture, held by Dr. Armin
Fiedler, Dr. Christoph Benzmueller and Andreas Meier. This includes
the programs Omega and Prex.

I would like to thank Magdalena Wolska, Mark Buckley, and Marc
Wagner for helping me eliminate many of the question-marks in this
summary. Furthermore, Dr. Claus-Peter Wirth deserves my thanks for
scanning this summary rigorously, removing numerous errors.

By reading the following text, you accept that the author does not
accept any responsibility for the correctness or completeness of
this text. If you have any corrections or remarks (especially
concerning the statements marked with a "(?)"), please send me a mail. 
This is the only way to make the publication of this summary useful 
for me, too.

My e-mail address is f.m.suchanek@zweb.de, but the letter 'z' has to 
be removed from the address.



~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Sets
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Set: An unordered collection of different elements.
 S = {s1,...sn}
 S = { a | p(x) } is the set of all those x for which p(x) holds

Extensional set: A set given by an enumeration of all its elements.

Intensional set: A set given by a property of all its elements.

Size, cardinality of a set: The number of its elements.
 Notation: |{s1,s2,...sn}| = n

Finite set: A set with a finite size.

Intersection of two sets: The set of those elements which occur in
 both of them.
 Notation: X /\ Y

Union of two sets: The set of all of their elements.
 Notation: X \/ Y

Difference of two sets: The set of those elements which occur in the
 first one, but not in the second one.
 Notation: X \ Y

Disjoint sets: Sets, the intersection of which is empty.

Union of disjoint sets: The union of these sets with the knowledge that
 the sets are disjoint.
 Notation: A \+/ B

Subset of a set S: A set, the elements of which are all contained in S.
 Notation: S' =< S

Strict subset of a set S: A subset different from S.
 Notation: S' < S

Superset of a set S: A set, which contains all elements of S.
 Notation: S' >= S

Strict super-set of a set S: A super-set different from S.
 Notation: S' > S

Partition of a set S: A set of subsets of S, such that each element of
 S is contained in exactly one of the subsets.

Powerset of a set S: The set of all subsets of S.
 Notation: P(S)

Urelement: An object, which is not a set.

Class: A set or a proper class.
 Roughly speaking, a class is
 * either an ordinary set or
 * a proper class, i.e. a collection of sets, that is somehow too
   large to be a set.
 // This definition is indirectly recursive together with the
 // definition of "proper class".
 // <CP>

Superclass of a class C: A class, which contains all elements of C.

Proper class: A class, which does not have a superclass.
 A proper class is a collection of sets, which is too large to be a
 set.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Tuples
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Sequence, Tuple: An ordered collection of elements.
 Notation: t=(t[1],t[2],...t[n])
 Example: t=(1,'A',abc) is a tupel

Index of an element t in a tuple T: The number of elements preceding t
 in T.

Length, Dimension of a tupel: The number of its elements.

Pair: A tupel of dimension 2.

Reflexive pair: A pair, the first and the second element of which are
 equal.

Algorithm: A sequence of instructions.
 // For a detailed understanding, see "Theoretische Informatik"
 // (infod.txt, in German)

Termination of an algorithm: The phenomenon that the algorithm stops.

Cartesian Product of sets A[1],A[2],...A[n]: The set of all
 possible tuples, the first element of which is in A[1], the second
 element of which is in A[2] etc.
 Notation: A x B x C = D
 Example: {1,2} x {a,b,c} = { (1,a), (2,a), (1,b), (2,b), (1,c), (2,c)}


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Relations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Relation over the classes A[1],...A[n]: A subset of the cartesian
 product of A[1],...A[n].

Projection of a relation R to components i[0],...i[m]: The relation
 proj[i[0],...i[m]](R) := { (x[i[0]],...x[i[m]]) |
      Ex x[0],...x[i[0]-1],x[i[0]+1],...x[i[1]-1],x[i[1]+1],... :
      (x[0],...x[n]) in R }
 That is: The set of all tuples of R, where only the elements indicated
 by the indices are kept. The components are usually counted 1-based.

Binary relation: A relation over two classes.
 Notation for a relation R < A x B:
 *  (a,b) is an element of the relation R
 *  r(a,b)
 *  a r b
 *  (a,b) is in r
 Example: The relation ">" is the set of all pairs of real numbers,
  in which the first number is greater than the second.
  It holds: ">" = { (1,0), (27.3,12.5), (17,-12), ... }
  One writes: >(3,2)  or  3 > 2  or  (3,2) is in ">".

Going in a relation R < A x B: Taking an element a of A and finding a
 b with R(a,b). Thus, R determines from which elements one can go to
 which other elements. The relation can be interpreted as a set of
 one-way-streets. Another interpretation is a graph, in which the
 elements of A and B are the nodes and R constitutes the links.

Reverse of a relation R < A x B: The set of all those (b,a), for
 which R(a,b).
 Notation: R^-1 := {(b,a) | R(a,b)}
           R^-1 =< B x A

Domain of a relation R < A x B: The projection of R to its first
 component.
 Notation: dom(R) := proj[1](R) = {a | Ex (a,b) in R}

Domain-Restriction, restriction of a relation R < A x B to a set A':
 The relation of all pairs of R, the first element of which is in A'.
 Notation: |R with A' as an index to the left, here:
           domrestr(R,A') := R \ ((A\A') x B)
                           = {(a,b) | (a,b) in R, a in A'}
                           = R /\ (A' x B)

Range of a relation R < A x B: The projection of the relation to its
 second component.
 Notation: ran(R) := proj[2](R) = {b | Ex (a,b) in R}

Range-restriction of a relation R < A x B to a set B': The relation of
 all pairs of R, the second element of which is in B'.
 Notation: R| with B' as an index to the right, here:
           ranrestr(R,B') := R \ (A x (B\B'))
                           = {(a,b) | (a,b) in R, b in B'}
                           = R /\ (A x B')

Image of a set A' under a relation R < A x B: The set of all second
 elements of all pairs of R, where the first element is in A'.
 Notation: <A'>R := ran(domrestr(R,A'))
                  = {b | Ex (a,b) in R, a in A'}
                  = proj[2](R /\ (A' x B))

Reverse-Image of a set B' under a relation R < A x B: The set of all
 first elements of all pairs of R, where the second element is in B'.
 Notation: R<B'> := dom(ranrestr(R,B'))
                  = {a | Ex (a,b) in R, b in B'}
                  = proj[1](R /\ (A x B'))

Composition of two relations R1 < A x B and R2 < B x C: The relation
    R1 o R2 := {(a,c) | Ex b : (R1(a,b) and R2(b,c)) }
 If one interprets a relation as a set of one-way-streets, the
 relation R1 o R2 corresponds to a shortcut from the domain of R1 via
 some hidden element to the range of R2.

Relation on a set A: A relation R < A x A.

Relation R on A to a power of n:
 If n=0, then the restriction of the identity to A;
         R^0 := domrestr(id,A)
              = id /\ (A x A)
              = {(a,a) | a in A}
 If n=1, then R
         R^1 := R
 If n>1, then R to the power of n-1, composed with R
         R^n := R^(n-1) o R
 The relation R^n corresponds to a way of n steps from one element
 of A to another.

Transitive closure of a relation R on A: The union of all its
 powers. That is: It contains all pairs of elements of A, which can
 be reached by multiple steps within R.
 Notation: R+ := \/ { R^n | n=1,...INF }

Reflexive and Transitive Closure of a relation R on A: The
 transitive closure of R united with all reflexive pairs.
 Notation: R* := \/ { R^n | n=0,... INF }

Reflexive relation: A relation on a set A, which contains all reflexive
 pairs of A.

Strict, Irreflexive relation: A binary relation, which does not
 include any reflexive pair. That is:  id /\ R = {}

Symmetric relation: A binary relation R, which for every (a,b) in R
 also contains (b,a).

Anti-symmetric relation: A binary relation, which contains both
 (a,b) and (b,a) only in case of b=a.

Asymmetric relation: A binary relation, which does not contain both
 (a,b) and (b,a).

Transitive relation: A relation on a set A, which for every (a,b) and
 (b,c) it contains, also contains (a,c).

Terminating relation: A relation R on a set X, in which one cannot go
 forever. If X is finite, then this boils down to: Its transitive
 closure does not contain any reflexive pair.

Locally confluent relation: A relation R on a set X, such that
   All a (Ex b1,b2 (R(a,b1) /\ R(a,b2)))
          => Ex c (R*(b1,c) /\ R*(b2,c))
 That is: If one can go from one starting element a directly to two
 distict successor elements b1 and b2, then the distinct ways will
 somewhen lead to the same element c again.

Confluent relation: A relation R on a set X, such that
   All a (Ex b1,b2 (R*(a,b1) /\ R*(a,b2)))
           => Ex c (R*(b1,c) /\ R*(b2,c))
 That is: If one can go from one starting element a to distict
 successor elements b1 and b2 in any way, then the distinct ways will
 somewhen lead to the same element c again.
 // <CP>

Serial relation: A relation R on a set X, such that for every x in X,
 there is a x' with R(x,x').

Triangular relation: A relation R on a set X, such that if R(a,b) and
 R(a,c), then also R(b,c).

Equivalence relation: A reflexive, symmetric and transitive relation.
 Example: '='

Quasi-ordering: A transitive and reflexive relation.

Reflexive ordering, partial ordering: An anti-symmetric quasi-ordering.
 That is: A reflexive, anti-symmetric and transitive relation.
 Example: '=<'

Irreflexive ordering, strict partial ordering: An irreflexive and
 transitive relation.

Element smaller than x in an ordering R: An element y, for which R(y,x).

Cycle in a relation R < A x A: A sequence x[1],...x[n] of elements of
 A, such that R(x[1],x[2]), R(x[2],x[3]),... R(x[n],x[1]).

Cyclic relation: A relation containing a cycle. As a result, the
 transitive closure contains a reflexive pair.

Minimal element of a set A' in a relation R on A: An element b of
 A', such that there is no element a in A' with R(a,b). A' must be
 a subset of A.

Well-founded relation on a set A': A relation R on a set A, such that
 every non-empty set A'<A has a minimal element. If A is finite, this
 boils down to the fact that R may not contain a cycle.

S-Reflexive relation: A binary relation R, which contains all reflexive
 pairs of S. That is:
              domrestr(id,S) =< R
              {(s,s)|s in S} =< R
              R(s,s) for all s in S

Wellfoundedness-Lemma: (?)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Functions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Right-unique relation, Function: A relation f over two sets A and B,
 such that for every a in A there is either none or exactly one element
 b in B with a f b.
 Notation for f: f:A->B
 Notation for "a f b": f(a)=b.
 Notation for "(a,b,c,...) f z": f(a,b,c...)=z
 Notation for f by extension: {a->f(a), b->f(b),...}
 Any notion, which depends on some other notion may be considered a
 function. In particular, all definitions in this summary of the form
     "x of y and z: something"
 can be interpreted as a function x(y,z) := something.

Result of a function f:A->B for an argument x: The element of B
 such that f(x)=b.

Application of a function: The calculation of a result.

Argument types of a function f:A x B x ... -> Z: The sets A, B, ... .

Arity of a function f:A->B: The number of (simple) sets, the cartesian
 product of which makes up A.

Total function: A function f:A->B, such that for every a in A, there is
 a b in B, such that f(a)=b.

Partial function: A function, which is not total.
 Notation: f:A~>B

Simple type: A set of objects.

Function type A->B: The set of all total functions mapping from A to B,
 where A and B are types.

Function type A~>B: The set of all partial functions mapping from A to B,
 where A and B are types.

Truth-value, Boolean: The simple type {true, false}.
 Notation: A greek small omega. Here:
           o := {true, false}

Natural: The simple type of natural numbers.
 Notation: A 'N' with its left vertical line doubled.
 // See "Constraints over the Reals" (cr.txt) for more details

Natural+: Natural \ {0}.
 Notation: A 'N' with its left vertical line doubled and with '+' as an
           index.

Integer: The simple type of integer numbers.
 Notation: A 'Z' with its diagonal line doubled.
 // See "Constraints over the Reals" (cr.txt) for more details

Constant of a simple type T: An element of T. A constant can be seen
 as a 0-ary function to T.

Operation: A 2-ary function. One defines
       a f b := f(a,b)   "Infix-Notation"

Operator precedence: An irreflexive and transitive relation on
 operators and functions. Given two operations f and g, one says
 that f has a higher priority/precedence than g, if (f,g) is in the
 operator precedence. In this case, one defines
    a f b g c := (a f b) g c

Associative operation: An operation f, for which
 a f (b f c) = (a f b) f c

Commutative operation: An operation f, for which
 a f b = b f a

Right-associative operation: An operation f, for which
 a f b f c = a f (b f c).

Left-associative operation: An operation f, for which
 a f b f c = (a f b) f c.

Composition of two functions f:A->B and g:B->C: The function
 (f o g):A->C, where (f o g)(x) = g(f(x)).

Set function: An associative commutative operation applied to a
 set. For an associative and commutative operation f and a set
 X={x[1],x[2],...x[n]}, one defines
           f X := x[1] f x[2]  f ...  f x[n]
 Usually, the operation symbol is enlarged or upcased.
 Examples: SUM, MIN, MAX, \/, /\

Identity: The function id(x):=x.

Arithmetic if: The function '?' with
  true ? a : b := a
  false ? a : b := b

Equality: The operation
    ==:Type x Type -> Boolean
 which returns 'true', if its arguments are equal and 'false' else.

Logical operator: An operation f:Boolean x Boolean -> Boolean.

Conjunction, Logical and: The logical operator
   a /\ b := (a==true) ? b : false

Disjunction, Logical or: The logical operator
   a \/ b := (a==true) ? true : b

Logical negation: The function
   ~:Boolean->Boolean
   ~ a := (a==false)

Logical implication, material implication: The logical operator
   a => b := ~a \/ b

Logical equivalence: The logical operator
   a <=> b := (a => b) /\ (b=>a)

Ex falso quod libet: The fact that an implication from a false
 statment always yields 'true',
   (false => x) <=> true

iff: If and only if.

Currying: The interpretation of a function f:A x B x ... -> Z
 as a function f: A -> B -> ... -> Z. That is: A function requiring
 n arguments is a function, which requires 1 argument and returns a
 function, which requires n-1 arguments. From now on, functions will
 be given in their curryed version.
 Notations: f(a)(b)(c) := f(a,b,c)
            (f a b c) := f(a,b,c)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Decidability
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Countable set: A set S, for which there is a function f:S->Natural, such
 that every s in S is mapped to a different natural number. Each finite
 set is countable.
 Example: The Integers are countable, because there exists
   f(i)=i<0?-i*2+1:i*2.

Decision-Problem: A tuple of a set S and a subset S'. S is the set of
 possible objects and S' is the set of those objects with a certain
 property. For a given object s of S, it has to be decided whether
 s is in S'. Mostly, S and S' are not given extensionally, but
 intensionally. Conveniently speaking, it has to be decided whether an
 object has a property. Here, the notion "Problem" will refer to
 decision-problems.
 // ...although there are plenty of other situations in this summary
 // where the word might be applicable as well.

Solution set of a problem (S,S'): S'.

Semi-decidable problem: A problem (S,S'), for which there exists an
 algorithm, which terminates for each s in S' with the answer "Yes".
 For s of S\S', it may not terminate.

Co-semi-decidable problem: A problem (S,S'), for which there exists an
 algorithm, which terminates for each s in S\S' with the answer "No".
 For s of S', it may not terminate.

Decidable problem: A problem (S,S'), for which there exists an
 algorithm, which terminates for each s in S and answers "Yes" if s in
 S' and "No" else.

Semi-decidability-Theorem: The fact that every problem, which is
 semi-decidable and co-semi-decidable is also decidable. Proof: The
 deciding algorithm is the following: Run the semi-deciding and the
 co-semi-deciding algorithm. Report the result of whoever terminates
 first. Vice versa, every decidable problem is semi-decidable and
 co-semi-decidable.

Enumerability-Theorem: The fact that every problem is semi-decidable
 iff its solution is countable.
 Proof: Suppose the solution is countable. Then there exists an
 algorithm which semi-decides the problem: It simply compares the
 input with all elements of the solution. If the input is in the
 solution, the algorithm will stop somewhen. (Note that we do not
 need to know this algorithm, we just know that there can be such
 an algorithm). On the other hand, if we have a semi-deciding
 algorithm, then the solution set must be countable: (?)

Halting problem: The problem of deciding whether an algorithm
 terminates. This problem is not co-semi-decidable and hence not
 decidable. Proof: Imagine there was such a decision algorithm H. Now
 consider the following algorithm X:
      IF H(X)=true THEN
         WHILE true DO nothing
      STOP
 If H decides that X terminates, then X does not terminate. If H
 decides that X does not terminate, then X does not terminate.
 Hence H cannot exist.

Decidable set: A set S, such that the problem (X,S) is decidable,
 where X is a general super-set of S.

Computable function: A function, for which there can be an algorithm,
 which computes it. There exist uncomputable functions, because the
 set of functions f:Natural->Natural e.g. is not countable. But the
 set of programs is countable.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Languages
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Alphabet: A finite set of symbols.

Sequence over an alphabet S: A sequence of symbols of S.

Kleene-set of an alphabet S: The set of all sequences over S.
  Notation: S* := { <s[1],...s[i]> | s[1],...s[i] in S, i=1,2,3,...}

Language over an alphabet S: A subset of the Kleene-set of S.

Rewrite-rule over an alphabet S: A tuple of S* x S*. For a pair (a,b)
 in this relation, one says that "a generates b".
 Notation: <s[1],...s[i]> -> <s'[1],...s'[j]>

Grammar: A tuple of
 * an alphabet N of "non-terminal symbols"
 * an alphabet T of "terminal symbols"
 * a set of rewrite-rules '->' over N \/ T
 * a "start-symbol" s0 of N
 N and T must be disjunct. The left sides of the rewrite-rules must
 contain at least one non-terminal symbol.

Language generated by a grammar (N,T,->,s0): The set of all sequences
 of symbols of T, which can be generated by '->' from s0.
 Notation: L(N,T,->,s0) := { s | s in T*,
                             Ex s[1], s[2],...s[n] :
                                s0 -> s[1] -> ... s[n] -> s }

Simple type symbol: A symbol.

Type symbol: A simple symbol or a pair of two type symbols. A
 type symbol will later be mapped to a simple type. The pair will be
 mapped to a function type.

Function symbol: A symbol, to which one associates a type.

Constant symbol: A function symbol associated to a simple type.

Variable: A small letter from the end of the latin alphabet, associated
 to a type symbol T.
 Notation: v:T

Formula language: A language generated by a grammar, in which
 * T is a set of
    function symbols,
    constant symbols,
    variable symbols,
    the symbols '(', ',', ')'
 * N is
    {Term}
 * s0 is
    Term
 * the rewrite-rules are
    Term -> c                 for all constant symbols c
    Term -> v                 for all variable symbols v
    Term -> Term f Term       for all operator symbols
    Term -> f(Term)           for all function symbols f of arity 1
    Term -> f(Term, Term)     for all function symbols f of arity 2
    ...                          ...
 All sets may be restricted or extended by additional symbols/rules.
 If a new notation for the language is defined, then this adds the
 appropriate rewrite-rules. The syntactical level of the language is
 also referred to as "object level".

Term: An element of L.

Atomic term: A term which has no sub-terms.

Main function of a term: The function symbol appearing in the rule
 which generated the term.

Type symbol of a term: If the term is a variable or constant, then
 its type symbol, else the type symbol which the main function symbol
 maps to.

Well-typed term:
 * a variable OR
 * a constant OR
 * a term starting with a function symbol, where the arguments of
   the function symbol are well-typed terms of the type symbols
   required by the function symbol
 We will assume all terms to be well-typed.

Higher-order-language: A language which allows variables of function
 symbol types.

Built-in symbols of a formula language: A set of function symbols,
 type symbols and constant symbols of the formula language, which are
 considered to be present. These symbols stand for certain functions,
 types and constants, which are known a priori.
 // These entities are usually referred to as "the symbols of the
 // formula language". But since the notion "symbol" is also used
 // in a more general meaning, this summary refers to these
 // entities as "built-in symbols".

Signature of a formula language: The set of its type symbols, its
 function symbols and its constant symbols, without its built-in
 symbols.

Frame, Domain for a formula language: A set of constants, functions
 and types.

Structure for a formula language: A partial function from the signature
 to the frame. I.e. it maps
 * function symbols to functions
 * type symbols to their types, i.e. set of objects
 * constant symbols to values of their type
 A signature replaces term symbols by their "meaningful"
 counterparts in the real world. For a signature Sigma, the structure
 is often called Sigma-Structure.
 // A structure is also called "model". But since this notion
 // interferes with another logical concept called "model", this
 // summary sticks to the notion of "structure".

Valuation according to a structure: A partial function from variables
 to elements of the type, which the structure yields for the type
 symbol associated to the variable.
 // A valuation is also called "assignment". In order to avoid useless
 // notions, this term is not used in this summary.

Interpretation for a formula language: The union of a structure and
 an according valuation.

Evaluation for a formula language L: A function
     eval: Interpretations x Terms ~> Value(s)
 That is: The function receives an interpretation and a term and
 yields a value. It basically extends the interpretation to terms
 by
     eval(I,f(a,b,...))  :=  eval(I,f)(eval(I,a), eval(I,b),...)
                              for functions, types and constants f
     eval(I,x)           :=  I(x)
     eval(I,a o b)       :=  eval(I,a) o eval(I,b)
                              for symbols of the logic o
 If a new notation is defined for the formula language (such as
 right/left-associativity or precedence), then this causes the
 evaluation-function to treat terms of this new notation like
 the corresponding term of the old notation.

Math language: The formula language comprising the built-in functions
 +,-,*,... etc. All symbol strings given in this summary are
 formulae of the math language. When using the math language, one
 usually does not make a difference between the evaluation of a
 formula (i.e its result) and the sequence of symbols.
 Example: One writes
             4 + x = 6  with x=2
 for saying: eval({x->2},"4+x")=6
 // But 'eval({x->2},"4+x")' is itself a term. Why can we write
 // term=value in *this* case (?). The abstraction from types,
 // functions and constants to type symbols, function symbols
 // and constant symbols seems useless, as long as we talk about
 // it using again types, functions and constants.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Logic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Logic: A formula language, which has at least the type symbol 'o'
 built-in.
 It has to be taken care that the sets of well-formed formulae, types
 and terminal symbols be countable and decidable.

Formula of a logic: A term of type symbol 'o'.

Two-valued logic: A logic where 'o' is the Boolean type.
 This course only deals with two-valued logic. For multi-valued logic
 see "Softcomputing" (sc.txt, in German).

Predicate: A function mapping to Boolean.
 Predicates may represent sets by returning 'true' for elements of the
 set and 'false' for other objects. One says that "a predicate holds
 for an object" if the predicate returns 'true' for it.

Predicate symbol: A function symbol for a predicate. This function
 symbol is of the type symbol i -> i -> ... -> i -> o.

Axiom: A formula of a logic, which is considered basic.

Tautology: A formula of a logic, the evaluation of which is always
 'true'.

Equivalent terms: Two terms, which always evaluate to the same value
 under the same interpretation.

Lemma: A formula, which has been found to be a tautology.

Binder: A function symbol, the first argument of which must be
 given in form of a variable and the second argument of which must
 be given in form of a term. The variable may occur in the term.
 The binder has highest priority.
 Notation:   BINDER x a f b = (BINDER x a) f b
               The binder is stronger than any function symbol
             (BINDER x . term f term) := BINDER x (term f term)
              By putting a big dot after the variable, one means that
              the binder extends over all of the following terms up
              to the next ')' or to the end of the term.

Scope of a binder: Its term.

Variable of a term t: A variable symbol, which occurs in t.
 Notation for the set of variables of term t: V(t)

Bound variable of a term t: A variable of t, which occurs after a
 binder.
 Notation for the set of bound variables of t: Vbound(t)

Free variable of a term: A variable, which is not bound.

Closed formula, sentence: A formula with no free variables.

Substitution: A function from free variables to terms of the same
 type symbol. A substitution is often given by extension like
 { x -> a, y -> b, ... }. The substitution function can also be
 applied to terms. One defines
     x s := s(x)                        for a free variable x in dom(s)
     x s := x                           for other variables
     c s := c                           for constants
     f(a,b,...) s := f(s(a), s(b), ...)
     a f b s := s(a) f s(b)
 Notation: A substitution is often denoted by a greek small sigma.
           Here, a substitution is denoted by 's'.

Instantiation of a variable: The application of a substitution to it.

Object: The most general type symbol denoted by 'i'. It may be
 partitioned into subsets.

Sort: A type symbol for a subset of the type denoted by i.

Constructor of a sort S: A constant symbol of S or a function symbol
 of the type symbol S -> S .. -> S.
 Example: For the natural numbers, the constructors are 0 and the
  successor-function.

Destructor of a sort S: A function symbol of the type S->S, which is
 mapped to the reverse of the function which a constructor is mapped
 to.
 Example: For the natural numbers, the predecessor-function is a
  destructor.

Signature of a Logic: The set of its type symbols, its
 function symbols and its constant symbols, without its built-in
 symbols. This is often the set of
 * the sorts of the logic
 * the constructors of these sorts
 * the operations on these sorts
 together with axioms on these operations

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Proofs
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Inference rule, deduction rule for a logic: A relation from formulae
 (A,B) to formulae C, such that A/\B=>C. B may be empty. An inference
 rule is noted by a horizontal line. Example:
         A  B       <-- What I have
        ------
          C         <-- What I want
 means: If I know that A and B are true, then C is true.

Premise of an inference rule: Its first element

Conclusion of an inference rule: Its second element.

Weakening inference rule: An inference rule (A,B)-----C, where C does
 not imply A/\B. Such a rule looses information. Example:
        All x (human(x) => mortal(x))          <-- I know much
       ----------------------------
        human(socrates) => mortal(socrates)    <-- and need only this

Joining inference rule: An inference rule (A,B)-----C, where both A
 and B are non-empty formulae.

Reduction rule: The reverse of an inference rule. That is: A relation
 between formulae C and pairs of formulae (A,B), such that (A/\B)=>C.
 Reduction rules are also noted by a horizontal line. Example:
          C       <-- What I want
        -----
         A B      <-- What I can prove instead
 means: If I want to prove C, I can prove A and B as well.

Strengthening reduction rule: The reverse of a weakening inference
 rule. That is: A reduction rule C-----(A,B), where C does not imply
 A/\B. Such a rule generalizes. Example:
     man(socrates) => human(socrates)  <-- I need this
   -----------------------------------
     All x (man(x) => human(x))        <-- I can prove this as well
                                          (it's more difficult, though)

Branching reduction rule: The reverse of a joining inference rule.
 That is: A reduction rule C-----(A,B), where both A and B are
 non-empty formulae.

Save inference rule, save reduction rule, Rewrite-rule: A relation
 between formulae, which are equivalent. Rewrite-rules are
 non-weakening non-joining inference rules and non-strengthening
 non-branching reduction rules. They are also noted by a horizontal
 line.
 Example:
              A /\ B
              ------
              B /\ A

Premise: A formula, which one assumes to be a tautology.

Conjecture, Hypothesis: A formula, of which one wants to know whether
 it is a tautology.

Proof line: A formula or a tuple of proof lines.

Proof object: A (possibly empty) sequence of proof lines,
 together with a hypothesis and a set of premises.
 // This notion is kept quite abstract in order to be applicable to
 // Natural Deduction, Hilbert's Calculus, Tableau Calculus and
 // Sequent Calculus

Proof step on a proof object P: Applying an inference rule or a
 reduction rule to formulae in P to generate a new proof object,
 which is identical to P but has one more line. One notes with each
 line by which rule it has been generated.

Linear proof object: A proof object, each line of which is a formula.

Joining proof tree: A proof object, in which each line is
 a copy of the line before, in which
 * a formula has been replaced by another OR
 * a pair of two formulae has been replaced by a formula
 These proof objects are usually depicted as follows:
  Proof object:                  Notation:
  ((A,B),(C,D))                 A
  ((D,B),(C,D))                 D B     C D
  (  E,  (C,D))                  E       F
  (  E,    F  )                      G
  (     G     )

Branching proof tree: A proof object, in which each line is
 a copy of the line before, in which
 * a formula has been replaced by another OR
 * a formula has been replaced by a pair of two formulae
 Branching trees are the reverse of joining trees.
 These proof objects are usually depicted as follows:
  Proof object:                  Notation:
  (     G     )
  (  E,    F  )                      G
  (  E,  (C,D))                  E       F
  ((D,B),(C,D))                 D B     C D
  ((A,B),(C,D))                 A

Branch of a proof tree: A sequence, which contains a formula
 of the first line, the corresponding formula of the next line etc.
 up to the last line.

Calculus: A set of rules specifying
 * how proof objects look like
 * how to insert premises and hypothesis into the proof object
 * how to do proof steps
 * when the proof object is considered "complete"

Derivation, Proof of a hypothesis H from premises P by a calculus C:
 A complete proof object for H and P in C. One writes
          P |-C H

Positive Constructive Calculus: A calculus, which starts from the
 premises and consideres the proof object complete if the hypothesis
 appears in the last line.
 A positive constructive calculus starts off with true formulae,
 i.e. premises and axioms. It tries to assemble them in such
 a way that the hypothesis results.

Positive Reductive Calculus: A calculus, which starts from the
 hypothesis.
 A positive reductive calculus disassembles the hypothesis into
 its components and shows that these components are true
 formulae (premises and axioms).

Lemma application: Extending the set of premises of a proof-object
 by a lemma. This can be done during the process of finding a proof.
 The lemma may then be inserted into the proof-object according
 to the calculus.

Deductively, Syntactically valid formula in a calculus: A formula,
 which can be derived from no premises by the calculus.
 Notation:  |- formula

Consistency of a calculus: Its property that 'false' is not a
 syntactically valid formula.

Inconsistent set of formulae in a calculus: A set of formulae,
 from which 'false' can be derived.

Consistent set of formulae in a calculus: A set of formulae, from
 which 'false' cannot be derived.

Formula consistent with a set of formulae G: A formula F, such that
 F /\ G is consistent.

Decision problem of Logic, Entscheidungsproblem: The problem of
 deciding whether a formula is valid. It has been shown that this
 problem is semi-decidable, i.e. there is an algorithm which says "Yes"
 if the formula is valid. But it is not co-semi-decidable, i.e. there
 cannot exist an algorithm which says "No" if the formula is not valid.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               First-Order-Logic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Propositional logic: The logic with the following built-in function
 symbols
   ~: o -> o
   \/: o x o -> o
   /\: o x o -> o
   =>: o x o -> o
   <=: o x o -> o
   =:  i x i -> o
   <=>: o x o -> o
 These functions are all operators, i.e. they can be written infix.
 They have a precedence order, which is given by the above
 enumeration. All of them associate to the left, except for "=>",
 which associates to the right. The following constants are built-in:
   true : o
   false : o
 No variables are allowed. No constant symbols are allowed. No
 function symbols are allowed, except for 0-ary predicate symbols.

FOL, First-order-logic: Propositional logic, extended by the
 following two binders:
   Ex:  i x o -> o
   All: i x o -> o
 Variables, constants and any function symbols are allowed. Variables
 may only be of simple type symbols.

Existential quantifier: The binder "Ex".

existentially quantified variable: A variable bound
 by an existential quantifier.

Universal quantifier: The binder "All".

universally quantified variable: A variable bound
 by a universal quantifier.

First-order-language: A certain FOL, specified by a signature
 containing
 * A countable set R of predicate symbols
 * A countable set F of (other) function symbols
 * A countable set C of constant symbols

Model of a first-order-language: A structure of this language. This
 structure is often split into
  * a non-empty set D called the domain
  * a mapping I, called the "interpretation", which maps
    * constants symbols to elements of D
    * function symbols to functions from D^n->D
    * predicate symbols to predicates
 // The notion of a "Model of a first-order-language" will not be used
 // in this summary, because the terms "model", "domain" and
 // "interpretation" are all reserved for different concepts in this
 // summary. The notion "structure of a first-order-language" suffices
 // fully and is also well-defined.

FOL Rewrite-rules: The following rewrite rules:
 * ~(A /\ B)   <----> ~A \/ ~B
 * ~(A \/ B)   <----> ~A /\ ~B
 * A => B      <----> ~ A \/ B
 * A <=> B     <----> (A => B) /\ (B => A)
 * A /\ B      <----> B /\ A
 * A \/ B      <----> B \/ A
 * A \/ (B /\ C) <----> (A \/ B) /\ (A \/ C)
 * A /\ (B \/ C) <----> (A /\ B) \/ (A /\ C)
 * ~~A         <----> A
 * A /\ true   <----> A
 * A /\ false  <----> false
 * A \/ true   <----> true
 * A \/ false  <----> A
 * A /\ ~A     <----> false
 * A \/ ~A     <----> true
 Other rewrite rules result in the transitive closure:
 * A => B      <----> ~B => ~A  ("contraposition")
 Most calculi on FOL allow replacing any formula in a proof object by
 another formula according to these rewrite-rules.

Hilbert's predicate calculus: A constructive calculus for FOL,
 where
 * the proof objects are linear
 * inference rules may be applied to any two formulae in a
   proof object in order to generate a new line
 * Axioms, lemmata and premises may always be added as a new line
 * The proof object is considered complete as soon as the
   hypothesis appears.
 The following axioms hold:
   1. All tautologies are axioms
   2. All x A => A{x->t}
      i.e. if we have a universally quantified formula, it holds
      for any term t
   3. A{x->t} => Ex x A
      i.e. if we know that A holds for t, then there exists an x,
      such that A holds for x (namely t)
   4. t=t
      Equals are equal
 Inference rules for formulae A, B, objects s, t, a bound variable
 x and a free variable yd-.
  1. A => B                        yd- must not be in V(A)
    --------                       x must not be in V(B)
     A => All x B{yd- -> x}

     That is: Free variables may be replaced by universally
     quantified variables (Why only in implications (?))

  2. A => B                        yd- must not be in V(A)
    --------                       x must not be in V(B)
      Ex x A{yd- -> x} => B

     That is: If a free variable does not occur in A, then
     it may savely be replaced (Why only in implications (?))

   3. A    A=>B                    "Modus Ponens"
     -----------
         B

      That is: If I know A and I know that A implies B, then
      I know that B

   4.   A                          "Instantiation"
       ---
       As

      That is: If free variables occur in a term, they may be
      instantiated.

   5. s=t    A{yd- -> s)
     --------------------
        A{yd- -> t}

      That is: If I have a term in which t occurs and t=s, then
      I may replace t by s in the term. Actually, the rule should
      be   s=t, A ~~~~~~> A{s->t}
      but substitutions were just defined on free variables.
 Implicitly, all lines of a Hilbert proof object are /\-connected.
 // Mr Wirth does not like Hilbert's predicate calculus


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Improved Logic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Universal closure of a FOL-term T: The FOL-term
      UC(T) := All x : All y : ... T
 where x, y, ... are the free variables of T.

Capturing of a variable: The phenomenon that a bound variable is
 replaced by a free variable or a variable bound elsewhere by a
 substitution. This may also appear vice versa: A free variable may
 be replaced by a bound variable. Both phenomena change the
 evaluation of the formula, so that one tries to avoid capturing.

Lambda: A binder used in the form
      LAMBDA <variable> <term>
 The evaluation of this lambda-term is a function, which takes one
 argument and returns the <term>, where the <variable> has been
 replaced by the argument. By Currying, lambda-terms can represent
 functions with more arguments.
 Notation: LAMBDA is a small greek lambda.

Alpha-Renaming: A symmetric relation on terms, which causes the renaming
 of a bound variable. The new name may not occur bound or unbound in the
 term.
 Notation:  BINDER x term  <---alpha--->  BINDER y (term {x -> y})

Beta-reduction: A relation on terms, which causes the application of a
 lambda-term. Beta-reduction is confluent and terminating.
 Notation:  (LAMBDA x term) argument  -------beta----->
                 term { x -> argument }
 Beta-reduction cannot be applied, if
 * the <term> contains a binder on a variable z AND
 * x occurs in the scope of this binder AND
 * z occurs freely in <argument>
 Example:    (LAMBDA x (All z: x)) z   -----/---beta----> All z: z
 We need alpha-renaming in this case:
             (LAMBDA x (All z: x)) z   -----alpha---->
             (LAMBDA x (All y: x)) z   -----beta----->
                        All y: z

Eta-reduction: A relation on terms, which allows the skipping of wrapper
 LAMBDA-binders. Eta-reduction is confluent and terminating.
 Notation:   (LAMBDA x (f x)) ---------eta---------->  f

BetaEta-Reduction: The union of beta-reduction and eta-reduction.

AlphaBeta-Reduction: The cartesian product of alpha-renaming and
 beta-reduction. (?) That is: First, alpha-renaming is carried out and
 then beta-reduction is done. Since often, alpha-renaming is a
 necessary precondition for beta-reduction, and since a superfluous
 alpha-renaming does not harm, we talk of alphabeta-reduction
 when we mean a carefully applied beta-reduction.

AlphaBeta-irreducible term: A term t, for which there is no term t'
 such that t ---alphaBeta---> t'.

Normal form of a term t: The term t', such that t' is irreducible
 and t -----alphaBeta--->* t'.

Improved Logic, IL: The FOL with the following amendments:
 * the set of free variables and the set of bound variables are
   disjoint: Vbound /\ Vfree == {}
 * the lambda-binder is allowed.
 * predicates are used in their curryed version. Predicates may be
   given by lambda-terms.
 * the types include function types, i.e. predicates and functions
   may be given by variables.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Semantics
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

g-variant of a function f: The function
    gVarf := domrestr(f,dom(f)\dom(g)) \+/ g
 where g is a function.
 That is: For elements defined in g, gVarf behaves like g. For all
 others, gVarf works like f. One has expanded the function g by f for
 elements, for which g would not be defined.

Interpretation for the improved logic: An interpretation,
 which maps
 * constant symbols to values of their type
 * predicate symbols to predicates
 * function symbols (except for the built-in logical functions) to
   functions
 * o to {true, false}
 * other type symbols to their set of objects
 * variables to elements of the type corresponding to their type
   symbol

Universe, carrier, object domain of a interpretation I: The set of
 all objects in the interpretation, i.e. I(i).

Evaluation of the improved logic: An evaluation function, which
 works as follows:
     eval: Interpretations -> Formulae ~> o
     eval: Interpretations -> Terms ~> i
     eval: Interpretations -> Type ~> P(i).
 One defines:
   // Recurse a function down to its symbol and arguments
   eval(I)(f(a,b,...)) := eval(I)(f) ( eval(I)(a), eval(I)(b), ...)
   // Evaluate logical operators
   eval(I)(a f b) := eval(a) f eval(b)    for a logical operators f
   // Evaluate negation
   eval(I)(~a) := ~ eval(a)
   // Evaluate universal quantifiers for all elements of the
   // universe of I
   eval(I)(All x  A) := true    if eval(I')(A) = true for all
                                {x->b}-variants I' of I for all
                                b in I(i)
                        false   else
   // Evaluate existential quantifier for all elements of the
   // universe of I, check whether it applies to some
   eval(I)(Ex x  A) := true     if eval(I')(A)=true for at least one
                                {x->b}-variants i' of I for all
                                b in I(i)
 Notation for eval(I)(F): F with I as a superscript

Valuation satisfying a formula F in a structure S: A valuation V,
 such that eval(V \/ S)(F)=true.

Satisfiable formula in a structure S: A formula, for which there is
 a valuation, which satisfies it.

Semantically valid formula for an interpretation I: A formula F,
 such that eval(I)(F)=true.
 Notation: |=I F        where the 'I' is a sub-script

Model of an IL-formula F: An interpretation I, for which
 eval(I)(F)=true.

Semantically valid IL-formula: A formula F, such that eval(I)(F)=true
 for all interpretations I.
 Notation: |= F

True sentence: A sentence, the evaluation of which yields true.

False sentence: A sentence, the evaluation of which yields false.

Sound calculus: A calculus, where 'true' cannot be derived from
 semantically invalid formulae.
 Hilbert's predicate calculus is sound.

Complete calculus: A calculus, which can produce 'true' from all
 semantically valid formulae.
 Hilbert's predicate calculus is complete.

Semantic entailment: The fact that if F is a formula and F' is its
 universal closure, then
 (?)
 Definition of A |= B (?)

Deduction theorem: The fact that
     B |= A    iff     |= (UC(B) => A)

Explicitness-lemma: The fact that, given a formula and a structure,
 the evaluation of the formula depends only on the valuation for
 the free variables. Formally: Be S a structure, be tau a valuation, be
 F a formula, then
      eval(S \+/ tau)(F) = eval(S \+/ domrestr(tau,Vfree(F)))(F)

Substitution-lemma: The fact that the evaluation of a formula, which
 has undergone a substitution, does not change if the substitution is
 left away but instead added to the valuation.
      eval(S \+/ tau)(Fs) = eval(S \+/ (ids o tau))(F)
 where
 * S is a structure
 * V is a valuation
 * s is a substitution
 * ids is the s-variant of id, i.e. s expanded to identity for
   undefined variables, ids = domrestr(id,Variables\dom(s)) \+/ s
 // I am afraid the "o eval(S\+/tau)" in the slides causes a type
 // mismatch. I think it should just be "(ids o tau)", i.e. the new
 // valuation first applies the substitution and then the old
 // valuation.

Herbrand model: (?)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Q0
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Russel's iota: A binder used in the form
     iota x A,
 where 'iota' is the greek small iota, x is a variable and A is a term,
 which may contain x. The evaluation of "iota x A" is the object z,
 such that A{x->z} evaluates to 'true'. That is: The iota picks the
 object of the universe, which makes the term true. It is the function
 "the x, such that". The problem is that this object may either not
 exits or may not be unique. Then iota is not defined.

Hilbert's epsilon: A binder used in the form
     eps x A,
 where 'eps' is the greek small epsilon, x is a variable and A is a term,
 which may contain x. The evaluation of "i x A" is any object z, such
 that A{x->z} evaluates to 'true'. Different from Russel's iota, there
 may be multiple such objects and Hilbert's epsilon just returns one of
 them. It is the function "any x, such that". If there exists no such
 x, then the result is any (!) value. The following axioms hold
   1.  Ex x A   => A{x->eps x A}          "(eps0)"
   2.  Ex x A  <=> A{x->eps x A}          "(eps1)"
   3.  All x A <=> A{x->eps x ~A}         "(eps2)"
       If "All x A" is not valid, then there is a k, such that
       ~A{x->k} is true. We have eps chose this k. Then A{x->k} is
       not valid. Hence the equivalence is 'false' <=> 'false'.
       If "All x A" is valid, then there is no k, such that ~A{x->k}
       holds. Hence eps will pick any object b. Since A holds for
       all objects, it also holds for b. Hence A{x->b} is true and the
       equivalence is 'true' <=> 'true'.

Type Theory Q0, Q0: The logic comprising the following built-in
 type symbols
 *  o
 *  i
 *  a->b, if both a and b are types (function types)
    ba    alternative notation
          This is the type of functions from a to b
 Notation for a term t of type b: t with a subscript b, if occurring for
                                  the first time. Here: t[b]
 Q0 has the following built-in function symbols:
   LAMBDA x term            (Lambda-binder)
   Q: alpha -> alpha -> o   (equality, for any type alpha)
   iota : (i -> o) -> i     (iota-binder)
 Variables may be of any type symbols. The substitution is extended
 over function variables as follows:
   (f[ba] t[a]) s := (f s)(t s)
   (LAMBDA x t) s := LAMBDA x (t s)
 The currying-notation is preferred for functions.
 Be alpha a type symbol, be x1,x2,x3 variables of type symbol alpha,
 be b and b' variables of type symbol 'o', be t and s and A terms
 of type symbol alpha, be f and g function-variables of type
 symbol o -> o -> o. One defines the following notations:
  // Abbreviation for curried functions
  LAMBDA x1, x2, x3, ... t := LAMBDA x1 (LAMBDA x2 (LAMBDA x3... t)...)
  // Write '=' instead of Q for equality
  s=t                      := Q[oalphaalpha](s)(t)
  // Define 'true' by the result of Q applied to two equal things
  true                     := Q[ooo]=Q[ooo]
  // Define 'All' by the help of Q, which judges two functions equal
  // if they are equal for all arguments
  All x A                  := (LAMBDA x true) = (LAMBDA x A)
  // Define 'false' by claiming that 'true' is equal to the identity
  false                    := (LAMBDA b true) = (LAMBDA b b)
  // Define 'and' by asking whether all functions f return the
  // same for (true,true) as for (arg1,arg2)
  /\                       := LAMBDA b, b' (
                                (LAMBDA f (f true true)) =
                                (LAMBDA g (g b b')
                              )
                           // Do we really need g here (?)
                           // Wouldn't it be easier to write
                           // All f ((f true true) = (f b b')) ?
  // Define '=>' by asking whether its first argument is equal
  // to the conjunction of both arguments
  =>                       := LAMBDA b, b' (b=(b /\ b'))
  // Define 'not' by asking whether its argument is equal
  // to false
  ~                        := Q[ooo] false
  // Define 'or' by the usual de-Morgan-rule
  \/                       := LAMBDA b, b' ~(~b /\ ~b')
  // Define 'Ex' by the usual conversion
  Ex x A                   := ~ (All x ~A)
  // Define inequality as the negation of equality
  s =/= t                  := ~(s=t)
  // Define unique existance
  Ex! x A                  := Ex x All y (A{x->y} => x=y)
  // Define iota. It holds:
  //   iota[i(oi)] in i
  // Define iota for boolean predicates:
  // Either the predicate is equal to the identity (Q[ooo] true),
  //   then 'true' will do the job
  // or the predicate is equal to negation, i.e. not equal to
  //   identity, then 'false' will do the job
  iota[o(oo)]              := Q[o(oo)(oo)] (Q[ooo] true)
  // Define iota for predicates on function-types
  iota[(ba)(o(ba))]        :=
     LAMBDA h[o(ba)]        // Get the predicate
      LAMBDA x[a]           // Return a function a->b
       iota y[b]            // This function returns the y such that
        Ex f[ba]            // there is a function f:a->b
         (h(f)              // which fulfills h
          /\ f(x) = y)      // and maps x to y

     That is: We construct the function which fulfills the predicate.
     This function takes an argument x and maps it to the result of
     a function f, which fulfills the predicate.
 The following axioms hold in Q0:
  // If a boolean predicate holds for 'true' and for 'false', then
  // it holds for all values of type Boolean (which are 'true' and
  // 'false')
  (p[oo] true) /\ (p false) = All b[o] (p b)
  // If x and y are equal, then they should fulfill the same
  // predicates
  (x[a] = y[a]) => ( p[oa](x) = p(y) )
  // Two functions are equal, if their results are equal for all
  // possible arguments
  (f[ab] = g[ab]) = (All x[b] (f(x)=g(x)))
  // A function returning a constant always does so
  (LAMBDA x[a] A) t[a] = A      if A is a constant or a variable!=x
  // The identity always returns its argument
  (LAMBDA x[a] x) t[a] = t[a]
  // A function applied to a function call can be recursed down
  (LAMBDA x[a] (B[cb] C[b])) A[a]  = ((LAMBDA x B) A) ((LAMBDA x C) A)
  // Arguments may be swapped
  (LAMBDA x[a] LAMBDA y B) A[a] = (LAMBDA y ((LAMBDA x B) A))
       where y must be different from x and all other variables in A
  // Overwritten variables can be ignored
  (LAMBDA x (LAMBDA x B)) A = (LAMBDA x B)
  // If iota seeks for an object, which is equal to y, it returns y
  iota[i(oi)] (Q[oii] y[i]) = y

Interpretation for Q0: A partial function I, which maps
 * o to {true, false}
 * other type symbols to their set of objects
 * variables to a value of the type corresponding to their type symbol
 * Q[ott] for every type t to a function I(Q):I(t) -> I(t) -> I(o),
   such that I(Q)(a)(b)='true' iff a=b.
   That is: Q is mapped to the equality function.
 * iota[i(oi)] to a function I(iota):(I(i)->I(o))->I(i), such that
   I(iota)(p)(x) is the x, for which p becomes 'true'.
   That is: iota is mapped to the Russel's iota.

Standard interpretation for Q0: An interpretation for Q0, which maps
 the type of functions A->B to the set of functions A->B
       I(A->B) = I(A) -> I(B)
 for types A, B and an interpretation I.

General interpretation for Q0: An interpretation for Q0, which maps
 the type of functions A->B to a subset of functions A->B
       I(A->B) < I(A) -> I(B)
 for types A, B and an interpretation I.

Evaluation for Q0: An evaluation function, which works as follows:
     eval: Interpretations -> Formulae ~> o
 One defines for all types a,b and terms t and functions f and
 variables x:
   // Function application
   eval(I)(f[ba]t[a]) := eval(I)(f)(eval(I)(t))
   // Evaluation of a lambda-term yields a function
   eval(I)(LAMBDA x[a] t[b]) := { (z,eval(I')(t)) |
                                   I' is the {x->z}-variant of I,
                                   z is an element of I(a) }
     That is: The lambda-term is mapped to the function, which maps
     all z of the domain type to the term t, where the variable x
     has been replaced by z. It holds:
     eval(I)(LAMBDA x[a] t[b]) in I(a -> b)

Inference rule for Q0, Rule R: The inference rule
         C  A[a]=B[a]
       ---------------
          C'
 where C' is C with one occurance of A replaced by B. Bound variables
 may not be replaced. This is the simplest inference rule, which allows
 substituting equal terms.

Calculus for Q0: The constructive positive calculus, the proof objects
 of which are linear. Proof steps may always add a
 line containing an axiom or a premise. The only inference rule, the
 rule R, may be applied to any two lines in order to generate a new
 line. The proof is considered complete if the hypothesis appears.
 This calculus is similar to Hilbert's calculus, but
 * the formulae are Q0-formulae
 * the only inference rule is the rule R

General model: A structure, in which each formula has a value with each
 possible valuation.

Properties of Q0:
 * The explicitness-lemma holds
 * The substitution-lemma holds
 * Q0 is consistent
 * Q0 is sound
 * Q0 is complete in every general countable interpretation
 * Q0 is compact, if every finite subset of a set S of formulae has a
   general model, then S has a general model (?)
 * Q0 is a super-set of First-Order-Logic


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Equality
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Notion: A word for a property. This is usually just an adjective, a
 verb or a noun.

Extension of a notion: The set of objects which have the property
 denoted by the notion.

Intension of a notion: The denoted property.
 If two notions have the same intension, they also have the same
 extension. But two notions may have different intensions and the
 same extension (the extensions of "Featherless biped" and "human"
 are the same, namely the set of those entities, which the reader
 of this summary belongs to).

Individual notion: A notion with a singleton extension.

Extension of a function definition: The function defined.

Intension of a function definition: The sequence of symbols used for
 the definition, regardless of the naming of variables.

Leibniz substitutability theorem (?), Extensionality axiom: The fact
 that two notions with the same extension may be exchanged without the
 sentence to change its truth-value.

Alpha-equality: The alpha-renaming relation, considered as equality. (?)
 That is: Two terms with an equal structure are considered equal.

Primitive equality: The equality built-in in the structure.
 Tarski claimed that primitive equality was a logical notion, i.e.
 every logic should support it. Primitive equality is implemented
 in Q0 by the Q[oaa]-function.

Indiscernability, Leibniz equality: The relation between those objects,
 for which there is no property which one of them has and the other
 does not have. That is: If two objects have all the same properties,
 then they are indiscernable and may thus be considered equal.
 Formally: L[oaa] := LAMBDA x[a], y[a]  (All P[oa] (P(x)=P(y)))
 Primitive equality implies Leibniz-equality.

Functional-extensional equality: The relation between those functions,
 which for the same arguments return the same results. That is: If two
 functions always produce the same output for all inputs, then these
 functions may be considered equal.
 Formally: E[o(ba)(ba)] := LAMBDA f[ba], g[ba] (All x[a] (f(x)=g(x)))
 Leibniz-equality implies functional-extensional equality.

Beta-equality: The relation of beta-reduction, considered as equality.
 That is: A lambda-term applied to an argument is considered equal to
 its result.

f-principle: The principle that
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) => f=g)
 This is the Functional-extensional equality.
 (So what is it good for (?))

eta-principle: The principle that
   All f[ba] ( (LAMBDA x[a] (f x)) = f )
 This means that a LAMBDA-wrapper can be left away.

xi-principle: (Or whatever this greek char is called (?))
 The principle that
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) =>
                         ( (LAMBDA x (f x))= (LAMBDA x (g x)) ))
 This is a combination of the f- and eta-principle. If one accepts
 beta-equality, then it holds that the f-principle is the same as
 the eta-principle together with the xi-principle. Proof:
 If one has the f-principle, then one can show the eta-principle by
   // f-principle
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) => f=g)
   // Application to (LAMBDA x[a] (f x)) and f
   (All x[a] ((LAMBDA x[a] (f x)) x) = f(x)) => (LAMBDA x[a] (f x))=f
   // Beta-reduction
   (All x[a] (f(x) = f(x))) => (LAMBDA x[a] (f x))=f
   // Definition of Q
   true => (LAMBDA x[a] (f x))=f
   // Definition of implication
   (LAMBDA x[a] (f x))=f
 If one has the eta-principle, one can show the xi-principle by
   // f-principle
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) => f=g)
   // Plug in the eta-principle
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) =>
                ((LAMBDA x[a] (f x))=(LAMBDA x[a] (g x))))
 If one has the eta- and the xi-principle, one can show the
 f-principle by
   // xi-principle
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) =>
                         ( (LAMBDA x (f x))= (LAMBDA x (g x)) ))
   // Plug in the eta-principle
   All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) =>
                         ( (LAMBDA x (f x))= (LAMBDA x (g x)) ))

Choice-function: A function which takes a set and returns an element
 of it.
 Formally:      All p[oa]   ( (Ex x[a] p(x))  =>      p(f(p)) )
             for all sets p     if p!={}     then   f(p) is in p

Axiom of Choice: The postulation that there must be choice function.
 Formally: Ex f[a(oa)] All p[oa] ( (Ex x[a] p(x)) => p(f(p)) )

Predicate-Descriptor: A function f: (i->o) -> o, which returns 'true'
 for certain predicates and 'false' for others. That is: It describes
 a property of predicates.

Choice set of a Predicate-Descriptor P: A set of objects, such that for
 every predicate p with the property P, there is an element in the
 choice set for which p holds.

Choice-set: The range of a choice function. (?)
 Example:  All sets:        {a,b,c} {d,e,f} {g,h,i} ...
           Choice function:    |     |       |
                               V     V       V
           Choice set:  {      b,    d,      g,     ...        }


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Modal Logic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Poly-modal Logic: The first-order logic, extended by
 * The type W ("world")
 * The binders
    AllWorld : W x o -> o      (notation: box symbol)
    SomeWorld: W x o -> o      (notation: diamond symbol)
 * The object
     I of type W (the "current world")
 * The function
     R: W x W -> o  ("Reachability")
 Modal logic treats truths in several "worlds". These worlds are
 interconnected by the relation R, i.e. one may go from one world to
 certain other worlds. The binder "AllWorld" evaluates to 'true', if
 the given formula holds in all worlds reachable from the given world.
 Similarly, "SomeWorld" evaluates to true if this is the case for some
 of the reachable worlds. All predicates take an additional argument of
 type W. By modal logic, one can model for instance
 * time: What is true now does not need to be true tomorrow
 * possible worlds: What is true in our state of the world may not
    be true under other circumstances.
 * permission and obligation
 * knowledge and belief

Multi-modal logic: Poly-modal logic, extended by other types similar
 to W. The two binders may be used with all of these types, there
 is a current world and a reachability relation for all of them
 and predicates take an additional argument for each of them.

Evaluation for poly-modal logic: The evaluation for FOL extended by
 the following definitions
 // AllWorld: Evaluate term for all worlds reachable from I
   eval(S)(AllWorld w A) := true    if eval(S')(A) = true for all
                                    {w->b,I->b}-variants S' of I
                                    for all b with S(R(I,b))=true
                            false   else
 // SomeWorld: Also evaluate term for all worlds reachable from I.
 // The formula becomes true, if the term holds in at least one world
   eval(S)(SomeWorld w A) := true   if eval(S')(A) = true for some
                                    {w->b,I->b}-variants S' of S
                                    for all b with S(R(I,b))=true
                             false  else
 This definition respects the Explicitness-Lemma and the
 Substitution-Lemma.

Mono-modal Logic, Modal logic: A restriction of poly-modal logic, where
 the AllWorld-binder, the SomeWorld-binder and any predicate may only
 take the world variable w as an argument. Hence a term cannot refer to
 a variable bound by a binder outside the current scope. Predicates
 outside the scope of a world-binder must take the current world I
 as an argument. Hence one can ommit this argument.
 Notation: AllWorld term  := AllWorld w term
           SomeWorld term := SomeWorld w term
           p(a,b,c,...)   := p(a,b,c,...w)  if inside a binder scope
           p(a,b,c,...)   := p(a,b,c,...I)  else
 Depending on the properties of the evaluation of R, one distinguishes
 different kinds of mono-modal logic:

  Name  Conditions on R          Axioms

   K      none                    true
   T      reflexive               Allworld P => P
   K4     transitive              Allworld P => Allword Allworld P
   D      serial                  Allworld P => Someworld P
   (5)    triangular              Someworld P => Allworld Someworld P
   (Sym)  symmetric               P => Allworld Someworld P
   B      reflexive, symmetric    Axioms of T and (Sym)
   S4     reflexive, transitive   Axioms of T and K4
   S5     equivalence relation    Axioms of T, (Sym) and K4
   S5     reflexive, symmetric,
          transitive              Axioms of T, (5) and B

Intensional type in Modal Logic: The type
    W->b
 for a type b. In Modal Logic, the intension of a notion is a function,
 which accepts a world as an argument. As soon as the notion is applied
 to the world, the real predicate (the extension) results.
 Notation: Instead of W->b, one writes "b", preceded by an upwards
           arrow. Here: ^b := W->b
           For a term s, instead of "LAMBDA w s", one writes "s",
           preceded by an upwards arrow. This corresponds to the
           abstraction from the extension to the intension of s. Here:
           ^s             := LAMBDA w s
           For a term s, instead of "s w", one writes "s", preceded
           by a downwards arrow. This corresponds to the extension of s
           in the (only) world w. Here:
           vs             := w s
 Example: Let the "worlds" be the facts known in different
  civilizations. Consequently, "AllWorlds A" means that all
  civilizations know A. Let h be the intention of Hesperus (the morning
  star) and p be the intention of Phosphorus (the evening star). Hence
  h and p are functions from worlds to predicates (=sets=extensions).
  In modal logic, the statement
       (xd- = yd-) => AllWorld (xd- = yd-)
  evaluates to false, because we have as a counterexample h and p:
  Hesperus and Phosphorus were not known to be different in all
  civilizations. If we replace (xd-,yd-) by (h,p), we get:
       (vh = vp) => AllWorld (vh = vp)
  This stands for:                         ('I' is the current world)
       (h(I) = p(I)) => AllWorld w (h(w) = p(w))
  The left-hand-side of the implication says that the extensions of h
  and p are the same in our world. This is true. The right-hand-side
  says that the extensions are equal in all worlds -- which is false.
  Hence the implication evaluates to false. If we quit mono-modal
  logic, we can make the term true:
       (h(wd-) = p(wd-)) => AllWorld w (h(wd-) = p(wd-))
  This means: Suppose the extensions of h and p are equal in a world
  wd-. Then the left-hand-side of the implication becomes true. At the
  same time, the sub-term "(h(wd-) = p(wd-))" on the right-hand-side
  becomes true. Since the dependence of h and p upon a world has been
  taken away by the specific argument wd-, the bound variable w does
  not have any influence on the right-hand-side, the whole right
  term becomes true and so does the implication. This means: Tell
  a Babylonian that in our world, Hesperus and Phosphorus are the
  same. Then he will know, that in our world, Hesperus and Phosphorus
  are the same.

Extensional type in Modal Logic: A type, which is not extensional and
 does not involve W.

Intuitionistic Logic and Modal logic S4: (?)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Variables
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Delta-minus-variable, Eigenvariable: A free variable, which may not
 appear more than once. The set of all delta-minus-variables of a
 term t is noted Vd-(t).

Gamma-variable: A free variable, which may not appear more than once and
 can be instantiated once in a proof process. This instantiation
 changes all formulae of the proof instantly. Thereby, the gamma-
 variable disappears. Gamma-variables enable us to compute with some
 fixed value, which we will only know at some time later during the
 proof. A proof can only be complete if all gamma-variables have been
 instantiated. The set of all gamma-variables of a term t is noted
 Vgamma(t).
 // A gamma-variable is also called "Meta-variable". Mr Wirth does not
 // like this notion, because he sees gamma-variables as integral part
 // of the proof and not as something above it. Another name is
 // "free variable". This notion is to general and is hence not used
 // in this summary.

Condition on a variable x: A formula with x as a free variable.

Constant fulfilling a condition: A constant c, such that instantiating
 the free variable of the condition by c causes the formula to
 evaluate to 'true'.

Delta-plus-variable: A gamma-variable, which has a condition
 associated. It may only be instantiated by a constant fulfilling this
 condition. The set of all delta-plus-variables in a formula t is noted
 Vd+(t).

Alpha-rule: A non-branching reduction rule, which does not introduce
 new variables.

Beta-rule: A *b*ranching reduction rule.

Gamma-rule: A reduction rule, which introduces a gamma-variable from
 an existentially quantified formula.

Delta-minus-rule: A reduction rule, which introduces a delta-minus-
 variable from a universally quantified formula.

Liberalized delta-rule, Delta-plus-rule: A reduction rule, which
 introduces a delta-plus-variable from a universally quantified
 formula.

Choice-condition: The relation between delta-plus-variables and
 their conditions. If a delta-plus-rule is applied to
         All x A
 and intrduces the delta-plus-variable xd+, then the choice condition
 stores (xd+,~A{x->xd+}). That is: The newly introduced delta-plus-
 variable needs to be replaced by something, which does not fulfill A.
 Or, put differently, xd+ must be replaced by eps(~A).
 Example: Assume the following reductive proof of "All x P(x)":
    All x P(x)           apply delta-plus-rule
      P(xd+)             with choice condition {(xd+,~P(xd+)}
 Now assume "All x P(x)" is false for an object k. We decide to
 instantiate xd+ and the choice condition yields k as a possible
 instantiation:
      P(k)
 But P(k) is false, hence the proof fails -- which is good, because
 "All x P(x)" is false. Now assume it is true. We decide to
 instantiate xd+ and ask for an object k such that the choice condition
 is fulfilled. We get for instance k=eps(~P(x)), because eps
 just returns any object if its set is empty. Of course, P(k) holds,
 since P(x) holds for any x. Now we are left with proving
      P(k)
 ...and P(k) holds, the proof succeeds.

Multiplicity of an existentially quantified sub-formula: The number of
 times where gamma-variables have been introduced from this formula.
 One can imagine this as making multiple copies of the fomula and then
 introducing gamma-variables. Increased multiplicity is for instance
 necessary to prove:
         All x P(x) => (P(a) /\ P(b))      Apply rewrite-rules
         Ex x ~P(x) \/ (P(a) /\ P(b))      Apply gamma-rule
            ~P(xg) \/ (P(a) /\ P(b))
 Instantiating xg with a would help. But xg also needs to be
 instantiated to b! Positive proofs instantate gamma-variables, because
 existentially quantifieds terms result from a universally quantified
 term in the premise.

Skolemization: The transformation of a FOL-formula as follows:
    Ex x All y P(x,y)   ~~~~~~>   All y' Ex x P(x,y'(x))
 where y' is a function variable, called Skolem-Function. Skolemization
 moves the All-quantifiers to the very left and gives them some
 existentially quantified variables as arguments. Problems of
 Skolemization:
 * It may change the notions of Herbrand Models (?)
 * It may imply the Axiom of Choice (?)
 * Inductive theorem proving by Descente infinie (s.b.) becomes
   impossible (?)

Raising, Lifting: The transformation of a FOL-formula as follows:
    All x Ex y P(x,y)   ~~~~~~>   Ex y' All x P(x,y'(x))
 where y' is a function variable, called Raising-Function. Advantages:
 * The newly introduced raising functions do not introduce new objects
   in the Herbrand Model (?)
 * The raising functions do not imply the axiom of choice due to their
   existential character (?)
 * Inductive theorem proving by Descente infinie (s.b.) is
   still possible (?)

Variable-condition: A relation on free variables, noted R.
 R(x,y) means: The free variable x is older than the variable y. As a
 result, we may not instantiate x with a term containing y. R can
 therefore be understood as a blocking relation
      R(x,y)  blocks x from being instantiated by y
 Each proof involving gamma-variables needs a variable-condition,
 which is empty in the beginning. With every application of a
 * delta-rule x->eigenvariable, the variable-condition needs to
   be extended by
     { (z,eigenvariable) | z is a gamma-variable or a
                           delta-plus-variable in the whole formula}
 * delta-plus-rule x->eigenvariable, the variable-condition needs to
   be extended by
     { (z,eigenvariable) | z is a gamma-variable or a
                           delta-plus-variable in the
                           quantified sub-formula}
   Furthermore, the Choice-condition is updated by
     { (eigenvariable,term) }
   where "term" is the quantified sub-term.
 * substitution free-gamma-variable -> term
     { (z, free-gamma-variable) | z is a free variable in term }

 Example: Positive reductive disjunctive sequent proof
       Ex x All y x=y      the variable conmdition is empty: {}
          All y xg = y     where xg is gamma-variable
           xg = yd-        where yd- is a delta-variable
                           the variable condition is updated to:
                           {(xg,yd-)}
  Now, the variable condition prevents us from instantiating xg by yd-.
 Example:
       All x Ex y x=y      the variable conmdition is empty: {}
          Ex y  xd-= y     where xd- is a delta-variable
                            the variable-condition is still empty
           xd- = yg        where yg is gamma-variable
  Now, we may instantiate yg->xd- and get a complete proof.
 In general, the variable-condition is a hindrance in proving,
 because it prevents one from instantiating the gamma-variables
 deliberately. This is where delta-plus-variables come into play.
 Example: Positive reductive proof
     Ex x (  (All y ~P(y))   \/   P(x) )
       All y ~P(y) \/ P(xg)         where xg is a gamma-variable
  Assume we choose a delta-rule:
        ~P(yd-), P(xg)              where yd- is a free delta-variable
                                    and the variable condition is
                                    { (xg,yd-) }
  The variable condition prevents us from choosing xg=yd-, although
  this would be a sound step. This is why we choose a delta-plus-rule:
       All y ~P(y) \/ P(xg)
         ~P(yd+) \/ P(xg)          with choice-condition {(yd+,P(yd+))}
  Now we decide to instantiate yd+. We choose yd+ -> xg, because we
  will choose xg such that P(xg).
         ~P(xg) \/ P(xg)
  Now instantiating xg with anything yields 'true', the sentence is
  proved.

Existential relation of a substitution s: The relation
    E(s) := { (zg, x) | x in dom(s) /\ zg is a gamma-variable
                                       in s(x) }
 This relation collects variable pairs (x,y) and says: I have replaced
 y by something containing x.

Universal relation of a substitution s: The relation
    U(s) := { (zd-, x) | x in dom(s) /\ zd- is a free delta-variable
                                        in s(x) }
 This relation collects variable pairs (x,y) and says: I have replaced
 y by something containing x. This means: Block x from being replaced
 by something containing y:
         y ~~~> x
    =>  block (x,y)

Variable condition update: Replacing the variable condition R by
        R \/ E(s) \/ U(s)
 after having applied the substitution s in a delta-rule in a proof.
 That is: By introducing a gamma-variable, store in the variable
 condition on which gamma-variables it depended.
 // Better use the description in "variable-condition" and drop this.

R-condition: The demand that a variable condition must be well-founded
 (i.e. acyclic). The proof is sound iff the R-condition is fulfilled.
 This is because a pair (x,y) in the variable-condition means that we
 may not replace x by a term containing y. If we now do such an illegal
 substitution x->y, the existential relation or the universal relation
 of the substitution will contain (y,x). Thus, the variable condition
 update will produce a cyclic relation.

R-substitution for a variable condition R: A substitution s, such that
    R \/ E(s) \/ U(s)
 is well-founded (i.e. acyclic).

(S,R)-valuation: A function which takes a gamma-variable and a partial
 valuation for free delta-variables and returns an element of the
 domain.
    e: Vgamma -> (Vdelta ~> S) ~> S
 where S is the structure (or the domain(?)). That is: The function is
 supposed to give values to the gamma-variables. In order to do so, it
 may read the values of the delta-variables, which the gamma-variable
 depends on.

Semantical relation of a (S,R)-valuation e: The relation
     S(e) := { (y,x) | x in dom(e) /\ y in dom(UNION dom(e(x))) }
 That is: The relation between the gamma-variables taken by e and
 the delta-variables being read by e. It is required that
      R \/ S(e)
 be well-founded, i.e. the valuation may only read delta-variables,
 which are older than the gamma-variable.

Delta-set of a semantical relation S(e) for a gamma-variable x: The
 set of those delta-variables, the values of which are read by the
 (S,R)-valuation e in order to interpret x.
     S(e)<{x}>
 It is required that all valuations for free variables which e takes
 have the same delta-set. In this case, e is called "semantical".

Eps-function: The function eps, which takes an (S,R)-valuation e, a
 valuation d for delta-variables and a variable x and returns
   eps(e)(d)(x) := e(x)(domrestr(d,S(e)<{x}>))
 That is: It valuates x.

Valid formula in a structure S: A sentence, which evaluates to 'true'
 in S. (?)

Valid set of formulae in a structure S: A set of formulae, each of which
 is valid in S.

(d,e,S)-valid set of formula: A set of formulae, which is valid in
  S \/ eps(e)(d) \/ d

(e,S)-valid set of formulae: A set of formulae, which is (d,e,S)-valid
 for all valuations d of delta-variables.

R-valid set of formulae: A set of formulae, such that there exists a
 (S,R)-valuation e, such that the set is (e,S)-valid. That is: If I
 can find values for the existential variables for all possible choices
 of universal variables, then the formulae are valid. That is: Each
 formula F in the set evaluates as follows:
         eval(S \+/ eps(e)(d) \+/ d)(F)=true
 for a valuation d of the universal variables. Here, the valuation eps
 for the existential variables can look into the cards of some
 universal variables to make its choice of valuation. The valuation
 e is split up into the valuation of existential variables and
 the valuation of delta-plus-variables.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Sequent calculus
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Unifier for two terms: A pair of substitutions, such that the
 application of the first one to the first term and the second one to
 the second term makes the two terms equal.

Matching for a term A to another term B: A substitution, which makes A
 equal to B.

Unifyable formulae: Two formulae, for which there is a substitution.
 For higher-order-languages, the problem of finding out whether two
 formlae are unifyable is undecidable.

Negated formula: A formula starting by "~".

Polarity of a formula: Its property of being negated or not. The
 polarity is expressed by a '+' or a '-'.

Connection: A pair of unifyable formulae of different polarity.

Sequent: A formula of the First-Order Logic of the following form:
       (A1 /\ A2 /\ ... Ak) => (B1 \/ B2 \/ ... Bm)
 It is usually noted in the form:
      A1, A2, ... Ak --> B1, B2, ... Bm
 Any formula can be expressed in sequent form. A missing A-formula
 is replaced by a 'true' and a missing B-formula is replaced by
 a 'false'.

Antecedent of a sequent: The first sequence of formulae.
 The sequence is to be understood as connected by '/\' (Conjunction).
 If the antecedent is empty, it is an implicit 'true'.

Succedent of a sequent: The second sequence of formulae.
 The sequence is to be understood as connected by '\/' (Disjunction).
 If the succedent is empty, it is an implicit 'false'.
 If both the antecedent and the succedent are empty, this is
 shorthand for 'false'.

Sequent inference rules: The following inference rules on sequents.
 Be A and B formulae and be X,Y,Z sub-sequences of formulae:

 Init:             ---------------
                    X, A --> Y, A          This is a tautology

 /\-Left:          X, A, B --> Y
                  ---------------
                  X, (A/\B) --> Y          Antecedent is '/\' anyway

 /\-Right          X --> Y, A, [-B]  ;   X --> Y, B, [-A]
                  ---------------------------------------
                              X --> Y, (A/\B)

                  Here, either -A or -B or none may be present, but
                  not both


 =>-Left           X --> Y, A  ;  X, B --> Y
                  ---------------------------
                   X, (A=>B) --> Y

 =>-Right          X, A --> Y, B
                  ---------------
                   X --> Y, (A=>B)

 False-Left:      ---------------
                   X, false --> Y

 True-Right:      ---------------
                    X --> true, Y

 Negation-Left:    X --> Y, A
                  ------------
                   X, ~A --> Y

 Negation-Right:   X, A --> Y
                  ------------
                   X --> Y, ~A

 \/-Right:         X --> Y, A, B
                  ---------------
                   X --> Y, (A\/B)

 \/-Left:          X, A, [-B] --> Y   ;   X, B, [-A] --> Y
                  -----------------------------------------
                              X, (A\/B) --> Y

                  Here, either -A or -B or none may be present, but
                  not both

 All-Left:          X, All x A, A{x->t} --> Y     (weakening)
                   ---------------------------
                    X, All x A --> Y

 All-Right:         X --> Y, A{x->t}              (when used in
                   ------------------              reduction, t is a
                    X --> Y, All x A              delta-minus-variable)

 Ex-Left:           X, A{x->t} --> Y              (weakening)
                   ------------------
                    X, Ex x A --> Y

 Ex-Right:          X --> Y, Ex x A, A{x->t}      (weakening)
                   --------------------------     (when used in
                    X --> Y, Ex x A                reduction, t is a
                                                   gamma-variable)
 Cut-Rule:          A --> B,C   ;  A,B --> C
                    -------------------------
                               A --> C

Sequent reduction rules: The reverse of the sequent inference rules.
 Hence, the notions of "alpha-rules", "beta-rules", "gamma-rules" and
 "delta-rules" become applicable.

Init-element: A sequent containing a formula in the antecedent and one
 in the succedent, which are unifyable.

Positive Constructive Sequent Calculus: The calculus, where
 * the proof objects are joining tree objects
 * all formulae are sequents
 * the formulae in the initial line must be init-elements
 * sequent inference rules are applied to a pair of formulae and
   they replace it by the result of the rule in a new line
 * the proof object is complete if the last line is of the
   form   premises --> hypothesis
 * lemmata may always be added in the antecedent of any
   sequent
 Example: Proof of A/\B => B /\ (C\/A) from no premises

                           -------------- init
                           A, B --> C, A
     init -----------     ---------------- /\-Left
          A, B --> B       A/\B --> C, A
  /\-Left -----------     ---------------- \/-Right
          A/\B --> B       A/\B --> C\/A
         --------------------------------- /\-Right
                 A/\B --> B /\ (C\/A)
              ------------------------- =>-Right
               --> A/\B => B /\ (C\/A)

 Implicitly,
 * all sequents are /\-connected
 * and all lines are /\-connected
 A positive constructive sequent proof is a kind of
 ordered Hilbert proof. One tries to deduce the hypothesis by starting
 from true formulae. If one introduces a "/\" between the branches,
 then each line implies the next one. Each proof can
 be transformed to a Hilbert proof: Replace all sequent form formulae
 by their normal form. Then flatten each line of the proof tree into
 several lines, one for each contained formula.
 Example: Proof of Ex x All y P(x,y) => All y' Ex x' P(x',y')  (?)
      All y P(c,y), P(c,y) --> P(c,y)
      -------------------------------------          All-Left
      All y P(c,y) --> P(c,y)
      ----------------------------------             Ex-Left
      Ex x All y P(x,y) --> P(c,y)
      -------------------------------------          Ex-right
      Ex x All y P(x,y) --> Ex x' P(c,y)
      -----------------------------------------      All-right
      Ex x All y P(x,y) --> All y' Ex x' P(x,y)
      --------------------------------------------   =>-Right
      --> Ex x All y P(x,y) => All y' Ex x' P(x,y)

Positive Reductive Sequent calculus: The calculus, where
 * the proof objects are branching tree objects
 * all formulae are sequents
 * the formulae in the initial line is of the form
       premises --> hypothesis
 * the sequent reduction rules are applied to a formula and
   replace it by the result of the rule in the next line
 * the proof object is complete if the last line contains only
   init-elements
 * lemmata may always be added to the antecedent of any
   sequent
 Example: Proof of A/\B => B /\ (C\/A) from no premises
               --> A/\B => B /\ (C\/A)
              ------------------------- =>-Right
                 A/\B --> B /\ (C\/A)
         --------------------------------- /\-Right
          A/\B --> B       A/\B --> C\/A
  /\-Left -----------     ---------------- \/-Right
          A, B --> B       A/\B --> C, A
     init -----------     ---------------- /\-Left
                           A, B --> C, A
                           -------------- init

 A positive reductive sequent proof is just the inverse of a positive
 constructive sequent proof. Implicitly,
 * all sequents are /\-connected
 * all lines are /\-connected
 If one connects the branches by "/\" ,then each line is implied by
 the following line.
 Example: Proof of Ex x All y P(x,y) => All y' Ex x' P(x',y')
      --> Ex x All y P(x,y) => All y' Ex x' P(x',y')
      --------------------------------------------   =>-Right
      Ex x All y P(x,y) --> All y' Ex x' P(x',y')
      -----------------------------------------      Delta-rule
      Ex x All y P(x,y) --> Ex x' P(x',yd-')
      -------------------------------------          Gamma-rule
      Ex x All y P(x,y) --> P(xg',yd-')
      ----------------------------------             Ex-Left
      All y P(c,y) --> P(xg',yd-')
      -------------------------------------          All-Left
      All y P(c,y), P(c,yd-') --> P(xg',yd-')
      -------------------------------------          Instantiate xg'=c
      All y P(c,y), P(c,yd-') --> P(c,yd-')
 The variable-condition is not enlarged by the delta-rule, hence all
 steps are OK.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Disjunctive Sequent calculus
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Conjugate of a formula: If the formula is of the form ~A, then the
 formula A; if the formula is of the form A, then the formula ~A.
 Notation: the formula with a bar above it, here: -A

Disjunctive sequent: A formula of the form
        "-A1, ...-Ak, B1, ...Bm",
 where all components are formulae and where the comma is to be
 understood as a '\/' (Disjunction). This is the disjunctive form of
 the sequent  A1, ... Ak --> B1, ... Bm.

Disjunctive sequent rules: The following reduction rules:
 Alpha-rules:  (non-branching reduction rules)
                      A \/ B
                     --------
                       A, B

                     ~(A /\ B)
                     ---------
                       -A, -B

                     A => B
                     ------
                     -A, B

 Beta-rules: (branching reduction rules)
                    A /\ B
                    ------
                    A ; B

                    ~(A \/ B)
                    ---------
                    -A  ; -B

                    ~(A=>B)
                    -------
                    A ; -B

                    ~~A
                    ---
                    A

 Gamma-rules:  (introducing a gamma-variable xg)
                    Ex x A
                    ------
                    A{x->xg}

                    ~All x A
                    --------
                    ~A{x->xg}

 Delta-rules:  (introducing a delta-variable xd-)
                    All x A
                    -------
                    A{x->xd-}

                    ~Ex x A
                    -------
                    ~A{x->xd-}


Positive reductive disjunctive sequent calculus: The calculus
 where
 * proof objects are branching trees of disjunctive sequents
 * the initial proof object is
      -premise, hypothesis
 * disjunctive sequent rules may be applied
 * the proof is complete if in the last line, every disjunctive
   sequent contains 'true' or a connection
 * lemmata may always be added in negated form to any sequent.
 Example: Proof of A/\B => B /\ (C\/A) from no premises
         A/\B => B /\ (C\/A)
         -------------------
         ~(A/\B), B /\ (C\/A)
         --------------------
      ~(A/\B), B      ~(A/\B), (C\/A)
      ----------      ---------------
      ~A, ~B, B       ~(A/\B), C, A
                      ---------------
                      ~A, ~B, C, A
 The positive reductive disjunctive sequent calculus is a variant of
 the positive reductive sequent calculus. Any complete proof object
 can be transformed to a complete proof object of the positive
 reductive sequent calculus by inserting '-->' and distributing negated
 formulae to the left and non-negated formulae to the right.
 Example: Proof of Ex x All y P(x,y) => All y' Ex x' P(x',y')
      ~ Ex x All y P(x,y) , All y' Ex x' P(x',y')
      -----------------------------------------   Delta-rule
      ~ All y P(xd-,y)    , All y' Ex x' P(x',y')
      -----------------------------------------   Delta-rule
      ~ All y P(xd-,y)    , Ex x' P(x',yd-')        VC:{(xd-,yd-)}
      -----------------------------------------   Gamma-rule
      ~ P(xd-,yg)         , Ex x' P(x',yd-')
      -----------------------------------------   Gamma-rule
      ~ P(xd-,yg)         , P(xg',yd-')
      -----------------------------------------   Instantiate yg=yd-'
      ~ P(xd-,yd-')       , P(xg',yd-')        VC:{(xd-,yd-),(yd-,yg)}
      -----------------------------------------   Instantiate xg'=xd-
      ~ P(xd-,yd-')       , P(xd-,yd-')             VC:{(xd-,yd-),
                                                    (yd-,yg),(xd-,xg')}

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Tableau calculus
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Positive Tree rules: The disjunctive sequent rules.

Negative Tree rules: The reverses of the disjunctive sequent rules.
 Example: The alpha-rule becomes
      A /\ B
      ------
        A,B

Positive Tableau calculus: The reductive calculus, where
 * the proof objects are branching proof trees
 * the first line is of the form
       premises => hypothesis   or    hypothesis
 * a positive tree rule can be applied to any formula of the same
   branch. Alpha-rules create two new lines with their formulae
   while beta-rules produce a pair of two formulae. Gamma- and
   Delta-rules create one more line.
 * the proof object is complete if each branch contains 'true'
   or a connection
 * lemmata may be added as a line anytime, if they are negated
 Example: Proof of A/\B => B /\ (C\/A) from no premises

  1         A/\B => B /\ (C\/A)
  2              ~(A/\B)           alpha-rule from 1
  3            B /\ (C\/A)         alpha-rule from 1
  4                ~A              alpha-rule from 2
  5                ~B              alpha-rule from 2
  6              B    C\/A         beta-rule from 3
  7                    C           alpha-rule from 6
  8                    A           alpha-rule from 6

 Implicitly,
 * the lines are \/-connected
 * the branches are /\-connected
 Consequently, the "contradiction" required to terminate a branch is
 a tautology. A tableau proof is an abbreviation for a sequent proof,
 because it avoids copying identical sub-formulae. Each positive
 tableau proof can be transformed to a dijunctive sequent
 proof: The first line becomes the sequent
    -premises, hypothesis
 Each next line in the sequent proof copies the formulae from its
 predecessor. If two alpha-rules produced two formulae, then the
 sequent proof contains one more line, where the original formula
 has been replaced by its two alpha-components, separated by a comma.
 If a beta-rule split the tree, the sequent proof contains one more
 line with two sequents, one for each branch. Both contain copy the
 whole previous sequent, but each replaces the split formula by one
 of its parts. The last lines of the sequent proof can the easily
 be transformed to init-elements. As a result, each positive tree
 proof can be transformed to a Hilbert proof.
 Example: Proof of Ex x All y P(x,y) => All y' Ex x' P(x',y')
  1   Ex x All y P(x,y) => All y' Ex x' P(x',y')
  2   ~Ex x All y P(x,y)            alpha-rule from 1
  3   All y' Ex x' P(x',y')         alpha-rule from 1
  4   Ex x' P(x',yd-')              delta-rule from 3
  5   ~All y P(xd-,y)               delta-rule from 2 VC:{(yd-,xd-)}
  6   P(xg',yd-')                   gamma-rule from 4
  7   ~P(xd-,yg)                    gamma-rule from 5
  8   P(xd-,yd-')                   instantiated 6
                                      VC:{(yd-,xd-),(xd-,xg')}
  9   ~P(xd-,yd-')                  instantiated 7
                                      VC:{(yd-,xd-),(xd-,xg'),(yd-,yg)}

Negative Tableau calculus: The reductive calculus, where
 * the proof objects are branching proof trees
 * the first line is of the form
       ~(premises => hypothesis)   or    ~hypothesis
 * a negative tree rule can be applied to any formula of the same
   branch. Alpha-rules create two new lines with their formulae
   while beta-rules produce a pair of two formulae. Gamma- and
   Delta-rules create one more line.
 * the proof object is complete if each branch contains 'false'
   or a connection
 * lemmata may be added as a line anytime
 Example: Proof of A/\B => B /\ (C\/A) from no premises

           ~(A/\B => B /\ (C\/A))
                (A/\B)
              ~(B /\ (C\/A))
                  A
                  B
               ~B    ~(C\/A)
                        C
                        A
 This is just a positive tableau-proof, where all formulae have been
 negated. Implicitly,
 * the lines are /\-connected
 * the branches are \/-connected
 Consequently, the "contradiction" required to terminate a branch is
 a real contradiction, implying the falsehood of the negated hypothesis
 -- and thus its valdity. Each negative tableau proof can be
 transformed to a positive tableau proof, and thus to a sequent proof
 and a Hilbert proof.
 Example: Proof of Ex x All y P(x,y) => All y' Ex x' P(x',y')
  1   ~ (Ex x All y P(x,y) => All y' Ex x' P(x',y'))
  2   Ex x All y P(x,y)           alpha-rule from 1
  3   ~All y' Ex x' P(x',y')      alpha-rule from 1
  4   ~Ex x' P(x',yd-')           delta-rule from 3
  5   All y P(xd-,y)              delta-rule from 2  VC:{(yd-,xd-)}
  6   ~P(xg',yd-')                gamma-rule from 4
  7   P(xd-,yg)                   gamma-rule from 5
  8   ~P(xd-,yd-')                instantiated 6
                                      VC:{(yd-,xd-),(xd-,xg')}
  9   P(xd-,yd-')                 instantiated 7
                                      VC:{(yd-,xd-),(xd-,xg'),(yd-,yg)}

Closed Branch, Closure: A branch of a tableau proof tree, which contains
 the same formula twice, once negated and once not negated.

Atomically closed branch, Atomic closure: A branch, which is closed on
 a predicate. If any closure is possible, then closure on the atomic
 level can always be managed.

Strict Tableau Proof: A tableau proof, in which no formula has had an
 expansion rule applied to it twice on the same branch.
 For classical propositional logic, it is never necessary to use a
 formula more than once on any branch. But in FOL, gamma-rules must be
 applicable multiple times in order to ensure completeness.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Natural deduction calculus
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Natural deduction inference rules: The following inference rules:
  /\-introduction:     Z1->A ; Z2->B
                       -----------
                       Z1,Z2 -> A /\ B

 /\-elimination:       Z->A /\ B      Z->A /\ B
                       ---------      ---------
                       Z->A           Z->B

 \/-introduction:       Z->A           Z->B
                       -------        ------
                       Z->A\/B         Z->A\/B

 \/-elimination:       Z->A \/ B ; A->C ; B->C
                       -------------------------
                                Z->C

 All-introduction:     Z-> F{x->xd-}      where xd- is a eigenvariable
                       ----------
                       Z-> All x  F

 All-elimination:       Z-> All x  F
                        ------------
                        Z-> F{x->t}       where t is any term

 Ex-introduction:        Z-> F{x->t}       where t is any term
                         -----------
                         Z-> Ex x F

 Ex-elimination:       Z1-> Ex x F  ;  Z2->F{x->xd-}->C   where xd- is
                       --------------------------------   eigenvariable
                             Z1,Z2->C

 =>-introduction:       A -> B
                        ------
                        A => B

 =>-elimination:        Z1->A ; Z2->A=>B
                        ------------------
                           Z1,Z2->B

 ~-introduction:        A->false
                        --------
                           ~A

 ~-elimination:         Z->A  ; Z->~A
                        --------------
                          Z->false

 Ex-falso-quod-libet:    Z->false
                         --------
                           Z->A

Natural deduction: The positive constructive calculus, where
 * the proof objects are joining tree objects
 * all formulae are sequents with at most one formula in the
   antecedent and at most one formula in the succedent
 * the formulae in the initial line must be of the form
       A -> A
 * natural deduction inference rules are applied to a pair of
   formulae and replace it by the result of the rule in the
   next line
 * the proof object is complete if the last line is of the
   form   premises => hypothesis
 The antecedent of the sequents is usually not written.
 Proof of A/\B => B /\ (C\/A) from no premises
                   A/\B
                   ----
            A/\B    A
            ----   ----
             B     C\/A
            ------------
   A/\B      B /\ (C\/A)
   ---------------------
    A/\B => B /\ (C\/A)

 Each natural deduction proof can be transformed to a positive
 constructive sequent proof and hence to a Hilbert proof.
 Natural deduction was developed by Gerhard Gentzen.
 Example: Proof of Ex x All y P(x,y) => All y' Ex x' P(x',y')
            All y P(c,y)
            ------------
              P(c,yd-)
            -----------
            Ex x' P(x',yd-)
            ---------------
            All y' Ex x' P(x',y')     Ex x All y P(x,y)
            --------------------------------------------
             Ex x All y P(x,y) => All y' Ex x' P(x',y')

Proof in normal form: A natural deduction proof, where all lines in
 the first part are constructed by natural deduction inference rules,
 which introduce an operator. All lines in the second part are
 constructed by rules which eliminate an operator (see the names of
 the rules). Proofs of this kind are also called "intercalation
 proofs", "detour-free proofs" or "roundabout-free proofs". Proofs
 in normal form are minimal in the sense that they no not introduce
 formulae, which they later do not need. A proof in normal form is
 not unique.

Normal form calculus: Natural deduction with the restriction that
 only proofs in normal form are admitted. The normal form calculus is
 complete if and only if the cut-rule of sequent calculus can be
 avoided in general. This is the case if and only if the cut-rule can
 be expressed by other inference rules. Gerhard Gentzen showed that
 this is possible. As a result, each sequent proof can be transformed
 to a sequent proof without the cut-rule. Hence, each Natural Deduction
 proof can be transformed to a proof in normal form. By this fact, one
 can proove the consistency of natural deduction.

Law of the excluded middle: The theorem P \/ ~P.

Law of double negation: The theorem P <=> ~~P.

Law of contradiction: The theorem (~A => false)=> A.

Classical logic: The logic where the law of the excluded middle, the
 law of double negation or the law of contradiction hold, which are
 all equivalent.

Intuitionistic Logic: The logic where the law of double negation
 (and hence the law of the excluded middle and the law of
 contradiction) do not hold. In classical logic, ~P means that P is
 false. As a result, ~~P=>P is a theorem, because if it is not true
 that P is false, then is true. In the intuitionistic logic, ~P means
 that P cannot be proved. As a result, ~~P=>P is not a theorem
 (cannot be proven), because if there is no proof stating that P
 cannot be proven, this does not mean that P has a proof. Each
 calculus can choose to be either classical or intuitionistic by
 accepting inference rules or reduction rules mirroring one of the
 three laws mentioned above.
 // From: Wikipedia "Intuitionistic Logic"


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Matrix calculus
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Problems of sequent calculus: The following disadvantages:
 * Notational redundancy
   Each line in a sequent proof repeats formulae of the previous line
 * Irrelevance
   Some formulae carried around in a sequent are not used for the
   proof. Eventually, one tries to prove these sub-formulae, although
   the real proof can work without them.
   Example: Positive reductive Disjunctive sequent proof:
               A, ~B, B
   One might try to prove A, although this is completely useless.
 * Non-permutability
   It is not possible to permute the order of applied beta-rules
   afterwards.

Matrix: A FOL-formla, in which the only built-in symbols are "Ex",
 "All", "/\", "\/" and "~". "~" may only occur before atomic terms.
 Each formula can be transferred to a matrix by the FOL-rewrite rules.
 A matrix is mostly noted by writing all \/-connected terms beneath
 each other and all /\-connected terms above each other. Negations
 are expressed by the polarity. Binders are put in superscript before
 their sub-formulae.
 Example:
     _                  _
    |        _  _        |
    | All x | A+ |       |    =   (All x (A /\ ~B)) \/ C
    |       |_B-_|  C+   |
    |_                  _|

Path in a matrix M:
 * If M is atomic, then M
 * If M is of the form "A \/ B" then a path in matrix A, concatenated
   with a path in matrix B
 * If M is of the form "A /\ B" then a path in matrix A or a path in
   matrix B
 * If M is of the form "BINDER x A" then the sequence of "BINDER x",
   concatenated with a path in A
 In the matrix notation, a path corresponds to a line in the matrix,
 which touches each element of those standing beneath each other and
 which touches only one element of those standing above each other.
 Example: In the above matrix, there are two possible paths:
  All x A+,C+   and  All x B-,C+

Closed path in a matrix: A path containing a connection.

Positive matrix calculus: The calculus, where
 * the proof object is a matrix
 * the proof starts with the matrix of
         premises => hypothesis
 * no inference rules are applied
 * the proof is considered complete if all possible paths in the matrix
   are closed.
 Example: Matrix proof of A/\B => B /\ (C\/A)
                      <=> ~(A/\B) \/ (B /\ (C \/ A))
                      <=> ~A \/ ~B \/ (B /\ (C \/ A))
                             _                  _
                            |          _     _   |
                            |         | B+    |  |
                            | A-  B-  |_C+ A+_|  |
                            |_                  _|
 The proof is complete, because every path is closed:
    A- B- B+
    A- B- C A
 The matrix calculus is an abbreviation of the tableau calculus, which
 checks all branches simltaneously. Each complete matrix proof object
 can be transferred to a complete positive tableau proof tree as
 follows: Reorder the matrix such that the simple components (atomic
 formlae, sub-matrices with simple components) stand to the left. Write
 the whole matrix (in form of a formula) as a line. Now start from the
 left in the matrix and scan all \/-connected sub-formulae (i.e all
 those standing beneath each other). Put every atomic formula you meet
 as a single line, expanding negative polarities to negation. If you
 meet a /\-sub-term (i.e. matrices standing above each other), write
 the /\-sub-term as a line. Then expand each of the sub-matrices
 recursively to a tableau-tree and attach them as children to the tree.
 Continue like this in the original matrix, adding any lines you create
 to all leaves of the tree.
 Example:
            ~A \/ ~B \/ (B /\ (C \/ A))       // write as line
            ~A                                // tree of A-
            ~B                                // tree of B-
            B /\ (C \/ A)                     // line for B/\(C\/A)
          B                                      // tree of B
                  C \/ A                         // tree of C\/A
                     C                              // tree of C
                     A                              // tree of A
 // For proofs with existential and universal binders, gamma- and
 // delta-variables have to be introduced. It is also possible to
 // do negative matrix proofs, where /\-connected components are
 // placed above each other and \/-connected components are placed
 // beneath each other. These details have not been dealt with in
 // the course.


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Induction
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Inductively defined universe: A universe, which is defined by
 sorts and constructors (i.e. recursively).

Inductively valid formula: A formula, which is valid in inductively
 defined universes.

Sort of natural numbers: The type symbol N with the constant symbol 0
 of N and the constructor s:N -> N.

Peano's Axioms: The following axioms for the sort of natural numbers
  nat2: All x  s(x)!=0
        i.e. the natural numbers are 0, s(0), s(s(0)) etc.
  nat3: All x All y (s(x)=s(y) => x=y)
        i.e. all natural numbers are different
  S:    P(0) /\ All y (P(y) => P(s(y)) => All x P(x)
        where P is any predicate
        i.e. any other property of natural numbers can be derived

Inductive theorem proving, Noetherian Induction: Using the following
 theorem in a proof
     (N):  well-founded(<) /\ All v ( (All u (u<v=>P(u))) => P(v) )
                                => All x P(x)
 This is the generalization of the usual induction: If I have any
 well-founded relation '<' and I know that P(v) if all predecessors
 u have P(u), then P holds for all x. Note that this is a theorem
 and not an axiom, i.e. it can be proved (?).

Counter-example of a universally quantified hypothesis: An
 instantiation of the universally quantified variable, which makes the
 hypothesis invalid.

Proof of a hypothesis by descente infinie: Showing that for every
 counter-example of the hypothesis there is a counter-example, which
 is smaller in the sense of a well-founded ordering. Since one cannot
 go for ever towards smaller elements in a well-founded ordering, this
 implies that there cannot be any counter-example. This proof is
 usually carried out as follows: One wants to prove a hypothesis A.
 One applies reduction rules and finds for instance that
 (X /\ Y /\ Z) => A. One can prove X and Y and one sees that Z is a
 somehow smaller instance of A. I.e. one is left with proving Z=>A.
 One transforms this by contraposition to ~A=>~Z and says by descente
 infinie: Assume there was a counter example ~A. Then there is a
 counter-example ~Z, which is smaller. It remains to show that the
 ordering, in the sense of which ~Z is smaller than ~A, is
 well-founded.
 Example: Proof of 0+x=x
  Assume there was a counter-example x,such that 0+x != x.
  Then x!=0, because 0+0=0. Since x!=0, there is a predecessor y
  of x in the natural numbers. If s:Natural->Natural denotes the
  successor function on the natural numbers, then we have
      0+s(y)=s(y)  is a counter-example
  <=> s(0+y)=s(y)  is a counter-example
  <=>   0+y = y    is a counter-example
  Now define the "weight" of this counter-example as being the value
  y. Then the weight of the new counter-example is smaller than the
  weight of the original countr-example in the sense of '<'. '<' is
  a well-founded ordering. Thus, a counter-example cannot exist.
 Example: Proof of the irrationality of sqrt(2)
  Assume there were natural numbers n and m, such that sqrt(2)=n/m
  Then m^2 = n^2/2
  (?)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Quodlibet
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

// The following sections only provide an incomplete and unstructured
// overview over the programs covered in the lecture.

Modeling of partial functions: Making partial functions total functions
 by introducing error elements, to which the function maps if it is
 undefined.
 Example: Introduce the element "onebyzero". Then the division function
 "/" simply returns: 1 / 0 = onebyzero.

Algebra: A structure, which does not have any predicates, but just
 equality.

Constructor variable: A variable, which is to be valuated to a
 function, to which also a constructor is valuated (?).

Constructor term: A term consisting of constructors and variables.

Constructor substitution: A substitution, which maps a constructor
 variable to a constructor term.

Inductive substitution: A constructor substitution, which is total on
 the constructor variables and which, if applied to a variable, yields
 a term without constructor variables.

Conditional function symbol definition: A term of the form
    f(a,b) := <term>    <-  <condition on a and b>
 where f is the function symbol being defined and a and b are free
 variables. This definition means: If the condition on the variables
 is fulfilled, then f(a,b) takes the value indicated by the term.
 It is furthermore required that
 * f may not be a constructor symbol
 * no variable has multiple occurences in f(a,b)
 * the condition must be a conjunction of terms of special forms

General hypothesis: A hypothesis involving many universally quantified
 variables.

Problem of generalization: The problem of finding a slightly more
 general hypothesis, which implies the original hypothesis, but is
 easier to prove.
 Example: In LISP, be the hypothesis
            append(l,append(l,k))=append(append(l,l),k)
          It turns out that it's easier to prove
            append(l,append(m,k))=append(append(l,m),k)


~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Omega
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Program: An algorithm, which can be executed by a compter.

Theorem prover: A program for finding proofs for hypotheses.
 // Strictly speaking, the notion "theorem prover" is mislading:
 // Theorems need not to be proven, since they are already proven.
 // Otherwise, they would not be theorems.

Omega: A certain human-oriented theorem prover. Its interface shows
 * the proof tree
 * the proof in the reductive sequent calculus
 * a "pretty print window", displaying the current formula nicely
 * an output window

White-box-inclusion: The principle of using the results of external
 theorem provers, but checking their proof by one's own means. The
 external provers are used to find the proof, but the proof is then
 transformed to a proof object in the own representation. This
 corresponds to the principle "use but do not trust".

Mathematical database: A collection of mathematical theorems.
 There exist large mathematical databases, but every research group
 develops its own mathematical database for its own theorem prover.
 This is a huge waste of work.

Tactic: A sequence of inference rules or reduction rules. A tactic is
 a shortcut for often-used sequences of rules.
 Example:  All x All y All z P(x,y,z)
              allows to infer
                P(c1,c2,c3)
  There are 3 applications of an inference rule needed, which can be
  abbreviated to a tactic named for instance "All*".

Method: A tactic together with two sets of conditions, called
 preconditions and postconditions. The preconditions state when the
 tactic is applicable. The postconditions state what conditions will be
 fulfilled after the tactic has been applied. By methods, a theorem
 prover can estimate the applicability and the use of a tactic.

PAI, partial argument instantiation: The instantiation of some, but not
 all variables of a formula.

Agent: A very small program, which is executed independently from other
 programs.

Agent-oriented theorem prover: A theorem prover, which involves agents,
 which run through the proof object and search for positions where
 the preconditions of tactics are fulfilled. Each tactic also has an
 agent, which applied the tactic if the other agent found that all
 preconditions are fulfilled.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
               Prex
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

NLG, Natural Language Generation: The production of text in a human
 language. The general architecture of NLG is as follows:
    non-linguistic input
   _______|_______
  | Macroplanner  |    produces semantic representation
  |_______________|      Content determination, rhetorical structure
          |               also called Dialog planner
   Discourse plan
   _______|_______
  | Microplanner  |    does the sentence planning
  |_______________|      Segmentation, Referring, Aggregation
          |                also called sentence planner
   Linguistic specification
   _______|_______
  | Realizer      |    produces the real text
  |_______________|
          |
   Natural language output

Content determination: The choice of the information to be
 represented, with respect to
 * the communicative goal
 * the audience
 * certain constraints (space etc.)
 * the underlying information source

Rhetorical structure: The relations between pieces of information in a
 sentence.

Segmentation: The grouping of pieces of informations. The groups are
 called "constituents". Segmentation can be done on several levels.

Aggregation: The merging of pieces of information. There are different
 rules of how to aggregate information.
 Example: Dogs are mammals. Cats are mammals. ---->
          Dogs and cats are mammals.
 Example: a => b   and   a=>c ~~~~~~>
          a => b and c

Ordering: The linearization of the pieces of information into a
 sequence.

Referring expressions: The reference to concepts and entities in a
 text. This is usually done by introducing names for concepts or by
 using pronouns.

Lexicalization: The mapping from concepts to  syntactic structure
 (words).

Linguistic realization: The mapping from linguistic specification
 to surface text.

Prex: A certain program, which translates a proof tree to natural
 language. It has the following architecture:
     Proof <------->    Dialog Planner    <---------> User Models
                        |            ^
                  Sentence planner   |
                        |            |
                     Realizer    Analyzer
                        |            |
                        V            |
                        User Interface

 * Allows logical reprsentation of proofs
 * Usermodeling and dialog planing in a uniform framework
 * Plan-operators, dialog-driven adaptation to user

Discourse structure: The structure of communication. Basic model:
 A tree with
 * its subtrees being the "segments"
 * its the leaves being the minimal elements of communication, called
   "messages"
 * highlightes subtrees, called "attentional frames", which model
   the focus of attention

Speech act:
 * Mathematics Communicate Act (MCA)
   Verbalization of mathematical concepts
 * Interpersonal communicative Act (ICA)
   Needed in dialogs

User interactions in P.rex:
 * "Too detailed"
   Then P.rex chooses a higher level of abstraction
 * "Too difficult"
   Then P.rex checks whether the premises are understoood and if
   the proof can be represented on a lower level of abstraction
 P.rex memorizes these answers in its user model and produces
 the adequate level of abstraction automatically next time.

Textstructure in P.rex:
 * ideational dimension: Upper Model (Ontology tree)
 * Textual dimension: Textual semantic categories
     Syntax tree non-terminals

Resource tree: Syntax tree of a constituent (?).

Lexicalization in Prex: Mapping of content to a resource tree in two
 stages:
 * Mapping the content to upper model objects
        parallel(C1,C2) ~~~~~~~~>   property-relation(parallel,C1,C2)
 * Mapping the upper model object into the resource tree
     property-relation(parallel,C1,C2) ~~~~~>  np[parallel,conj[C1,C2]]


Surface realization in P.rex: Tree Adjoining Grammars. That is: The
 construction of sentences by the following syntax trees
 * initial trees, describing the phrase structure
 * auxiliary trees, which have a foot node equal to the root node and
   which can be plugged into initial trees


Progressive refinement: The following process for the development of
 software:
            Modeling
           ^         |
           | |       |
           | V       V
      Empirical      Partial
      simulation  <- implementation
      studies

Wizard-of-Oz-Expriment: An experiment, where the subjects interact
 with a computer, but where the responses of the computer are
 controlled secretly by a human.

DiaWoz: (?)

Plan-operators: Operators to assemble the MCAs of the textbook-proof.
 Example: If the goal is to show Z and we have the rule
             R: A, B, C => Z
          and this rule is the most abstract rule known to the user,
          then produce the MCA
             derive(Reasons(A,B,C),Conclusion(Z),method(R))

Assertion: An axiom, a lemma, a theorem or a definition. An assertion
 entails multiple inference rules.
 Example: Def<:  All S1 All S2  (S1 < S2 <=> (All x x in S1 => x in S2))
  This entails:      F < G   a in F
                    ----------------
                       a in G

                    F < G    a not in G
                    -------------------
                       a not in F

                    a in F    a not in G
                    --------------------
                       not F < G

 The entailed inference rules can be proven (e.g. by natural deduction)
 and thus be used in a proof.

Tramp: A certain program, which can translate proofs in any format at the
 assertion level to natral deduction proofs. Tramp provides the interface
 between Omega and other theorem provers.

Intelligent tutoring system:
 Problem with conventional systems: Intelligent tutor systems only have
   static and precompiled knowledge, they compar the student's answers
   to what is stored as a solution. As a consequence, alternative
   solutions are rejected.
 Architecture with P.rex:

              linguistic system
   User
                knowledge bases
               (User, pedagogical, mathematical)

       learing environment            mathematical assistant
       (Activemath)                       (Omega)

Requirements for Tutoring:
 * Domain Ontology (Mathmatical concepts, proofs tc.)
 * Student answer categories
   Relevance, Completeness, Accuracy, Finegrainedness
 * Hint taxonomy
   Type and amount of information given away or hidden
 In a tutoring system, the proof mnager and the dialog manager
 work together.

Proof representation language: The proof representation used by the
 tutoring system. This language
 * encodes the proof formally and at the same time close to the
   original text
 * represents underspecifications

Proof checking rules: Rules which decide whether a proof in the proof
 representation language is valid.
 The proof checking rules
 * provide the semntics of the proof representation language
 * make the context of the proof explicit
 * provide means for resolving underspecifications
 * verify the validity of proof steps

Underspecification: The phenomenon that human beings do not explicitly
 state necessary information. In theorem proving, this includes:
 * forward vs backward step
 * references to used assertions
 * instantiations of quantified variables
 * positions of considered subformulae
 In this case, the tutoring system has to keep all options open and
 deduce at run-time what was meant.

Didactic strategy: Teaching everything in a monologue.

Socratic strategy: Have the student find the proof by her/himself.
 This involves giving hints if the student does not find the answer.
 If the student still does not find the answer, switch to didactic
 strategy. Later switch back to socratic strategy.

Act-R: A framework for user modeling, dialog planning nd dialog
 history. Act-R consists of
 * a cognitive architecture, modeling the human cognition
 * declarative knowledge: working memory
 * procedural knowledge: production rule base (?)
 * a goal stack