fom
Posts:
1,030
Registered:
12/4/12
|
|
Re: fom - 01 - introduction
Posted:
Dec 11, 2012 9:24 PM
|
|
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.
|
|