[Inquiry] Re: Futures Of Logical Graphs

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

FOLG.  Note 61

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Arisbe List, Cybernetics List,

Proof as Semiosis

We have been looking at several different ways of proving
one particular example of a propositional equation, and
along the way we have been exemplifying the species of
sign transforming process that is commonly known as
a "proof", more specifically, an equational proof
of the propositional equation at issue.

Let us now draw out these semiotic features of
the business of proof and place them in relief.

Our syntactic domain !S! contains an infinite number
of signs or expressions, any of which we may choose
to view in either its string or its graphic forms,
glossing over for now the many details of their
particular correspondence.

Here are some of the expressions that
we find salient enough to single out
and confer an epithetic nickname on:

   e_0  =  "()"

   e_1  =  " "

   e_2  =  "(p (q))(p (r))"

   e_3  =  "(p (q r))"

   e_4  =  "(p q r, (p))"

   e_5  =  "(( (p (q))(p (r)) , (p (q r)) ))"

Under ExG we have the following interpretations:

   e_0 expresses the logical constant "false"

   e_1 expresses the logical constant "true"

   e_2 says "not p without q, and not p without r"

   e_3 says "not p without q and r"

   e_4 says "p and q and r, or else not p"

   e_5 says that e_2 and e_3 say the same thing

We took up the Equation E_1 that reads as follows:

   (p (q))(p (r))  =  (p (q r)).

Each of our proofs is a finite sequence of signs,
and thus, for a finite integer n, takes the form:

   s_1, s_2, s_3, ..., s_n.

Proof 1 proceeded by the "straightforward approach",
starting with e_2 as s_1 and ending with e_3 as s_n,
That is, it commenced from the sign "(p (q))(p (r))"
and ended up at the sign "(p (q r))" by legal moves.

Proof 2 lit on by "burning the candle at both ends",
changing e_2 into a normal form that reduced to e_4,
changing e_3 into a normal form that reduced to e_4,
in this way tethering e_2 and e_3 to a common point.
We got that (p (q))(p (r)) is equal to (p q r, (p)),
then we got that (p (q r)) is equal to (p q r, (p)),
so we got that (p (q))(p (r)) is equal to (p (q r)).

Proof 3 took the path of reflection, expressing the
"meta" equation between e_2 and e_3 via the "object"
equation e_5, then taking e_5 as s_1 and exchanging
it by dint of value preserving steps for e_1 as s_n.
Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))"
to the blank expression that ExG recognizes as true.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o