% -*- TeX:EN -*-
%%% ====================================================================
%%% @LaTeX-file qedeq_logic_language_0.00.00.tex
%%% Generated at 2007-01-14 21:55:27,718
%%% ====================================================================
%%% Permission is granted to copy, distribute and/or modify this document
%%% under the terms of the GNU Free Documentation License, Version 1.2
%%% or any later version published by the Free Software Foundation;
%%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts.
\documentclass[a4paper,german,10pt,twoside]{book}
\usepackage[english]{babel}
\usepackage{makeidx}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{color}
\usepackage[bookmarks,bookmarksnumbered,bookmarksopen,
colorlinks,linkcolor=webgreen,pagebackref]{hyperref}
\definecolor{webgreen}{rgb}{0,.5,0}
\usepackage{graphicx}
\usepackage{xr}
\usepackage{epsfig,longtable}
\usepackage{tabularx}
\newtheorem{thm}{Theorem}[chapter]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{lem}[thm]{Lemma}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{ax}{Axiom}
\newtheorem{rul}{Rule}
\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition}
\newtheorem{idefn}[thm]{Initial Definition}
\theoremstyle{remark}
\newtheorem{rem}[thm]{Remark}
\newtheorem*{notation}{Notation}
\addtolength{\textheight}{7\baselineskip}
\addtolength{\topmargin}{-5\baselineskip}
\setlength{\parindent}{0pt}
\frenchspacing \sloppy
\makeindex
\title{\textbf{Hilbert~II} \\
\vspace*{1cm}
Presentation of \\
Formal Correct \\
Mathematical Knowledge \\
\vspace*{1cm} Logical Language}
\author{
Michael Meyling
}
\begin{document}
\maketitle
\setlength{\parskip}{0pt}
\tableofcontents
\setlength{\parskip}{5pt plus 2pt minus 1pt}
\chapter*{Description} \label{chapter0} \hypertarget{chapter0}{}
\addcontentsline{toc}{chapter}{Description}
The project \textbf{Hilbert~II} includes formal correct mathematical knowledge. Here we introduce
the underlying formal language for the mathematical formulas. This is done in an informal way. Important theorems (e.g.: universal decomposition, and any proofs) are left out.
\par
All we will do is manipulate symbols. We build lists of symbol strings and use certain simple rules to get new lists. So by starting with a few basic lists we create a whole universe of derived symbol lists.
It turns out that these lists could be interpreted as a view to the incredible world of mathematics.
%% end of chapter Description
\chapter{Entities} \label{chapter1} \hypertarget{chapter1}{}
There are different basic things we have to do with. These are predicates, functions, subject variables and logical connectives. In the following all of them are named and described.
\section{Elements, Atoms and Lists} \label{chapter1_section0} \hypertarget{chapter1_section0}{}
The basic structure we have to deal with is an element. An element is either an atom or a list.
\par
An atom carries textual data, atoms are just strings.
\par
Each list has an operator and can contain elements again. An operator is also nothing more than a simple string. A list has a size: the number of elements it contains. Their elements can be accessed by their position number. An atom has no operator, no size and no subelements in the previous sense.
\par
Lists are categorized according to their operators.
\subsection{Operator Overview
}
Before we introduce the formal language in detail the used operators are briefly listed.
\par
\begin{tabularx}{\columnwidth}{lll}
\multicolumn{2}{l@{}}{\qquad\emph{logical}} \vspace*{1mm} \\
\emph{AND} & logical conjunction operator & $\land$ \\
\emph{OR} & logical disjunction operator & $\lor$ \\
\emph{IMPL} & logical implication operator & $\rightarrow$ \\
\emph{EQUI} & logical biconditional operator & $\leftrightarrow$ \\
\emph{NOT} & logical negation operator & $\neg$ \\
\\
\multicolumn{2}{l@{}}{\qquad\emph{logical quantifiers}} \vspace*{1mm} \\
\emph{FORLL} & universal quantifier & $\forall$ \\
\emph{EXISTS} & existential quantifier & $\exists$ \\
\emph{EXISTSU} & unique existential quantifier & $\exists !$ \\
\\
\multicolumn{2}{l@{}}{\qquad\emph{variables}} \vspace*{1mm} \\
\emph{VAR} & subject variables & $x, y, z, \ldots$ \\
\emph{PREDVAR} & predicate variables & $A, B, R, \ldots$ \\
\emph{FUNCVAR} & function variables & $f, g, h, \ldots$ \\
\\
\multicolumn{2}{l@{}}{\qquad\emph{constants}} \vspace*{1mm} \\
\emph{PREDCON} & predicate constants & $=, \in, \subseteq, \ldots$ \\
\emph{FUNCCON} & function constants & $\emptyset, \mathfrak{P}, \ldots$ \\
\emph{CLASS} & class term & $ \{ x | \phi(x) \}$
\end{tabularx}
\section{Terms and Formulas} \label{chapter1_section1} \hypertarget{chapter1_section1}{}
Now we define recursivly our formal language. We call some elements \emph{subject variables}, \emph{terms} and some other \emph{formulas}. We also define the relations a subject variable \emph{is free in} and \emph{is bound in} a term or a formula. If something is not according to the formal rules errors occur. The error codes are also described.
\subsection{General Error Codes
}
The atoms and lists that build up a formula or term are subject to restrictions. The following errors occur if an atom has no content or has content with length of $0$ or an list has no operator or one of its sub-elements does not exist.
\begin{tabularx}{\linewidth}{llX}
30400 & no element & an element doesn't exist - it is null \\
30410 & no atom & an atom doesn't exist - it is null \\
30420 & no list & a list doesn't exist - it is null \\
30430 & no atom content & an atom has no content - it is null \\
30440 & atom content empty & an atom has content with $0$ length \\
30450 & no operator & a list has no operator - it is null \\
30460 & operator empty & a list has an operator with $0$ length \\
30470 & list expected & list element expected but not found
\end{tabularx}
\subsection{Subject Variable
}
We call an element \emph{subject variable} iff it has the operator \emph{VAR} and its list size is $1$ with an atom as its only argument.
\par
Each subject variable is also called a \emph{term}. Only the subject variable itself is free in itself. No subject variable is bound in a subject variable.
\begin{tabularx}{\linewidth}{llX}
30710 & not exactly one argument & list has not exactly one element \\
30730 & atom element expected & the first and only list element must be an atom
\end{tabularx}
\subsection{Function Term
}
If an element has the operator \emph{FUNVAR} or \emph{FUNCON} and its list size is greater than or equal to $1$ with an atom as its first argument and the remaining arguments are all terms then it is called a term too.
\par
Iff a subject variable is free in any sub-element it is also free in the new term. No other subject variables are free. Analogous for bound subject variables.
\begin{tabularx}{\linewidth}{llX}
30720 & argument(s) missing & if operator is \emph{FUNCON} the list must have at least one element \\
30730 & atom element expected & the first list element must be an atom \\
30740 & argument(s) missing & if operator is \emph{FUNVAR} the list must have more than one element \\
30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\
30780 & free bound mixed & found a free subject variable that is already bound in a previous list element \\
30690 & undefined constant & the operator is \emph{FUNCON} and this function constant has not been defined for this argument number
\end{tabularx}
\par
Any other error for term checks may occur due to the fact that all (but the first) sub-elements must be terms too.
\subsection{Predicate Formula
}
If an element has the operator \emph{PREDVAR} or \emph{PREDCON} and its list size is greater than or equal to $1$ with an atom as its first argument and the remaining arguments are all terms and no errors occur then it is called a \emph{formula}.
\par
Iff a subject variable is free in any sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables.
\begin{tabularx}{\linewidth}{llX}
30720 & argument(s) missing & list must have at least one element \\
30730 & atom element expected & the first list element must be an atom \\
30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\
30780 & free bound mixed & found a free subject variable that is already bound in a previous list element \\
30590 & undefined constant & the operator is \emph{PREDCON} and this predicate constant has not been defined for this argument number
\end{tabularx}
\par
Any other error for formula checks may occur due to the fact that all (but the first) sub-elements must be terms.
\subsection{Logical Connectives
}
If an element has the operator \emph{AND}, \emph{OR}, \emph{IMPL} or \emph{EQUI} and its list size is greater than or equal to $2$ and the remaining arguments are all formulas and no errors occur then it is called a formula too.
\par
Iff a subject variable is free in any sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables.
\begin{tabularx}{\linewidth}{llX}
30740 & argument(s) missing & list must have more than one element \\
30760 & exactly $2$ elements expected & the operator is \emph{IMPL} and this list size is not equal to $2$ \\
30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\
30780 & free bound mixed & found a free subject variable that is already bound in a previous list element
\end{tabularx}
\par
Any other error for formula checks may occur due to the fact that all sub-elements must be formulas.
\subsection{Negation
}
If an element has the operator \emph{NOT}, its list size is exactly $1$ and its only sub-element arguments is a formula then it is called a formula too.
\par
Iff a subject variable is free in the sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables.
\begin{tabularx}{\linewidth}{llX}
30710 & exactly $1$ argument expected & list must have exactly than one element \\
\end{tabularx}
\par
Any other error for formula checks may occur due to the fact that the sub-element must be a formula.
\subsection{Quantifiers
}
If an element has the operator \emph{FORALL}, \emph{EXISTS} or \emph{EXISTSU} its first sub-element is a subject variable and its second and perhaps its third sub-element is a formula then the element is called a \emph{formula} too.
\par
Iff a subject variable is free in the sub-element it is also free in the new formula. No other subject variables are free. Analogous for bound subject variables.
\begin{tabularx}{\linewidth}{llX}
30760 & $2$ or $3$ arguments expected & list must have exactly $2$ or $3$ elements \\
30540 & subject variable expected & first sub-element must be a subject variable \\
30550 & already bound & subject variable already bound in second or third sub-element \\
30560 & subject variable missing & list size is $3$ and the subject variable doesn't occur in the restriction formula (the second sub-element) \\
30770 & free bound mixed & found a bound subject variable that is already free in a previous list element \\
30780 & free bound mixed & found a free subject variable that is already bound in a previous list element
\end{tabularx}
\par
Any other error for formula checks may occur due to the fact that the sub-element must be a formula.
\subsection{Class Term
}
An list element with the operator \emph{CLASS}, containing an subject variable and an formula is a term.
\par
Iff a subject variable is free in the formula and is not equal to the first sub-element (which is a subject variable) it is also free in the new term. No other subject variables are free. If a subject variable is bound in the formula it is bound in the new term. Also the first sub-element is bound. No other subject variables are bound.
\begin{tabularx}{\linewidth}{llX}
30760 & $2$ arguments expected & the list must contain exactly two arguments \\
30540 & subject variable expected & the first sub-element must be a subject variable \\
30550 & already bound & the subject variable is already bound in the formula \\
30680 & undefined class operator & the class operator is still unknown
\end{tabularx}
\par
Any other error for formula checks may occur due to the fact that the second sub-element must be a formula.
\subsection{Term
}
When checking an element for beeing a term the element must have the operator for a \emph{Subject Variable}, \emph{Function Term} or \emph{Class Term}.
\begin{tabularx}{\linewidth}{llX}
30620 & unknown term operator & element has no operator that is known as a term operator
\end{tabularx}
\par
Any other error for the accordant operator checks may occur.
\subsection{Formula
}
When checking an element for beeing a formul the element must have the operator for a \emph{Predicate Formula}, \emph{Logical Connective}, \emph{Negation} or \emph{Quantifier}.
\begin{tabularx}{\linewidth}{llX}
30530 & unknown logical operator & element has no known logical operator
\end{tabularx}
\par
Any other error for the accordant operator checks may occur.
\section{Representations} \label{chapter1_section2} \hypertarget{chapter1_section2}{}
The representation of elements differ according to the viewpoint. Lets take the following formula for example.
$$y \ = \ \{ x \ | \ \phi(x) \} \ \leftrightarrow \ \forall z\ (z \in y\ \leftrightarrow \ z \in \{ x \ | \ \phi(x) \} )$$
If within an XML document it may look like the following.
\begin{verbatim}
`
``
``
`
`
``
``
`
`
``
``
`
\end{verbatim}
The same element can be created within java code by the following.
\begin{verbatim}
Element el = new ElementListImpl("EQUI", new Element[] {
new ElementListImpl("PREDCON", new Element[] {
new AtomImpl("equal"),
new ElementListImpl("VAR", new Element[] {
new AtomImpl("y"),
}),
new ElementListImpl("CLASS", new Element[] {
new ElementListImpl("VAR", new Element[] {
new AtomImpl("x"),
}),
new ElementListImpl("PREDVAR", new Element[] {
new AtomImpl("\\phi"),
new ElementListImpl("VAR", new Element[] {
new AtomImpl("x"),
})
})
})
}),
new ElementListImpl("FORALL", new Element[] {
new ElementListImpl("VAR", new Element[] {
new AtomImpl("z"),
}),
new ElementListImpl("EQUI", new Element[] {
new ElementListImpl("PREDCON", new Element[] {
new AtomImpl("in"),
new ElementListImpl("VAR", new Element[] {
new AtomImpl("z"),
}),
new ElementListImpl("VAR", new Element[] {
new AtomImpl("y"),
})
}),
new ElementListImpl("PREDCON", new Element[] {
new AtomImpl("in"),
new ElementListImpl("VAR", new Element[] {
new AtomImpl("z"),
}),
new ElementListImpl("CLASS", new Element[] {
new ElementListImpl("VAR", new Element[] {
new AtomImpl("x"),
}),
new ElementListImpl("PREDVAR", new Element[] {
new AtomImpl("\\phi"),
new ElementListImpl("VAR", new Element[] {
new AtomImpl("x"),
})
})
})
})
})
})
});
\end{verbatim}
%% end of chapter Entities
\backmatter
\addcontentsline{toc}{chapter}{\indexname} \printindex
\end{document}