Propositional calculus, first order theories, models, completeness

Question

In the usual context of model theory one studies first order theories: the Gödel completeness theorem asserts that $\varphi$ is a theorem of a theory $T$ (i.e. $\varphi$ is provable from the axioms of a theory $T$) if and only if $\varphi$ is true in any model $M$ of this theory. The nontrivial part is of course that being true in any model implies the existence of a formal proof. But of course there is also a famous incompleteness theorem (also due to Godel) which states that in any (sufficiently rich) theory there are statements which cannot be proved and cannot be disproved. Finally there is also a second incompleteness theorem which states that any (again, sufficiently rich) theory cannot prove its own consistency.

I would like to compare this picture with a much simpler framework of the propositional calculus.

For the completeness part we have the following theorem: $F$ is a theorem of the propositional calculus if and only if it is a tautology.

1. Is there a way to view this theorem as a special case for the Gödel's completeness theorem for the first order logic? What would be a model of a theory being propositional calculus?

Of course I certainly agree that such formulation would be rather artificial. Nevertheless still I'm interested whether it is possible?

For the incompleteness part:

2. Is it right to think that propositional calculus is incomplete in the sense that simply it is always possible to construct a formula which for two different truth assigments gives true sentence for the first one and false for the second?

Now, regarding the proof of its own consistency: from the completeness of the propositional calculus follows that propositional calculus is consistent

3. Is it right to say that propositional calculus proves its own consistency?

And finally since proving theorems in propositional calculus boils down to checking whether something is a tautology, it follows that there is an effective algorithm for proving every theorem of the propositional calculus: so among three parts of the Hilbert program (completeness, consistency and decidability) the first has negative answer for the propositional calculus while the second and the third have positive answers.

4. Is this summary correct?

Answer 1

Unfortunately I don't quite agree with your summary.

First, in the context of propositional logic, the relevant notion of model is simply a row of the truth table, a propositional world, a valuation assigning every propositional atom a truth value. Thus, a propositional assertion is satisfiable if it is true in some model (i.e. on some row of the truth table), and valid or tautological if it is true in all models, that is, on all rows of the truth table.

And yes, the propositional completeness theorem asserts that a propositional assertion is true in all models (that is, it is a tautology) if and only if it is provable in any of the standard proof systems.

Usually one proves the propositional completeness theorem by using a proof system specifically geared to propositional logic, typically a simpler proof system than used in first-order predicate logic---the propositional systems have no quantifier rules or axioms and no rules for equality or variable substitution or generalization. I tend to think of propositional completeness as mainly a warm-up in a simpler context with a simpler system, but involving the same metatheoretic issues that will arise again later more fully in predicate logic.

Regarding question 1, however, yes, one can view propositional completeness as a consequence of the completeness theorem for FOL, since a propositional model can be viewed as a model in first-order logic by interpreting each atom as a 0-ary relation. All predicate-logic models correspond with a specific propositional world.

I wrote an elementary account of these ideas on my substack, where I am serializing the chapters and sections of my logic book, A Panorama of Logic. Check out the installment on A Formal Proof System for Propositional Logic.

Regarding question 2, frankly I don't find your statement a compelling analogue of the incompleteness theorem in arithmetic, which asserts at bottom that there is no computably axiomatizable complete theory of arithmetic, extending a certain minimal theory.

In propositional logic, the fact is that every satisfiable finite list of axioms admits a computable completion. Simply take any row on which those finitely many axioms are true, and then extend to a row with all atoms by taking all other atoms as true. This row can then be used to define a computable completion of the given axioms. In this sense, the propositional analogue of the incompleteness theorem is false.

Another way to see this is that the propositional analogue of the Entsheidungsprobleme is that propositional validity is decidable. Namely, there is a computable procedure to determine whether $\varphi\models\psi$ for any propositional assertions $\varphi,\psi$. We can just check the truth table, which is a computable process.

For question 3, my view would be that we lack an interpretation of arithmetic notions such as consistency in propositional logic, and so I see no reasonable sense in which propositional logic can be said even to assert its own consistency, let alone prove it.

So I don't quite agree with your summary.

A more positive view. We might take the theme of your question to be:

To what extent does the metamathematics of propositional logic foreshadow the metamathematics of predicate logic?

To this I answer quite positively indeed, and when I teach introductory logic I try to bring this feature out as much as I can. In my view almost all the central metamathematical ideas in first-order logic have incipient elementary analogues in propositional logic. We have notions of a formal language, notions of model, satisfiability, validity, proof, consistency, completeness, and so forth, all a bit simpler and more accessible in the propositional context. This makes the situation very useful pedagogically, for the easier context helps lead the students to the corresponding concepts in first-order predicate logic.

The compactness theorem especially, which you didn't mention but which I would find more important than completeness, is an excellent case. The proof of the propositional compactness theorem involves the same process of completing a finitely satisfiable theory to a complete finitely satisfiable theory, in a manner that is more elementary than the predicate logic version, but which nevertheless involves many of the same key ideas as in predicate logic. See my treatement on Infinitely More at Compactness for Propositional Logic.