Re: Question about first-order arithmetic

george wrote:
lugita15@xxxxxxxxx wrote:
My question is, does there exist
a properly axiomatized formal system whose axioms can use the language
of first-order arithmetic such that its theorems are precisely the
ZF-truths of arithmetic?

This question is stupider than you think.

The question as stated is rather trivial, but not for the silly reason you give. If we ask, as seems to have been lugita15's intention, whether there exists a finite number of schemata in the language of arithmetic axiomatizing the set of arithmetical consequences of ZFC, the question is an interesting one, and the solution far from obvious. We can recast the question in terms you might find more congenial:

Is there a finite set A of formulas in the language <+,*,S,0> augmented
with an n-ary predicate symbol P^n_i for every n,i in N, such that
the theory {Q | ZFC |= "PA^2 |= Q"} is axiomatized by A' = {Q | Q is
obtained from a formula Q in A by replacing every P^n_i occurring in Q
by a formula in the language <+,*,S,0> with the arguments to P^n_i
substituted for the n first variables should they occur in the
formula}?

Here "PA^2 |= Q" for a Q in the language <+,*,S,0> is the standard set theoretical formalization in the language <epsilon> of the assertion that the conjunction of the usual axioms of second order Peano arithmetic logically imply Q, and + and * are taken to be binary function symbols, S a unary function symbol, 0 a constant and epsilon a binary relation.

--
Aatu Koskensilta (aatu.koskensilta@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
.

Relevant Pages

  • Re: primitive recursive: obsolete?
    ... we have to add more axioms. ... all true sentences of arithmetic in the language of PA. ... logic we define the set of sentences true in the standard model of PA ... theorems" or not has no bearing on the fact that what I said is ...
    (sci.logic)
  • Re: Question about first-order arithmetic
    ... a properly axiomatized formal system whose axioms can use the language ... of first-order arithmetic such that its theorems are precisely the ... function symbols, S a unary function symbol, 0 a constant and epsilon a ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... from ZF + other axioms. ... are all theorems of pure ZF or ZFC. ... language, in this case, of course, the language of set theory. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... are all theorems of pure ZF or ZFC. ... first-order language, in this case, of course, the language of set ... there is one set theory text whose proofs are all expressed ... carried out using only the ZF axioms. ...
    (sci.logic)
  • Re: Cantors circular "proof" that evens = integers
    ... independently of any choice of axioms. ... side CALLS "a language" is completely IRrelevant to ... I KNOW what an interpretation is! ... predicates and term for term-functors) and -arity. ...
    (sci.logic)