Completeness theorem for first-order logic

Stream: Is there code for X?

[Sky Wilshaw]

I can see that mathlib4 has the compactness theorem docs#FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, but I can't see the completeness theorem. It seems the compactness theorem is proven using ultraproducts, which would subvert the usual reason to prove completeness.

[Jason Rute]

It appears to be part of this project: https://github.com/iehality/lean4-logic (LO.FirstOrder.completness)
There is some discussion on moving this into Mathlib here: #general > Gödel's first incompleteness theorem

[Sky Wilshaw]

I don't see any discussion there on the completeness theorem, just the first incompleteness theorem. The first link is useful, however, thank you.

[Sky Wilshaw]

More than anything, I'm surprised that Flypitch doesn't (seem to) have this theorem.

[Jason Rute]

What would Flypitch need it for?

[Sky Wilshaw]

I wouldn't have assumed that you could get that far in model theory without any discussion of syntactic proof.

[Floris van Doorn]

Sky Wilshaw said:

More than anything, I'm surprised that Flypitch doesn't (seem to) have this theorem.

The completeness theorem is proven in Flypitch here: https://github.com/flypitch/flypitch/blob/master/src/completeness.lean#L47 It was the "warm-up exercise" for the independence of CH.

[Sky Wilshaw]

Ah, thanks!