Can computer use the Henkin method?

Question

To prove completeness of First order logic,we have Henkin's method to build a Maximal consistent modal to satisfy a consistent set of formulae. How can we formalize Henkin method(in the sense that we can formalize Godel's completeness proof)? And how can computer use the Henkin method,in consideration that there is a step in Henkin method that Sn+1=ψ,if ψ is consistent with Sn and examining whether a formula iscobsistent with a set is not decidable. Also,as a commonplace talk of ATP,how can computer thinks up to "consider a model that…" by itself?

Answer 1

There's an important difference between formalizing a proof and implementing a construction.

Formalizing a proof really just means writing it down "all the way" - that is, breaking it into a sequence of sentences in the appropriate language which follow from each other via the appropriate inference rules. A fully-formal proof can be checked by computer, and is an entirely finite object (a finite string of symbols satisfying algorithmically-checkable properties). I don't know if the completeness theorem specifically has been given a computer-checkable proof, but it wouldn't be too hard to do so (and if it hasn't, someone should!).

That doesn't mean, however, that the various objects whose existence we establish in the course of a formal proof can be constructed in any meaningful sense by a computer. For example, we can whip up a computer-checkable proof of the incomputability of the halting problem - but that doesn't mean we can actually compute the halting problem. Godel's completeness theorem gives another example of this: there are computable consistent theories with no computable completions or computable models, and the issue is exactly (as you say) that consistency checking is undecidable.

One standard example of this phenomenon is (first-order) Peano arithmetic together with a new constant symbol $c$ and axioms saying that $c$ is bigger than each specific natural number; a nicer example is $I\Sigma_1+\neg Con(I\Sigma_1)$, which is finitely axiomatizable. A key tool here is Tennenbaum's theorem. As an interesting aside, note that Robinson arithmetic is subject to Godel's first incompleteness theorem but not to Tennenbaum's theorem.

It's also worth noting that we can rigorously study the "incomputability" of the completeness theorem: the Turing degrees which compute models or completions of all computable consistent theories are called the PA degrees, and are extremely well-understood. Probably their most useful characterization is via trees: a Turing degree d is PA iff for each infinite computable binary tree $T\subseteq 2^{<\omega}$, there is a d-computable path through $T$ (it's a good exercise to check that whenever $A$ is a computable theory there is a corresponding computable tree $T_A$ whose paths correspond exactly to consistent completions of $A$). This article is a good survey of the topic.

---

So we have to distinguish between talking about a construction, or using it in a proof, and actually implementing the construction. The general situation is that computers can do the former (that is, when we actually do have a proof!) but not always the latter.

Note that all of this is separate from the issue of how a computer can (per your last sentence) "think up" a proof technique. Ignoring the philosophical issues, computer-generated proof (as opposed to computer-verified proof) is still to my knowledge in its relative infancy, and I'll go out on a limb and claim the following:

We do not currently have any good computer-proof-generation heuristics which would plausibly lead a computer to discover the Henkin proof (or any other proof) of the completeness theorem.