Re: 2nd-order logic in lower-order language
- From: George Greene <greeneg@xxxxxxxxxxxxx>
- Date: Wed, 20 May 2009 16:49:39 -0700 (PDT)
The linguistic question next arises, what linguistic primitives are
you going to have in a logical/formal language where everything in the
domain is a subclass of some universal class (which is also an
element, but NOT a subclass, of the domain).
Since having the domain be a powerclass necessarily forces it to be
a boolean algebra, one could argue that the linguistic primitives must
at a bare minimum be those occurring in an axiomatization of boolean
algebra. The problem is that there are COMPETING DEFINITIONAL
axiomatizations. Wikipedia seems to think that the following
axiomatization
is definitional:
a \/ (b \/ c) = (a \/ b) \/ c a /\ (b /\ c) = (a /\ b) /\ c
associativity
a \/ b = b \/ a a /\ b = b /\ a commutativity
a \/ (a /\ b) = a a /\ (a \/ b) = a absorption
a \/ (b /\ c) = (a \/ b) /\ (a \/ c)
a /\ (b \/ c) = (a /\ b) \/ (a /\ c) distributivity
a \/ ~a = 1 a /\ ~a = 0 complements
The mere occurrence of "=" in this is obviously problematic --
is = supposed to be a defined predicate or a logical one??
More to the point, the "biconditional" boolean connective -- the
one with the opposite truth-table from XOR -- arguably ALREADY
MEANS "=" in this context, which creates the very serious
problem OF HOW TO EVEN EVALUATE "a <-> b = (what??)"
<-> and = are ALREADY SO COMPLETELY IDENTICAL TO BEGIN WITH
that "evaluation" becomes a no-op.
The above equations ACTUALLY ARE NOT "equations" or even
definitions or even axioms BUT RATHER *rewrite rules*.
And rewriting down to smaller or more basic operators is
always going to be possible until and unless you confine yourself
to NOR or NAND. But given the illegibility of that, it really does
seem preferable to just go ahead and put all 16 binary boolean
functions
(with the POSSIBLE exception of <->, for reasons already mentioned)
on an equal and equivalent footing.
Later in the same article, however, we get the Robbins algebra
version,
x \/ y = y \/ x.
(x \/ y) \/ z = x \/ (y \/ z).
n( n(x \/ y) \/ n(x \/ n(y)) ) = x,
preceded by the Huntington version,
1. Commutativity: x + y = y + x.
2. Associativity: (x + y) + z = x + (y + z).
3. Huntington equation: n(n(x) + y) + n(n(x) + n(y)) = x.
which was taken as definitional
of "Boolean Algebra" to begin with (the other version was
contrastingly
declared to define a "Robbins Algebra" UNTIL they were proved
equivalent
in one of the most celebrated triumphs of automated theorem proving
as it existed in the 1990s).
Later than that, one will run into the problem that every Boolean
Algebra
is actually ALSO A BOOLEAN RING, AND VICE VERSA, which would
tend to imply that maybe one wants to get one's logical primitives
from
the axiomatization of boolean rings instead of boolean algebras.
http://www.springerlink.com/content/kj64113h44462n37/
and
http://www.math.uwaterloo.ca/~snburris/htdocs/scav/boolean/boolean.html
if there is anyone else who didn't already know but wanted to.
Back in first-order logic, we were able to get by with 1 first-order
rule of inference (resolution), if we confined ourselves to \/ and ~
as operators and used clauses.
Here, the "basic alphabet" question will also be related to the
question of what counts as a rule of inference, and things will
continue to be strange because
resolution is complete for the first-order theory of these axioms,
while the
fact that the whole space is 2nd-order tends to imply that a complete
recursive set of inference rules cannot exist!
.
- References:
- 2nd-order logic in lower-order language
- From: George Greene
- Re: 2nd-order logic in lower-order language
- From: George Greene
- 2nd-order logic in lower-order language
- Prev by Date: Re: FOL and AST
- Next by Date: Re: Incompressible, infinite strings
- Previous by thread: Re: 2nd-order logic in lower-order language
- Next by thread: Re: 2nd-order logic in lower-order language
- Index(es):
Relevant Pages
|
