Re: Inside or Outside ?


Nam Nguyen wrote:
Rupert wrote:

Nam Nguyen wrote:

Rupert wrote:

Nam Nguyen wrote:

Rupert wrote:

Nam Nguyen wrote:

P(x) df= Ayz[((x /= 0) /\ (x /= S0) /\ (S0 < y) /\ (y < x)) -> ~(x=y*z)]


How about

P(x) df= ((x /= 0) /\ (x /= SO)) /\ Ayz[((S0 < y) /\ (y < x)) ->
~(x=y*z)]

Sure. I don't see anything wrong with your def. (Did you see anything
mine?)

Yes, by your definition 0 and 1 would be prime.


I see: x was free in mine. Thanks.

Nothing wrong with x being free, it's got to be free. The problem is
having (x!=0)/\(x!=S0) as part of the hypothesis of the conditional.

Well then maybe my eyes are tired, but didn't I have that on the left
sign of the "->"?


It shouldn't be part of the conditional at all. If you make it part of
the hypothesis, then when it's false the conditional will be true.
That's why your definition counts 0 and 1 as prime.

"2 is a prime" then is just P(SS0). The key question is then can we
prove P(SS0), without depending on a) the assumed PA's consistency

Yes.

and b) proof by contradiction?

Define when a proof does not use proof by contradiction.

Assuming T is consistent, a proof that "does not use proof by
contradiction" is a proof that is not a proof-by-contradiction.


What's a proof-by-contradiction?

One in which you assume ~(conclusion) and prove (F /\ ~F). The
proof of (A /\ ~A) cited before is not such a proof.


Okay, well let's clarify what your definition of a proof is. On the
usual definition of a proof from a given set of axioms in the predicate
calculus, you never assume anything in proofs at all. Each step of the
proof is either an axiom or a logical axiom or a formula that follows
from previous formulas in the proof by means of one of the rules of
inference.

"My" definition of a (general) proof? You asked for a def. of a
*specific* kind of proof. Where did you or I even wonder about
a general definition of a proof? Technicality errors is one thing,
unless you claim all proofs *must be* proofs-by-contradiction,
could you stop this nonsensical keyboard-"fiddling" and answer
the rather direct question: can there be a proof of P(SS0) that's
not a proof by contradiction?


I have encountered a definition of a proof from a set of axioms in
first-order logic. On this definition, no proof ever makes any
assumptions at all. You are apparently using a different definition, so
I asked you what it was. I'm not engaging in nonsensical
keyboard-fiddling, I'm trying to get you to state your question
precisely. I can't answer it until you define your terms. I can do a
proof of P(SS0) from the axioms of Peano arithmetic in which each line
is either an axiom of Peano Arithmetic, a logical axiom, or follows
from some previous lines by means of one of the rules of inference of
the predicate calculus. At no point do I assume something and then
derive a contradiction from it. So is that a proof by contradiction or
not? I don't know under what circumstances you would call such a thing
a proof by contradiction and under what circumstances you wouldn't.
You've got to tell me. Until you've told me, your question doesn't mean
anything.

For the record, in one post I already gave a _specific example_
in which the proof of (A \/ ~A) cited there is not a proof-of-
contradiction!


--
-----------------------------------------------------

What we call 'I' is just a swinging door which moves
when we inhale and exhale.
Shunryu Suzuki
----------------------------------------------------



--
-----------------------------------------------------

What we call 'I' is just a swinging door which moves
when we inhale and exhale.
Shunryu Suzuki
----------------------------------------------------

.

Relevant Pages

  • Re: What is md5sum?
    ... Of course - unfortunately proof by contradiction only holds in boolean ... contradiction with the classical proof that the decimals are cardinally ... You seem to think that mathematics is stuck in socrates time. ... In the 1930s Cohen proved the independence of the axiom of choice from ...
    (comp.os.linux.setup)
  • Re: Review of Mueckenheims book.
    ... it is not a contradiction that there is no greatest ordinal. ... In any model of ZFC the ZFC axioms are valid. ... the empty set (usually by axiom). ... ZFC is not a theory of physics. ...
    (sci.math)
  • Re: Request for Peer Review - Refutation of Cantor Theorem Conclusion
    ... The box, just like f, is an indirect means to a contradiction. ... and x notin y", of which only x should be free. ... y subset S and x notin y} exist by the Axiom Schema of Separation ... Surjectivity requires that FOR ALL y in Pthere exists x in S such ...
    (sci.logic)
  • Re: Goedel - interesting problem?
    ... >> I can just introduce an axiom that Forall true formula, there exists a proof for that formula. ... "Forall true formula, there exists a proof for that formula" IS FALSE ... Contradiction, therefore nothing exists ... > theorem that there is a formula representing provability in any theory T ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... I don't see anything wrong with your def. ... Define when a proof does not use proof by contradiction. ... contradiction" is a proof that is not a proof-by-contradiction. ... proof is either an axiom or a logical axiom or a formula that follows ...
    (sci.logic)