-1
$\begingroup$

I am starting to program a proof assistant in Python. The proof assistant will be based in FOL. I might be interested in proving the soundness and completeness theorem for first-order logic in my proof assistant. However, these results involve the$\models$ (satisfiability) relation, which (unless I am mistaken) is defined in terms of an axiom schema. It seems like it would be difficult to prove anything about$\models$ directly from the inductive definition, because the proof assistant I am trying to make would be able to use specific instances of an axiom schema but not reason about the schema itself.

Can the completeness theorem and similar theorems actually be proven in FOL? How would a proof assistant handle an axiom schema?

For reference: I asked a related question on math stack a few days ago (link)

Cross-posted on proof-assistants stack exchange (link)

askedNov 19 at 1:59
Pineapple Fish's user avatar
$\endgroup$
3
  • 1
    $\begingroup$It sounds like you're confusing (a) the proof system as the tool you will be building and using, with (b) the proof system as the mathematical object you would like to define and prove things about. You can set up (b) so that it has the same properties as (a), but (a) will never "know that it is talking about itself".$\endgroup$CommentedNov 19 at 2:23
  • 1
    $\begingroup$The way you implement axiom schemas for (a) (in Python) will be different from the way you describe the axiom schemas used by (b) (in the logical framework provided to you by (a) once you have built (a)).$\endgroup$CommentedNov 19 at 2:29
  • $\begingroup$Huh, Karl just pointed out what I told you on the proofassistant stackexchange. Neat.$\endgroup$CommentedNov 22 at 0:54

2 Answers2

4
$\begingroup$

It's sort of meaningless to ask whether something can be proved in FOL. We need to specify a language and a background theory (possibly empty in each case) to do the expressing and proving.

In the language of set theory it's straightforward to state the completeness theorem, and it is indeed provable in$\mathsf{ZFC}$. The full version does however need choice; if you want a$\mathsf{ZF}$-provable version you need to settle for "Every consistent theoryin a well-orderable language has a model."

What about the other natural context for such foundational considerations, namely the language of arithmetic? Well, here it's much trickier to evenexpress the completeness theorem. If our intended model is$\mathbb{N}$, then most structures as such are not (represented by) elements of the universe; onlyfinite structures can be directly encoded by individual numbers, and the completeness theorem fails for finite model theory (in a strong way: seeTrakhtenbrot's theorem). However, we can save things by using a more subtle statement of the completeness theorem; this is thearithmetized completeness theorem, which is indeed provable in$\mathsf{PA}$ as one would hope.

Finally, there's the intermediate setting; the language ofsecond-order arithmetic (which despite the name is still fully first-order), where we can talk directly about countably infinite objects. Here a version of the completeness theorem is straightforwardly stateable (namely "theory," a priori, has to range over onlycountable theories) and the resulting statement is provable in the weak theory$\mathsf{WKL}_0$ (for comparison, proof-theoretically$\mathsf{WKL}_0$ is weaker than$\mathsf{PA}$ even though the language is richer).

answeredNov 19 at 2:12
Noah Schweber's user avatar
$\endgroup$
14
  • $\begingroup$Can you provide some more detail? I do know the proof of the completeness theorem in ZFC (via Henkin's construction) but I doubt that it is strictly a proof because it uses statements like $\mathcal{M}\models\forall x\phi(x)\iff\forall x(\mathcal{M}\models\phi(x))$, which are really instances of Tarski's schema. The $x$ on both sides are not the same, and actually requires a choice of variable. I don't know that first order logic can mechanically handle this kind of thing, except in specific cases.$\endgroup$CommentedNov 19 at 2:48
  • $\begingroup$@PineappleFish It is strictly a proof. E.g. we can represent formulas by sets/natural numbers/whatever, define by recursion a relation $\mathsf{IsTrueAt}$ between structures and tuples of elements and formulas, and prove "For every $\mathcal{M}$ and every (code for a) formula $\varphi$ of the form $\forall x\theta$ we have $\mathsf{IsTrueAt}(\mathcal{M},\emptyset,\varphi)$ iff for every $m\in\mathcal{M}$ we have $\mathsf{IsTrueAt}(\mathcal{M},\langle x,m\rangle, \theta)$." There's no difficulty, although it is - as expected - extraordinarily tedious. (Another approach is via Skolem functions.)$\endgroup$CommentedNov 19 at 3:08
  • $\begingroup$And I think the proof of the completeness theorem (in an appropriate background theory) has even been verified in Isabelle: seepeople.compute.dtu.dk/ahfrom/….$\endgroup$CommentedNov 19 at 3:12
  • $\begingroup$What is the $\emptyset$ in $(\mathcal{M},\emptyset,\varphi)$ doing?$\endgroup$CommentedNov 19 at 3:18
  • $\begingroup$Incidentally,this old answer of mine talks a bit about theSkolem functions approach to the satisfaction relation.$\endgroup$CommentedNov 19 at 3:18
3
$\begingroup$

Not directly. FOL cannot quantify over formulas, so statements like completeness and soundness are metatheorems. You can handle axiom schemas at the meta level (via functions in your code that take formulas as arguments and return concrete first-order statements).

answeredNov 19 at 2:19
Simone Coppola's user avatar
$\endgroup$
5
  • $\begingroup$No, any reasonable foundational logic for mathematics is able to talk about and quantify over its own formulas through arithmetization, as shown by Gödel. And as long as it has enough for talking and reasoning about sets, the completeness theorem for FOL will be provable internally.$\endgroup$CommentedNov 20 at 18:59
  • 1
    $\begingroup$@JeanAbouSamra Arithmetization requires a stronger theory; plain FOL cannot quantify over formulas.$\endgroup$CommentedNov 21 at 3:04
  • $\begingroup$As pointed out in Noah's answer, it's not really meaningful to talk about provability or definability in "plain FOL" without specifying the background theory. Peano Arithmetic, a theory in FOL, and thus any metatheory at least as strong, is certainly able to do arithmetization and thus quantify over its formulas through quantification on natural numbers, as shown in any proof of Gödel's incompleteness theorems.$\endgroup$CommentedNov 21 at 6:43
  • 1
    $\begingroup$@JeanAbouSamra That's precisely why I said they're metatheorems, i.e. you can prove them at the meta level.$\endgroup$CommentedNov 21 at 17:32
  • 1
    $\begingroup$@JeanAbouSamra Huh, so satisfiability is in the metalanguage after all. Who knew?$\endgroup$CommentedNov 22 at 1:09

You mustlog in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.