Skip to main content
Correction: "first theories" → "first-order theories".
Source Link

So, first-order theories can always be realized by models, which makes first order logic complete. This is more precisely stated in the abstract, excerpted below, to "First-Order Theories as Many-Sorted Algebras" (Notre Dame Journal Of Formal Logic 25(1), January 1984 https://www.researchgate.net/publication/38355700_First-order_theories_as_many-sorted_algebras)

So, first theories can always be realized by models, which makes first order logic complete. This is more precisely stated in the abstract, excerpted below, to "First-Order Theories as Many-Sorted Algebras" (Notre Dame Journal Of Formal Logic 25(1), January 1984 https://www.researchgate.net/publication/38355700_First-order_theories_as_many-sorted_algebras)

So, first-order theories can always be realized by models, which makes first order logic complete. This is more precisely stated in the abstract, excerpted below, to "First-Order Theories as Many-Sorted Algebras" (Notre Dame Journal Of Formal Logic 25(1), January 1984 https://www.researchgate.net/publication/38355700_First-order_theories_as_many-sorted_algebras)

Source Link

First order logic is just algebra, in disguise, while higher order logic is analysis. Theories formulated in first order logic can be expressed as algebraic systems: a system which contains a set of operations, a set of distinguished objects, and a set of equational identities; while theories formulated in higher-order logic that are not equivalently expressible or reducible to first-order theories, may be rightly regarded as calculi.

For instance, an Abelian group can be expressed as an algebra containing a single operation ("-" for subtraction), a distinguished object ("0"), and the following identities: 0 - 0 = 0, x - (x - y) = y and x - (y - z) = z - (y - x).

Also, for instance, an Affine Geometry A over a specific field F can be expressed as a two-sorted algebra containing the ternary operators a,f,b ∈ A×F×A ↦ [a,f,b] ∈ A and a,b,c ∈ A×A×A ↦ abc ∈ A that embodies the operations [a,f,b] = (1 - f)a + fb and abc = a - b + c. An example of axioms (suitable, except for the two fields F = GF(2) of size 2 and F = GF(3) of size 3) is: [a,0,b] = a, [a,1,b] = b, [a,rt(1-t),[b,s,c]] = [[a,rt(1-s),b],t,[a,rs(1-t),c]], abc = [[b,1/(1-t),a],t,[b,1/t,c]], where t is arbitrarily chosen as any member of the field F other than 0 or 1.

For algebraic theories, the "free algebra" is the one which contains just the distinguished objects and whatever other objects can be made from them using the algebra's operations. One can also talk about the "free algebra generated from a set X", where the members of the set X are added to the list of distinguished objects. For instance, the subtraction algebra, above, freely generated from the set {1} is one and the same as the algebra of integer subtraction, and contains also the algebra of integer addition by way of the definitions, -x = (x - x) - x, and x + y = x - (-y). (One can prove x - x = 0 using the axioms, namely by: x = 0 - (0 - x) = x - (0 - 0) = x - 0, and x - x = x - (x - 0) = 0, so -x = 0 - x is an equivalent definition, but less self-contained.)

So, first theories can always be realized by models, which makes first order logic complete. This is more precisely stated in the abstract, excerpted below, to "First-Order Theories as Many-Sorted Algebras" (Notre Dame Journal Of Formal Logic 25(1), January 1984 https://www.researchgate.net/publication/38355700_First-order_theories_as_many-sorted_algebras)

Completeness ensures that a proof for any valid statement can be found by a finite search. Failure to find a proof, when a statement is invalid, occurs only after the unending search through all possible proofs never ends. So, you would have to wait for forever to never end, first, before seeing a "no" answer to the query "is it valid?". In order to be decidable, the "no" answer has to be forthcoming some time before forever is never finished happening.

The key excerpt from the abstract:

"In this paper, by developing the study of first-order logic through many-sorted algebras, we show that every first-order theory is a particular algebra verifying axioms in equational form (see Section 2); therefore we are able to apply Birkhoff's theorems concerning the varieties (see Section 1 [and two references contained in the paper]) and to obtain the Henkin models algebraically, whence the completeness theorem of first-order logic (see Section 3)."

Punchline: "Many-sorted" is the key-phrase - so, add in a boolean type and remake predicates as boolean-valued operators.