Date: Dec 11, 2012 9:24 PM
Author: fom
Subject: Re: fom - 01 - introduction


In 1999, Pavicic and Megill published
"Non-orthomodular Models for Both
Standard Quantum Logic and Standard
Classical Logic: Repercussions for
Quantum Computers". In that document,
they examined the sentential logic
axiomatized with


Def: (A -> B) = (-(A \/ B))



axiom schemata


Ax1: |- (A \/ A) -> A

Ax2: |- A -> (A \/ B)

Ax3: |- (A \/ B) -> (B \/ A)

Ax4: |- (A -> B) -> ((C \/ A) -> (C \/ B))



and inference rule


Det: ((|- A) /\ (|- (A -> B)) => (|- B))



They concluded that Boolean algebras were
not the canonical model for this logic.
What they discovered was that the lattice
mapping


(a /\ (b /\ c)) = ((a \/ b) /\ (a \/ c)) |--> 1



did not force a lattice model to be distributive.
According to their analysis, the source of
confusion on the models comes from interpreting


A=B <=> |- ((-(A \/ B)) /\ (-(B \/ A)))



where A=B would mean either


( (A |--> 1) /\ (B |--> 1))



or


( (A |--> 0) /\ (B |--> 0))



in standard completeness proofs. This, of
course, reflects the fact that the logic begins
with a restriction that its terms be propositions
having no other valuations.

They claim that the canonical model is a
weakly distributive lattice obtained from
formula algebras of the form


L = <Phi(L), -, /\, \/>



satisfying the ortholattice axioms,


OL1: ((A \/ B) = (B \/ A)) |--> 1

OL2: (((A \/ B) \/ C) = (A \/ (B \/ C))) |--> 1

OL3: ((-(-(A)) = A) |--> 1

OL4: ((A \/ (B \/ (-(B))))) = (B \/ (-(B)))) |--> 1

OL5: ((A \/ (A /\ B)) = A) |--> 1

OL6: ((A /\ B) =(-((-(A)) \/ (-(B))))) |--> 1



and the distributivity mapping that they had
been investigating


DL1: ((A /\ (B /\ C)) = ((A \/ B) /\ (A \/ C))) |--> 1



With the understanding that these lattice
models for the logic need not be Boolean
lattices, they concluded that


A=B <=>def

{Antecedents} |- ((-(A \/ B)) /\ (-(B \/ A)))

and

(For every map o from the formulas of the language
into the lattice O^6)(For every formula X in
{Antecedents})...

... ((o(X) |--> 1) => ((o(A) = o(B)))




The lattice O^6 has the form


1

/ \
/ \
/ \
/ \
/ \
/ \

-B -A

| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |

A B

\ /
\ /
\ /
\ /
\ /
\ /

0




The constructions that have been presented
with the "fom" tag use other means to
establish anticipated properties of
truth functions.

Specifying the namespace of logical constants
with a geometry established the relations
of negation, contraposition, and conjugation
without truth tables.

Specifying the connectivity algebra of
intensional functions established functionality
without truth tables.

Formulating a syntactic form to label a geometry
so that any particular selections following an
algorithmic procedure could be interpreted
uniformly as logical equivalence established
"pretheoretic" truth table semantics.

Formulating an algorithm to enumerate the
namespace of the connectivity algebra so that
an order would be given for the first two
components of a truth table relative to
a form interpretable as a complete connective
established "pretheoretic" conditions formula
generation.

Topologizing the connectivity algebra
established possibility of interpreting the
truth table forms in accordance with Fregean
notions of "the True" and "the False."

With these conditions established, the
truth conditions for expressions taken to
be propositions was given relative to
the extension of NOR functionality to
arbitrary symbol strings. This part
of the strategy applies principles
of presupposition,


A presupposes B <=>def Neither A nor -A is true if B is false



In this case, B=(NOR is a truth-functional connective)
and free Demorgan lattices on one generator
provided the algebraic form for mapping the
truth values of the expression and a truth
functional connective simultaneously and
coherently


TRU --> TRU
NOR(NOR(A,NOR(A,A)),NOR(A,NOR(A,A))) --> TRU

NTRU --> NOT
NOR(NOR(A,A),NOR(NOR(A,A),NOR(A,A))) --> NOT



The last item, "lexical blocking" explains
why the lattice O^6 had been essential to the
work of Pavicic and Megill. For, in the
definition of propositions, it was also required
to map the proposition and its (NOR form)
negation to an orthocomplemented pair different
from 1 or 0 (TRU or NOT). In order for
a typical deductive system to be sound, the
propositions it generates as consequences of
its assumptions must be compatible with
those assumptions. Mapping the free DeMorgan
algebras into O^6 as sets of propositions
creates tree structures that work like
models of modal logic.

I need to think more about that. Anyway,
while I doubt anyone has been looking
at those constructions, this is how the
explanation begins.