In my mind this is literally what math is. We start with axioms, and derive conclusions. There's probably more to it than that, but that's the understanding I'm at now.

▲

galaxyLogic 10 days ago | parent | next [-]

But shouldn't it also be part of the axioms what are the rules that allow you to derive new theorems from them?

So then you could self-apply it and start ... deriving new rules of how you can derive new theorems and thus also new rules, from axioms?

I'm jusr confused a bit about "axioms" and "rules". What's the difference?

	▲	sroelants 10 days ago \| parent \| next [-]
		The rules that you use to compose axioms and propositions are a different set of axioms defined by the Logic system you're using. e.g., can a proof consist of infinitely many steps? Can I use the law of excluded middle? Some logic systems won't let you re-use the same proposition more than once, etc,... They're usually considered separate, because they're orthogonal to the foundational axioms you're using to build up your mathematical systems. With the exact same system of axioms, you might be able to prove or disprove certain things using some logic systems, but not others.
	▲	10 days ago \| parent \| prev [-]
		[deleted]

▲

JonChesterfield 10 days ago | parent | prev [-]

Choosing the axioms is difficult.

	▲	petesergeant 10 days ago \| parent \| next [-]
		Presumably made easier by something like Lean where you can have a very minimal set of axioms, because things you might use as axioms already have proved versions, in Lean.
	▲	10 days ago \| parent \| prev [-]
		[deleted]