What is the difference between the implication/conditional truth function and the notion of logical entailment?
My naive understanding as a computer programmer is that the conditional is a function on two Boolean inputs, whereas entailment is some sort of more abstract idea about consequence.
Anything that's a thought or reference is deeply appreciated.
The conditional/implication (→), as you said, is a function on statements/propositions (sentences that can be true or false). Consequence/entailment (⊨) is a relation between sets of statements and a statement. From the classical bivalent point of view, the distinction can be characterized as follows:
Implication. (φ → ψ) is true iff (¬φ ∨ ψ) is true.
That's the classical view of →. To evaluate (φ → ψ), it will suffice to evaluate φ, check its value: if the value is false, short-circuit and output true as the value of the whole thing; if the value is true, continue and evaluate ψ and output the value of ψ as the value of the whole thing.
Entailment. (Γ ⊨ ψ) is true iff every interpretation that makes all φ ∈ Γ true, makes ψ true.
That's the classical view of ⊨. To evaluate (Γ ⊨ ψ), it will suffice to consider an arbitrary interpretation of the logical symbols of the underlying language that makes all statements in Γ true, and check whether that (arbitrary) interpretation also makes ψ true. In some logic textbooks they phrase that same thing by saying that: ψ is a logical consequence of Γ just in case it's impossible to make all of Γ true and ψ false.
The characterization of each of these relations depends on the underlying logic. The classical view of both is significantly different from the views of intuitionistic, paraconsistent, relevantist, and other logics. Those SEP articles will introduce you to those perspectives and talk about their motivations.
