Are Axioms of Propositional Logic Chosen Without Considering Semantic Meaning?

[honestrosewater]

Well yes, but IN FC the theorems are derived from the axioms -- the axioms are primitive, the theorems are derived from them. Nowadays presentations of propositional logic starts with different primitive rules and derives the axioms of FC from those rules.

Presentations vary. There are lots of different presentations used and infinitely many to choose from. And maybe this is me reading too much into word choice, but you don't deduce formulas from rules; you deduce formulas with rules, from sets of formulas. (Logical) Theorems are formulas that you can deduce from the empty set. Axioms are theorems that you can deduce from the empty set without needing to apply any rules. That's the only relevant difference that I can think of between axioms and other theorems. Anywho, it sounded like you were saying that the deduction theorem is only provable for calculi with those two axioms, which I wanted to point out isn't the case.

 

[dobry_den]

One more thing about induction:

Mathematical induction generally proceeds in accordance with the following sort of procedure:

Find some way of "ordering" what you are taking about (e.g., by complexity of formula or whatever).

Show that some property P holds of the first element in this ordering.

Show that if P holds of one element in the ordering, it holds of the "next" element.

Infer that P holds of every element in the ordering.

----------

"Math" is involved in a loose and informal sense in representing the ordering: for instance, we can say that some formulas are more complex than others because they contain "more" logical operators or what-not.

But we don't need anything as sophisticated as Peano's axioms in order to accomplish this. We can count and order things (e.g., in terms of "more" and "less" without using axioms for arithmetic.

Thanks for this "additional note" about mathematical induction. It makes it clear for me :-)

Replies to everything else are coming along, slowly but surely. I'm actually trying to find a bigger-picture way of explaining things, but I haven't ever seen it explained the way I want to explain it, so I want to triple-check everything.

Then I'm really looking forward to reading it.

 

[loseyourname]

Presentations vary. There are lots of different presentations used and infinitely many to choose from. [. . .] Axioms are theorems that you can deduce from the empty set without needing to apply any rules. That's the only relevant difference that I can think of between axioms and other theorems. Anywho, it sounded like you were saying that the deduction theorem is only provable for calculi with those two axioms, which I wanted to point out isn't the case.

I think what he is saying is that Frege and Church chose these three axioms as the foundations of their system of deduction in much the same way Euclid chose his - they're true because we say they're true. They are not themselves deduced from anything else. As such the deduction theorem is not proven by them, it is simply taken as true axiomatically. Contemporary derivations of a similar deduction system, however, do not take the same path. Nick isn't saying it has to be done this way, only that this is the way Frege and Church did it. He is making an historical claim, not a logical claim.

 

[yossell]

You cannot 'well order' the rational numbers (unless we assume the axiom of choice, but the well ordering will have nothing to do with an numerical properties).

You don't need axiom of choice to well order the rational numbers, do you? For sure, the rationals ordered by the familiar GREATER THAN relation are not well ordered, but you can use their numerical properties to enumerate them in a way which is a well ordering.

Or have I misunderstood?