simply a test of whether I can or cannot export an LyX file to html

This is just a “proof of concept” check to see how well (and not so well) I can export from LyX to html to post on my blog.

Proof Schemes

Proof schemes are deduction or transformation apparatuses. Once defined, they can be used to efficiently describe both well-formed formulas and proofs within a formal system.

Let $U$ be the universe of discourse and $F_0\subseteq U$, called the foundation of the proof scheme. When applied to well-formed formulas (wffs), the foundation will be the set of atomic wffs. When applied to formal systems, the foundation will be the set of axioms of that formal system.

A transformation rule $R$ is an $n$-ary function in $\left[H\to U\right]$ where $H\subseteq U^n$. By $\left[H\to U\right]$, we mean the set of all functions whose domain is $H$ and range is $U$. Let $R$ be the set of transformation rules for the proof scheme.

A proof is a finite sequence $langle{x}_1,\mathrm{...},x_{n}rangle$ of elements of $U$ such that for all $k\in \left\{1,\mathrm{...},n\right\}$ we have either $x_k\in F_0$ or there is an $R\in R$ and a subsequence $langle{y}_1,\mathrm{...},y_{k-1}rangle\subseteq langle{x}_1,\mathrm{...},x_{n}rangle$ such that $x_k=R\left(y_1,\mathrm{...},y_{k-1}\right)$. If $langle{x}_1,\mathrm{...},x_{n}rangle$ is a proof then it is called a proof of $x_n$. $x$ is called provable if there is a proof $langle{x}_1,\mathrm{...},x_{n}rangle$ in which $x=x_n$. This is written $⊢x$ or $\varnothing ⊢x$.

A proof scheme can be specified by an ordered triple $\left(F_0,U,R\right)$ where $U$ is any set with $F_0\subseteq U$ and $R$ is a set of transformation rules. If $P=\left(F_0,U,R\right)$ is a proof scheme then we will let $T\left(P\right)=\left\{x\in U:⊢x\right\}$. Intuitively, $T\left(P\right)$ is the set of all tautologies of the proof scheme $P$.

Formal Systems

A formal system is a deduction apparatus in which one defines wffs over an alphabet and proves theorems from a set of axioms using some inference rules. More formally, a formal system $F$ is a 4-tuple $\left(A,G,T,I\right)$ where $A$ is a finite set (considered to be symbols), $S\left(A\right)$ is the set of all finite strings (also called utterances), $G\subseteq S\left(A\right)$ is the set of wffs (also called statements), $T\subseteq G$ is the set of axioms, and $I$ is the set of inference rules. $I$ is called an inference rule if there exists an $n\ge 1$ and there is an $H\subseteq G^n$ such that $I\in \left[H\to G\right]$.

Sometimes one defines $G$ by specifying a set of atomic wffs $G_0$ and a set of transformation rules $R$ that enable us to “build” new wffs from old wffs. We then can say that $G=T\left(G_0,S\left(A\right),R\right)$, considering the proof scheme $\left(G_0,S\left(A\right),R\right)$. When specifying a formal system this way, a formal system can be said to be a 5-tuple $\left(A,G_0,R,T,I\right)$ where $G_0\subseteq S\left(A\right)$ is a set of atomic wffs and $R$ is the set of formation rules (which are viewed as transformation rules) for wffs, $T\subseteq G$ is a set of axioms, and $I$ is a set of inference rules.

A proof in a formal system is a finite sequence $langle{x}_1,\mathrm{...},x_{n}rangle$ of elements of $G$ such that for all $k\in \left\{1,\mathrm{...},n\right\}$ we have either $x_k\in T$ (i.e., $x_k$ is an axiom) or there is an $I\in I$ and a subsequence $langle{y}_1,\mathrm{...},y_{k-1}rangle\subseteq langle{x}_1,\mathrm{...},x_{n}rangle$ such that $x_k=I\left(y_1,\mathrm{...},y_{k-1}\right)$. If $langle{x}_1,\mathrm{...},x_{n}rangle$ is a proof then it is called a proof of $x_n$. $x$ is called provable if there is a proof $langle{x}_1,\mathrm{...},x_{n}rangle$ in which $x=x_n$. This is written $⊢x$ or $\varnothing ⊢x$. If $M\subseteq G$ and there is a finite sequence $langle{x}_1,\mathrm{...},x_{n}rangle$ of elements of $G$ such that for all $k\in \left\{1,\mathrm{...},n\right\}$ we have either $x_k\in M\cup T$ or there is an $I\in I$ and a subsequence $langle{y}_1,\mathrm{...},y_{k-1}rangle\subseteq langle{x}_1,\mathrm{...},x_{n}rangle$ such that $x_k=I\left(y_1,\mathrm{...},y_{k-1}\right)$, then we say $M⊢x_n$.

Here are the first few digits of pi in base 10
3.1415926535897932384626433832795028841971693993751058209749445923078164062862089986280348253421170679821480865132823066470938446095505822317253594081284811174502841027019385211055596446229489549303819644288109756659334461284756482337867831652712019091456485669234603486104543266482133936072602491412737245870066063155881748815209209628292540917153643678925903600113305305488204665213841469519415116094330572703657595919530921861173819326117931051185480744623799627495673518857527248912279381830119491298336733624406566430860213949463952247371907021798609437027705392171762931767523846748184676694051320005681271452635608277857713427577896091736371787214684409012249534301465495853710507922796892589235420199561121290219608640344181598136297747713099605187072113499999983729780499510597317328160963185950244594553469083026425223082533446850352619311881710100031378387528865875332083814206171776691473035982534904287554687311595628638823537875937519577818577805321712268066130019278766111959092164201989380952572010654858632788659361533818279682303019520353018529689957736225994138912497217752834791315155748572424541506959508295331168617278558890750983817546374649393192550604009277016711390098488240128583616035637076601047101819429555961989467678374494482553797747268471040475346462080466842590694912933136770289891521047521620569660240580381501935112533824300355876402474964732639141992726042699227967823547816360093417216412199245863150302861829745557067498385054945885869269956909272107975093029553211653449872027559602364806654991198818347977535663698074265425278625518184175746728909777727938000816470600161452491921732172147723501414419735685481613611573525521334757418494684385233239073941433345477624168625189835694855620992192221842725502542568876717904946016534668049886272327917860857843838279679766814541009538837863609506800642251252051173929848960841284886269456042419652850222106611863067442786220391949450471237137869609563643719172874677646575739624138908658326459958133904780275900994657640789512694683983525957098258226205224894077267194782684826014769909026401363944374553050682034962524517493996514314298091906592509372216964615157098583874105978859597729754989301617539284681382686838689427741559918559252459539594310499725246808459872736446958486538367362226260991246080512438843904512441365497627807977156914359977001296160894416948685558484063534220722258284886481584

Pi is traditionally defined to be the ratio of circumference to diameter in any circle. In the taxicab space which forms a rectangular grid of possible routes the taxi can take (streets), the distance between (0,0) and (1,1) is 2 (a whole number). As the crow flies, the Pythagorean theorem would tell us that distance is the length of the shortest route between (0,0) and (1,1) is the square root of 2 (an irrational number).

Pi is involved in what many say is the most beautiful of equations, attributed to Euler:
e^(i Pi) + 1 = 0

You can probably change the definition of Pi to be the only real number between 3 and 4 that is a solution to this equation:
e^(i x) + 1 = 0

I wonder if anything special would come of defining Pi that way.

There are various set theories that have a universal set (which would be absolutely infinite)...one involves using 3-valued logic.

The thing to research regarding this is the axiom of comprehension, as it is called.

If set theory A has a completely unrestricted axiom of comprehension, set theory A will automatically then have a universal set, namely the A-set consisting of all A-sets that equal themselves.

For the axiom of comprehension is a powerful way to "generate" new X-sets from the other X-sets known to exist.  The general idea is that a set can be defined in an unambiguous way as being the ensembles all of whose members share a common property.  For example, the description "integers having remainder 2 when divided by 3" "generates" a set as described.

If we take an unrestricted axiom of comprehension, then it states something along these lines:
For every description there is a set whose elements fit that description.
(Hmm, I wonder if "grammatical systems" would help here.)

Seems innocent enough, right?  Well Russell came along and showed that this unrestricted axiom of comprehension, devised by Cantor, leads to a set theory in which every statement is both true and false; a set theory in which every statement is both true and false is probably not going to be considered interesting at all.

Russell came up with a particularly clever and brutal disproof of the axiom of unrestricted comprehension that Cantor believed was true.  This, some speculate, is why Cantor finished his days in an asylum because, deep down, he had lost his faith and lost his way by even acknowledging the possibility that God does not exist.  He thought set theory was a mathematical description of God as the ultimate set so big it contains all sets.

If anthropomorphizing God (God to man) is tricky and/or wrong, then going in reverse (man to God) is probably equally as uncertain.  Cantor was trying to do this with his set theory, imho.

If only Cantor had lived a bit longer.  His successors eventually came up with different set theories in which there is an ultimate set so big it contains all sets.

To Cantor it might have been his goal to prove that God exists but that argument which still happens a lot to this day often boil down to one's definition of the word God, or say undefined if not.

In NFU, the universal set is "generated" by an axiom and there is an axiom of restricted comprehension.  In a paper by Skolem, three-valued logic was used to reveal a set theory with an unrestricted axiom of comprehension was, in fact, a theorem!

I am not sure which of these set theories are stronger or weaker than the others (except in the obvious cases).

Imho, Cantor is one of the giants on whose shoulders his successors do rest.  I'd have to say he's one of my favorite mathematicians.

More on Grammatical Systems

Variations on a theme here. Some interesting and perhaps seemingly different things all share something in common... Music that can be written in sheet music, language that can be faithfully written, a huge chunk of math (if not all maybe), martial arts kata and choreographed dance, games like chess and baseball, and basically anything communicated by some symbols, all share some essential features. I think linguists have a name for these types of structures; I wrote earlier that I would call them Grammatical Systems. So if one can prove something about all grammatical systems, it would hold true for all the items in the list automatically. Trouble is I'm not sure how much I can prove about GS's. I did find one fact about GS's which isn't really deep but it's a start. Trying to find out if others worked in this already, linguists or philosophers of language so I don't have to re-invent the wheel. Well, we'll see where this goes...

Now what I think about a TOE is that it would be like blueprints for reality. I think I can explain it with an analogy: reality is to a TOE as music is to its sheet music. The latter being a sort of mathematical encoding of reality from which all of reality can be "recovered" if deciphered correctly. Looking at it this way, actually writing a TOE down seems pretty far off.

However, if there are blueprints to reality, reality's sheet music if you will, then that would make reality itself a grammatical system. I'd like to know if that's true or not. I doubt it but I feel it's worth investigating. The grammar would roughly speaking be the laws of physics.

A poem about everything

A poem about everything.


May you find your compass
use it to return home
don't close conduits of connections
God is the ONLY voice you hear
allow the water around you to send ripples
many out of one
one out of many
reverse, reverse, reverse
how am I going to be the only one who remembers
times before the physical was discovered
we led incorporeal lives
no possible way to describe a full portrait of God
because there is no need
and in no need, may the suffering cease
and in ceasing of suffering, you find
everything

This picture cold represent how a map of reality might look.  Here, one color can represent corporeal and the other color can represent the incorporeal.  Notice that both colors are shown to varying degrees of brightness.  This could mean that there are many types or levels of existence.  The two, corporeal and incorporeal, in some convoluted way form a confluence, that confluence being singular and the underlying principles behind the scenes are revealed. 

Proofs and Formal Systems

This entry is intentionally left blank.

formal systems and spacetime signatures

I wonder about spacetime signatures.


I don't think I've told anyone that I hypothesize that reality actually is a formal system, though what "formal system" would mean there might not be what it is elsewhere in literature so I would of course have to first define what I mean. 


Now, formal systems are very much like laboratories except these are mathematical laboratories.  In these laboratories, there must be four components:
1.  the symbols to be used (e.g., for communicating)


2.  a conglomerate of which utterances are considered in this laboratory to be grammatically correct


3. a conglomerate of which grammatically correct strings of symbols (i.e., statements) are axioms and assumed true in this laboratory


4.  a conglomerate of transformation rules that input so many statements (called premises) and output another set  of statements called conclusions (or the conclusion if there is only one statement in the output).  The transformation rules are called inference rules.


The only other related and relevant concept pertaining to formal systems is what could be called "the consequence closure of the formal system."  In order to discuss this, one needs to define what a proof is and what a theorem is.


A proof of a statement (i.e., grammatically correct utterances) is a finitely long sequence of statements such that, for all statements in the proof, that statement is either an axiom or the output of any of the transformation rules when applied to all previous statements in the proof.


A theorem is just any statement that is embeddable in a proof (which is a finite sequence of statements).  Intuitively, a theorem is true relative to the ambient formal system; within this formal system a theorem is merely a true statement (truth being relative here).


The consequence closure of a formal system is the ensemble of all theorems of that formal system.




Finally, back to spacetime signatures.  If reality is a formal system, then we must be among its theorems.  A parallel universe would just be any formal system embeddable within reality (viewed as a formal system).  Perhaps the consequence closure of that parallel universe is a good way to define its spacetime signature.