Understanding the definition of soundness

Definitions, as far as I understand them:

A formal system is sound if $\vdash A$ implies $\vDash A$.

Semantic entailment $\vDash A$ means that in every model of this system (that is, on every interpretation, satisfying its axioms), $A$ is true.

I was trying to make an example of unsound Hilbert-style system (that is, some axioms and Modus Ponens (MP) inference rule scheme : $\frac{\phi \to \psi \quad \phi}{\psi}$), however, by the definition of soundness, and because Modus Ponens is sound, it seems that any such system would be sound. For example, if we pick a formal system with an only axiom $A$ and and MP inference rule scheme, such a system will be sound (since $A$ is the only theorem of this system, so when $A$ is satisfied, it is indeed satisfied!).

Now, consider an equivalent (in the sense of provable propositions) system with no axioms and additional inference rule $\frac{}{A}$. Now, every interpretation of such a formal system will be its model since there are no axioms. However, such a system is clearly unsound because $\vdash A$ and one could assign $A = False$.

What part(s) of definitions am I missing? Should the semantic entailment definition demand soundness of the inference rules too?

"Every interpretation of such a formal system will be its model since there are no axioms." No. A model for a theory, in the general case, is required not just to make the axioms true but to make the rules of inference truth-preserving, so that the model will indeed make all theorems true [for making the theorems all true is the crucial feature of those interpretations which count as models].

Of course, we typically are considering first-order theories regimented with just logical rules of inference, and the conformity of first-order models with first-order logical rules of course comes for free: so in this case modelling the axioms suffices for modelling the whole theory. But you are considering the case with the non-logical rule "from no premisses, infer $A$", so now you do need to take note of the requirement that a model fits not just axioms but also inference rules and hence makes all theorems true. Or you get into exactly the trouble you note!

• Another way of looking at this is that we can choose the class of models we want to look at, and if we have a set of inference rules in mind we only choose models which make the inference rules sound. So soundness, in the general case, shows that the models that have been chosen match the inference rules that have been chosen. – Carl Mummert Jul 29 '13 at 1:31
• @peter-smith Thanks! But then won't any formal system be sound, by that definition? Because if by the definition of semantic entailment the axioms are true and the inference rules are truth-preserving, all theorems of this formal system will be true. – karlicoss Jul 29 '13 at 7:05
• By "any formal system" I meant any formal system with true axioms.Actually this question arose when I tried to make an example of a consistent but unsound formal theory, what confuses me is that if I satisfy all axioms, I won't ever get false theorem in a formal system, that is won't get unsoundness. – karlicoss Jul 29 '13 at 7:18

Define a Hilbert system with modus ponens and uniform substitution as rules of inference. Select any finite number of classical (two-valued) tautologies which have the material conditional as their principal connective and only have material conditional symbols as their connectives to serve as your axioms (no negations, disjunctions, or conjunctions appear in the formulas... though you can do this, it'll take more work). Suppose you have the following formation rules:

1. All lower case letters of the Latin alphabet are propositional formulas.
2. If $\alpha$ and $\beta$ are propositional formulas, then C$\alpha$$\beta$ is a propositional formula.

You might then choose for your axiom set {CpCqp}, {CCpqCCqrCpr, CpCqp}, or {CpCqp, CCpCqrCCpqCpr}. Now indicate that your semantics gets indicated by this table for your conditional C (note modus ponens is still valid according to the table):

  p/q  0  .5  1
0    1   1  1
.5   .5 .5  1
1*   0  .5  1


I starred "1" to indicate it as the designated element. For all your axioms, it holds that ⊢A, because you get that by default for any axioms chosen (⊢A just means that A consists of either an axiom or can get derived from axiom set using only the rules of inference.. it does NOT mean that "A is satisfied" as you said in your question). You can still make formal deductions in this system, since formal deductions have no reference to meaning. However, you can show that where A indicates any such axiom, $\forall$A(⊨A) is false, which means your Hilbert system is not sound. In other words, you can show that $\forall$A(⊨A), the valuation of A is not 1 for some selection of values for the propositional variables. Do you see how you might show that?

Well, you don't need to in order to show that soundness doesn't hold. You only need to show that at least one of your axioms does not qualify as a tautology, or equivalently that ⊨A is false for at least one axiom, or equivalently that the valuation (or truth value assignment) of A for some axiom A is not 1 here. I think you can do that.