# Syntactic VS Semantic Provability

Consider a new Conjecture C. The task is to determine whether the conjecture is true or false. Now let us suppose, after working very hard, we are finally able to establish the truth or falsehood of C. A sequence of statements, S1, S2, ..., Sn are written down, where each of them follows from the previous one, and is therefore correct beyond dispute. The terminal statement Sn expresses the truth or falsity of Conjecture C.

The prover, for the first time in the world, was able to write the statement Sn which expresses the truth status, and let us suppose the result was True.

So S1, S2, ..., Sn syntactically prove the Truth of C, and that is how we know the status of the conjecture.

It seems to me that like Sn, statements S1,S2,.., Sn-1, due to being correct, also express different truths (semantic notions). So, effectively, we migrate from one truth to another. Equations merely express them. While it is clear that migration in the domain of equations (i.e. manipulation of the symbols of equation) is governed by the rules of syntax, what is the relation between the truths expressed by the statements S1, S2, .., Sn ?

More concretely, if I decide to work strictly with what equations or statements express, is it possible to migrate from semantic counterpart of S1 to semantic counterpart of S2 , and so on till I reach Sn (and therefore solve the conjecture C), without the aid of syntax (the statements S1, S2, .., Sn)? Why or why not?

(If there is a strict correspondence between syntax and semantics, shouldn't there exist a parallel method in semantics to solve the conjecture C?)

It depends on what you mean by semantics, and by "work strictly with what equations or statements express." (In fact, I think this is vague enough that the question is borderline unanswerable; however, what follows may help clarify the issues.)

The first point I want to make is that in my opinion natural language isn't an appropriate proxy. Natural language arguments are either too vague to be considered "true" proofs (that is, in the formal as opposed to sociological sense), or are so precise that they're basically equivalent to purely formal (= syntactic) proofs even if they're not expressed that way. In order to make this question interesting, I think we need to be more ambitious.

## Model checking

Let's start naively. A sentence (resp. set of sentences) really describes a class of models - namely, the class of structures in which that sentence (resp., each sentence in that set) is true. When we claim that T entails p, what we mean is that every model of T is also a model of p.

From now on, for simplicity I'll restrict attention to finite sets of hypotheses T.

Exactly what the above means depends on what logic we're working in exactly. For example, in propositional logic, the structures we're looking at are valuations (= maps from the set of propositional atoms to {True,False}); in first-order logic, the structures are much more complicated objects (= sets with various designated relations/functions/elements).

The naive notion of "semantic argument," in my opinion, is the following: check to see of p holds in every model of T. For very weak logical systems this is possible, and for example works in propositional logic: since our T is finite, to tell if T entails p we only care about finitely many propositional atoms (those occurring in T and p), and so there are only finitely many valuations we need to check. (By contrast, if we allow T to be infinite then we'll never be completely sure that T doesn't entail p - if T does entail p we'll find out eventually, by the compactness theorem for propositional logic, but we won't get the other half.)

## Why syntax?

But that's a bit silly: nobody really cares about whether a given propositional sentence is a tautology or not. Rather, we're interested in stronger logics, like first-order logic.

Here we run into a problem: model checking is almost never possible. For example:

• Too many models: A single sentence q can have many - even uncountably - non-elementarily-equivalent models. So unlike in the propositional case, to check whether a finite theory entails a given sentence we can't reduce to a finite set of models.

• Too complicated models: Even if there are only finitely many models (up to elementary equivalence) of T, they won't all be computable. So we could find ourselves in a situation where there is a model of T in which p fails, but that model isn't computable, so we can't find it.

• Too complicated theories: Even if a structure A is computable, it may be impossible to determine algorithmically what sentences A satisfies. So even if we "have the countermodel in hand" we can't necessarily tell that it satisfies T and not p.

All of this serves to indicate that first-order entailment is impossibly complicated. The completeness theorem demonstrates that it is in fact at least somewhat computable, but it does so by drawing a connection between the a priori intractable semantics and a syntactic framework. You're interested in moving from a syntactic framework to a semantic one, but the point is that the role of the syntactic framework is to provide a mechanism for actually carrying out semantic analyses which at first glance seem impossible. (See also this old answer of mine.)

## An algebraic (meta-)approach

It's possible, however, that you feel that the above misses the mark. It's focusing on implementability, which isn't the only interesting way to interpret your question. You could also ask:

Is there a mathematical way to treat the "meanings" of sentences as mathematical objects in their own right, so that syntactic proofs are paralleled by direct manipulations of these objects?

This is motivated by the situation with propositional logic: a propositional deduction "T entails p" has an algebraic meaning - it asserts that a certain equation holds in a certain Boolean algebra. The elements of this Boolean algebra are equivalence classes of propositional sentences, and we can think of the equivalence class of such a sentence as its "meaning."

This is the motivating idea behind algebraic logic, and can be extended (with increasing difficulty) far beyond propositional logic. For example, the usual algebraic approach to first-order logic is via cylindric algebras, and there we indeed get a parallel between syntactic reasoning in the first-order framework and actual equations in the associated algebra. There's a lot of existing work on what logical systems admit satisfying "algebrizations," and it's a very interesting issue.

Does this count as a "semantic counterpart" to syntactic arguments? I'm not sure. Algebraic approaches forget the actual models of the sentences involved; roughly speaking, an element in the associated algebra represents a class of structures, but in a "purely abstract" way.

In truth-functional logic the semantic way to show validity is to use a truth table. The syntactic way would involve a derivation using rules of inference to go from any premises, line by line, to the conclusion.

For example, suppose we want to show that the argument P, P → Q ∴ Q is valid. A Fitch-style natural deduction derivation would look like the following using the proof checker associated with the forallx textbook: These three lines would correspond to S1, S2, S3 with the first two lines being premises and the last the conclusion.

One could put these together with premises as a conjunction in the antecedent of a conditional that has the consequence as the conclusion: (P ∧ (P → Q)) → Q. The truth table shows that this is a tautology. To see this with a specific truth table generator, put this string, (P && (P=>Q))=>Q, into the Stanford Truth Table Tool: In Chapter 20, "Soundness and completeness", the authors of forallx sketch a proof that for truth functional logic the semantic approach leads to the same valid arguments as the syntactic approach.

Here is the question:

More concretely, if I decide to work strictly with what equations or statements express, is it possible to migrate from semantic counterpart of S1 to semantic counterpart of S2 , and so on till I reach Sn (and therefore solve the conjecture C), without the aid of syntax (the statements S1, S2, .., Sn)? Why or why not?

Any of the intermediate lines of a derivation with all discharged assumptions added as premises could be placed into a truth table generator. The conclusion would be the intermediate line not the original goal, Sn. This would be a tautology if the derivation was valid up to that point.

This might be a useful way to check if the derivation is correct or not if one does not have a proof checker to guide one's results. However, these steps are unnecessary.

Stanford Truth Table Tool. http://web.stanford.edu/class/cs103/tools/truth-table-tool/

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/