Re: A question on FOL inference
Keith Ramsay wrote:
Nam Nguyen wrote:
|All right, based upon your hints and suggestion, let me re-formulate
|the question. Let:
|
|- L be a language rich enough to support an incomplete theory;
|- a singleton theory over L means the theory has only one axiom;
|- F be a non-logical formula of L.
|
|Then the question is: Is there any non-singleton theory T over
|L in which F is a non-trivial theorem, and in which the following
|condition would be satisfied?
|
|Condition: if A is an axiom of T, then F is not syntactically part
| of A.
You appear to be trying to rule out various ways in which F could
be "too easily" or too trivially a consequence of the axioms, but I
don't think there's any reasonable nontriviality requirement that will
turn the answer to your question into "no".
In essence I'm certainly weeding out *certain* "trivial" theories.
{F} is certainly one of such theory, so is {(F /\ F)}. I actually have
in mind more theories to exclude. But I suppose I've run into difficulty
defining what "more" should be, despite some seemingly good intuition
on it. I'll try again to clarify my position on the definition of "more"
by mentioning a couple of things.
First, I think there are 2 different senses in the words "imply" and
"equivalence" that have been used in this thread (by DCU). Are the 2
statements "triangle Tr has 2 equal side" and "triangle Tr has 2 equal
angles" 'equivalent'? In other words, does the 1st statement 'imply'
the 2nd, and vice versa? The long and short of it is it depends by
what we mean by 'imply' and hence 'equivalent'. The 2 statements can
never be *logically equivalent*: no matter how we manipulate the
(sentential ?) logic rules (and not the FOL's inference rules),
we simply can not "convert" a 'side' into an 'angle'! On the other hand,
if by "imply" we mean *inferentially imply* then are the 2 statements
*inferentially equivalent*? The answer would depend on the underlying
theory in question plus the definition of what a triangle be.
In Euclidean geometry with a normal definition of a triangle,
,for instance, then yes they are [inferentially] equivalent. (And people
do use this sense of 'imply' and 'equivalent'.) But it wouldn't take us
much to change the definition of a triangle so that one having 2 equal
sides doesn't necessary inferentially imply it having 2 equal angles.
(We just use the *general* sense of "line", instead of "straight line"!)
In brief, given the *dual use* of "imply" and "equivalent", I think
we should be careful in asking question like:
> [...] "Is it possible to find axioms
> that imply F, such that the axioms do not imply
> F?"
As the examples in the next section show, if we're not careful
with the dual use, the *essence* of the question I've been trying
to form would be obscure or invisible. If nothing else, let me just
say this. If in FOL the name of an expression is the expression itself,
then *logically* equivalent formulae are just different names for
the fact that any of them doesn't reveal new information, additionally
than the information they collectively posses. And this is automatic, by
the very definition of logical equivalence. *Inferential equivalent*
formulae are *not always* "equivalent": it depends on the context of
theory and/or definition; hence the formulae could possess different
meanings in different context.
Secondly, now that we make a distinction between the 2 senses of "imply"
and "equivalence", let's illustrate my difficulty in forming the
intended question. Let L be the language of group theory with + be the
binary function, and e be the constant individual (which would be the
identity element w.r.t. the theory itself). Consider the following formula:
(1) Axy[(x + y) = (y +x)] /* the usual Ablelian-group (axiom) formula */
So over the language L, what would be a set of axioms (or theory T),
in which (1) would be a non-trivial theorem. Certainly it's not the
set S1 = {(1)}, right? What could be the alternatives? Let consider
the 2 sets S2, S3:
S2 = {((1) /\ (1))}
S3 = S3a U S3b, where S3a consists of all the normal group axioms, and
S3b df= ExAy(y = x)
So there we have them: (1) would be a non-trivial theorem in either S2
or S3! But which one would we prefer? Imho, we should prefer S3: S2 only
contains as much "inferential information" as S1, so why bother? hence
we should weed out S2 as well. But the difficulty here seems to be how
we could _formulate_ a set S of axioms such that:
a) S has F as a non-trivial theorem
b) S is "not the same kind" such as S2.
Well, by now it seems to me there is a way around the difficulty [but I
could still be wrong with this "intuition", of course]. Which is that
we still insist on a) but formulate b) as:
b) If we strictly use *logical operators and rules* to form a formula
F', out of the axioms of S, then F and F' are not *logically*
equivalent.
With this formulation of b) then the question is: given a non-logical
formula F over an L, can there always exist a set S of axioms that
satisfy a) and b). Again thanks for any help on this (including the
effort of formulating the question itself, based upon the "essence" that
(1) and S3 exemplify).
If axioms A1,...,An are equivalent to B1&~C1, B2&~C2, ...,
B_{n-1}&~C_{n-1}, Bn&(C1vC2vC3v...vC_{n-1} v F), then they
imply F. The statements ~C1,...,~C_{n-1} rule out some cases,
and then C1v...vC_{n-1}vF rules out every other case besides F.
Moreover, it's not hard to show that for any axioms A1,...,An
that imply F, there are formulas B1,...,Bn,C1,...,C_{n-1} for which
A1,...,An are equivalent to B1&~C1,....,B_{n-1}&~C_{n-1},
Bn&(C1v...vC_{n-1}vF).
That just leaves us with whether the axioms are "too obviously"
equivalent to formulas of this form. I don't see that you have any
reason at all to expect such an equivalence to be hard to disguise.
There's no algorithm for determining whether two formulas are
equivalent.
Look at it from a different point of view. There are infinitely many
nonequivalent formulas. Enumerate formulas in order of complexity:
P1,P2,P3,.... It's not very hard to show that there are infinitely many
formulas that aren't implied by any consistent subset of the previous
formulas. So if what you were actually hoping is to find a way for F
to be a consequence of axioms simpler than F, then certainly there
are cases where it's impossible.
Again since the centre is about FOL's inferencibility rather than
logical equivalence of formula, complexity of equivalence of formulae
doesn't seem to be the issue [I think].
Keith Ramsay
--
----------------------------------------------------
Time passes, there is no way we can hold it back.
Why then do thoughts linger, long after everything
else is gone?
Ryokan
----------------------------------------------------
.
Relevant Pages
- Re: An uncountable countable set
... What is the language, primitives, axioms, and rules of inference? ...
(sci.math) - Re: Proof that ZFC is inconsistent
... What is the syntax of the language for your own theory, ... inference, axioms, and definitions? ...
(sci.math) - Re: Axiom of choice
... No, in ordinary set theories, it's not an axiom but is a theorem. ... theorem from the axioms. ... Then you should specify exactly your language, rules of inference, ... No, they're very opaque since you haven't stated your language, rules ...
(sci.math) - Re: primitive recursive: obsolete?
... we have to add more axioms. ... all true sentences of arithmetic in the language of PA. ... logic we define the set of sentences true in the standard model of PA ... theorems" or not has no bearing on the fact that what I said is ...
(sci.logic) - Re: Cantors circular "proof" that evens = integers
... independently of any choice of axioms. ... side CALLS "a language" is completely IRrelevant to ... I KNOW what an interpretation is! ... predicates and term for term-functors) and -arity. ...
(sci.logic) |
|
