Summary Humanoriented Theorem Proving
(c) 20040424 Fabian M. Suchanek
http://suchanek.name
This is a summary of the first part of the course "Humanoriented
TheoremProving" held by Dr. ClausPeter Wirth in the WS 2003 at
Saarland University. Its topics are:
* Sets * Proofs * Sequent calculus
* Tuples * FirstOrderLogic * 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 wellfounded
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 questionmarks in this
summary. Furthermore, Dr. ClausPeter 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.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 superset of a set S: A superset 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".
//
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 1based.
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
onewaystreets. 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}
DomainRestriction, 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}
Rangerestriction 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: R := ran(domrestr(R,A'))
= {b  Ex (a,b) in R, a in A'}
= proj[2](R /\ (A' x B))
ReverseImage 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 := 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 onewaystreets, 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 n1, composed with R
R^n := R^(n1) 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).
Antisymmetric 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.
//
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: '='
Quasiordering: A transitive and reflexive relation.
Reflexive ordering, partial ordering: An antisymmetric quasiordering.
That is: A reflexive, antisymmetric 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.
Wellfounded relation on a set A': A relation R on a set A, such that
every nonempty set 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.
Truthvalue, 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 0ary function to T.
Operation: A 2ary function. One defines
a f b := f(a,b) "InfixNotation"
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
Rightassociative operation: An operation f, for which
a f b f c = a f (b f c).
Leftassociative 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 n1 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.
DecisionProblem: 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
decisionproblems.
// ...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'.
Semidecidable 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.
Cosemidecidable 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.
SemidecidabilityTheorem: The fact that every problem, which is
semidecidable and cosemidecidable is also decidable. Proof: The
deciding algorithm is the following: Run the semideciding and the
cosemideciding algorithm. Report the result of whoever terminates
first. Vice versa, every decidable problem is semidecidable and
cosemidecidable.
EnumerabilityTheorem: The fact that every problem is semidecidable
iff its solution is countable.
Proof: Suppose the solution is countable. Then there exists an
algorithm which semidecides 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 semideciding
algorithm, then the solution set must be countable: (?)
Halting problem: The problem of deciding whether an algorithm
terminates. This problem is not cosemidecidable 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 superset 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.
Kleeneset of an alphabet S: The set of all sequences over S.
Notation: S* := {  s[1],...s[i] in S, i=1,2,3,...}
Language over an alphabet S: A subset of the Kleeneset of S.
Rewriterule 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: >
Grammar: A tuple of
* an alphabet N of "nonterminal symbols"
* an alphabet T of "terminal symbols"
* a set of rewriterules '>' over N \/ T
* a "startsymbol" s0 of N
N and T must be disjunct. The left sides of the rewriterules must
contain at least one nonterminal 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 rewriterules 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 rewriterules. 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 subterms.
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.
Welltyped term:
* a variable OR
* a constant OR
* a term starting with a function symbol, where the arguments of
the function symbol are welltyped terms of the type symbols
required by the function symbol
We will assume all terms to be welltyped.
Higherorderlanguage: A language which allows variables of function
symbol types.
Builtin 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 "builtin symbols".
Signature of a formula language: The set of its type symbols, its
function symbols and its constant symbols, without its builtin
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 SigmaStructure.
// 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/leftassociativity or precedence), then this causes the
evaluationfunction to treat terms of this new notation like
the corresponding term of the old notation.
Math language: The formula language comprising the builtin 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'
builtin.
It has to be taken care that the sets of wellformed formulae, types
and terminal symbols be countable and decidable.
Formula of a logic: A term of type symbol 'o'.
Twovalued logic: A logic where 'o' is the Boolean type.
This course only deals with twovalued logic. For multivalued 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
successorfunction.
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 predecessorfunction is a
destructor.
Signature of a Logic: The set of its type symbols, its
function symbols and its constant symbols, without its builtin
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 nonempty 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
nonempty formulae.
Save inference rule, save reduction rule, Rewriterule: A relation
between formulae, which are equivalent. Rewriterules are
nonweakening nonjoining inference rules and nonstrengthening
nonbranching 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 proofobject
by a lemma. This can be done during the process of finding a proof.
The lemma may then be inserted into the proofobject 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 semidecidable, i.e. there is an algorithm which says "Yes"
if the formula is valid. But it is not cosemidecidable, i.e. there
cannot exist an algorithm which says "No" if the formula is not valid.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
FirstOrderLogic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Propositional logic: The logic with the following builtin 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 builtin:
true : o
false : o
No variables are allowed. No constant symbols are allowed. No
function symbols are allowed, except for 0ary predicate symbols.
FOL, Firstorderlogic: 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.
Firstorderlanguage: 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 firstorderlanguage: A structure of this language. This
structure is often split into
* a nonempty 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 firstorderlanguage" 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 firstorderlanguage" suffices
// fully and is also welldefined.
FOL Rewriterules: 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 rewriterules.
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 FOLterm T: The FOLterm
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
The evaluation of this lambdaterm is a function, which takes one
argument and returns the , where the has been
replaced by the argument. By Currying, lambdaterms can represent
functions with more arguments.
Notation: LAMBDA is a small greek lambda.
AlphaRenaming: 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})
Betareduction: A relation on terms, which causes the application of a
lambdaterm. Betareduction is confluent and terminating.
Notation: (LAMBDA x term) argument beta>
term { x > argument }
Betareduction cannot be applied, if
* the contains a binder on a variable z AND
* x occurs in the scope of this binder AND
* z occurs freely in
Example: (LAMBDA x (All z: x)) z /beta> All z: z
We need alpharenaming in this case:
(LAMBDA x (All z: x)) z alpha>
(LAMBDA x (All y: x)) z beta>
All y: z
Etareduction: A relation on terms, which allows the skipping of wrapper
LAMBDAbinders. Etareduction is confluent and terminating.
Notation: (LAMBDA x (f x)) eta> f
BetaEtaReduction: The union of betareduction and etareduction.
AlphaBetaReduction: The cartesian product of alpharenaming and
betareduction. (?) That is: First, alpharenaming is carried out and
then betareduction is done. Since often, alpharenaming is a
necessary precondition for betareduction, and since a superfluous
alpharenaming does not harm, we talk of alphabetareduction
when we mean a carefully applied betareduction.
AlphaBetairreducible 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 lambdabinder is allowed.
* predicates are used in their curryed version. Predicates may be
given by lambdaterms.
* the types include function types, i.e. predicates and functions
may be given by variables.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Semantics
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
gvariant 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 builtin 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 subscript
Model of an ILformula F: An interpretation I, for which
eval(I)(F)=true.
Semantically valid ILformula: 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)
Explicitnesslemma: 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)
Substitutionlemma: 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 svariant 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 builtin
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 builtin function symbols:
LAMBDA x term (Lambdabinder)
Q: alpha > alpha > o (equality, for any type alpha)
iota : (i > o) > i (iotabinder)
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 curryingnotation 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 functionvariables 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 deMorganrule
\/ := 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 functiontypes
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 lambdaterm 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 lambdaterm 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 Q0formulae
* 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 explicitnesslemma holds
* The substitutionlemma 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 superset of FirstOrderLogic
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 truthvalue.
Alphaequality: The alpharenaming relation, considered as equality. (?)
That is: Two terms with an equal structure are considered equal.
Primitive equality: The equality builtin 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 Leibnizequality.
Functionalextensional 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)))
Leibnizequality implies functionalextensional equality.
Betaequality: The relation of betareduction, considered as equality.
That is: A lambdaterm applied to an argument is considered equal to
its result.
fprinciple: The principle that
All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) => f=g)
This is the Functionalextensional equality.
(So what is it good for (?))
etaprinciple: The principle that
All f[ba] ( (LAMBDA x[a] (f x)) = f )
This means that a LAMBDAwrapper can be left away.
xiprinciple: (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 etaprinciple. If one accepts
betaequality, then it holds that the fprinciple is the same as
the etaprinciple together with the xiprinciple. Proof:
If one has the fprinciple, then one can show the etaprinciple by
// fprinciple
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
// Betareduction
(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 etaprinciple, one can show the xiprinciple by
// fprinciple
All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) => f=g)
// Plug in the etaprinciple
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 xiprinciple, one can show the
fprinciple by
// xiprinciple
All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) =>
( (LAMBDA x (f x))= (LAMBDA x (g x)) ))
// Plug in the etaprinciple
All f[ba] All g[ba] ((All x[a] (f(x)=g(x)) =>
( (LAMBDA x (f x))= (LAMBDA x (g x)) ))
Choicefunction: 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)) )
PredicateDescriptor: 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 PredicateDescriptor 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.
Choiceset: 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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Polymodal Logic: The firstorder 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
Multimodal logic: Polymodal 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 polymodal 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 ExplicitnessLemma and the
SubstitutionLemma.
Monomodal Logic, Modal logic: A restriction of polymodal logic, where
the AllWorldbinder, the SomeWorldbinder 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 worldbinder 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 monomodal 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 lefthandside of the implication says that the extensions of h
and p are the same in our world. This is true. The righthandside
says that the extensions are equal in all worlds  which is false.
Hence the implication evaluates to false. If we quit monomodal
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 lefthandside of the implication becomes true. At the
same time, the subterm "(h(wd) = p(wd))" on the righthandside
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 righthandside, 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
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Deltaminusvariable, Eigenvariable: A free variable, which may not
appear more than once. The set of all deltaminusvariables of a
term t is noted Vd(t).
Gammavariable: 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. Gammavariables 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 gammavariables have been
instantiated. The set of all gammavariables of a term t is noted
Vgamma(t).
// A gammavariable is also called "Metavariable". Mr Wirth does not
// like this notion, because he sees gammavariables 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'.
Deltaplusvariable: A gammavariable, which has a condition
associated. It may only be instantiated by a constant fulfilling this
condition. The set of all deltaplusvariables in a formula t is noted
Vd+(t).
Alpharule: A nonbranching reduction rule, which does not introduce
new variables.
Betarule: A *b*ranching reduction rule.
Gammarule: A reduction rule, which introduces a gammavariable from
an existentially quantified formula.
Deltaminusrule: A reduction rule, which introduces a deltaminus
variable from a universally quantified formula.
Liberalized deltarule, Deltaplusrule: A reduction rule, which
introduces a deltaplusvariable from a universally quantified
formula.
Choicecondition: The relation between deltaplusvariables and
their conditions. If a deltaplusrule is applied to
All x A
and intrduces the deltaplusvariable xd+, then the choice condition
stores (xd+,~A{x>xd+}). That is: The newly introduced deltaplus
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 deltaplusrule
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 subformula: The number of
times where gammavariables have been introduced from this formula.
One can imagine this as making multiple copies of the fomula and then
introducing gammavariables. Increased multiplicity is for instance
necessary to prove:
All x P(x) => (P(a) /\ P(b)) Apply rewriterules
Ex x ~P(x) \/ (P(a) /\ P(b)) Apply gammarule
~P(xg) \/ (P(a) /\ P(b))
Instantiating xg with a would help. But xg also needs to be
instantiated to b! Positive proofs instantate gammavariables, because
existentially quantifieds terms result from a universally quantified
term in the premise.
Skolemization: The transformation of a FOLformula as follows:
Ex x All y P(x,y) ~~~~~~> All y' Ex x P(x,y'(x))
where y' is a function variable, called SkolemFunction. Skolemization
moves the Allquantifiers 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 FOLformula as follows:
All x Ex y P(x,y) ~~~~~~> Ex y' All x P(x,y'(x))
where y' is a function variable, called RaisingFunction. 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 (?)
Variablecondition: 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 gammavariables needs a variablecondition,
which is empty in the beginning. With every application of a
* deltarule x>eigenvariable, the variablecondition needs to
be extended by
{ (z,eigenvariable)  z is a gammavariable or a
deltaplusvariable in the whole formula}
* deltaplusrule x>eigenvariable, the variablecondition needs to
be extended by
{ (z,eigenvariable)  z is a gammavariable or a
deltaplusvariable in the
quantified subformula}
Furthermore, the Choicecondition is updated by
{ (eigenvariable,term) }
where "term" is the quantified subterm.
* substitution freegammavariable > term
{ (z, freegammavariable)  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 gammavariable
xg = yd where yd is a deltavariable
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 deltavariable
the variablecondition is still empty
xd = yg where yg is gammavariable
Now, we may instantiate yg>xd and get a complete proof.
In general, the variablecondition is a hindrance in proving,
because it prevents one from instantiating the gammavariables
deliberately. This is where deltaplusvariables 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 gammavariable
Assume we choose a deltarule:
~P(yd), P(xg) where yd is a free deltavariable
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 deltaplusrule:
All y ~P(y) \/ P(xg)
~P(yd+) \/ P(xg) with choicecondition {(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 gammavariable
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 deltavariable
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 deltarule in a proof.
That is: By introducing a gammavariable, store in the variable
condition on which gammavariables it depended.
// Better use the description in "variablecondition" and drop this.
Rcondition: The demand that a variable condition must be wellfounded
(i.e. acyclic). The proof is sound iff the Rcondition is fulfilled.
This is because a pair (x,y) in the variablecondition 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.
Rsubstitution for a variable condition R: A substitution s, such that
R \/ E(s) \/ U(s)
is wellfounded (i.e. acyclic).
(S,R)valuation: A function which takes a gammavariable and a partial
valuation for free deltavariables 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 gammavariables. In order to do so, it
may read the values of the deltavariables, which the gammavariable
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 gammavariables taken by e and
the deltavariables being read by e. It is required that
R \/ S(e)
be wellfounded, i.e. the valuation may only read deltavariables,
which are older than the gammavariable.
Deltaset of a semantical relation S(e) for a gammavariable x: The
set of those deltavariables, 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 deltaset. In this case, e is called "semantical".
Epsfunction: The function eps, which takes an (S,R)valuation e, a
valuation d for deltavariables 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 deltavariables.
Rvalid 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 deltaplusvariables.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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 higherorderlanguages, 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 FirstOrder 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 Aformula
is replaced by a 'true' and a missing Bformula 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 subsequences 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)
FalseLeft: 
X, false > Y
TrueRight: 
X > true, Y
NegationLeft: X > Y, A

X, ~A > Y
NegationRight: 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
AllLeft: X, All x A, A{x>t} > Y (weakening)

X, All x A > Y
AllRight: X > Y, A{x>t} (when used in
 reduction, t is a
X > Y, All x A deltaminusvariable)
ExLeft: X, A{x>t} > Y (weakening)

X, Ex x A > Y
ExRight: X > Y, Ex x A, A{x>t} (weakening)
 (when used in
X > Y, Ex x A reduction, t is a
gammavariable)
CutRule: A > B,C ; A,B > C

A > C
Sequent reduction rules: The reverse of the sequent inference rules.
Hence, the notions of "alpharules", "betarules", "gammarules" and
"deltarules" become applicable.
Initelement: 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 initelements
* 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)
 AllLeft
All y P(c,y) > P(c,y)
 ExLeft
Ex x All y P(x,y) > P(c,y)
 Exright
Ex x All y P(x,y) > Ex x' P(c,y)
 Allright
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
initelements
* 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')
 Deltarule
Ex x All y P(x,y) > Ex x' P(x',yd')
 Gammarule
Ex x All y P(x,y) > P(xg',yd')
 ExLeft
All y P(c,y) > P(xg',yd')
 AllLeft
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 variablecondition is not enlarged by the deltarule, 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:
Alpharules: (nonbranching reduction rules)
A \/ B

A, B
~(A /\ B)

A, B
A => B

A, B
Betarules: (branching reduction rules)
A /\ B

A ; B
~(A \/ B)

A ; B
~(A=>B)

A ; B
~~A

A
Gammarules: (introducing a gammavariable xg)
Ex x A

A{x>xg}
~All x A

~A{x>xg}
Deltarules: (introducing a deltavariable 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 nonnegated 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')
 Deltarule
~ All y P(xd,y) , All y' Ex x' P(x',y')
 Deltarule
~ All y P(xd,y) , Ex x' P(x',yd') VC:{(xd,yd)}
 Gammarule
~ P(xd,yg) , Ex x' P(x',yd')
 Gammarule
~ 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 alpharule 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. Alpharules create two new lines with their formulae
while betarules produce a pair of two formulae. Gamma and
Deltarules 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) alpharule from 1
3 B /\ (C\/A) alpharule from 1
4 ~A alpharule from 2
5 ~B alpharule from 2
6 B C\/A betarule from 3
7 C alpharule from 6
8 A alpharule 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 subformulae. 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 alpharules produced two formulae, then the
sequent proof contains one more line, where the original formula
has been replaced by its two alphacomponents, separated by a comma.
If a betarule 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 initelements. 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) alpharule from 1
3 All y' Ex x' P(x',y') alpharule from 1
4 Ex x' P(x',yd') deltarule from 3
5 ~All y P(xd,y) deltarule from 2 VC:{(yd,xd)}
6 P(xg',yd') gammarule from 4
7 ~P(xd,yg) gammarule 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. Alpharules create two new lines with their formulae
while betarules produce a pair of two formulae. Gamma and
Deltarules 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 tableauproof, 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) alpharule from 1
3 ~All y' Ex x' P(x',y') alpharule from 1
4 ~Ex x' P(x',yd') deltarule from 3
5 All y P(xd,y) deltarule from 2 VC:{(yd,xd)}
6 ~P(xg',yd') gammarule from 4
7 P(xd,yg) gammarule 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, gammarules 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
Allintroduction: Z> F{x>xd} where xd is a eigenvariable

Z> All x F
Allelimination: Z> All x F

Z> F{x>t} where t is any term
Exintroduction: Z> F{x>t} where t is any term

Z> Ex x F
Exelimination: 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
Exfalsoquodlibet: 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", "detourfree proofs" or "roundaboutfree 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 cutrule of sequent calculus can be
avoided in general. This is the case if and only if the cutrule 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 cutrule. 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 subformulae, 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.
* Nonpermutability
It is not possible to permute the order of applied betarules
afterwards.
Matrix: A FOLformla, in which the only builtin symbols are "Ex",
"All", "/\", "\/" and "~". "~" may only occur before atomic terms.
Each formula can be transferred to a matrix by the FOLrewrite 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 subformulae.
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, submatrices 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 subformulae (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 /\subterm (i.e. matrices standing above each other), write
the /\subterm as a line. Then expand each of the submatrices
recursively to a tableautree 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
// deltavariables 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): wellfounded(<) /\ All v ( (All u (uP(u))) => P(v) )
=> All x P(x)
This is the generalization of the usual induction: If I have any
wellfounded 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 (?).
Counterexample 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
counterexample of the hypothesis there is a counterexample, which
is smaller in the sense of a wellfounded ordering. Since one cannot
go for ever towards smaller elements in a wellfounded ordering, this
implies that there cannot be any counterexample. 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
counterexample ~Z, which is smaller. It remains to show that the
ordering, in the sense of which ~Z is smaller than ~A, is
wellfounded.
Example: Proof of 0+x=x
Assume there was a counterexample 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 counterexample
<=> s(0+y)=s(y) is a counterexample
<=> 0+y = y is a counterexample
Now define the "weight" of this counterexample as being the value
y. Then the weight of the new counterexample is smaller than the
weight of the original countrexample in the sense of '<'. '<' is
a wellfounded ordering. Thus, a counterexample 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) := <
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 humanoriented 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
Whiteboxinclusion: 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 oftenused 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.
Agentoriented 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:
nonlinguistic 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
* Planoperators, dialogdriven 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 nonterminals
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) ~~~~~~~~> propertyrelation(parallel,C1,C2)
* Mapping the upper model object into the resource tree
propertyrelation(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
WizardofOzExpriment: An experiment, where the subjects interact
with a computer, but where the responses of the computer are
controlled secretly by a human.
DiaWoz: (?)
Planoperators: Operators to assemble the MCAs of the textbookproof.
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 runtime 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.
ActR: A framework for user modeling, dialog planning nd dialog
history. ActR consists of
* a cognitive architecture, modeling the human cognition
* declarative knowledge: working memory
* procedural knowledge: production rule base (?)
* a goal stack