\documentclass[11pt]{jarticle}
\addtolength{\textwidth}{50pt}
\title{情報論理学 レポート問題}
\author{} % 千葉大学 理学部 数学・情報数理学科 古森 雄一}
\date{2003 年 7 月 8 日 (火)} % 7 月 6 日 (日) 作成, 8 日 改訂
\begin{document}
\maketitle
「ユークリッド原論」の第一巻の２までを古典述語論理の上での形式化を次のように試みる。

言語: 2 変数述語 $=$; 0 変数関数 $0$, $1$; 1 変数関数 $-, abs, nor, regtrig$; 2 変数関数 $+, *$

公理:
\[
\begin{array}{rl}
1. & \forall x \forall y \forall z ( (x + y) + z = x + (y + z) ), \\
2. & \forall x \forall y ( x + y = y + x ), \\
3. & \forall x ( x + 0 = x ), \\
4. & \forall x ( x + (-x) = 0 ), \\
5. & \forall x ( abs(-x) = abs(x) ), \\
6. & \forall x ( abs(0) = 0 ), \\
7. & \forall x ( abs(abs(x)+abs(y)) = abs(x)+abs(y) ), \\
8. & \forall x ( abs(regtrig(x)) = abs(x) ), \\
9. & \forall x ( abs(regtrig(x) + (-x)) = abs(x) ), \\ 
10. & \forall x \forall y ( abs(x * y) = abs(x) * abs(y) ), \\
11. & \forall x ( abs(nor(x)) = 1 ), \\
12. & \forall x ( x * 1 = x ), \\
13. & \forall x \forall y \forall z ( (y * x) + (z * x) = (y + z) * x ), \\
14. & \forall x ( x = abs(x)*nor(x) ). 
\end{array}
\]

ここで $d, e, f$ を次のように定義する。
\[
\begin{array}{rl}
D. & d = regtrig(b + (-a)) + a , \\
E. & e = abs(c + (-b)) * nor(b + (-d)) + b , \\
F. & f = abs(e + (-d)) * nor(a + (-d)) + d .
\end{array}
\]
このとき, 第一巻の２の主張は
\[ abs(f + (-a)) = abs(c + (-b)) \]
となる。

以下の等式を証明せよ。証明には上記の公理以外には述語論理の規則と公理および等号について
規則と公理である。証明は日本語で書いてよい。何処でどの公理が使われているかを明記すること。
% ただし, \ref{tho} については公理が不足して証明できない可能性がある。そのときは公理を補っ
% て証明すること。
\begin{enumerate}
\item	$ abs(e + (-d)) = abs(b + (-d)) + abs(c + (-b)) $ .
\item 	$ abs(abs(e + (-d)) + (-abs(a + (-d))) = abs(e + (-d)) + (-abs(a + (-d))) $ .
\item\label{tho} 	$ abs(f + (-a)) = abs(c + (-b)) $ .
\end{enumerate}

\vspace{7mm}
以下に関数記号の直観的意味を記す。もちろん証明にはこれらの直観的意味を
用いてはいけない。
\begin{enumerate}
\item $x + y$ : 平面上の点をベクトルとみなし, ベクトル $x$, $y$ の和。
\item $-x$ : ベクトル $x$ の反対向きで大きさがベクトル $x$ と同じベクトル。
\item $x * y$ : スカラー $x$ とベクトル $y$ の積。スカラーはベクトルと別物ではなく特殊なベクトル
	をスカラーとみなしている。
\item $abs(x)$ : ベクトル $x$ の大きさ。
\item $nor(x)$ : ベクトル $x$ と同じ方向の大きさ 1 のベクトル。
\item $regtrig(x)$ : $x$ と原点を頂点とする正三角形の頂点。
\end{enumerate}
\end{document}
