Re: Inside or Outside ?


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 wrote 'In other words, how to prove P(SS0) in PA, where P(x) is
simply "x is a prime".'

I assumed by P(SS0) you meant some formula in the first-order language
of arithmetic (otherwise of course it can't be proved in PA). Which
formula in the first-order language of arithmetic did you mean?

.

Relevant Pages

  • 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 ... 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 ... I have noticed that, even tough the theorems should be in S, the ... 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 ... 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)