# Is semantic truth independent of inference rules?

In propositional logic, a syntactic proposition can be evaluated to be correct or not semantically via truth tables. However this appears to exclude the context of the proposition, that is its inference rules - natural deduction or axiomatic.

That is the semantic truth of a proposition is independent of the inference rules that allow us to syntactically/logically establish a proof from the axioms. I find this a little odd. Surely a proof should have also a semantic status too?

This varies depending on which logical system you're working in.

If the system is both sound and complete you can move between semantic "proofs" (I prefer the term "verifications") and syntactic proofs freely (since we know there is a perfect match between syntactic and semantic validity).

When systems lack soundness or completeness (generally completeness, people are usually reluctant to put forward proof systems whose acceptable inferences don't preserve truth) you won't be able to assume this perfect match.

Some systems have both sorts of proofs in a single style of representation. For instance, in An Introduction To Non-Classical Logic, Graham Priest gives a tableaux system of proof where a single proof-tree/truth-tree is both a semantic and a syntactic proof of the proposition in question. A downside of this is that you have to accept that you'll have some proofs which branch infinitely (so, you don't have a decidable proof system). This can generally be recognized because you'll just have to keep reapplying a rule that creates a new branch, and you can see that you'll just get stuck in this sort of "infinite loop" but that none of these branches will serve to "close" the tree (i.e., derive a contradiction on that branch). It is hell on automated theorem provers, though.

So this brings me to the final answer to your question "surely a proof should have some semantic status too?". Yes, generally people think that it should. This is why soundness and completeness are desirable properties for a system to have (though there are trade-offs to be made, as evidenced by the fact that most of the more interesting mathematical systems will be incomplete). But ultimately these are meta-theoretic properties and proofs are carried out in the meta-language. I think we keep these notions (syntactic and semantic validity) separate so we can modify our system along two dimensions to allow for theories where the syntactically and semantically valid propositions are not the same.

• Just to add to your excellent response, for sound systems the relationship between proofs and truth is a very formal, mathematical one. It's known as a "galois adjunction". The only requirement for this relationship is soundness (it still holds for incomplete systems and shows the space of expressions without truth values determined by syntax is functorially described). – ex0du5 Mar 4 '13 at 23:35
• @ex0du5: This isn't quite correct. A galois adjunction is actually very general terminology. Its a specialisation of an adjunction in category theory to the specific context of posets. What Lawvere pointed out is that the space of theories and of models are both posets and that there is an adjunction between them: For any given set of theories you can ask for the largest set of models, and for any set of models you can ask for the smallest set of theories for it. I don't think (but am not sure) that completeness or soundness has anything to do with this. – Mozibur Ullah Mar 5 '13 at 10:34
• I see what you're getting at. What surprised me was that truth of a proposition in a 0-logic (is this standard language for a propositional logic?) was prior to internal-proof, but I see now that truth here should be understood as external or meta-proof of the proposition - then I find it not surprising. – Mozibur Ullah Mar 5 '13 at 10:55
• @MoziburUllah Yes, I think that's a good way to think of it--- truth is external to the logical system. The reason we can recognize the Godel sentences of a system as true is that we have some pre-theoretic grasp of truth that goes beyond provability in a system. – Dennis Mar 5 '13 at 13:58

A syntactic proposition can be evaluated to be correct or not semantically via truth tables.

This probably refers to propositional logic, because I doubt it will be true for predicate logic. But for propositional logic, it's easy to establish a close relationship between semantic truth and inference rules.

But also for predicate logic systems like second order logic, semantic truth is rarely completely independent of inference rules. Considering that (nearly) all popular logical systems are (assumed to be) sound, the semantic truth of a proposition follows from its provability by the inference rules. Hence semantic truth is not independent of inference rules. The surprising part is that sometimes the semantic truth doesn't imply provability.

But how is this possible? Semantic truth depends on an implicit "for all models (of the set of propositions S)":

A syntactic proposition P follows semantically from a set of syntactical propositions S, if P is true for each model that satisfies every proposition from S.

The meta-set theory may not allow/contain certain models which would falsify some unprovable proposition also semantically. Even for first order logic, the meta-set theory (and the exact definition of a valid model) can have more impact than intuitively expected.

• yes. its for propositional logic only. – Mozibur Ullah Mar 5 '13 at 8:37