I Syntactic vs semantic logical consequence (entailment)

[cianfa72]

TL;DR Summary

About the "connection" between syntactic vs semantic logical consequence (aka entailment or logical implication)

I would ask for a clarification about the "link/connection" between syntactic vs semantic logical implication (entailment).

As explained here logical consequence, syntactic logical implication (entitlement) $\vdash$ is about the existence of a formal proof within a formal system such that from the premises (i.e. the list of axioms $\Gamma = \{a_1, a_2, ... a_n\}$ assumed to be true by definition) one proves/entails the conclusion $q$ is also true. In symbols: $$\Gamma \vdash q$$
In a formal proof, the above boils down to show that there exists a finite sequence of propositions $p_1,p_2,...p_m$ (either an axiom or a theorem previously proven in the sequence) such that one gets $q$ (as true) by means of (valid) rules of inference, writing $\{p_1,p_2,...p_m \} \vdash q$. Note that syntactic logical consequence does not depend at all on any model/interpretation of the formal system.

Now, which is the relation between syntactic logical consequence $\Gamma \vdash q$ and semantic logical consequence $\Gamma \models q$ ?

I believe the point is that, found a valid argument/proof for $\Gamma \vdash q$, then any model/interpretation that satisfies the axioms (i.e. that makes true the axiom's atomic propositions) automatically makes true also the conclusion $q$ (based on modus ponens inference rule).

 

[.Scott]

Let me examine your statement:
---------------------
As explained here logical consequence, syntactic logical implication (entitlement) ⊢ is about the existence of a formal proof within a formal system such that from the premises (i.e. the list of axioms Γ={a1,a2,...an} assumed to be true by definition) one proves/entails the conclusion q is also true. In symbols:
Γ⊢q
---------------------
1) I believe your "(entitlement)" was intended to be "(entailment)".
2) In the context of this discussion, you can demonstrate that an entailment exists, but you can't really 'entail' something. So, your "proves/entails" should simply be "proves".

Also, I like your inclusion of the term "logical", since there are a few variations of "entailment" (as described in the reference that you have linked to).


Then you post:
---------------------
In a formal proof, the above boils down to show that there exists a finite sequence of propositions p1,p2,...pm (either an axiom or a theorem previously proven in the sequence) such that one gets q (as true) by means of (valid) rules of inference, writing {p1,p2,...pm}⊢q. Note that syntactic logical consequence does not depend at all on any model/interpretation of the formal system.
---------------------
I understand what you're trying to say. Your new term "sequence" (indicating an order list) is useful. I will throw in "set" to indicate an unordered list. I think this distinction will make it easier to see where your crossing the line between a logical "proof" and an "entailment".

Earlier you use the term "axiom" and your citation uses the term "premise". These "axioms"/"premises" are an unordered set of assertions. I would not call them a "sequence" because the order in which they are listed is not important.

Your "exists a finite sequence of propositions p1,p2,...pm (either an axiom or a theorem previously proven in the sequence)" simply means "exists a proof". Those "propositions" are an order set of statements within the proof that you are now attempting to use as axioms. You are probably thinking, after all, that once p1 has been proven from (a1, ... an), it can join the axiom list to yield (a1, ... an, p1).

But notice this: (a1, ... an)⊢q ⟶ (a1, ... an, p1)⊢q
That first entailment ((a1, ... an)⊢q) is a more powerful statement than the second. The p1 needn't be included.
More generally: (a1, ... an)⊢q ⟶ (a1, ... an, px)⊢q

Also, does your list (p1, p2, ...pm) include everything up to and including q?
If so, you are saying (p1, p2, ... q)⊢q which is a trivial statement.
If not, (p1, p2, ...pm) may not entail q. But (a1, a2, ...an, p1, p2, ...pm) would.

Then you post:
---------------------
Now, which is the relation between syntactic logical consequence Γ⊢q and semantic logical consequence Γ⊨q ?
---------------------
If you look at the definitions provided in your reference, you'll notice that "semantics" relies on a "model". As an example, that "model" might be an agreed-upon way of using the English language. And notice that they include "interpretation" - an acknowledgement of how the model (such as English) can be used to create ambiguous statements.

 

[cianfa72]

1) I believe your "(entitlement)" was intended to be "(entailment)".
2) In the context of this discussion, you can demonstrate that an entailment exists, but you can't really 'entail' something. So, your "proves/entails" should simply be "proves".

Yes, definitely.

Your new term "sequence" (indicating an order list) is useful. I will throw in "set" to indicate an unordered list. I think this distinction will make it easier to see where your crossing the line between a logical "proof" and an "entailment".

Sorry, not sure to get your point. According to you, what is the difference/distinction between "logical proof" vs. "entailment" ?

But notice this: (a1, ... an)⊢q ⟶ (a1, ... an, p1)⊢q
That first entailment ((a1, ... an)⊢q) is a more powerful statement than the second. The p1 needn't be included.
More generally: (a1, ... an)⊢q ⟶ (a1, ... an, px)⊢q

Since the syntactic turnstile symbol $\vdash$ (syntactic entailment) is not a symbol of the object formal language, (a1, ... an)⊢q ⟶ (a1, ... an, p1)⊢q is not a well-formed formula (i.e. it is not a wff/proposition) of the object language. So what does actually mean the material conditional connective ⟶ in it ?

 

[.Scott]

Implies.
In other words, if (a) entails q, then (a,anything else) will also entail q.

 

[cianfa72]

Implies.
In other words, if (a) entails q, then (a,anything else) will also entail q.

LHS and RHS of (a1, ... an)⊢q ⟶ (a1, ... an, p1)⊢q are propositions/sentences of the meta-language discourse about the object formal language, hence the symbol ⟶ in between should be replaced by $\implies$ or better $\vDash$ as a symbol of the meta-meta-language (it basically asserts that whenever the LHS is true, the RHS is also true as both statements of the meta-language).

 

[cianfa72]

Sorry to be boring, just to recap my understanding so far. Consider the following in the context of predicate logic (aka predicate calculus or first-order logic).

"If $x$ is even then $x^2$ is even"

According to predicate logic, "is even" is a predicate, let's assign it the predicate symbol $E$. $x$ is a variable taking values from the domain of discourse $D$. $(.)^2$ is a non-logical function symbol. The expression "If...then" is the conditional logical connective $\to$, therefore we have the (predicate logic) well-formed formula (wff): $$E(x) \to E((x)^2)$$ Call the LHS wff as $P(x)$ and the RHS wff as $Q(x)$, hence the $P(x) \to Q(x)$ wff. Note that the latter isn't a proposition (i.e. it hasn't a truth value) since the variable $x$ isn't bounded. Actually in order to assign it a truth value, one needs to define a semantics through an interpretation/model.

Fixed the mathematical theory of natural numbers as interpretation, the domain of discourse $D$ becomes the set of natural numbers $\mathbb N$, the predicate associated to predicate symbol $E$ the obvious "is even" and $(.)^2$ the "square operator".
For any given value of $x$, $P(x), Q(x)$ and $P(x) \to Q(x)$ are all propositions. Therefore one may ask: regardless of the actual value of $x$, does $P(x) \to Q(x)$ always evaluate to true? What one has to check is only one thing: namely that in all cases $P(x)$ evaluates to true, $Q(x)$ evaluates to true as well. Full stop.

For the aforementioned wff, using the "natural" mathematical interpretation, it turns out to be true. Therefore at meta-logic level one can assert: $P(x) \implies Q(x)$. Note the use of the meta-logic symbol $\implies$, since the symbol $\models$ is reserved for semantic logical implication, i.e. in case $P(x) \to Q(x)$ evaluates as true regardless the interpretation.

In the aforementioned case, $P(x) \models Q(x)$ is not the case since, for instance, one may define a different meaning/interpretation of the function symbol $(.)^2$ such that the above doesn't hold anymore. In other words $\forall x : P(x) \to Q(x)$ is just a mathematical truth.