Re: Inside or Outside ?


Nam Nguyen wrote:
Rupert wrote:

Nam Nguyen wrote:

Nam Nguyen wrote:



Rupert wrote:


Nam Nguyen wrote:


Rupert wrote:



Nam Nguyen wrote:



bargiax wrote:




We talk about a theory for arithmetic S. Suppose that we are in
the standard
model, with the natural numbers (0 included) as semantic structure.
A numerical relation R(x_1,...,x_n) is said to be expressible in S
iff there
exists a wff A(x_1,...,x_n) of S with n free variables such that
for every
natural number k_1,...,k_n:

1) if R(k_1,...,k_n) holds, then |- A(#k_1,...,#k_n) in S;
2) if R(k_1,...,k_n) does not hold, then |- ~A(#k_1,...,#k_n) in S.

("#a" means the "numeral of a".)

I have noticed that, even tough the theorems should be in S, the
proofs
appearing on the right of the statements above depends a lot on the
structure...
In a few words, I don't understand whether (for example)
A(#k_1,...,#k_n) is
really provable *inside* of S or it is provable in S due to some
external
conditions.

Example: Mendelson's book says that the equality relation is
expressed by
the formula x_1=x_2 in S. Indeed, if k_1=k_2 in N, then one can
prove (in S)
that #k_1=#k_2 (and that is the clause 1), it is ok for me).
But if k1<>k2 then the book says that there is a proof in S of
#k1<>#k2. Do
you believe it or not, but the statement that allows to affirm
that uses
concepts that are *outside* of S (namely, some inequalities in N).

So, the proofs of A (or ~A) are -technically- really in S?
Thank you


It's entirely a coincidence! But in pursuing a certain (possible)
resolution to GC (Goldbach Conjecture), I've tumbled into a similar
(if not essentially the same) situation. I once asked in this forum
how the proof of "2 is a prime" could be done. In other words, how
to prove P(SS0) in PA, where P(x) is simply "x is a prime". Similarly
to what you might have alluded to, I didn't see any "obvious"
provability path of P(SS0) (from the axioms), despite the fact that
we "know" it's a theorem.



It's easy to prove that 2 is prime in PA. I think it can even be done
in Q. If you want to see the proof in detail, for a start, give an
explicit translation of "2 is prime" into the first-order language of
arithmetic.


Of course it's easy to prove that in PA: there exist no number between
1 and 2 that could be a divisor! But what *didn't* seem obvious to me
is what PA's axioms and inference rules that would eventually yield the
expression SS0 in the conclusion formula.



Give a translation of "2 is prime" into the first-order language of
arithmetic which you doubt can be proved in PA.


Where did I say that I doubted "2 is a prime" can be proved?

[You don't seem to realize that the *keywords* here for the proof of
P(SS0) are "outside", "external", "really in S", etc... but not the
"translation" of '2 is a prime' to, say L(PA), which is trivial.]


To emphasize on these keywords, let me do a little futher analysis
on the proof of "2 is a prime" (that I know of). Informally the proof
is that there can be no divisors in between 1 and 2, therefore 2
satisfies the definition of P(2). Naturally. But there is something
a bit interesting at the formal level. The formal proof would use the
contradiction of the form (F /\ ~F), where F = (S(1) = 2).
The "interesting" thing here is this proof-by-contradiction assumes
the consistency of PA.


No. PA includes classical logic, which allows proof by reductio ad
absurdum. The assumption of the consistency of PA is not needed.

Right. Also, in the other post:

Jack Campin also wrote:

> It assumes no such thing. Why shouldn't a proof by contradiction go
> through in an inconsistent system?

Yes, I made an error and thanks for pointing that out. (This correction
actually might help to define odd-prime theorems a bit more precise than
I previously did. But let's leave for later posts).

Of course if PA is inconsistent then who would really care to talk about
whether or not any feature of a proof of "2 is a prime" is obvious,
right? So for the sake of furthering the discussion about "outside",
"external", etc... why don't we just assume that PA be consistent.
In addition, despite that I said it's trivial, you seem desire to know
the formulation of "2 is a prime"; let's then define it:

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

"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.

.

Relevant Pages

  • Re: Inside or Outside ?
    ... A numerical relation Ris said to be expressible in S ... I have noticed that, even tough the theorems should be in S, the ... provability path of P, ... a bit interesting at the formal level. ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... A numerical relation Ris said to be expressible in S ... provability path of P, ... Give a translation of "2 is prime" into the first-order language of ... a bit interesting at the formal level. ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... A numerical relation Ris said to be expressible in S iff there ... I have noticed that, even tough the theorems should be in S, the proofs ... provability path of P, ... expression SS0 in the conclusion formula. ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... A numerical relation Ris said to be expressible in S iff there ... provability path of P, ... Give a translation of "2 is prime" into the first-order language of ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... A numerical relation Ris said to be expressible in S iff there ... I have noticed that, even tough the theorems should be in S, the proofs ... provability path of P, ...
    (sci.logic)