inquire4more said:
I think I follow what you are trying to state here. But, more to the point, it seems to me that no value of F would ever be assigned to an L. By your definition, L would be arrived at, in a purely mechanistic fashion, from axioms assigned T, by accepted inference rules. L would only be arrived at in the case that L is T. It is not that we may say the assertion L is F. We may not make the assertion L at all, unless of course L is T. Only L which are T may be stated, no others would occur, not in this fashion. I agree with your point here, at least in reference to roygabv's assertion.
Right, because S has been set up precisely so that we can't prove any formula unless it's true- it has been set up to be sound (and complete BTW). There certainly are false formulas; The negation of each theorem in S, by the axioms and rules of S, are false- we just can't derive them in S. With different axioms or rules, we could derive false formulas, as you noted about inconsistent axiom systems.
It is here that I disagree. That a theorem may follow from another theorem by a rule, I take as a true statement.
Good because you couldn't disagree with that- it's how theorems were defined.
That an axiom may follow from an application of a rule on a set of expressions or formulas, I do not.
We have to build up a language before we can even state an axiom. That's what the symbols, expressions, and formulas are for- they tell us how the language works and allow us to actually say things in the language. We may create a rule- not an inference rule though, those are different- that decides which formulas are axioms, or we can just state each of them (if there are finitely many, of course). What I outlined above is the usual way of building axiom systems. Well, it's the syntactic side of axiom systems, dealing with the formal aspects, symbols, and such; There's also a semantic side, dealing with concepts, meaning and such, but I'll get to that.
As a rule, an axiom is an irreducible, an underivable assertion.
From your experience, axioms may be what you say. But as defined in this system, axioms are formulas. They really have to be- you can't state them otherwise. And axioms don't have to be irreducible. Here are a few examples of axiom schemas of axiom systems for propositional logic- don't worry if you don't understand them- a B alone is a formula, as are ~B and (B -> C), so these are certainly reducible:
A1) (B -> (C -> B))
A2) ((B -> (C -> D)) -> ((B -> C) -> (B -> D)))
A3) (((~C) -> (~B)) -> (((~C) -> B) -> C))
__
B1) B v B -> B
B2) B -> B v C
B3) B v C -> C v B
B4) (C -> D) -> (B v C -> B v D)
__
C1) B -> (B & B)
C2) B & C -> B
C3) (B -> C) -> (~(C & D) -> ~(D & B))
__
D1) [(((B -> C) -> (~D -> ~E)) -> D) -> F] -> [(F -> B) -> (E -> B)]
-taken from Mendelson's "Intro to Mathematical Logic", 4th. Notice they also use different symbols; That's part of the language. :)
On the semantic, conceptual side of axiom systems, you may want your axioms to be as simple as possible, but it isn't necessary. Simpler axioms may make the rest of your work easier. You may also want other people to understand what you're talking about without having to explain a lot or for people to accept that your axioms are true "outside" of the system. But none of these are necessary. You only need to consider your choice of axioms if you want your axiom system to behave in a certain way, and even then, you may have several axiom sets that do the job equally well, as is the case above.
Though you may not call a primitive expression an axiom, it is still nonetheless. Your axioms then, as defined in your statement, would really more aptly be called theorems,
Ah, but axioms
are theorems- though a special kind of theorem, granted. ;)
as they follow from the application of some set of procedures on these primitives. If, by chance, you are referring to metastatements, as preceding statements, then I think we must treat the metacase as a different case. If I missed your point, or misinterpreted you in any way, let me know.
You would be right if they were metastatements, but they aren't. We wouldn't have to build the language then; We could just start talking about axioms right away.

Oh, BTW, you actually use some of the properties of expressions and formulas to prove things
about not
in the axiom system. For instance, you may use the length of a formula (the number of symbols in it) to prove something about the system. So you don't just use them at the beginning and forget them.