Re: Inside or Outside ?



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?)


"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 we call 'I' is just a swinging door which moves
when we inhale and exhale.
Shunryu Suzuki
----------------------------------------------------

.

Relevant Pages

  • Re: Inside or Outside ?
    ... Rupert wrote: ... without depending on a) the assumed PA's consistency ... Define when a proof does not use proof by contradiction. ... contradiction" is a proof that is not a proof-by-contradiction. ...
    (sci.logic)
  • Re: JSH: Math proofs
    ... > Well, GIGO. ... so there is a contradiction. ... Depending on how you use intermediate ... Did you ever test your polynomial factorisation proof with the null test? ...
    (sci.math)
  • Re: What is a logical contradiction?
    ... but that would not serve his point. ... we have a contradiction (depending on how we interpret formulas with ... We have a contradiction ONLY if dog refers to the same reidentifiable spatiotemporal position. ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... Define when a proof does not use proof by contradiction. ... proof is either an axiom or a logical axiom or a formula that follows ... when we inhale and exhale. ...
    (sci.logic)
  • Re: Z[sqrt(2)] not a field?
    ... Rupert wrote: ... equation should work in this context to show that it isnt a field. ... So a=1/2 so a is not an integer, contradiction. ...
    (sci.math)
Quantcast