Re: Inside or Outside ?


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.

.

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, ... 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 iff there ... provability path of P, ... Give a translation of "2 is prime" into the first-order language of ...
    (sci.logic)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... I am referring to the two incompleteness theorems ... Godel's second incompleteness theorem refutes Hilbert's goal of ... If you are unwilling to even read a free online translation of Godel's ... provability is not the same as provability, ...
    (sci.logic)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... I am referring to the two incompleteness theorems ... Godel's second incompleteness theorem refutes Hilbert's goal of ... If you are unwilling to even read a free online translation of Godel's ... provability is not the same as provability, ...
    (comp.lang.prolog)