Talk:First-order logic

Syntax-semantics distinction and history

Would it help to include some information on the history of the syntax-semantics distinction? (E.g. according to Ebbinghaus's Ernst Zermelo (2007), pp.182--183, acceptance of it was what set "classic" set theory researchers such as Zermelo and Fraenkel apart from the younger generation of set theory researchers such as Goedel, Skolem, and von Neumann). In this way the syntax-semantics distinction appears much more recent than the advent of first-order logic. C7XWiki (talk) 21:23, 20 April 2024 (UTC)

If-then-else

The article currently states:

This definition of a formula does not support defining an if-then-else function ite(c, a, b), where "c" is a condition expressed as a formula, that would return "a" if c is true, and "b" if it is false. This is because both predicates and functions can only accept terms as parameters, but the first parameter is a formula. Some languages built on first-order logic, such as SMT-LIB 2.0, add this.

I don't understand what this is trying to say. Is it trying to say that one can extend first-order logic with if-then-else, and get a (meta-)theory that is still equivalent to first-order logic? This seems incorrect at first blush: ite(P, P, Q) with P as a predicate corresponds to "the simplest second-order sentence admitting a nontrivial model", if I understand the article on second-order logic correctly. But if the extension of first-order logic with ite yields second-order logic, then why not come out and say that? Maybe the result is something else entirely? If so, what is that? Does it have a name? Are all such extensions equivalent/isomorphic to SMTLIB-2.0 or are there non-equivalent extensions? What, exactly, is the above paragraph trying to say? 84.15.176.27 (talk) 10:35, 18 June 2024 (UTC)

It seems rather odd to me too. If C, A and B are propositional variables then $ite(C,A,B)$ is equivalent to $(C\rightarrow A)\wedge (\neg C\rightarrow B)$ which is a well-defined truth function. Dezaxa (talk) 15:19, 18 June 2024 (UTC)

I removed the statement on if-then-else for now; in my opinion it is certainly misplaced in the paragraphs defining formulas (there are many extensions that are not supported, why highlight this one), and it is confusing at least to the posters in this section and to me. Felix QW (talk) 19:31, 18 June 2024 (UTC)

Comment: I think this paragraph referred to expressions like ite(x>0, x, -x) that are known from programming languages, e.g. (x>0 ? x : -x) can be used in C to denote the absolute value of x. See Ternary conditional operator for details in many programming languages. Such expressions, however, do not fit into the scheme of terms admitted by first-order logic. - Jochen Burghardt (talk) 05:00, 19 June 2024 (UTC)

Possible problem with the variable assignment function way to interpret truth in a model

Please correct me if I'm wrong. There is this example, ∃x (Px  ∧ ∃x (Qx)). This is a well-formed formula, yet if use that approach listed in "Evaluation of truth values", then we run into a problem. It's perfectly possible for there to be a model where this is true and exactly two objects of the domain have the properties P and Q respectively, but the variable assignment approach described overlooks this. ElskverdigHug (talk) 00:30, 26 July 2025 (UTC)

No. In the rule for existential quantifiers in sect. First-order_logic#Evaluation_of_truth_values, the variable assignment $\mu '$ needn't agree with $\mu$ on $x$.

The rule is such that applying a bounded renaming to the variable doesn't change the evaluation result. In your example, the argument for P is bound by the outer quantifier, while that of Q is bound by the inner one. Renaming the latter results in $\exists x(Px\land \exists y(Qy))$, and the problem disappeared.

Alternatively, if e.g. the domain of discourse is the natural numbers, and P and Q is satisfied by 0 and 1, respectively, then the formula $\exists x(Qx)$ is satisfied by an assignment $\mu '$ mapping x to 1. Hence, by the rule for existential quantifiers, is is also satisfied by an assignment mapping x to 0, since $\mu$ and $\mu '$ are allowed to disagree on the variable under consideration, viz. x. Hence, $\mu$ evaluates $Px\land \exists x(Qx)$ to true. Hence, every assignment evaluates the complete (closed) formula to true. - Jochen Burghardt (talk) 14:55, 26 July 2025 (UTC)

Atomic Formulas

The article currently states:

The formulas obtained from the first two rules are said to be atomic formulas.

The first two rules are 1) predicate symbols and 2) negation. I think that only formulas obtained from the first rule are atomic formulas:

1. The linked page Atomic formula does not mention negation.
2. In the BNF grammar, atomic formulas do not include negation.
3. The page Literal (mathematical logic) says: "a literal is an atomic formula (also known as an atom or prime formula) or its negation."
4. The Stanford Encyclopedia of Philosophy article on Classical Logic has a section on Atomic formulas and their definition does not include negation https://plato.stanford.edu/entries/logic-classical/#AtomForm
5. The definition of "atom" in Chapter 1, § 1 of "Mathematical Logic" by Stephen C. Kleene does not include negation. In fact, it states: "If $A$ is a given formula, then $\neg A$ is a (composite) formula."

~2026-20727-4 (talk) 20:06, 10 January 2026 (UTC)

Fixed. JRSpriggs (talk) 20:24, 10 January 2026 (UTC)

Wording of comparison with second-order semantics

I made this edit removing the statement that first order logic "only has one semantics"; it was reverted on the grounds that the article notes game semantics agrees with Tarskian semantics. I agree with the reversion in the sense that it's true that game semantics in FOL agrees with Tarskian semantics (eg that M models phi under Tarski iff. it models phi under game theoretic semantics for instance).

I initially made the edit because when I first read the phrase, (and I admit that this may be slightly pedantic, but it did throw me off) I interpreted it to mean literally that "only one semantics is studied", which reads like a claim on semantic frameworks, not the number of distinct validity relations.

After thinking about it I'd like to propose adding the word "standard" to the front of "semantics", which Second-order logic#Semantics already has. It kind of brings it closer to meaning the canonical model theoretic interpretation used to define truth, which for FOL is Tarskian, and seems to be more intuitive. Hijiri Suzuki (talk) 00:03, 20 September 2026 (UTC)

Is there some other semantics for first order logic? If so, what is it? Otherwise, it would be misleading to add an adjective which suggests that there exist non-standard semantics for FOL. JRSpriggs (talk) 11:38, 20 September 2026 (UTC)

It's important to distinguish semantics from conservation of semantics. That is, even within this article, we are presented with game theoretic semantics, which preserves Tarskian semantics (like mentioned above, $M\models _{\text{game}}\phi \iff M\models _{\text{Tarski}}\phi$); however, this does not imply they are the same semantics. There also exists the distinct example of team semantics, which is studied in FOL but is often characterized as being reduced to Tarskian semantics via the conservativity theorem. The conservativity theorem itself is not vague about the fact that they are two separate semantic frameworks. The fact that they reduce to Tarskian semantics is fine, and it's why I generally accept the revert, but the current framing is still unclear for the above reason and that is why I am proposing this change.

The first few sources to support this within published literature after a google scholar search, wrt. both game and team semantics:

- https://www.sciencedirect.com/science/chapter/edited-volume/abs/pii/B9780444817143500096 This is locked behind paywall, but the summary states "GTS is only one of the possible semantical treatments of first-order logic."

- In https://www.researchgate.net/publication/226118972_From_Games_to_Dialogues_and_Back, "An alternative to the Tarskian way of specifying the semantics would be game-theoretical semantics... which captures the very same satisfaction conditions in terms of the existence of a winning strategy for a certain player in a semantic game, associated with a formula, a model and a variable assignment"

- Proposition 4 of https://www.sciencedirect.com/science/article/pii/S0890540115000760 states "In particular, a first-order sentence ϕ is true in a model M with respect to team semantics if and only if it is true in M with respect to Tarski's semantics."

- https://seop.illc.uva.nl/entries/logic-dependence/ states that: "Team semantics, first developed by Wilfrid Hodges in the context of independence friendly logic (Hodges 1997), is a generalization of Tarski’s semantics for first order logic to the case of multiple assignments of elements to variables"; notably it does not attempt to claim it is the same semantics, but rather goes on to demonstrate it conserves/reduces to Tarskian semantics. Team semantics operates in FOL, but is distinguished here.

- This MLQ publication: https://onlinelibrary.wiley.com/doi/10.1002/malq.202200072 implies these are two different semantics with the sentence "the semantics that we obtain in this way is equivalent to the usual Tarski semantics of first-order logic"

To be even more explicit, since the above are all case specific and part of literature related to game theoretical semantics or team semantics:

- https://link.springer.com/book/10.1007/978-94-017-0452-6 This textbook has an entire chapter titled "Alternatives to Standard First-Order Semantics", in which they detail other semantic frameworks that are equivalent to Tarski but are separate

Generally, there are many kinds of math structures that can be reduced to a common example. For instance the canonical homomorphism for $\mathbb {Z} \to \mathbb {Z} \setminus n\mathbb {Z}$ is the quotient map $k\mapsto [k]$. It would nevertheless be wrong (and trivially easy to disprove) that it is the only homomorphism, just that it's the standard one (for example, maps of the form $k\mapsto [mk]$ are also group homomorphisms). In the same vein, I think that here there are other semantic frameworks that are reducible to or conserve Tarskian semantics, and Tarski's is clearly by and far the standard one, but it does not mean there are other semantic frameworks studied in FOL and that makes the wording incorrect in my eyes. Hijiri Suzuki (talk) 14:15, 20 September 2026 (UTC)

Also of note is the fact that the writer of the Second Order Logic article already thought it necessary to specify standard semantics for FOL: specifically the quote was "Unlike first-order logic, which has only one standard semantics" from that page. This page, First Order Logic, itself already states "the standard or Tarskian semantics for first-order logic... the standard or Tarskian semantics for first-order logic". These are, strictly, separate semantic frameworks

I'd like to discuss it here especially with the context of the revert, but I also think that the other page having it is kind of precedent and having equivalence here would clear up the confusion that I had when I first saw the statement, which I still would not understand as being correct. Hijiri Suzuki (talk) 14:23, 20 September 2026 (UTC)

When I tried to read the Stanford Encyclopedia article, it seemed incoherent to me. They do not give a definite definition of team semantics, but rather describe it using analogy and ambiguous or contradictory conditions. Please give a finite and complete example of a set of boys and girls and a love-relationship which cannot be described with standard Tarskian logic. JRSpriggs (talk) 15:10, 20 September 2026 (UTC)

I don't think such an example can exist if we restrict ourselves to ordinary first-order formulas, and that is actually the point of the conservativity result I cited above. The point is that they are conserved over Tarskian semantics, but are not Tarski semantics. If you wanted a clear definition of team semantics, you can find it eg at https://www.researchgate.net/publication/236864394_Upwards_Closed_Dependencies_in_Team_Semantics, or at one of the other papers I cited.

The point is that it's not about whether it can be described with standard Tarskian logic. There can nevertheless be equivalent semantics that are separate frameworks, and this is why the wording seems incorrect to me. Separately from this most recent comment of yours and relevant to the point of this thread as a whole, the second order logic article (and indeed even this article) is willing to qualify Tarski as the only *standard* semantics, but neither use just "one semantics".

I think at this point, we're kind of talking past each other. I am willing to request a third opinion at WP:3O and an RfC if necessary. Hijiri Suzuki (talk) 16:55, 20 September 2026 (UTC)

Third Opinion Summary

This dispute is on whether the comparison with second order logic in the Semantics section of the main article should say that first order logic has "only one semantics" or "only one standard semantics".

One view is that "only one semantics" is acceptable because alternative frameworks (eg. game semantics, team semantics) are conservative over or are equivalent to Tarskian semantics. The other view is that these are distinct semantic frameworks under literature, so "only one semantics" is too broad, while "only one standard semantics" more accurately identifies Tarskian semantics as the standard semantics without denying the existence of alternatives.

A third opinion is requested at WP:3O. Hijiri Suzuki (talk) 17:02, 20 September 2026 (UTC)

Hi all - as a quick disclaimer, I am unfamiliar with this article ecosystem, and I wasn't familiar with the number-of-first-order-semantics dispute prior to this discussion. However, I do understand Tarskian semantics, FOL, and prop logic pretty well from symbolic logic courses in college, so I'll do my best to resolve this dispute with what I remember.

I reviewed the discussion above, and Hijiri offered 6 sources I'd like to review:

• Source 1 explicitly states there are multiple first-order semantics (corroborates his claim)
• Source 2 says An alternative to the Tarskian way of specifying the semantics would be game-theoretical semantics, implying game-theoretic semantics and Tarskian semantics are both types of semantics in FOL
• Source 3 Is seemingly included to substantiate preservation Hiriji claimed exists between game theory and Tarskian semantics, substantiating his analysis of different semantics in first-order logic
• Source 4 and 5 imply a sibling relationship between Tarskian semantics and game-theoretical semantics
• Source 6 again seems to corroborate Hijiri's claims

From what I've seen, no sources have been offered that imply this assertion - that game-theoretic semantics are a type of FOL semantics - is WP:SERIOUSLYCONTESTED in the academic literature. JRSpriggs asking for a finite and complete example of a set of boys and girls and a love-relationship which cannot be described with standard Tarskian logic is (no offense) a little silly, because how in the world is someone supposed to represent that with game theoretic semantics? Just because it is impossible for someone to represent a finite and complete set of boys in girls using game-theoretic semantics does not mean game-theoretic semantics are not a type of first-order logic semantics. And when JRSpriggs said When I tried to read the Stanford Encyclopedia article, it seemed incoherent to me - respectfully, if I'm understanding correctly, you should probably not be contesting other editors' changes on the topic if this is the case

I concur with Hijiri's suggestion of adding "only one standard semantics", which I agree will be sufficient clarification to avoid incorrectly implying there only exists one semantics in FOL. Hopefully this resolves the 3O and let me know if there's any other questions. Alexandraaaacs1989 (talk) 06:12, 29 September 2026 (UTC)

Thanks for the 3O. Given the sources and 3O, I plan to make the edit as stated above, matching the wording already used at Second-order logic#Semantics. I'll leave this open for a day if JRSpriggs has any objections before making the change Hijiri Suzuki (talk) 14:12, 29 September 2026 (UTC)