Talk:First-order logic
This is the talk page for discussing improvements to the First-order logic article. This is not a forum for general discussion of the article's subject. |
Article policies
|
Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
Archives: 1, 2, 3, 4, 5, 6Auto-archiving period: 12 months |
This level-4 vital article is rated B-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
First-order logic with equality IS decidable!
[edit]Example of definable functions
[edit]I would like to add function application to the abelian group example, as I think it would make the ability of FOL to apply functions more clear. For example we can construct a formula φ(x,y) that's true iff y = x + x + x, so we can said to have defined f(x) = x + x + x. Some formula such as makes sense in this context even though f isn't a function symbol in the language, since we read this as . But I don't have proper sourcing to write this section, this book by K. Kunen gives a similar example of how we read function expressions within a formula for "" but not the general case, nor "". C7XWiki (talk)
Edit: Maybe Quine 1940 is another sufficient source. C7XWiki (talk) 18:48, 28 July 2023 (UTC)
First-Order Sentence definition
[edit]According to my understanding a first-order sentence (or just sentence) is defined by not having any free variables. In the article it is stated that a formula is called a sentence when there are no free variable occurrences, specifically: "A formula in first-order logic with no free variable occurrences is called a first-order sentence.".
Does that imply that if we have only one occurrence of a variable to be free (but is bound in the whole formula), the formula is no valid sentence?
If not, it would be good to remove the word "occurrences" in the definition. Dark.Rider85 (talk) 07:32, 31 July 2023 (UTC)
- "Free" and "bound" are not predicates that apply to variable symbols, like , but to particular occurrences of variable symbols, e.g. the first and second occurrence of in the formula is free and bound, respectively. Therefore, your question doesn't make sense, imo (or maybe, I didn't understand it properly?).
- On the other hand, I'm not sure that the distinction "sentence" / "formula" is made consistently throughout the article. For example
First-order logic ... allows the use of sentences that contain variables
in the lead's 2nd sentence could as well be generalized toFirst-order logic ... allows the use of formulas that contain variables
. I didn't check the rest, but I noticed that "sentence" is often used to refer to a natural language sentence, which is a possible source of confusion, but maybe unavoidable. - Jochen Burghardt (talk) 08:38, 31 July 2023 (UTC)
Syntax-semantics distinction and history
[edit]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
[edit]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 is equivalent to 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 ofx
. 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)
- B-Class level-4 vital articles
- Wikipedia level-4 vital articles in Mathematics
- B-Class vital articles in Mathematics
- B-Class Philosophy articles
- High-importance Philosophy articles
- B-Class logic articles
- High-importance logic articles
- Logic task force articles
- B-Class mathematics articles
- Top-priority mathematics articles
- B-Class Statistics articles
- Top-importance Statistics articles
- WikiProject Statistics articles
- B-Class Computer science articles
- High-importance Computer science articles
- WikiProject Computer science articles