Re: Looking for Undecidable Propositions in Systems without a certainamountof arthimetic.



Nam Nguyen wrote:
herbzet wrote:

Nam Nguyen wrote:
herbzet wrote:
Scott wrote:
On Aug 13, 2:52 pm, Chris Menzel <cmen...@xxxxxxxxxxxxxxxxxxxx> wrote:
uninteresting, and implies nothing about the completeness of first-order
theories generally. The question of completeness is interesting only
If the undecidable proposition is derivable
If by "derivable" you mean "deducible" then you have a contradiction
of terms: a proposition that is deduced is thereby decided -- it
isn't undecidable.

in FOL, it should be
A validity. I presume you mean deducible in pure FOL with no
non-logical axioms.

Pure FOL as a theory with no non-logical axioms has undecidable
propositions -- every contingent formula is undecidable.
Better yet, such a theory would have infinite undecidable formulas
which are not logical formulas and which are of the forms:

Ex0Ay(x0=y)
Exox1Ay(x0=y \/ x1=y)
Exox1x2Ay(x0=y \/ x1=y \/ x2=y)
...

Not sure I'm getting the joke. All these are true in a domain
with exactly one object.

It's not a joke. I just showed you that for the "pure FOL" theory
you mentioned above, it would be much a stronger statement if the
undecidable formulas that are not contingent formulas!

A formula is undecidable in pure FOL if and only if it is contingent.

(I take it
here "contingent formula" means non-logical formulas).

Contingent formulae are non-logical formulae, but so are
contradictions.

[After all,
this "pure FOL" theory wouldn't have any theorems that are non-logical
formulas, right?]

Right. But your formulae above are contingent. They are not true in
infinite domains, or in sufficiently large finite domains -- that
is, for each formula in the series, there are finite domains in
which it is false.

That is, there are propositions /in the language/ of FOL that
are not /in the theory/ -- no contingent formula is provable
in pure FOL.

derivable in any theory. Doesn't this make any theory incomplete? If
not, how does a theory prevent the derivation?
What on earth do you mean by a "derivation"? Get persnickity here!
From axioms one deduces theorems! One doesn't deduce non-theorems!
One _decides_ a proposition by proving it or its negation!

If we add contingent formulae as non-logical axioms to pure FOL
then we get a first-order theory. It might be complete, it might
be incomplete (there are undecideable formula), it might be
essentially incomplete.

It also might be inconsistent, if we add axioms that contradict each
other.

Adding contingent formulae as non-logical axioms allows us to prove
-- to decide -- other contingent formulae. That's how it works.

Note though it's also possible to prove logical formulas from non-logical
formulas!

Even better, it's possible to prove any formula from any contradiction!

Correct. So, "Adding contingent formulae as non-logical axioms" might allow
more than just "other contingent formulae" as theorems, right?

Yes:
Adding contingent formula as axioms will not prove any new validities;
they're already all provable in FOL. But if you add an inconsistent
set of contingent formulae, you'll be able to prove all the contradictions
as well as all the contingent formulae.

--
hz
.

Relevant Pages