Set Differences

Off-day in the AM. Planning to hit the cafe to study 1) set differences, 2) MathJax's indentation limitations, 3) encoding propositions that are machine-readable, for popular automated theorem solvers.

As if there are "popular" automated theorem solvers. Sometimes I look at myself and wonder if I'm crazy. (Almost everyone else already seems sure that I am.)

9pm update: 1) and 2) addressed. A number of irrelevant distractions from errands and accidental participation in a staff meeting seem to have exhausted my ability to study. Time for a break.

---

Theorem:

\begin{align*}
\forall A\forall B\forall C,\quad&
(``\text{A is a set}" \wedge
``\text{B is a set}" \wedge
``\text{C is a set}") \implies \\
&C \backslash(A\cup B) =(C\backslash A)\cap(C\backslash B)
\end{align*}

Proof:

\begin{align*}
x\in C \backslash(A\cup B)
&= \underbrace{x\in C}\wedge\underbrace{x\notin (A\cup B)}\\
&= \underbrace{x\in C}\wedge\underbrace{(x\notin A\wedge x\notin B)}\\
&= \underbrace{(x\in C \wedge x\notin A)}\wedge \underbrace{(x\in C \wedge x\notin B)}\\
&= \underbrace{x\in (C\backslash A)} \wedge \underbrace{x\in (C\backslash B)}\\
&=x\in \underbrace{(C\backslash A)\cap(C\backslash B)}
\end{align*}

"Are you the mathematician? I heard that this place has a mathematician."
"Er, well, I'm studying math, but I'm not sure if that makes me a mathematician. Today I'm reading about 'power sets' - ask me in a coupla years what those are for."

:P

Proofs

ProofWiki: good stuff here - finally having time to appreciate it, now that I basically know how to deploy an equivalent cloud service. All this needs is an automated theorem prover feature... maybe it's there, but I don't see it.

Anyway, all in line with further studies in demonstrating why people are boring.

Demonstrate a machine that can beat humans in an argument.

Step one... learn how to encode human arguments in a machine-readable language.

Well, at least as of today, I've managed to link up my understandings of LaTeX, and Haskell, via mathematical proofs and the functionality of Agda.

What did you think... of course I'm not interested in math for math's sake... pooh pooh...

Also of interest, some other stuff in automated theorem solving, automated theorem checking, and proof assistance:

Mizar system
Metamath

Annoying as it seems (either my own ignorance of the counterexample, or the fact that) there is no standard, like an ISO, for computer readable mathematical proofs.

HOL (subject: higher-order logic) also looks like it needs serious looking into - for my education, on how this stuff is currently treated by the world at large. Ah, time is always short. (A family member of HOL being Isabelle, and Haskabelle.Haskabelle by the HOL-ML-Haskell project group.)

I already kinda know Haskell - but OCaML seems to have been more closely associated with this sort of software in the past. Also checking out HaskHOL. Much to learn.

Proof Assistants - history, ideas, and future

Unions & Intersections

Some of the more interesting exercises (a purely subjective qualification). Easy concepts, difficult language. Boo.

---

Theorem:

The following are equivalent:
- the union of C and (the union of the B-alphas, over the alphas in lambda,)
- the union of (the union of C and the B-alpha), over the alphas in lambda.

Proof:

\begin{align*}


p(x, C, \{B_\alpha\}_{\alpha\in\Lambda})& = \underbrace{x \in
\left\{C \cup
\left[\bigcup_{\alpha\in\Lambda}B_\alpha\right]
\right\}}\\[1em]

& = \underbrace{(x \in C)} \vee
\underbrace{\left( x \in
\left[\bigcup_{\alpha\in\Lambda}B_\alpha\right]
\right)}\\[1em]

& = \underbrace{
(x \in C)} \vee \underbrace{(\exists(B_\alpha), x\in B_\alpha)
}\\[1em]

& =
\underbrace{
\exists(C\cup B_\alpha), x \in (C\cup B_\alpha)
}\\[1em]

&=\underbrace{x\in \left\{\bigcup_{\alpha\in\Lambda}(C\cup B_\alpha)\right\}}\\[1em]

\end{align*}

Less than seven hours till first alarm. I really should get out of the office.

---

Theorem:

The following are equivalent:
- the intersection of C and (the intersection of the B-alphas, over the alphas in lambda,)
- the intersection of (the intersection of C and the B-alpha), over the alphas in lambda.

Proof:

\begin{align*}

p(x, C, \{B_\alpha\}_{\alpha\in\Lambda})& = \underbrace{x \in
\left\{C \cap
\left[\bigcap_{\alpha\in\Lambda}B_\alpha\right]
\right\}}\\[1em]

& = \underbrace{(x \in C)} \wedge
\underbrace{\left( x \in
\left[\bigcap_{\alpha\in\Lambda}B_\alpha\right]
\right)}\\[1em]

& = \underbrace{
(x \in C)} \wedge \underbrace{(\forall(B_\alpha), x\in B_\alpha)
}\\[1em]

& =
\underbrace{
\forall(C\cap B_\alpha), x \in (C\cap B_\alpha)
}\\[1em]

&=\underbrace{x\in \left\{\bigcap_{\alpha\in\Lambda}(C\cap B_\alpha)\right\}}\\[1em]

\end{align*}

---

De Morgan's law:

Theorem:

Where all \((A_\alpha)\)s are subsets of U, the following are equivalent:
- the complement in U of (the union over the alphas in lambda, of the A-alphas)
- the intersection over the alphas in lambda of (the complements in U, of the A-alphas)

Proof:

\begin{align*}

p(x, U, \{A_\alpha\}_{\alpha\in\Lambda})& = x\in\left[\bigcup_{\alpha\in\Lambda} A_\alpha\right]^{\mathsf{\complement}}_{U}\\[1em]

&=(x\in U)\wedge
(\underbrace{\forall A_\alpha, A_\alpha \in U)}\wedge \underbrace{\neg(\exists A_\alpha, x\in A_\alpha)}
\\[1em]

&=(x\in U)\wedge
(\underbrace{\forall A_\alpha, A_\alpha \in U)}\wedge \underbrace{(\forall A_\alpha, x\in (A_\alpha)^{\complement}_U)}
\\[1em]

&= x\in
\left[\bigcap_{\alpha\in\Lambda} (A_\alpha)^{\mathsf{\complement}}_{U}\right]\\[1em]


\end{align*}

Theorem:

Where all \((A_\alpha)\)s are subsets of U, the following are equivalent:
- the complement in U of (the intersection over the alphas-in-lambda, of the A-alphas)
- the union over the alphas-in-lambda of (the complements in U, of the A-alphas)

Proof:

\begin{align*}

p(x, U, \{A_\alpha\}_{\alpha\in\Lambda})& = x\in\left[\bigcap_{\alpha\in\Lambda} A_\alpha\right]^{\mathsf{\complement}}_{U}\\[1em]

&=(x\in U)\wedge
(\underbrace{\forall A_\alpha, A_\alpha \in U)}\wedge \underbrace{\neg(\forall A_\alpha, x\in A_\alpha)}
\\[1em]

&=(x\in U)\wedge
(\underbrace{\forall A_\alpha, A_\alpha \in U)}\wedge \underbrace{(\exists A_\alpha, x\in (A_\alpha)^{\complement}_U)}
\\[1em]

&= x\in
\left[\bigcup_{\alpha\in\Lambda} (A_\alpha)^{\mathsf{\complement}}_{U}\right]\\[1em]


\end{align*}

---

Theorem:

Proof:

Offline HTML LaTex Notebook

Well that didn't take more than a few minutes to figure out:

1. Download MathJax.

2. Unzip the files.

3. The MathJax directory contains a file at ./test/sample-dynamic-2.html which renders LaTeX as you type it.

I forked MathJax on GitHub, modified this file, and committed it, to make offline-draughting easier. LaTeX script on left, rendered LaTeX on right.

Remedial Study of Proofs

2013-12-23

Disproportionately proud of myself. This is very, very late homework. Like 10 years late. (I think I got it right - let me know where the mistakes are, if you see any.)

---

Theorem:

\(\forall x: (\frac{x}{2} \in \mathbb{Z}) \implies (\frac{x^2}{2} \in \mathbb{Z}) \)

"The square of an even integer, is always an even integer."

Proof:

1. axiom \(A\):

   \(\frac{x}{2} \in \mathbb{Z}\)
   
   "x is an even integer."

2. axiom \(B\):

   \(\times\) (multiplication), an operation, is closed over the set of integers.

3. lemma \(C\) \(\Longleftarrow B\):

   \(\forall y: (\frac{y}{2}\in\mathbb{Z})\Longrightarrow\left((\frac{y}{2} \times 2) = y\right)\in\mathbb{Z})\)
   
   "If y/2 is an integer, then y is an integer."

4. lemma \(D\) \(\Longleftarrow B\):

   \(\forall z: (z\in \mathbb{Z})\implies(z^2 \in \mathbb{Z})\)
   
   "If z is an integer, then z squared is an integer."

5. lemma \(E\) \(\Longleftarrow (A \wedge D)\):

   \(\left((\frac{x}{2})^2 = (\frac{x^2}{4}) = \frac{(\frac{x^2}{2})}{2}\right) \in \mathbb{Z}\)
   
   "(x^2)/4 is an integer."

6. Theorem \(\Longleftarrow (C \wedge E)\):

   \( \left(\frac{(\frac{x^2}{2})}{2} \in \mathbb{Z}\right) \implies \left(\frac{x^2}{2} \in \mathbb{Z}\right) \)
   

   
   

LaTex: on Blogger, and iOS

Now I need to make some time to figure out MathJax (source), so that I can blog in LaTex.

MathJax test

inline:

\(x={-b \pm \sqrt{b^2 - 4ac} \over 2a}\)

displayed:

\[x={-b \pm \sqrt{b^2 - 4ac} \over 2a}\]

Well that's done it, then.

I couldn't add a gadget in Blogger, so I added the following to the Head tag of my HTML template:

<script type="text/x-mathjax-config;executed=true">

MathJax.Hub.Config({

  TeX: { equationNumbers: { autoNumber: "AMS" } }

});

</script>

<script type="text/javascript" src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">

</script>

(source)

On iOS I am using LaTex Assistant Lite, for quick LaTex reference, and I am using MathBot for drafting Latex. I am also using the PDF-d LaTeX WikiBook as a more general reference.