5 ms·

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

cdelsolar 12d ago
What are you nerds fighting about please explain
- deleted 12d ago
  [deleted]
andriy_koval 12d ago
you are entitled to have your opinion :-)
- Almondsetat 12d ago
  and you are entitled to talk about maths while rejecting maths
  - andriy_koval 12d ago
    coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants. I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another. ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it. Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.
    - Smaug123 12d ago
      Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
      - andriy_koval 11d ago
        > Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example. I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?
        Smaug123 11d ago
        Because you wrote: > what are exactly rules, which could be separate topic of research, this detail is skipped I am now confident you’re a troll, though, so I am going to bow out.
        andriy_koval 11d ago
        I referred to specific definition in wikipedia. Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

cdelsolar 12d ago

What are you nerds fighting about please explain

deleted 12d ago
[deleted]

andriy_koval 12d ago

you are entitled to have your opinion :-)

Almondsetat 12d ago
and you are entitled to talk about maths while rejecting maths
- andriy_koval 12d ago
  coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants. I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another. ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it. Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.
  - Smaug123 12d ago
    Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
    - andriy_koval 11d ago
      > Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example. I am aware, also I am not sure why you wrote all of this. Your unknown to me "first course" claims to be some authority of formalization purity?
      - Smaug123 11d ago
        Because you wrote: > what are exactly rules, which could be separate topic of research, this detail is skipped I am now confident you’re a troll, though, so I am going to bow out.
        andriy_koval 11d ago
        I referred to specific definition in wikipedia. Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.