Re: A new Arithmetic Principle?



>
> MT1: There exist a first order formula that's decidable
> but we can not know which way it decides.

This IS NOT POSSIBLE, NO MATTER WHAT meta-theory
you adopt. It bears stressing that almost NO formulae
are just plain "decidable" (and none whatsoever are just
plain "undecidable"). Formulae are decidable or undecidable
FROM SOME PRIOR AXIOMS. Given ANY fixed axiom-set, it
is NOT possible for ANY formula to be both 1) decidable from it,
and 2) not known to be so. At worst, it can be not YET known
to be so. In this context, DECIDABLE MEANS
PROVABLE (or disprovable, i.e., means that either the formula
or its negation IS A LOGICAL CONSEQUENCE OF the axioms).
WhenEVER this is the case, THAT IS *ALWAYS* knowable.
You just start the prover running on the axioms and wait
to see which gets output: the formula or its negation.
If it's decidable then BY DEFINITION, ONE of them MUST get
output eventually. Equivalently, you start 2 copies of the
same first-order-contradiction-confirmation TM on 2 different
input tapes, 1 the conjunction of the axioms with the formula,
and the other the conjunction of the axioms with the denial
of the formula. ONE of these MUST be logically inconsistent,
and the TM will eventually confirm that it is, and halt saying
so, AND THEN you KNOW.

.

Relevant Pages

  • Re: Skolems Paradox and why is math the way it is?
    ... determining what can be inferred from the axioms is the main thing ... Once one starts talking about logics for which we don't have a ... much closer to the second-order axiom, whose negation is expressible ... |specifically THE set theory of the STANDARD interpretation. ...
    (sci.math)
  • Re: what are the axioms of intuitionistic logic?
    ... Pure implication logic (no negation only ->) ... This with MT equals Intuistic logic (without EFQ) ... are finitely many axioms, substitution). ... axiom that is developed in Johansson, "Der minimalkalkul, ein ...
    (sci.logic)
  • Re: Cheshire cat, valid deductive argument ?
    ... it can be made valid by adding appropriate axioms ... one to add is the conclusion, adding the negation of any premiss will ... therefore our inference rules and proofs should never admit the ... that T should admit a non-classical model in which P&~P is the case, ...
    (sci.logic)
  • Re: Looking for Undecidable Propositions in Systems without a certain amount of arthimetic.
    ... the undecidable sentence in FOL is (Ex xex ~Ex xex), ... We have the negation of that sentence as a theorem of the ... theory with no non-logical axioms. ... without confusion. ...
    (sci.logic)
  • Re: All panduks are green
    ... negation are not provable or if the proof is infinitely long. ... The system is still capable of expressing all p.r. ... and all r.e. sers. ... or disprovable depends on what axioms you are assuming. ...
    (sci.logic)