Re: Question about first-order arithmetic

Aatu Koskensilta wrote:
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}?

Yes, that seems to be my intended question. But your (somewhat
technical) phraseology is a bit confusing, so I'm not sure whether or
not you mentioned the requirement that the von Neumann defintions of
natural numbers must be used. Does anyone have an answer for this
question?

Any further help would be greatly appreciated.
Thank You in Advance.
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
    ... of first-order arithmetic such that its theorems are precisely the ... 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. ... theoretical formalization in the language 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. ...
    (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)